\documentclass{amsart}
    \advance\textheight by 1.75in
    \advance\textwidth by 2in
    \advance\topmargin by -1in
    \advance\oddsidemargin by -1in
    \advance\evensidemargin by -1in
    \usepackage{amssymb}
    \parindent0pt
    \begin{document}
    \textbf{COM001+1.ax} Common axioms for progress/preservation proof






$\forall \mbox{ve}{:}\;\mbox{valphaEquivalent}(\mbox{ve},\mbox{ve})\qquad\mbox{fof}(\mbox{'alpha-equiv-refl'},\mbox{axiom})$

$\forall \mbox{ve}_2,\mbox{ve}_1{:}\;( \mbox{valphaEquivalent}(\mbox{ve}_1,\mbox{ve}_2) \ \Rightarrow \ \mbox{valphaEquivalent}(\mbox{ve}_2,\mbox{ve}_1) )\qquad\mbox{fof}(\mbox{'alpha-equiv-sym'},\mbox{axiom})$

$\forall \mbox{ve}_2,\mbox{ve}_1,\mbox{ve}_3{:}\;( ( \mbox{valphaEquivalent}(\mbox{ve}_1,\mbox{ve}_2)\mbox{ and }\mbox{valphaEquivalent}(\mbox{ve}_2,\mbox{ve}_3) ) \ \Rightarrow \ \mbox{valphaEquivalent}(\mbox{ve}_1,\mbox{ve}_3) )\qquad\mbox{fof}(\mbox{'alpha-equiv-trans'},\mbox{axiom})$

$\forall \mbox{vS},\mbox{vx},\mbox{vy},\mbox{ve}{:}\;( \neg\,\mbox{visFreeVar}(\mbox{vy},\mbox{ve}) \ \Rightarrow \ \mbox{valphaEquivalent}(\mbox{vabs}(\mbox{vx},\mbox{vS},\mbox{ve}),\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{vsubst}(\mbox{vx},\mbox{vvar}(\mbox{vy}),\mbox{ve}))) )\qquad\mbox{fof}(\mbox{'alpha-equiv-subst-abs'},\mbox{axiom})$

$\forall \mbox{ve},\mbox{vC},\mbox{ve}_1,\mbox{vT}{:}\;( ( \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{valphaEquivalent}(\mbox{ve},\mbox{ve}_1) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve}_1,\mbox{vT}) )\qquad\mbox{fof}(\mbox{'alpha-equiv-typing'},\mbox{axiom})$

$\forall \mbox{ve},\mbox{vx},\mbox{ve}_1{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{valphaEquivalent}(\mbox{ve},\mbox{ve}_1) ) \ \Rightarrow \ \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve}_1) )\qquad\mbox{fof}(\mbox{'alpha-equiv-FreeVar'},\mbox{axiom})$

\medskip\textbf{COM151+1.p} Common axioms for progress/preservation proof






$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/COM001+1.ax'})$

\medskip\textbf{COM002-1.p} A program correctness theorem

A computing state space, with eight states - P1 to P8.
 P1 leads to P3 via P2. There is a branch at P3 such that the
 following state is either P4 or P6. P6 leads to P8, which has
 a loop back to P3, while P4 leads to termination. The problem
 is to show that there is a loop in the computation, passing
 through P3.




$\mbox{follows}(\mbox{goal\_state},\mbox{start\_state}) \ \Rightarrow \ \mbox{succeeds}(\mbox{goal\_state},\mbox{start\_state})\qquad\mbox{cnf}(\mbox{direct\_success},\mbox{axiom})$

$( \mbox{succeeds}(\mbox{goal\_state},\mbox{intermediate\_state})\mbox{ and }\mbox{succeeds}(\mbox{intermediate\_state},\mbox{start\_state}) ) \ \Rightarrow \ \mbox{succeeds}(\mbox{goal\_state},\mbox{start\_state})\qquad\mbox{cnf}(\mbox{transitivity\_of\_success},\mbox{axiom})$

$( \mbox{has}(\mbox{start\_state},\mbox{goto}(\mbox{label}))\mbox{ and }\mbox{labels}(\mbox{label},\mbox{goal\_state}) ) \ \Rightarrow \ \mbox{succeeds}(\mbox{goal\_state},\mbox{start\_state})\qquad\mbox{cnf}(\mbox{goto\_success},\mbox{axiom})$

$\mbox{has}(\mbox{start\_state},\mbox{ifthen}(\mbox{condition},\mbox{goal\_state})) \ \Rightarrow \ \mbox{succeeds}(\mbox{goal\_state},\mbox{start\_state})\qquad\mbox{cnf}(\mbox{conditional\_success},\mbox{axiom})$

$\mbox{has}(p_1,\mbox{assign}(\mbox{register\_j},n_0))\qquad\mbox{cnf}(\mbox{state}_1,\mbox{hypothesis})$

$\mbox{follows}(p_2,p_1)\qquad\mbox{cnf}(\mbox{transition\_1\_to}_2,\mbox{hypothesis})$

$\mbox{has}(p_2,\mbox{assign}(\mbox{register\_k},n_1))\qquad\mbox{cnf}(\mbox{state}_2,\mbox{hypothesis})$

$\mbox{labels}(\mbox{loop},p_3)\qquad\mbox{cnf}(\mbox{label\_state}_3,\mbox{hypothesis})$

$\mbox{follows}(p_3,p_2)\qquad\mbox{cnf}(\mbox{transition\_2\_to}_3,\mbox{hypothesis})$

$\mbox{has}(p_3,\mbox{ifthen}(\mbox{equal\_function}(\mbox{register\_j},n),p_4))\qquad\mbox{cnf}(\mbox{state}_3,\mbox{hypothesis})$

$\mbox{has}(p_4,\mbox{goto}(\mbox{out}))\qquad\mbox{cnf}(\mbox{state}_4,\mbox{hypothesis})$

$\mbox{follows}(p_5,p_4)\qquad\mbox{cnf}(\mbox{transition\_4\_to}_5,\mbox{hypothesis})$

$\mbox{follows}(p_6,p_3)\qquad\mbox{cnf}(\mbox{transition\_3\_to}_6,\mbox{hypothesis})$

$\mbox{has}(p_6,\mbox{assign}(\mbox{register\_k},\mbox{times}(n_2,\mbox{register\_k})))\qquad\mbox{cnf}(\mbox{state}_6,\mbox{hypothesis})$

$\mbox{follows}(p_7,p_6)\qquad\mbox{cnf}(\mbox{transition\_6\_to}_7,\mbox{hypothesis})$

$\mbox{has}(p_7,\mbox{assign}(\mbox{register\_j},\mbox{register\_j} + n_1))\qquad\mbox{cnf}(\mbox{state}_7,\mbox{hypothesis})$

$\mbox{follows}(p_8,p_7)\qquad\mbox{cnf}(\mbox{transition\_7\_to}_8,\mbox{hypothesis})$

$\mbox{has}(p_8,\mbox{goto}(\mbox{loop}))\qquad\mbox{cnf}(\mbox{state}_8,\mbox{hypothesis})$

$\neg\,\mbox{succeeds}(p_3,p_3)\qquad\mbox{cnf}(\mbox{prove\_there\_is\_a\_loop\_through\_p}_3,\mbox{negated\_conjecture})$

\medskip\textbf{COM001-1.p} A program correctness theorem

A simple computing state space, with four states - P3, P4,
 P5, and P8 (the full version of this state space is in the
 problem COM002-1). There is a branch at P3 such that the
 following state is either P4 or P8. P8 has a loop back to P3,
 while P4 leads to termination. The problem is to show that
 there is a loop in the computation, passing through P3.




$\mbox{follows}(\mbox{goal\_state},\mbox{start\_state}) \ \Rightarrow \ \mbox{succeeds}(\mbox{goal\_state},\mbox{start\_state})\qquad\mbox{cnf}(\mbox{direct\_success},\mbox{axiom})$

$( \mbox{succeeds}(\mbox{goal\_state},\mbox{intermediate\_state})\mbox{ and }\mbox{succeeds}(\mbox{intermediate\_state},\mbox{start\_state}) ) \ \Rightarrow \ \mbox{succeeds}(\mbox{goal\_state},\mbox{start\_state})\qquad\mbox{cnf}(\mbox{transitivity\_of\_success},\mbox{axiom})$

$( \mbox{has}(\mbox{start\_state},\mbox{goto}(\mbox{label}))\mbox{ and }\mbox{labels}(\mbox{label},\mbox{goal\_state}) ) \ \Rightarrow \ \mbox{succeeds}(\mbox{goal\_state},\mbox{start\_state})\qquad\mbox{cnf}(\mbox{goto\_success},\mbox{axiom})$

$\mbox{has}(\mbox{start\_state},\mbox{ifthen}(\mbox{condition},\mbox{goal\_state})) \ \Rightarrow \ \mbox{succeeds}(\mbox{goal\_state},\mbox{start\_state})\qquad\mbox{cnf}(\mbox{conditional\_success},\mbox{axiom})$

$\mbox{labels}(\mbox{loop},p_3)\qquad\mbox{cnf}(\mbox{label\_state}_3,\mbox{hypothesis})$

$\mbox{has}(p_3,\mbox{ifthen}(\mbox{equal\_function}(\mbox{register\_j},n),p_4))\qquad\mbox{cnf}(\mbox{state}_3,\mbox{hypothesis})$

$\mbox{has}(p_4,\mbox{goto}(\mbox{out}))\qquad\mbox{cnf}(\mbox{state}_4,\mbox{hypothesis})$

$\mbox{follows}(p_5,p_4)\qquad\mbox{cnf}(\mbox{transition\_4\_to}_5,\mbox{hypothesis})$

$\mbox{follows}(p_8,p_3)\qquad\mbox{cnf}(\mbox{transition\_3\_to}_8,\mbox{hypothesis})$

$\mbox{has}(p_8,\mbox{goto}(\mbox{loop}))\qquad\mbox{cnf}(\mbox{state}_8,\mbox{hypothesis})$

$\neg\,\mbox{succeeds}(p_3,p_3)\qquad\mbox{cnf}(\mbox{prove\_there\_is\_a\_loop\_through\_p}_3,\mbox{negated\_conjecture})$

\medskip\textbf{COM012+1.p} Newman's lemma on rewriting systems 01, 00 expansion






$\forall w_0{:}\;( \mbox{aElement}_0(w_0) \ \Rightarrow \ \mbox{\$true} )\qquad\mbox{fof}(\mbox{mElmSort},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aRewritingSystem}_0(w_0) \ \Rightarrow \ \mbox{\$true} )\qquad\mbox{fof}(\mbox{mRelSort},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aRewritingSystem}_0(w_1) ) \ \Rightarrow \ \forall w_2{:}\;( \mbox{aReductOfIn}_0(w_2,w_0,w_1) \ \Rightarrow \ \mbox{aElement}_0(w_2) ) )\qquad\mbox{fof}(\mbox{mReduct},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aElement}_0(w_1) ) \ \Rightarrow \ ( \mbox{iLess}_0(w_0,w_1) \ \Rightarrow \ \mbox{\$true} ) )\qquad\mbox{fof}(\mbox{mWFOrd},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aRewritingSystem}_0(w_1)\mbox{ and }\mbox{aElement}_0(w_2) ) \ \Rightarrow \ ( \mbox{sdtmndtplgtdt}_0(w_0,w_1,w_2) \ \Rightarrow \ \mbox{\$true} ) )\qquad\mbox{fof}(\mbox{mTCbr},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aRewritingSystem}_0(w_1)\mbox{ and }\mbox{aElement}_0(w_2) ) \ \Rightarrow \ ( \mbox{sdtmndtplgtdt}_0(w_0,w_1,w_2)\iff ( \mbox{aReductOfIn}_0(w_2,w_0,w_1)\mbox{ or }\exists w_3{:}\;( \mbox{aElement}_0(w_3)\mbox{ and }\mbox{aReductOfIn}_0(w_3,w_0,w_1)\mbox{ and }\mbox{sdtmndtplgtdt}_0(w_3,w_1,w_2) ) ) ) )\qquad\mbox{fof}(\mbox{mTCDef},\mbox{definition})$

$\forall w_0,w_1,w_2,w_3{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aRewritingSystem}_0(w_1)\mbox{ and }\mbox{aElement}_0(w_2)\mbox{ and }\mbox{aElement}_0(w_3) ) \ \Rightarrow \ ( ( \mbox{sdtmndtplgtdt}_0(w_0,w_1,w_2)\mbox{ and }\mbox{sdtmndtplgtdt}_0(w_2,w_1,w_3) ) \ \Rightarrow \ \mbox{sdtmndtplgtdt}_0(w_0,w_1,w_3) ) )\qquad\mbox{fof}(\mbox{mTCTrans},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aRewritingSystem}_0(w_1)\mbox{ and }\mbox{aElement}_0(w_2) ) \ \Rightarrow \ ( \mbox{sdtmndtasgtdt}_0(w_0,w_1,w_2)\iff ( w_0 = w_2\mbox{ or }\mbox{sdtmndtplgtdt}_0(w_0,w_1,w_2) ) ) )\qquad\mbox{fof}(\mbox{mTCRDef},\mbox{definition})$

$\mbox{aElement}_0(\mbox{xx})\mbox{ and }\mbox{aRewritingSystem}_0(\mbox{xR})\mbox{ and }\mbox{aElement}_0(\mbox{xy})\mbox{ and }\mbox{aElement}_0(\mbox{xz})\qquad\mbox{fof}(\mbox{m\_}_{349},\mbox{hypothesis})$

$( \mbox{sdtmndtasgtdt}_0(\mbox{xx},\mbox{xR},\mbox{xy})\mbox{ and }\mbox{sdtmndtasgtdt}_0(\mbox{xy},\mbox{xR},\mbox{xz}) ) \ \Rightarrow \ \mbox{sdtmndtasgtdt}_0(\mbox{xx},\mbox{xR},\mbox{xz})\qquad\mbox{fof}(\mbox{m\_\_},\mbox{conjecture})$

\medskip\textbf{COM135+1.p} T-subst-var step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vy},\mbox{vT}_2{:}\;( ( \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{vvar}(\mbox{vy}),\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{vvar}(\mbox{vy})),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-var'},\mbox{conjecture})$

\medskip\textbf{COM024$\wedge$5.p} TPS problem THM9

A very naive version of the recursion theorem. TM X Y is the
 output of Turing machine X on input Y, TH F is the number of a
 Turing machine that computes function F.




$\mbox{cTM}{:}\;\mbox{\$i}\to \mbox{\$i}\to \mbox{\$i}\qquad\mbox{thf}(\mbox{cTM},\mbox{type})$

$\mbox{cTH}{:}\;( \mbox{\$i}\to \mbox{\$i} )\to \mbox{\$i}\qquad\mbox{thf}(\mbox{cTH},\mbox{type})$

$\forall g{:}\;\mbox{\$i}\to \mbox{\$i}{:}\;( \mbox{cTM}@ ( \mbox{cTH}@ g ) ) = g \ \Rightarrow \ \forall f{:}\;\mbox{\$i}\to \mbox{\$i}{:}\;\exists n{:}\;\mbox{\$i}{:}\;( \mbox{cTM}@ ( f@ n ) ) = ( \mbox{cTM}@ n )\qquad\mbox{thf}(\mbox{cTHM}_9,\mbox{conjecture})$

\medskip\textbf{COM009-2.p} Problem about UNITY theory






$\mbox{c\_UNITY\_Ototalize}(\mbox{v\_F},\mbox{t\_a}) = \mbox{v\_F} \ \Rightarrow \ \neg\,\mbox{c\_UNITY\_Oall\_\_total}(\mbox{v\_F},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_conjecture}_0,\mbox{negated\_conjecture})$

$\mbox{c\_UNITY\_Oall\_\_total}(\mbox{v\_F},\mbox{t\_a})\mbox{ or }\mbox{c\_UNITY\_Ototalize}(\mbox{v\_F},\mbox{t\_a}) = \mbox{v\_F}\qquad\mbox{cnf}(\mbox{cls\_conjecture}_1,\mbox{negated\_conjecture})$

$\mbox{c\_UNITY\_Oall\_\_total}(\mbox{v\_F},\mbox{t\_a}) \ \Rightarrow \ \mbox{c\_UNITY\_Ototalize}(\mbox{v\_F},\mbox{t\_a}) = \mbox{v\_F}\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oall\_\_total\_\_imp\_\_totalize}_0,\mbox{axiom})$

$\mbox{c\_UNITY\_Oall\_\_total}(\mbox{c\_UNITY\_Ototalize}(\mbox{v\_F},\mbox{t\_a}),\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oall\_\_total\_\_totalize}_0,\mbox{axiom})$

\medskip\textbf{COM129+1.p} Fresh-free-2 step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/COM001+1.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vy},\mbox{vS},\mbox{ve}_1,\mbox{vT}_2{:}\;( ( \mbox{vx}\ne \mbox{vy}\mbox{ and }\neg\,\mbox{visFreeVar}(\mbox{vy},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{ve}_1),\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{ve}_1)),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-abs-2-gen'},\mbox{axiom})$

$\forall \mbox{ve},\mbox{ve}_1,\mbox{vx},\mbox{vfresh}{:}\;( \mbox{vfresh} = \mbox{vgensym}(\mbox{vapp}(\mbox{vapp}(\mbox{ve},\mbox{ve}_1),\mbox{vvar}(\mbox{vx}))) \ \Rightarrow \ \mbox{vx}\ne \mbox{vfresh} )\qquad\mbox{fof}(\mbox{'fresh-unequal-var-3'},\mbox{axiom})$

$\forall \mbox{ve},\mbox{vx},\mbox{vfresh},\mbox{ve}_1{:}\;( \mbox{vfresh} = \mbox{vgensym}(\mbox{vapp}(\mbox{vapp}(\mbox{ve},\mbox{ve}_1),\mbox{vvar}(\mbox{vx}))) \ \Rightarrow \ \neg\,\mbox{visFreeVar}(\mbox{vfresh},\mbox{ve}_1) )\qquad\mbox{fof}(\mbox{'fresh-free-2'},\mbox{conjecture})$

\medskip\textbf{COM002-2.p} A program correctness theorem.

A computing state space, with eight states - P1 to P8.
 P1 leads to P3 via P2. There is a branch at P3 such that the
 following state is either P4 or P6. P6 leads to P8, which has
 a loop back to P3, while P4 leads to termination. The problem
 is to show that there is a loop in the computation, passing
 through P3.




$\mbox{fails}(\mbox{goal\_state},\mbox{start\_state}) \ \Rightarrow \ \neg\,\mbox{follows}(\mbox{goal\_state},\mbox{start\_state})\qquad\mbox{cnf}(\mbox{direct\_success},\mbox{axiom})$

$\mbox{fails}(\mbox{goal\_state},\mbox{start\_state}) \ \Rightarrow \ ( \mbox{fails}(\mbox{goal\_state},\mbox{intermediate\_state})\mbox{ or }\mbox{fails}(\mbox{intermediate\_state},\mbox{start\_state}) )\qquad\mbox{cnf}(\mbox{transitivity\_of\_success},\mbox{axiom})$

$( \mbox{fails}(\mbox{goal\_state},\mbox{start\_state})\mbox{ and }\mbox{has}(\mbox{start\_state},\mbox{goto}(\mbox{label})) ) \ \Rightarrow \ \neg\,\mbox{labels}(\mbox{label},\mbox{goal\_state})\qquad\mbox{cnf}(\mbox{goto\_success},\mbox{axiom})$

$\mbox{fails}(\mbox{goal\_state},\mbox{start\_state}) \ \Rightarrow \ \neg\,\mbox{has}(\mbox{start\_state},\mbox{ifthen}(\mbox{condition},\mbox{goal\_state}))\qquad\mbox{cnf}(\mbox{conditional\_success},\mbox{axiom})$

$\mbox{has}(p_1,\mbox{assign}(\mbox{register\_j},n_0))\qquad\mbox{cnf}(\mbox{state}_1,\mbox{hypothesis})$

$\mbox{follows}(p_2,p_1)\qquad\mbox{cnf}(\mbox{transition\_1\_to}_2,\mbox{hypothesis})$

$\mbox{has}(p_2,\mbox{assign}(\mbox{register\_k},n_1))\qquad\mbox{cnf}(\mbox{state}_2,\mbox{hypothesis})$

$\mbox{labels}(\mbox{loop},p_3)\qquad\mbox{cnf}(\mbox{label\_state}_3,\mbox{hypothesis})$

$\mbox{follows}(p_3,p_2)\qquad\mbox{cnf}(\mbox{transition\_2\_to}_3,\mbox{hypothesis})$

$\mbox{has}(p_3,\mbox{ifthen}(\mbox{equal\_function}(\mbox{register\_j},n),p_4))\qquad\mbox{cnf}(\mbox{state}_3,\mbox{hypothesis})$

$\mbox{has}(p_4,\mbox{goto}(\mbox{out}))\qquad\mbox{cnf}(\mbox{state}_4,\mbox{hypothesis})$

$\mbox{follows}(p_5,p_4)\qquad\mbox{cnf}(\mbox{transition\_4\_to}_5,\mbox{hypothesis})$

$\mbox{follows}(p_6,p_3)\qquad\mbox{cnf}(\mbox{transition\_3\_to}_6,\mbox{hypothesis})$

$\mbox{has}(p_6,\mbox{assign}(\mbox{register\_k},\mbox{times}(n_2,\mbox{register\_k})))\qquad\mbox{cnf}(\mbox{state}_6,\mbox{hypothesis})$

$\mbox{follows}(p_7,p_6)\qquad\mbox{cnf}(\mbox{transition\_6\_to}_7,\mbox{hypothesis})$

$\mbox{has}(p_7,\mbox{assign}(\mbox{register\_j},\mbox{register\_j} + n_1))\qquad\mbox{cnf}(\mbox{state}_7,\mbox{hypothesis})$

$\mbox{follows}(p_8,p_7)\qquad\mbox{cnf}(\mbox{transition\_7\_to}_8,\mbox{hypothesis})$

$\mbox{has}(p_8,\mbox{goto}(\mbox{loop}))\qquad\mbox{cnf}(\mbox{state}_8,\mbox{hypothesis})$

$\mbox{fails}(p_3,p_3)\qquad\mbox{cnf}(\mbox{prove\_there\_is\_a\_loop\_through\_p}_3,\mbox{negated\_conjecture})$

\medskip\textbf{COM128+1.p} Fresh-unequal-var-3 step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/COM001+1.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vy},\mbox{vS},\mbox{ve}_1,\mbox{vT}_2{:}\;( ( \mbox{vx}\ne \mbox{vy}\mbox{ and }\neg\,\mbox{visFreeVar}(\mbox{vy},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{ve}_1),\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{ve}_1)),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-abs-2-gen'},\mbox{axiom})$

$\forall \mbox{ve},\mbox{ve}_1,\mbox{vx},\mbox{vfresh}{:}\;( \mbox{vfresh} = \mbox{vgensym}(\mbox{vapp}(\mbox{vapp}(\mbox{ve},\mbox{ve}_1),\mbox{vvar}(\mbox{vx}))) \ \Rightarrow \ \mbox{vx}\ne \mbox{vfresh} )\qquad\mbox{fof}(\mbox{'fresh-unequal-var-3'},\mbox{conjecture})$

\medskip\textbf{COM010-2.p} Problem about UNITY theory






$\mbox{c\_UNITY\_OInit}(\mbox{v\_F},\mbox{t\_a}) = \mbox{c\_UNITY\_OInit}(\mbox{v\_G},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_conjecture}_0,\mbox{negated\_conjecture})$

$\mbox{c\_UNITY\_OActs}(\mbox{v\_F},\mbox{t\_a}) = \mbox{c\_UNITY\_OActs}(\mbox{v\_G},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_conjecture}_1,\mbox{negated\_conjecture})$

$\mbox{c\_UNITY\_OAllowedActs}(\mbox{v\_F},\mbox{t\_a}) = \mbox{c\_UNITY\_OAllowedActs}(\mbox{v\_G},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_conjecture}_2,\mbox{negated\_conjecture})$

$\mbox{v\_F}\ne \mbox{v\_G}\qquad\mbox{cnf}(\mbox{cls\_conjecture}_3,\mbox{negated\_conjecture})$

$\mbox{c\_UNITY\_Omk\_\_program}(\mbox{c\_Pair}(\mbox{c\_UNITY\_OInit}(\mbox{v\_y},\mbox{t\_a}),\mbox{c\_Pair}(\mbox{c\_UNITY\_OActs}(\mbox{v\_y},\mbox{t\_a}),\mbox{c\_UNITY\_OAllowedActs}(\mbox{v\_y},\mbox{t\_a}),\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))),\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a})))),\mbox{tc\_set}(\mbox{t\_a}),\mbox{tc\_prod}(\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))),\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))))),\mbox{t\_a}) = \mbox{v\_y}\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Osurjective\_\_mk\_\_program}_0,\mbox{axiom})$

\medskip\textbf{COM144+1.p} T-Preservation-T-abs step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{ve}_2,\mbox{vT}_2{:}\;( ( \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{ve}_2,\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{ve}_2),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vC},\mbox{veout},\mbox{vT}{:}\;( ( \mbox{vreduce}(\mbox{ve}_1) = \mbox{vsomeExp}(\mbox{veout})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve}_1,\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{veout},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Preservation-T-abs-IH'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{veout},\mbox{vT}{:}\;( ( \mbox{vreduce}(\mbox{vabs}(\mbox{vx},\mbox{vS},\mbox{ve}_1)) = \mbox{vsomeExp}(\mbox{veout})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vabs}(\mbox{vx},\mbox{vS},\mbox{ve}_1),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{veout},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Preservation-T-abs'},\mbox{conjecture})$

\medskip\textbf{COM003+1.p} The halting problem is undecidable






$\exists x{:}\;( \mbox{algorithm}(x)\mbox{ and }\forall y{:}\;( \mbox{program}(y) \ \Rightarrow \ \forall z{:}\;\mbox{decides}(x,y,z) ) ) \ \Rightarrow \ \exists w{:}\;( \mbox{program}(w)\mbox{ and }\forall y{:}\;( \mbox{program}(y) \ \Rightarrow \ \forall z{:}\;\mbox{decides}(w,y,z) ) )\qquad\mbox{fof}(p_1,\mbox{axiom})$

$\forall w{:}\;( ( \mbox{program}(w)\mbox{ and }\forall y{:}\;( \mbox{program}(y) \ \Rightarrow \ \forall z{:}\;\mbox{decides}(w,y,z) ) ) \ \Rightarrow \ \forall y,z{:}\;( ( ( \mbox{program}(y)\mbox{ and }\mbox{halts}_2(y,z) ) \ \Rightarrow \ ( \mbox{halts}_3(w,y,z)\mbox{ and }\mbox{outputs}(w,\mbox{good}) ) )\mbox{ and }( ( \mbox{program}(y)\mbox{ and }\neg\,\mbox{halts}_2(y,z) ) \ \Rightarrow \ ( \mbox{halts}_3(w,y,z)\mbox{ and }\mbox{outputs}(w,\mbox{bad}) ) ) ) )\qquad\mbox{fof}(p_2,\mbox{axiom})$

$\exists w{:}\;( \mbox{program}(w)\mbox{ and }\forall y{:}\;( ( ( \mbox{program}(y)\mbox{ and }\mbox{halts}_2(y,y) ) \ \Rightarrow \ ( \mbox{halts}_3(w,y,y)\mbox{ and }\mbox{outputs}(w,\mbox{good}) ) )\mbox{ and }( ( \mbox{program}(y)\mbox{ and }\neg\,\mbox{halts}_2(y,y) ) \ \Rightarrow \ ( \mbox{halts}_3(w,y,y)\mbox{ and }\mbox{outputs}(w,\mbox{bad}) ) ) ) ) \ \Rightarrow \ \exists v{:}\;( \mbox{program}(v)\mbox{ and }\forall y{:}\;( ( ( \mbox{program}(y)\mbox{ and }\mbox{halts}_2(y,y) ) \ \Rightarrow \ ( \mbox{halts}_2(v,y)\mbox{ and }\mbox{outputs}(v,\mbox{good}) ) )\mbox{ and }( ( \mbox{program}(y)\mbox{ and }\neg\,\mbox{halts}_2(y,y) ) \ \Rightarrow \ ( \mbox{halts}_2(v,y)\mbox{ and }\mbox{outputs}(v,\mbox{bad}) ) ) ) )\qquad\mbox{fof}(p_3,\mbox{axiom})$

$\exists v{:}\;( \mbox{program}(v)\mbox{ and }\forall y{:}\;( ( ( \mbox{program}(y)\mbox{ and }\mbox{halts}_2(y,y) ) \ \Rightarrow \ ( \mbox{halts}_2(v,y)\mbox{ and }\mbox{outputs}(v,\mbox{good}) ) )\mbox{ and }( ( \mbox{program}(y)\mbox{ and }\neg\,\mbox{halts}_2(y,y) ) \ \Rightarrow \ ( \mbox{halts}_2(v,y)\mbox{ and }\mbox{outputs}(v,\mbox{bad}) ) ) ) ) \ \Rightarrow \ \exists u{:}\;( \mbox{program}(u)\mbox{ and }\forall y{:}\;( ( ( \mbox{program}(y)\mbox{ and }\mbox{halts}_2(y,y) ) \ \Rightarrow \ \neg\,\mbox{halts}_2(u,y) )\mbox{ and }( ( \mbox{program}(y)\mbox{ and }\neg\,\mbox{halts}_2(y,y) ) \ \Rightarrow \ ( \mbox{halts}_2(u,y)\mbox{ and }\mbox{outputs}(u,\mbox{bad}) ) ) ) )\qquad\mbox{fof}(p_4,\mbox{axiom})$

$\neg\,\exists x_1{:}\;( \mbox{algorithm}(x_1)\mbox{ and }\forall y_1{:}\;( \mbox{program}(y_1) \ \Rightarrow \ \forall z_1{:}\;\mbox{decides}(x_1,y_1,z_1) ) )\qquad\mbox{fof}(\mbox{prove\_this},\mbox{conjecture})$

\medskip\textbf{COM137+1.p} T-Strong-app step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve1app})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve1app},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve1app},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong-app-IH1'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve2app})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve2app},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve2app},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong-app-IH2'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{vapp}(\mbox{ve1app},\mbox{ve2app}))\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vapp}(\mbox{ve1app},\mbox{ve2app}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vapp}(\mbox{ve1app},\mbox{ve2app}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong-app'},\mbox{conjecture})$

\medskip\textbf{COM145+1.p} T-Preservation-T-app step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{ve}_2,\mbox{vT}_2{:}\;( ( \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{ve}_2,\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{ve}_2),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vC},\mbox{veout},\mbox{vT}{:}\;( ( \mbox{vreduce}(\mbox{ve}_1) = \mbox{vsomeExp}(\mbox{veout})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve}_1,\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{veout},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Preservation-T-app-IH1'},\mbox{axiom})$

$\forall \mbox{vC},\mbox{veout},\mbox{vT}{:}\;( ( \mbox{vreduce}(\mbox{ve}_2) = \mbox{vsomeExp}(\mbox{veout})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve}_2,\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{veout},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Preservation-T-app-IH2'},\mbox{axiom})$

$\forall \mbox{vC},\mbox{veout},\mbox{vT}{:}\;( ( \mbox{vreduce}(\mbox{vapp}(\mbox{ve}_1,\mbox{ve}_2)) = \mbox{vsomeExp}(\mbox{veout})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vapp}(\mbox{ve}_1,\mbox{ve}_2),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{veout},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Preservation-T-app'},\mbox{conjecture})$

\medskip\textbf{COM149+1.p} T-Progress-T-var step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vx}{:}\;( ( \mbox{vtcheck}(\mbox{vempty},\mbox{vvar}(\mbox{vx}),\mbox{vT})\mbox{ and }\neg\,\mbox{visValue}(\mbox{vvar}(\mbox{vx})) ) \ \Rightarrow \ \exists \mbox{veout}{:}\;\mbox{vreduce}(\mbox{vvar}(\mbox{vx})) = \mbox{vsomeExp}(\mbox{veout}) )\qquad\mbox{fof}(\mbox{'T-Progress-T-var'},\mbox{conjecture})$

\medskip\textbf{COM007+1.p} Preservation of the Diamond Property under reflexive closure






$\mbox{reflexive\_rewrite}(a,b)\mbox{ and }\mbox{reflexive\_rewrite}(a,c)\qquad\mbox{fof}(\mbox{assumption},\mbox{axiom})$

$\forall a{:}\;( ( \mbox{reflexive\_rewrite}(b,a)\mbox{ and }\mbox{reflexive\_rewrite}(c,a) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{goal\_ax},\mbox{axiom})$

$\forall a{:}\;a{=}a\qquad\mbox{fof}(\mbox{reflexivity},\mbox{axiom})$

$\forall a,b{:}\;( a{=}b \ \Rightarrow \ b{=}a )\qquad\mbox{fof}(\mbox{symmtery},\mbox{axiom})$

$\forall a,b,c{:}\;( ( a{=}b\mbox{ and }\mbox{reflexive\_rewrite}(b,c) ) \ \Rightarrow \ \mbox{reflexive\_rewrite}(a,c) )\qquad\mbox{fof}(\mbox{substitution},\mbox{axiom})$

$\forall a,b{:}\;( a{=}b \ \Rightarrow \ \mbox{reflexive\_rewrite}(a,b) )\qquad\mbox{fof}(\mbox{equalish\_in\_reflexive\_rewrite},\mbox{axiom})$

$\forall a,b{:}\;( \mbox{rewrite}(a,b) \ \Rightarrow \ \mbox{reflexive\_rewrite}(a,b) )\qquad\mbox{fof}(\mbox{rewrite\_in\_reflexive\_rewrite},\mbox{axiom})$

$\forall a,b{:}\;( \mbox{reflexive\_rewrite}(a,b) \ \Rightarrow \ ( a{=}b\mbox{ or }\mbox{rewrite}(a,b) ) )\qquad\mbox{fof}(\mbox{equalish\_or\_rewrite},\mbox{axiom})$

$\forall a,b,c{:}\;( ( \mbox{rewrite}(a,b)\mbox{ and }\mbox{rewrite}(a,c) ) \ \Rightarrow \ \exists d{:}\;( \mbox{rewrite}(b,d)\mbox{ and }\mbox{rewrite}(c,d) ) )\qquad\mbox{fof}(\mbox{rewrite\_diamond},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{COM007+2.p} Preservation of the Diamond Property under reflexive closure






$\mbox{reflexive\_rewrite}(a,b)\mbox{ and }\mbox{reflexive\_rewrite}(a,c)\qquad\mbox{fof}(\mbox{assumption},\mbox{axiom})$

$\forall a{:}\;( ( \mbox{reflexive\_rewrite}(b,a)\mbox{ and }\mbox{reflexive\_rewrite}(c,a) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{goal\_ax},\mbox{axiom})$

$\forall a,b{:}\;( a = b \ \Rightarrow \ \mbox{reflexive\_rewrite}(a,b) )\qquad\mbox{fof}(\mbox{equal\_in\_reflexive\_rewrite},\mbox{axiom})$

$\forall a,b{:}\;( \mbox{rewrite}(a,b) \ \Rightarrow \ \mbox{reflexive\_rewrite}(a,b) )\qquad\mbox{fof}(\mbox{rewrite\_in\_reflexive\_rewrite},\mbox{axiom})$

$\forall a,b{:}\;( \mbox{reflexive\_rewrite}(a,b) \ \Rightarrow \ ( a = b\mbox{ or }\mbox{rewrite}(a,b) ) )\qquad\mbox{fof}(\mbox{equal\_or\_rewrite},\mbox{axiom})$

$\forall a,b,c{:}\;( ( \mbox{rewrite}(a,b)\mbox{ and }\mbox{rewrite}(a,c) ) \ \Rightarrow \ \exists d{:}\;( \mbox{rewrite}(b,d)\mbox{ and }\mbox{rewrite}(c,d) ) )\qquad\mbox{fof}(\mbox{rewrite\_diamond},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{COM012+3.p} Newman's lemma on rewriting systems 01, 02 expansion






$\forall w_0{:}\;( \mbox{aElement}_0(w_0) \ \Rightarrow \ \mbox{\$true} )\qquad\mbox{fof}(\mbox{mElmSort},\mbox{axiom})$

$\forall w_0{:}\;( \mbox{aRewritingSystem}_0(w_0) \ \Rightarrow \ \mbox{\$true} )\qquad\mbox{fof}(\mbox{mRelSort},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aRewritingSystem}_0(w_1) ) \ \Rightarrow \ \forall w_2{:}\;( \mbox{aReductOfIn}_0(w_2,w_0,w_1) \ \Rightarrow \ \mbox{aElement}_0(w_2) ) )\qquad\mbox{fof}(\mbox{mReduct},\mbox{axiom})$

$\forall w_0,w_1{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aElement}_0(w_1) ) \ \Rightarrow \ ( \mbox{iLess}_0(w_0,w_1) \ \Rightarrow \ \mbox{\$true} ) )\qquad\mbox{fof}(\mbox{mWFOrd},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aRewritingSystem}_0(w_1)\mbox{ and }\mbox{aElement}_0(w_2) ) \ \Rightarrow \ ( \mbox{sdtmndtplgtdt}_0(w_0,w_1,w_2) \ \Rightarrow \ \mbox{\$true} ) )\qquad\mbox{fof}(\mbox{mTCbr},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aRewritingSystem}_0(w_1)\mbox{ and }\mbox{aElement}_0(w_2) ) \ \Rightarrow \ ( \mbox{sdtmndtplgtdt}_0(w_0,w_1,w_2)\iff ( \mbox{aReductOfIn}_0(w_2,w_0,w_1)\mbox{ or }\exists w_3{:}\;( \mbox{aElement}_0(w_3)\mbox{ and }\mbox{aReductOfIn}_0(w_3,w_0,w_1)\mbox{ and }\mbox{sdtmndtplgtdt}_0(w_3,w_1,w_2) ) ) ) )\qquad\mbox{fof}(\mbox{mTCDef},\mbox{definition})$

$\forall w_0,w_1,w_2,w_3{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aRewritingSystem}_0(w_1)\mbox{ and }\mbox{aElement}_0(w_2)\mbox{ and }\mbox{aElement}_0(w_3) ) \ \Rightarrow \ ( ( \mbox{sdtmndtplgtdt}_0(w_0,w_1,w_2)\mbox{ and }\mbox{sdtmndtplgtdt}_0(w_2,w_1,w_3) ) \ \Rightarrow \ \mbox{sdtmndtplgtdt}_0(w_0,w_1,w_3) ) )\qquad\mbox{fof}(\mbox{mTCTrans},\mbox{axiom})$

$\forall w_0,w_1,w_2{:}\;( ( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aRewritingSystem}_0(w_1)\mbox{ and }\mbox{aElement}_0(w_2) ) \ \Rightarrow \ ( \mbox{sdtmndtasgtdt}_0(w_0,w_1,w_2)\iff ( w_0 = w_2\mbox{ or }\mbox{sdtmndtplgtdt}_0(w_0,w_1,w_2) ) ) )\qquad\mbox{fof}(\mbox{mTCRDef},\mbox{definition})$

$\mbox{aElement}_0(\mbox{xx})\mbox{ and }\mbox{aRewritingSystem}_0(\mbox{xR})\mbox{ and }\mbox{aElement}_0(\mbox{xy})\mbox{ and }\mbox{aElement}_0(\mbox{xz})\qquad\mbox{fof}(\mbox{m\_}_{349},\mbox{hypothesis})$

$( ( \mbox{xx} = \mbox{xy}\mbox{ or }( ( \mbox{aReductOfIn}_0(\mbox{xy},\mbox{xx},\mbox{xR})\mbox{ or }\exists w_0{:}\;( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aReductOfIn}_0(w_0,\mbox{xx},\mbox{xR})\mbox{ and }\mbox{sdtmndtplgtdt}_0(w_0,\mbox{xR},\mbox{xy}) ) )\mbox{ and }\mbox{sdtmndtplgtdt}_0(\mbox{xx},\mbox{xR},\mbox{xy}) ) )\mbox{ and }\mbox{sdtmndtasgtdt}_0(\mbox{xx},\mbox{xR},\mbox{xy})\mbox{ and }( \mbox{xy} = \mbox{xz}\mbox{ or }( ( \mbox{aReductOfIn}_0(\mbox{xz},\mbox{xy},\mbox{xR})\mbox{ or }\exists w_0{:}\;( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aReductOfIn}_0(w_0,\mbox{xy},\mbox{xR})\mbox{ and }\mbox{sdtmndtplgtdt}_0(w_0,\mbox{xR},\mbox{xz}) ) )\mbox{ and }\mbox{sdtmndtplgtdt}_0(\mbox{xy},\mbox{xR},\mbox{xz}) ) )\mbox{ and }\mbox{sdtmndtasgtdt}_0(\mbox{xy},\mbox{xR},\mbox{xz}) ) \ \Rightarrow \ ( \mbox{xx} = \mbox{xz}\mbox{ or }\mbox{aReductOfIn}_0(\mbox{xz},\mbox{xx},\mbox{xR})\mbox{ or }\exists w_0{:}\;( \mbox{aElement}_0(w_0)\mbox{ and }\mbox{aReductOfIn}_0(w_0,\mbox{xx},\mbox{xR})\mbox{ and }\mbox{sdtmndtplgtdt}_0(w_0,\mbox{xR},\mbox{xz}) )\mbox{ or }\mbox{sdtmndtplgtdt}_0(\mbox{xx},\mbox{xR},\mbox{xz})\mbox{ or }\mbox{sdtmndtasgtdt}_0(\mbox{xx},\mbox{xR},\mbox{xz}) )\qquad\mbox{fof}(\mbox{m\_\_},\mbox{conjecture})$

\medskip\textbf{COM003+2.p} The halting problem is undecidable






$\forall x{:}\;( \mbox{program\_decides}(x)\iff \forall y{:}\;( \mbox{program}(y) \ \Rightarrow \ \forall z{:}\;\mbox{decides}(x,y,z) ) )\qquad\mbox{fof}(\mbox{program\_decides\_def},\mbox{axiom})$

$\forall x{:}\;( \mbox{program\_program\_decides}(x)\iff ( \mbox{program}(x)\mbox{ and }\mbox{program\_decides}(x) ) )\qquad\mbox{fof}(\mbox{program\_program\_decides\_def},\mbox{axiom})$

$\forall x{:}\;( \mbox{algorithm\_program\_decides}(x)\iff ( \mbox{algorithm}(x)\mbox{ and }\mbox{program\_decides}(x) ) )\qquad\mbox{fof}(\mbox{algorithm\_program\_decides\_def},\mbox{axiom})$

$\forall x,y{:}\;( \mbox{program\_halts}_2(x,y)\iff ( \mbox{program}(x)\mbox{ and }\mbox{halts}_2(x,y) ) )\qquad\mbox{fof}(\mbox{program\_halts2\_def},\mbox{axiom})$

$\forall x,y,z,w{:}\;( \mbox{halts3\_outputs}(x,y,z,w)\iff ( \mbox{halts}_3(x,y,z)\mbox{ and }\mbox{outputs}(x,w) ) )\qquad\mbox{fof}(\mbox{halts3\_outputs\_def},\mbox{axiom})$

$\forall x,y{:}\;( \mbox{program\_not\_halts}_2(x,y)\iff ( \mbox{program}(x)\mbox{ and }\neg\,\mbox{halts}_2(x,y) ) )\qquad\mbox{fof}(\mbox{program\_not\_halts2\_def},\mbox{axiom})$

$\forall x,y,w{:}\;( \mbox{halts2\_outputs}(x,y,w)\iff ( \mbox{halts}_2(x,y)\mbox{ and }\mbox{outputs}(x,w) ) )\qquad\mbox{fof}(\mbox{halts2\_outputs\_def},\mbox{axiom})$

$\forall x,y,z,w{:}\;( \mbox{program\_halts2\_halts3\_outputs}(x,y,z,w)\iff ( \mbox{program\_halts}_2(y,z) \ \Rightarrow \ \mbox{halts3\_outputs}(x,y,z,w) ) )\qquad\mbox{fof}(\mbox{program\_halts2\_halts3\_outputs\_def},\mbox{axiom})$

$\forall x,y,z,w{:}\;( \mbox{program\_not\_halts2\_halts3\_outputs}(x,y,z,w)\iff ( \mbox{program\_not\_halts}_2(y,z) \ \Rightarrow \ \mbox{halts3\_outputs}(x,y,z,w) ) )\qquad\mbox{fof}(\mbox{program\_not\_halts2\_halts3\_outputs\_def},\mbox{axiom})$

$\forall x,y,w{:}\;( \mbox{program\_halts2\_halts2\_outputs}(x,y,w)\iff ( \mbox{program\_halts}_2(y,y) \ \Rightarrow \ \mbox{halts2\_outputs}(x,y,w) ) )\qquad\mbox{fof}(\mbox{program\_halts2\_halts2\_outputs\_def},\mbox{axiom})$

$\forall x,y,w{:}\;( \mbox{program\_not\_halts2\_halts2\_outputs}(x,y,w)\iff ( \mbox{program\_not\_halts}_2(y,y) \ \Rightarrow \ \mbox{halts2\_outputs}(x,y,w) ) )\qquad\mbox{fof}(\mbox{program\_not\_halts2\_halts2\_outputs\_def},\mbox{axiom})$

$\exists x{:}\;\mbox{algorithm\_program\_decides}(x) \ \Rightarrow \ \exists w{:}\;\mbox{program\_program\_decides}(w)\qquad\mbox{fof}(p_1,\mbox{axiom})$

$\forall w{:}\;( \mbox{program\_program\_decides}(w) \ \Rightarrow \ \forall y,z{:}\;( \mbox{program\_halts2\_halts3\_outputs}(w,y,z,\mbox{good})\mbox{ and }\mbox{program\_not\_halts2\_halts3\_outputs}(w,y,z,\mbox{bad}) ) )\qquad\mbox{fof}(p_2,\mbox{axiom})$

$\exists w{:}\;( \mbox{program}(w)\mbox{ and }\forall y{:}\;( \mbox{program\_halts2\_halts3\_outputs}(w,y,y,\mbox{good})\mbox{ and }\mbox{program\_not\_halts2\_halts3\_outputs}(w,y,y,\mbox{bad}) ) ) \ \Rightarrow \ \exists v{:}\;( \mbox{program}(v)\mbox{ and }\forall y{:}\;( \mbox{program\_halts2\_halts2\_outputs}(v,y,\mbox{good})\mbox{ and }\mbox{program\_not\_halts2\_halts2\_outputs}(v,y,\mbox{bad}) ) )\qquad\mbox{fof}(p_3,\mbox{axiom})$

$\exists v{:}\;( \mbox{program}(v)\mbox{ and }\forall y{:}\;( \mbox{program\_halts2\_halts2\_outputs}(v,y,\mbox{good})\mbox{ and }\mbox{program\_not\_halts2\_halts2\_outputs}(v,y,\mbox{bad}) ) ) \ \Rightarrow \ \exists u{:}\;( \mbox{program}(u)\mbox{ and }\forall y{:}\;( ( \mbox{program\_halts}_2(y,y) \ \Rightarrow \ \neg\,\mbox{halts}_2(u,y) )\mbox{ and }\mbox{program\_not\_halts2\_halts2\_outputs}(u,y,\mbox{good}) ) )\qquad\mbox{fof}(p_4,\mbox{axiom})$

$\neg\,\exists x{:}\;\mbox{algorithm\_program\_decides}(x)\qquad\mbox{fof}(\mbox{prove\_this},\mbox{conjecture})$

\medskip\textbf{COM142+1.p} T-Weak-app step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve1app},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve1app},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-app-IH1'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve2app},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve2app},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-app-IH2'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vapp}(\mbox{ve1app},\mbox{ve2app}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vapp}(\mbox{ve1app},\mbox{ve2app}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-app'},\mbox{conjecture})$

\medskip\textbf{COM132+1.p} T-subst-abs-3 step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/COM001+1.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vy},\mbox{vS},\mbox{ve}_1,\mbox{vT}_2{:}\;( ( \mbox{vx}\ne \mbox{vy}\mbox{ and }\neg\,\mbox{visFreeVar}(\mbox{vy},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{ve}_1),\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{ve}_1)),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-abs-2-gen'},\mbox{axiom})$

$\forall \mbox{ve},\mbox{ve}_1,\mbox{vx},\mbox{vfresh}{:}\;( \mbox{vfresh} = \mbox{vgensym}(\mbox{vapp}(\mbox{vapp}(\mbox{ve},\mbox{ve}_1),\mbox{vvar}(\mbox{vx}))) \ \Rightarrow \ \mbox{vx}\ne \mbox{vfresh} )\qquad\mbox{fof}(\mbox{'fresh-unequal-var-3'},\mbox{axiom})$

$\forall \mbox{ve},\mbox{vx},\mbox{vfresh},\mbox{ve}_1{:}\;( \mbox{vfresh} = \mbox{vgensym}(\mbox{vapp}(\mbox{vapp}(\mbox{ve},\mbox{ve}_1),\mbox{vvar}(\mbox{vx}))) \ \Rightarrow \ \neg\,\mbox{visFreeVar}(\mbox{vfresh},\mbox{ve}_1) )\qquad\mbox{fof}(\mbox{'fresh-free-2'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vy},\mbox{vS},\mbox{vT}_2{:}\;( ( \mbox{vx}\ne \mbox{vy}\mbox{ and }\mbox{visFreeVar}(\mbox{vy},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{veabs}),\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{veabs})),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-abs-3'},\mbox{conjecture})$

\medskip\textbf{COM130+1.p} T-subst-abs-1 step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vT}_2{:}\;( ( \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{veabs},\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{veabs}),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-IH-abs'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vy},\mbox{vS},\mbox{ve}_1,\mbox{vT}_2{:}\;( ( \mbox{vx} = \mbox{vy}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{ve}_1),\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{ve}_1)),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-abs-1'},\mbox{conjecture})$

\medskip\textbf{COM001\_1.p} A program correctness theorem

A simple computing state space, with four states - P3, P4,
 P5, and P8 (the full version of this state space is in the
 problem COM002-1). There is a branch at P3 such that the
 following state is either P4 or P8. P8 has a loop back to P3,
 while P4 leads to termination. The problem is to show that
 there is a loop in the computation, passing through P3.




$\mbox{state}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{state\_type},\mbox{type})$

$\mbox{label}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{label\_type},\mbox{type})$

$\mbox{statement}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{statement\_type},\mbox{type})$

$\mbox{register}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{register\_type},\mbox{type})$

$\mbox{number}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{number\_type},\mbox{type})$

$\mbox{boolean}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{boolean\_type},\mbox{type})$

$p_3{:}\;\mbox{state}\qquad\mbox{tff}(\mbox{p3\_type},\mbox{type})$

$p_4{:}\;\mbox{state}\qquad\mbox{tff}(\mbox{p4\_type},\mbox{type})$

$p_5{:}\;\mbox{state}\qquad\mbox{tff}(\mbox{p5\_type},\mbox{type})$

$p_8{:}\;\mbox{state}\qquad\mbox{tff}(\mbox{p8\_type},\mbox{type})$

$n{:}\;\mbox{number}\qquad\mbox{tff}(\mbox{n\_type},\mbox{type})$

$\mbox{register\_j}{:}\;\mbox{register}\qquad\mbox{tff}(\mbox{register\_j\_type},\mbox{type})$

$\mbox{out}{:}\;\mbox{label}\qquad\mbox{tff}(\mbox{out\_type},\mbox{type})$

$\mbox{loop}{:}\;\mbox{label}\qquad\mbox{tff}(\mbox{loop\_type},\mbox{type})$

$\mbox{equal\_function}{:}\;( \mbox{register}\times \mbox{number} )\to \mbox{boolean}\qquad\mbox{tff}(\mbox{equal\_function\_type},\mbox{type})$

$\mbox{goto}{:}\;\mbox{label}\to \mbox{statement}\qquad\mbox{tff}(\mbox{goto\_type},\mbox{type})$

$\mbox{ifthen}{:}\;( \mbox{boolean}\times \mbox{state} )\to \mbox{statement}\qquad\mbox{tff}(\mbox{ifthen\_type},\mbox{type})$

$\mbox{follows}{:}\;( \mbox{state}\times \mbox{state} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{follows\_type},\mbox{type})$

$\mbox{succeeds}{:}\;( \mbox{state}\times \mbox{state} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{succeeds\_type},\mbox{type})$

$\mbox{labels}{:}\;( \mbox{label}\times \mbox{state} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{labels\_type},\mbox{type})$

$\mbox{has}{:}\;( \mbox{state}\times \mbox{statement} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{has\_type},\mbox{type})$

$\forall \mbox{start\_state}{:}\;\mbox{state},\mbox{goal\_state}{:}\;\mbox{state}{:}\;( \mbox{follows}(\mbox{goal\_state},\mbox{start\_state}) \ \Rightarrow \ \mbox{succeeds}(\mbox{goal\_state},\mbox{start\_state}) )\qquad\mbox{tff}(\mbox{direct\_success},\mbox{axiom})$

$\forall \mbox{start\_state}{:}\;\mbox{state},\mbox{intermediate\_state}{:}\;\mbox{state},\mbox{goal\_state}{:}\;\mbox{state}{:}\;( ( \mbox{succeeds}(\mbox{goal\_state},\mbox{intermediate\_state})\mbox{ and }\mbox{succeeds}(\mbox{intermediate\_state},\mbox{start\_state}) ) \ \Rightarrow \ \mbox{succeeds}(\mbox{goal\_state},\mbox{start\_state}) )\qquad\mbox{tff}(\mbox{transitivity\_of\_success},\mbox{axiom})$

$\forall \mbox{goal\_state}{:}\;\mbox{state},\mbox{label}{:}\;\mbox{label},\mbox{start\_state}{:}\;\mbox{state}{:}\;( ( \mbox{has}(\mbox{start\_state},\mbox{goto}(\mbox{label}))\mbox{ and }\mbox{labels}(\mbox{label},\mbox{goal\_state}) ) \ \Rightarrow \ \mbox{succeeds}(\mbox{goal\_state},\mbox{start\_state}) )\qquad\mbox{tff}(\mbox{goto\_success},\mbox{axiom})$

$\forall \mbox{goal\_state}{:}\;\mbox{state},\mbox{condition}{:}\;\mbox{boolean},\mbox{start\_state}{:}\;\mbox{state}{:}\;( \mbox{has}(\mbox{start\_state},\mbox{ifthen}(\mbox{condition},\mbox{goal\_state})) \ \Rightarrow \ \mbox{succeeds}(\mbox{goal\_state},\mbox{start\_state}) )\qquad\mbox{tff}(\mbox{conditional\_success},\mbox{axiom})$

$\mbox{labels}(\mbox{loop},p_3)\qquad\mbox{tff}(\mbox{label\_state}_3,\mbox{hypothesis})$

$\mbox{has}(p_3,\mbox{ifthen}(\mbox{equal\_function}(\mbox{register\_j},n),p_4))\qquad\mbox{tff}(\mbox{state}_3,\mbox{hypothesis})$

$\mbox{has}(p_4,\mbox{goto}(\mbox{out}))\qquad\mbox{tff}(\mbox{state}_4,\mbox{hypothesis})$

$\mbox{follows}(p_5,p_4)\qquad\mbox{tff}(\mbox{transition\_4\_to}_5,\mbox{hypothesis})$

$\mbox{follows}(p_8,p_3)\qquad\mbox{tff}(\mbox{transition\_3\_to}_8,\mbox{hypothesis})$

$\mbox{has}(p_8,\mbox{goto}(\mbox{loop}))\qquad\mbox{tff}(\mbox{state}_8,\mbox{hypothesis})$

$\mbox{succeeds}(p_3,p_3)\qquad\mbox{tff}(\mbox{prove\_there\_is\_a\_loop\_through\_p}_3,\mbox{conjecture})$

\medskip\textbf{COM136+1.p} T-Strong-abs step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{veabs})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{veabs},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{veabs},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong-abs-IH'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vy},\mbox{vS}_1,\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}))\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong-abs'},\mbox{conjecture})$

\medskip\textbf{COM138+1.p} T-Strong-var step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vy},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{vvar}(\mbox{vy}))\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vvar}(\mbox{vy}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vvar}(\mbox{vy}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong-var'},\mbox{conjecture})$

\medskip\textbf{COM123+1.p} T-Weak-FreeVar-abs-1 step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{veabs})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{veabs},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{veabs},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar-abs-IH'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vy},\mbox{vS}_1,\mbox{vT}{:}\;( ( \mbox{vx}\ne \mbox{vy}\mbox{ and }\neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}))\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar-abs-1'},\mbox{conjecture})$

\medskip\textbf{COM003\_1.p} The halting problem is undecidable






$\mbox{program}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{program\_type},\mbox{type})$

$\mbox{algorithm}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{algorithm\_type},\mbox{type})$

$\mbox{input}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{input\_type},\mbox{type})$

$\mbox{output}{:}\;\mbox{\$tType}\qquad\mbox{tff}(\mbox{output\_type},\mbox{type})$

$\mbox{bad}{:}\;\mbox{output}\qquad\mbox{tff}(\mbox{bad\_type},\mbox{type})$

$\mbox{good}{:}\;\mbox{output}\qquad\mbox{tff}(\mbox{good\_type},\mbox{type})$

$\mbox{decides}{:}\;( \mbox{algorithm}\times \mbox{program}\times \mbox{input} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{decides\_type},\mbox{type})$

$\mbox{halts}_2{:}\;( \mbox{program}\times \mbox{input} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{halts2\_type},\mbox{type})$

$\mbox{halts}_3{:}\;( \mbox{program}\times \mbox{program}\times \mbox{input} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{halts3\_type},\mbox{type})$

$\mbox{outputs}{:}\;( \mbox{program}\times \mbox{output} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{outputs\_type},\mbox{type})$

$\mbox{algorithm\_of}{:}\;\mbox{program}\to \mbox{algorithm}\qquad\mbox{tff}(\mbox{algorithm\_of\_type},\mbox{type})$

$\mbox{as\_input}{:}\;\mbox{program}\to \mbox{input}\qquad\mbox{tff}(\mbox{as\_input\_type},\mbox{type})$

$\exists x{:}\;\mbox{algorithm}{:}\;\forall y{:}\;\mbox{program},z{:}\;\mbox{input}{:}\;\mbox{decides}(x,y,z) \ \Rightarrow \ \exists w{:}\;\mbox{program}{:}\;\forall y{:}\;\mbox{program},z{:}\;\mbox{input}{:}\;\mbox{decides}(\mbox{algorithm\_of}(w),y,z)\qquad\mbox{tff}(p_1,\mbox{axiom})$

$\forall w{:}\;\mbox{program},y{:}\;\mbox{program},z{:}\;\mbox{input}{:}\;( \mbox{decides}(\mbox{algorithm\_of}(w),y,z) \ \Rightarrow \ \forall y{:}\;\mbox{program},z{:}\;\mbox{input}{:}\;( ( \mbox{halts}_2(y,z) \ \Rightarrow \ ( \mbox{halts}_3(w,y,z)\mbox{ and }\mbox{outputs}(w,\mbox{good}) ) )\mbox{ and }( \neg\,\mbox{halts}_2(y,z) \ \Rightarrow \ ( \mbox{halts}_3(w,y,z)\mbox{ and }\mbox{outputs}(w,\mbox{bad}) ) ) ) )\qquad\mbox{tff}(p_2,\mbox{axiom})$

$\exists w{:}\;\mbox{program}{:}\;\forall y{:}\;\mbox{program}{:}\;( ( \mbox{halts}_2(y,\mbox{as\_input}(y)) \ \Rightarrow \ ( \mbox{halts}_3(w,y,\mbox{as\_input}(y))\mbox{ and }\mbox{outputs}(w,\mbox{good}) ) )\mbox{ and }( \neg\,\mbox{halts}_2(y,\mbox{as\_input}(y)) \ \Rightarrow \ ( \mbox{halts}_3(w,y,\mbox{as\_input}(y))\mbox{ and }\mbox{outputs}(w,\mbox{bad}) ) ) ) \ \Rightarrow \ \exists v{:}\;\mbox{program}{:}\;\forall y{:}\;\mbox{program}{:}\;( ( \mbox{halts}_2(y,\mbox{as\_input}(y)) \ \Rightarrow \ ( \mbox{halts}_2(v,\mbox{as\_input}(y))\mbox{ and }\mbox{outputs}(v,\mbox{good}) ) )\mbox{ and }( \neg\,\mbox{halts}_2(y,\mbox{as\_input}(y)) \ \Rightarrow \ ( \mbox{halts}_2(v,\mbox{as\_input}(y))\mbox{ and }\mbox{outputs}(v,\mbox{bad}) ) ) )\qquad\mbox{tff}(p_3,\mbox{axiom})$

$\exists v{:}\;\mbox{program}{:}\;\forall y{:}\;\mbox{program}{:}\;( ( \mbox{halts}_2(y,\mbox{as\_input}(y)) \ \Rightarrow \ ( \mbox{halts}_2(v,\mbox{as\_input}(y))\mbox{ and }\mbox{outputs}(v,\mbox{good}) ) )\mbox{ and }( \neg\,\mbox{halts}_2(y,\mbox{as\_input}(y)) \ \Rightarrow \ ( \mbox{halts}_2(v,\mbox{as\_input}(y))\mbox{ and }\mbox{outputs}(v,\mbox{bad}) ) ) ) \ \Rightarrow \ \exists u{:}\;\mbox{program}{:}\;\forall y{:}\;\mbox{program}{:}\;( ( \mbox{halts}_2(y,\mbox{as\_input}(y)) \ \Rightarrow \ \neg\,\mbox{halts}_2(u,\mbox{as\_input}(y)) )\mbox{ and }( \neg\,\mbox{halts}_2(y,\mbox{as\_input}(y)) \ \Rightarrow \ ( \mbox{halts}_2(u,\mbox{as\_input}(y))\mbox{ and }\mbox{outputs}(u,\mbox{bad}) ) ) )\qquad\mbox{tff}(p_4,\mbox{axiom})$

$\neg\,\exists x_1{:}\;\mbox{algorithm}{:}\;\forall y_1{:}\;\mbox{program},z_1{:}\;\mbox{input}{:}\;\mbox{decides}(x_1,y_1,z_1)\qquad\mbox{tff}(\mbox{prove\_this},\mbox{conjecture})$

\medskip\textbf{COM011-1.p} Problem about UNITY theory






$\mbox{include}(\mbox{'Axioms/MSC001-2.ax'})$

$\mbox{include}(\mbox{'Axioms/MSC001-0.ax'})$

$\mbox{c\_in}(\mbox{c\_Relation\_OId},\mbox{c\_UNITY\_OActs}(\mbox{v\_F},\mbox{t\_a}),\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a})))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_OId\_\_in\_\_Acts}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{c\_Relation\_OId},\mbox{c\_UNITY\_OAllowedActs}(\mbox{v\_F},\mbox{t\_a}),\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a})))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_OId\_\_in\_\_AllowedActs}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{v\_A},\mbox{c\_UNIV},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oconstrains\_\_UNIV2}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{c\_UNIV},\mbox{v\_B},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a})) \ \Rightarrow \ \mbox{v\_B} = \mbox{c\_UNIV}\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oconstrains\_\_UNIV\_\_iff1}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{c\_UNIV},\mbox{c\_UNIV},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oconstrains\_\_UNIV\_\_iff2}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{v\_A},\mbox{c\_emptyset},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a})) \ \Rightarrow \ \mbox{v\_A} = \mbox{c\_emptyset}\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oconstrains\_\_empty2\_\_iff1}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{c\_emptyset},\mbox{c\_emptyset},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oconstrains\_\_empty2\_\_iff2}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{c\_emptyset},\mbox{v\_B},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oconstrains\_\_empty}_0,\mbox{axiom})$

$( \mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{v\_A},\mbox{v\_A\_H},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\mbox{ and }\mbox{c\_lessequals}(\mbox{v\_B},\mbox{v\_A},\mbox{tc\_set}(\mbox{t\_a})) ) \ \Rightarrow \ \mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{v\_B},\mbox{v\_A\_H},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oconstrains\_\_weaken\_\_L}_0,\mbox{axiom})$

$\mbox{c\_insert}(\mbox{c\_Relation\_OId},\mbox{c\_UNITY\_OActs}(\mbox{v\_F},\mbox{t\_a}),\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))) = \mbox{c\_UNITY\_OActs}(\mbox{v\_F},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oinsert\_\_Id\_\_Acts}_0,\mbox{axiom})$

$\mbox{c\_insert}(\mbox{c\_Relation\_OId},\mbox{c\_UNITY\_OAllowedActs}(\mbox{v\_F},\mbox{t\_a}),\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))) = \mbox{c\_UNITY\_OAllowedActs}(\mbox{v\_F},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oinsert\_\_Id\_\_AllowedActs}_0,\mbox{axiom})$

$( \mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{c\_minus}(\mbox{v\_A},\mbox{v\_B},\mbox{tc\_set}(\mbox{t\_a})),\mbox{c\_union}(\mbox{v\_A},\mbox{v\_B},\mbox{t\_a}),\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\mbox{ and }\mbox{c\_in}(\mbox{v\_F},\mbox{c\_WFair\_Otransient}(\mbox{c\_minus}(\mbox{v\_A},\mbox{v\_B},\mbox{tc\_set}(\mbox{t\_a})),\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a})) ) \ \Rightarrow \ \mbox{c\_in}(\mbox{v\_F},\mbox{c\_WFair\_Oensures}(\mbox{v\_A},\mbox{v\_B},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_WFair\_OensuresI}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_WFair\_Oensures}(\mbox{v\_A},\mbox{v\_B},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a})) \ \Rightarrow \ \mbox{c\_in}(\mbox{v\_F},\mbox{c\_WFair\_OleadsTo}(\mbox{v\_A},\mbox{v\_B},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_WFair\_OleadsTo\_\_Basis}_0,\mbox{axiom})$

$( \mbox{c\_in}(\mbox{v\_F},\mbox{c\_WFair\_Otransient}(\mbox{v\_A},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\mbox{ and }\mbox{c\_lessequals}(\mbox{v\_B},\mbox{v\_A},\mbox{tc\_set}(\mbox{t\_a})) ) \ \Rightarrow \ \mbox{c\_in}(\mbox{v\_F},\mbox{c\_WFair\_Otransient}(\mbox{v\_B},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_WFair\_Otransient\_\_strengthen}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{v\_A},\mbox{c\_union}(\mbox{v\_A},\mbox{v\_B},\mbox{t\_a}),\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_conjecture}_0,\mbox{negated\_conjecture})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_WFair\_Otransient}(\mbox{v\_A},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_conjecture}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{c\_in}(\mbox{v\_F},\mbox{c\_WFair\_OleadsTo}(\mbox{v\_A},\mbox{v\_B},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_conjecture}_2,\mbox{negated\_conjecture})$

\medskip\textbf{COM131+1.p} T-subst-abs-2 step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vT}_2{:}\;( ( \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{veabs},\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{veabs}),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-IH-abs'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vy},\mbox{vS},\mbox{ve}_1,\mbox{vT}_2{:}\;( ( \mbox{vx} = \mbox{vy}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{ve}_1),\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{ve}_1)),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-abs-1'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vy},\mbox{vS},\mbox{vT}_2{:}\;( ( \mbox{vx}\ne \mbox{vy}\mbox{ and }\neg\,\mbox{visFreeVar}(\mbox{vy},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{veabs}),\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{veabs})),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-abs-2'},\mbox{conjecture})$

\medskip\textbf{COM133+1.p} T-subst-abs step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vT}_2{:}\;( ( \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{veabs},\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{veabs}),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-IH-abs'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vy},\mbox{vS},\mbox{ve}_1,\mbox{vT}_2{:}\;( ( \mbox{vx} = \mbox{vy}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{ve}_1),\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{ve}_1)),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-abs-1'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vy},\mbox{vS},\mbox{vT}_2{:}\;( ( \mbox{vx}\ne \mbox{vy}\mbox{ and }\neg\,\mbox{visFreeVar}(\mbox{vy},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{veabs}),\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{veabs})),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-abs-2'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vy},\mbox{vS},\mbox{vT}_2{:}\;( ( \mbox{vx}\ne \mbox{vy}\mbox{ and }\mbox{visFreeVar}(\mbox{vy},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{veabs}),\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{veabs})),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-abs-3'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vy},\mbox{vS},\mbox{vT}_2{:}\;( ( \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{veabs}),\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{vabs}(\mbox{vy},\mbox{vS},\mbox{veabs})),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-abs'},\mbox{conjecture})$

\medskip\textbf{COM126+1.p} T-Weak-FreeVar-app step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve1app})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve1app},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve1app},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar-app-IH1'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve2app})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve2app},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve2app},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar-app-IH2'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{vapp}(\mbox{ve1app},\mbox{ve2app}))\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vapp}(\mbox{ve1app},\mbox{ve2app}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vapp}(\mbox{ve1app},\mbox{ve2app}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar-app'},\mbox{conjecture})$

\medskip\textbf{COM004-1.p} Part of completeness of resolution

Part of [Bun83]'s proof of the completeness of resolution uses
 the notion of failure nodes. This proves a special case when a
 parent is the empty failure node.




$( \mbox{failure\_node}(x,\mbox{or}(c,p))\mbox{ and }\mbox{failure\_node}(y,\mbox{or}(d,q))\mbox{ and }\mbox{contradictory}(p,q)\mbox{ and }\mbox{siblings}(x,y) ) \ \Rightarrow \ \mbox{failure\_node}(\mbox{parent\_of}(x,y),\mbox{or}(c,d))\qquad\mbox{cnf}(\mbox{make\_node},\mbox{axiom})$

$\mbox{contradictory}(-x,x)\qquad\mbox{cnf}(\mbox{not\_x\_contradicts\_x},\mbox{axiom})$

$\mbox{contradictory}(x,-x)\qquad\mbox{cnf}(\mbox{x\_contradicts\_not\_x},\mbox{axiom})$

$\mbox{siblings}(\mbox{left\_child\_of}(x),\mbox{right\_child\_of}(x))\qquad\mbox{cnf}(\mbox{n\_left\_and\_n\_right\_are\_siblings},\mbox{axiom})$

$\mbox{failure\_node}(\mbox{n\_left},\mbox{or}(\mbox{empty},\mbox{atom}))\qquad\mbox{cnf}(\mbox{n\_left\_is\_atom},\mbox{hypothesis})$

$\mbox{failure\_node}(\mbox{n\_right},\mbox{or}(\mbox{empty},-\mbox{atom}))\qquad\mbox{cnf}(\mbox{n\_right\_is\_not\_atom},\mbox{hypothesis})$

$\mbox{n\_left} = \mbox{left\_child\_of}(n)\qquad\mbox{cnf}(\mbox{n\_left\_equals\_left\_child\_of\_n},\mbox{hypothesis})$

$\mbox{n\_right} = \mbox{right\_child\_of}(n)\qquad\mbox{cnf}(\mbox{n\_right\_equals\_right\_child\_of\_n},\mbox{hypothesis})$

$\neg\,\mbox{failure\_node}(z,\mbox{or}(\mbox{empty},\mbox{empty}))\qquad\mbox{cnf}(\mbox{goal\_is\_there\_an\_empty\_node},\mbox{negated\_conjecture})$

\medskip\textbf{COM009-1.p} Problem about UNITY theory






$\mbox{include}(\mbox{'Axioms/MSC001-2.ax'})$

$\mbox{include}(\mbox{'Axioms/MSC001-0.ax'})$

$\mbox{c\_in}(\mbox{c\_Relation\_OId},\mbox{c\_UNITY\_OActs}(\mbox{v\_F},\mbox{t\_a}),\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a})))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_OId\_\_in\_\_Acts}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{c\_Relation\_OId},\mbox{c\_UNITY\_OAllowedActs}(\mbox{v\_F},\mbox{t\_a}),\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a})))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_OId\_\_in\_\_AllowedActs}_0,\mbox{axiom})$

$\mbox{c\_UNITY\_Oall\_\_total}(\mbox{v\_F},\mbox{t\_a}) \ \Rightarrow \ \mbox{c\_UNITY\_Ototalize}(\mbox{v\_F},\mbox{t\_a}) = \mbox{v\_F}\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oall\_\_total\_\_imp\_\_totalize}_0,\mbox{axiom})$

$\mbox{c\_UNITY\_Oall\_\_total}(\mbox{c\_UNITY\_Ototalize}(\mbox{v\_F},\mbox{t\_a}),\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oall\_\_total\_\_totalize}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{v\_A},\mbox{c\_UNIV},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oconstrains\_\_UNIV2}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{c\_UNIV},\mbox{v\_B},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a})) \ \Rightarrow \ \mbox{v\_B} = \mbox{c\_UNIV}\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oconstrains\_\_UNIV\_\_iff1}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{c\_UNIV},\mbox{c\_UNIV},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oconstrains\_\_UNIV\_\_iff2}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{v\_A},\mbox{c\_emptyset},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a})) \ \Rightarrow \ \mbox{v\_A} = \mbox{c\_emptyset}\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oconstrains\_\_empty2\_\_iff1}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{c\_emptyset},\mbox{c\_emptyset},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oconstrains\_\_empty2\_\_iff2}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{c\_emptyset},\mbox{v\_B},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oconstrains\_\_empty}_0,\mbox{axiom})$

$\mbox{c\_insert}(\mbox{c\_Relation\_OId},\mbox{c\_UNITY\_OActs}(\mbox{v\_F},\mbox{t\_a}),\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))) = \mbox{c\_UNITY\_OActs}(\mbox{v\_F},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oinsert\_\_Id\_\_Acts}_0,\mbox{axiom})$

$\mbox{c\_insert}(\mbox{c\_Relation\_OId},\mbox{c\_UNITY\_OAllowedActs}(\mbox{v\_F},\mbox{t\_a}),\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))) = \mbox{c\_UNITY\_OAllowedActs}(\mbox{v\_F},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oinsert\_\_Id\_\_AllowedActs}_0,\mbox{axiom})$

$\mbox{c\_UNITY\_Ototalize}(\mbox{v\_F},\mbox{t\_a}) = \mbox{v\_F} \ \Rightarrow \ \neg\,\mbox{c\_UNITY\_Oall\_\_total}(\mbox{v\_F},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_conjecture}_0,\mbox{negated\_conjecture})$

$\mbox{c\_UNITY\_Oall\_\_total}(\mbox{v\_F},\mbox{t\_a})\mbox{ or }\mbox{c\_UNITY\_Ototalize}(\mbox{v\_F},\mbox{t\_a}) = \mbox{v\_F}\qquad\mbox{cnf}(\mbox{cls\_conjecture}_1,\mbox{negated\_conjecture})$

\medskip\textbf{COM148+1.p} T-Progress-T-app step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vT}{:}\;( ( \mbox{vtcheck}(\mbox{vempty},\mbox{ve}_1,\mbox{vT})\mbox{ and }\neg\,\mbox{visValue}(\mbox{ve}_1) ) \ \Rightarrow \ \exists \mbox{veout}{:}\;\mbox{vreduce}(\mbox{ve}_1) = \mbox{vsomeExp}(\mbox{veout}) )\qquad\mbox{fof}(\mbox{'T-Progress-T-app-IH1'},\mbox{axiom})$

$\forall \mbox{vT}{:}\;( ( \mbox{vtcheck}(\mbox{vempty},\mbox{ve}_2,\mbox{vT})\mbox{ and }\neg\,\mbox{visValue}(\mbox{ve}_2) ) \ \Rightarrow \ \exists \mbox{veout}{:}\;\mbox{vreduce}(\mbox{ve}_2) = \mbox{vsomeExp}(\mbox{veout}) )\qquad\mbox{fof}(\mbox{'T-Progress-T-app-IH2'},\mbox{axiom})$

$\forall \mbox{vT}{:}\;( ( \mbox{vtcheck}(\mbox{vempty},\mbox{vapp}(\mbox{ve}_1,\mbox{ve}_2),\mbox{vT})\mbox{ and }\neg\,\mbox{visValue}(\mbox{vapp}(\mbox{ve}_1,\mbox{ve}_2)) ) \ \Rightarrow \ \exists \mbox{veout}{:}\;\mbox{vreduce}(\mbox{vapp}(\mbox{ve}_1,\mbox{ve}_2)) = \mbox{vsomeExp}(\mbox{veout}) )\qquad\mbox{fof}(\mbox{'T-Progress-T-app'},\mbox{conjecture})$

\medskip\textbf{COM008+1.p} Induction step in Newman's Lemma






$\forall a{:}\;( ( \mbox{transitive\_reflexive\_rewrite}(b,a)\mbox{ and }\mbox{transitive\_reflexive\_rewrite}(c,a) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{found},\mbox{axiom})$

$\mbox{transitive\_reflexive\_rewrite}(a,b)\mbox{ and }\mbox{transitive\_reflexive\_rewrite}(a,c)\qquad\mbox{fof}(\mbox{assumption},\mbox{axiom})$

$\forall a{:}\;a{=}a\qquad\mbox{fof}(\mbox{reflexivity},\mbox{axiom})$

$\forall a,b{:}\;( a{=}b \ \Rightarrow \ b{=}a )\qquad\mbox{fof}(\mbox{symmetry},\mbox{axiom})$

$\forall a,b{:}\;( a{=}b \ \Rightarrow \ \mbox{transitive\_reflexive\_rewrite}(a,b) )\qquad\mbox{fof}(\mbox{equality\_in\_transitive\_reflexive\_rewrite},\mbox{axiom})$

$\forall a,b{:}\;( \mbox{rewrite}(a,b) \ \Rightarrow \ \mbox{transitive\_reflexive\_rewrite}(a,b) )\qquad\mbox{fof}(\mbox{rewrite\_in\_transitive\_reflexive\_rewrite},\mbox{axiom})$

$\forall a,b,c{:}\;( ( \mbox{transitive\_reflexive\_rewrite}(a,b)\mbox{ and }\mbox{transitive\_reflexive\_rewrite}(b,c) ) \ \Rightarrow \ \mbox{transitive\_reflexive\_rewrite}(a,c) )\qquad\mbox{fof}(\mbox{transitivity\_of\_transitive\_reflexive\_rewrite},\mbox{axiom})$

$\forall a,b,c{:}\;( ( \mbox{rewrite}(a,b)\mbox{ and }\mbox{rewrite}(a,c) ) \ \Rightarrow \ \exists d{:}\;( \mbox{transitive\_reflexive\_rewrite}(b,d)\mbox{ and }\mbox{transitive\_reflexive\_rewrite}(c,d) ) )\qquad\mbox{fof}(\mbox{lo\_cfl},\mbox{axiom})$

$\forall a,b,c{:}\;( ( \mbox{rewrite}(a,a)\mbox{ and }\mbox{transitive\_reflexive\_rewrite}(a,b)\mbox{ and }\mbox{transitive\_reflexive\_rewrite}(a,c) ) \ \Rightarrow \ \exists d{:}\;( \mbox{transitive\_reflexive\_rewrite}(b,d)\mbox{ and }\mbox{transitive\_reflexive\_rewrite}(c,d) ) )\qquad\mbox{fof}(\mbox{ih\_cfl},\mbox{axiom})$

$\forall a,b{:}\;( \mbox{transitive\_reflexive\_rewrite}(a,b) \ \Rightarrow \ ( a{=}b\mbox{ or }\exists c{:}\;( \mbox{rewrite}(a,c)\mbox{ and }\mbox{transitive\_reflexive\_rewrite}(c,b) ) ) )\qquad\mbox{fof}(\mbox{equalish\_or\_rewrite},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{COM134+1.p} T-subst-app step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vT}_2{:}\;( ( \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{ve}_1,\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{ve}_1),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-IH-app1'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vT}_2{:}\;( ( \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{ve}_2,\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{ve}_2),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-IH-app2'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{vT}_2{:}\;( ( \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{vapp}(\mbox{ve}_1,\mbox{ve}_2),\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{vapp}(\mbox{ve}_1,\mbox{ve}_2)),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst-app'},\mbox{conjecture})$

\medskip\textbf{COM011-2.p} Problem about UNITY theory






$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{v\_A},\mbox{c\_union}(\mbox{v\_A},\mbox{v\_B},\mbox{t\_a}),\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_conjecture}_0,\mbox{negated\_conjecture})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_WFair\_Otransient}(\mbox{v\_A},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_conjecture}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{c\_in}(\mbox{v\_F},\mbox{c\_WFair\_OleadsTo}(\mbox{v\_A},\mbox{v\_B},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_conjecture}_2,\mbox{negated\_conjecture})$

$\mbox{c\_in}(\mbox{v\_c},\mbox{c\_minus}(\mbox{v\_A},\mbox{v\_B},\mbox{tc\_set}(\mbox{t\_a})),\mbox{t\_a}) \ \Rightarrow \ \mbox{c\_in}(\mbox{v\_c},\mbox{v\_A},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_Set\_ODiffE}_1,\mbox{axiom})$

$\mbox{c\_in}(\mbox{c\_Main\_OsubsetI\_}_1(\mbox{v\_A},\mbox{v\_B},\mbox{t\_a}),\mbox{v\_A},\mbox{t\_a})\mbox{ or }\mbox{c\_lessequals}(\mbox{v\_A},\mbox{v\_B},\mbox{tc\_set}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_Set\_OsubsetI}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{c\_Main\_OsubsetI\_}_1(\mbox{v\_A},\mbox{v\_B},\mbox{t\_a}),\mbox{v\_B},\mbox{t\_a}) \ \Rightarrow \ \mbox{c\_lessequals}(\mbox{v\_A},\mbox{v\_B},\mbox{tc\_set}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_Set\_OsubsetI}_1,\mbox{axiom})$

$( \mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{v\_A},\mbox{v\_A\_H},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\mbox{ and }\mbox{c\_lessequals}(\mbox{v\_B},\mbox{v\_A},\mbox{tc\_set}(\mbox{t\_a})) ) \ \Rightarrow \ \mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{v\_B},\mbox{v\_A\_H},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oconstrains\_\_weaken\_\_L}_0,\mbox{axiom})$

$( \mbox{c\_in}(\mbox{v\_F},\mbox{c\_UNITY\_Oconstrains}(\mbox{c\_minus}(\mbox{v\_A},\mbox{v\_B},\mbox{tc\_set}(\mbox{t\_a})),\mbox{c\_union}(\mbox{v\_A},\mbox{v\_B},\mbox{t\_a}),\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\mbox{ and }\mbox{c\_in}(\mbox{v\_F},\mbox{c\_WFair\_Otransient}(\mbox{c\_minus}(\mbox{v\_A},\mbox{v\_B},\mbox{tc\_set}(\mbox{t\_a})),\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a})) ) \ \Rightarrow \ \mbox{c\_in}(\mbox{v\_F},\mbox{c\_WFair\_Oensures}(\mbox{v\_A},\mbox{v\_B},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_WFair\_OensuresI}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{v\_F},\mbox{c\_WFair\_Oensures}(\mbox{v\_A},\mbox{v\_B},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a})) \ \Rightarrow \ \mbox{c\_in}(\mbox{v\_F},\mbox{c\_WFair\_OleadsTo}(\mbox{v\_A},\mbox{v\_B},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_WFair\_OleadsTo\_\_Basis}_0,\mbox{axiom})$

$( \mbox{c\_in}(\mbox{v\_F},\mbox{c\_WFair\_Otransient}(\mbox{v\_A},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\mbox{ and }\mbox{c\_lessequals}(\mbox{v\_B},\mbox{v\_A},\mbox{tc\_set}(\mbox{t\_a})) ) \ \Rightarrow \ \mbox{c\_in}(\mbox{v\_F},\mbox{c\_WFair\_Otransient}(\mbox{v\_B},\mbox{t\_a}),\mbox{tc\_UNITY\_Oprogram}(\mbox{t\_a}))\qquad\mbox{cnf}(\mbox{cls\_WFair\_Otransient\_\_strengthen}_0,\mbox{axiom})$

\medskip\textbf{COM124+1.p} T-Weak-FreeVar-abs-2 step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/COM001+1.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vy},\mbox{vS}_1,\mbox{ve}_1,\mbox{vT}{:}\;( ( \mbox{vx}\ne \mbox{vy}\mbox{ and }\neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{ve}_1))\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{ve}_1),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{ve}_1),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar-abs-1-gen'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vy},\mbox{vS}_1,\mbox{vT}{:}\;( ( \mbox{vx} = \mbox{vy}\mbox{ and }\neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}))\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar-abs-2'},\mbox{conjecture})$

\medskip\textbf{COM150+1.p} Axioms for progress/preservation proof






$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/COM001+1.ax'})$

\medskip\textbf{COM146+1.p} T-Preservation-T-var step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar'},\mbox{axiom})$

$\forall \mbox{vT},\mbox{vC},\mbox{vx},\mbox{ve},\mbox{ve}_2,\mbox{vT}_2{:}\;( ( \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vT},\mbox{vC}),\mbox{ve}_2,\mbox{vT}_2) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{vsubst}(\mbox{vx},\mbox{ve},\mbox{ve}_2),\mbox{vT}_2) )\qquad\mbox{fof}(\mbox{'T-subst'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vC},\mbox{veout},\mbox{vT}{:}\;( ( \mbox{vreduce}(\mbox{vvar}(\mbox{vx})) = \mbox{vsomeExp}(\mbox{veout})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vvar}(\mbox{vx}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{veout},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Preservation-T-var'},\mbox{conjecture})$

\medskip\textbf{COM008+2.p} Induction step in Newman's Lemma






$\forall a{:}\;( ( \mbox{transitive\_reflexive\_rewrite}(b,a)\mbox{ and }\mbox{transitive\_reflexive\_rewrite}(c,a) ) \ \Rightarrow \ \mbox{goal} )\qquad\mbox{fof}(\mbox{found},\mbox{axiom})$

$\mbox{transitive\_reflexive\_rewrite}(a,b)\mbox{ and }\mbox{transitive\_reflexive\_rewrite}(a,c)\qquad\mbox{fof}(\mbox{assumption},\mbox{axiom})$

$\forall a,b{:}\;( a = b \ \Rightarrow \ \mbox{transitive\_reflexive\_rewrite}(a,b) )\qquad\mbox{fof}(\mbox{equality\_in\_transitive\_reflexive\_rewrite},\mbox{axiom})$

$\forall a,b{:}\;( \mbox{rewrite}(a,b) \ \Rightarrow \ \mbox{transitive\_reflexive\_rewrite}(a,b) )\qquad\mbox{fof}(\mbox{rewrite\_in\_transitive\_reflexive\_rewrite},\mbox{axiom})$

$\forall a,b,c{:}\;( ( \mbox{transitive\_reflexive\_rewrite}(a,b)\mbox{ and }\mbox{transitive\_reflexive\_rewrite}(b,c) ) \ \Rightarrow \ \mbox{transitive\_reflexive\_rewrite}(a,c) )\qquad\mbox{fof}(\mbox{transitivity\_of\_transitive\_reflexive\_rewrite},\mbox{axiom})$

$\forall a,b,c{:}\;( ( \mbox{rewrite}(a,b)\mbox{ and }\mbox{rewrite}(a,c) ) \ \Rightarrow \ \exists d{:}\;( \mbox{transitive\_reflexive\_rewrite}(b,d)\mbox{ and }\mbox{transitive\_reflexive\_rewrite}(c,d) ) )\qquad\mbox{fof}(\mbox{lo\_cfl},\mbox{axiom})$

$\forall a,b,c{:}\;( ( \mbox{rewrite}(a,a)\mbox{ and }\mbox{transitive\_reflexive\_rewrite}(a,b)\mbox{ and }\mbox{transitive\_reflexive\_rewrite}(a,c) ) \ \Rightarrow \ \exists d{:}\;( \mbox{transitive\_reflexive\_rewrite}(b,d)\mbox{ and }\mbox{transitive\_reflexive\_rewrite}(c,d) ) )\qquad\mbox{fof}(\mbox{ih\_cfl},\mbox{axiom})$

$\forall a,b{:}\;( \mbox{transitive\_reflexive\_rewrite}(a,b) \ \Rightarrow \ ( a = b\mbox{ or }\exists c{:}\;( \mbox{rewrite}(a,c)\mbox{ and }\mbox{transitive\_reflexive\_rewrite}(c,b) ) ) )\qquad\mbox{fof}(\mbox{equal\_or\_rewrite},\mbox{axiom})$

$\mbox{goal}\qquad\mbox{fof}(\mbox{goal\_to\_be\_proved},\mbox{conjecture})$

\medskip\textbf{COM010-1.p} Problem about UNITY theory






$\mbox{include}(\mbox{'Axioms/MSC001-1.ax'})$

$\mbox{include}(\mbox{'Axioms/MSC001-0.ax'})$

$\mbox{c\_UNITY\_OActs}(\mbox{c\_UNITY\_Omk\_\_program}(\mbox{c\_Pair}(\mbox{v\_init},\mbox{c\_Pair}(\mbox{v\_acts},\mbox{v\_allowed},\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))),\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a})))),\mbox{tc\_set}(\mbox{t\_a}),\mbox{tc\_prod}(\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))),\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))))),\mbox{t\_a}),\mbox{t\_a}) = \mbox{c\_insert}(\mbox{c\_Relation\_OId},\mbox{v\_acts},\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a})))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_OActs\_\_eq}_0,\mbox{axiom})$

$\mbox{c\_UNITY\_OActs}(\mbox{v\_F},\mbox{t\_a})\ne \mbox{c\_emptyset}\qquad\mbox{cnf}(\mbox{cls\_UNITY\_OActs\_\_nonempty}_0,\mbox{axiom})$

$\mbox{c\_UNITY\_OAllowedActs}(\mbox{c\_UNITY\_Omk\_\_program}(\mbox{c\_Pair}(\mbox{v\_init},\mbox{c\_Pair}(\mbox{v\_acts},\mbox{v\_allowed},\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))),\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a})))),\mbox{tc\_set}(\mbox{t\_a}),\mbox{tc\_prod}(\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))),\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))))),\mbox{t\_a}),\mbox{t\_a}) = \mbox{c\_insert}(\mbox{c\_Relation\_OId},\mbox{v\_allowed},\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a})))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_OAllowedActs\_\_eq}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{c\_Relation\_OId},\mbox{c\_UNITY\_OActs}(\mbox{v\_F},\mbox{t\_a}),\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a})))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_OId\_\_in\_\_Acts}_0,\mbox{axiom})$

$\mbox{c\_in}(\mbox{c\_Relation\_OId},\mbox{c\_UNITY\_OAllowedActs}(\mbox{v\_F},\mbox{t\_a}),\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a})))\qquad\mbox{cnf}(\mbox{cls\_UNITY\_OId\_\_in\_\_AllowedActs}_0,\mbox{axiom})$

$\mbox{c\_UNITY\_OInit}(\mbox{c\_UNITY\_Omk\_\_program}(\mbox{c\_Pair}(\mbox{v\_y},\mbox{c\_Pair}(\mbox{v\_acts},\mbox{v\_allowed},\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))),\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a})))),\mbox{tc\_set}(\mbox{t\_a}),\mbox{tc\_prod}(\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))),\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))))),\mbox{t\_a}),\mbox{t\_a}) = \mbox{v\_y}\qquad\mbox{cnf}(\mbox{cls\_UNITY\_OInit\_\_eq}_0,\mbox{axiom})$

$\mbox{c\_insert}(\mbox{c\_Relation\_OId},\mbox{c\_UNITY\_OActs}(\mbox{v\_F},\mbox{t\_a}),\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))) = \mbox{c\_UNITY\_OActs}(\mbox{v\_F},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oinsert\_\_Id\_\_Acts}_0,\mbox{axiom})$

$\mbox{c\_insert}(\mbox{c\_Relation\_OId},\mbox{c\_UNITY\_OAllowedActs}(\mbox{v\_F},\mbox{t\_a}),\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))) = \mbox{c\_UNITY\_OAllowedActs}(\mbox{v\_F},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Oinsert\_\_Id\_\_AllowedActs}_0,\mbox{axiom})$

$\mbox{c\_UNITY\_Omk\_\_program}(\mbox{c\_Pair}(\mbox{c\_UNITY\_OInit}(\mbox{v\_y},\mbox{t\_a}),\mbox{c\_Pair}(\mbox{c\_UNITY\_OActs}(\mbox{v\_y},\mbox{t\_a}),\mbox{c\_UNITY\_OAllowedActs}(\mbox{v\_y},\mbox{t\_a}),\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))),\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a})))),\mbox{tc\_set}(\mbox{t\_a}),\mbox{tc\_prod}(\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))),\mbox{tc\_set}(\mbox{tc\_set}(\mbox{tc\_prod}(\mbox{t\_a},\mbox{t\_a}))))),\mbox{t\_a}) = \mbox{v\_y}\qquad\mbox{cnf}(\mbox{cls\_UNITY\_Osurjective\_\_mk\_\_program}_0,\mbox{axiom})$

$\mbox{c\_UNITY\_OInit}(\mbox{v\_F},\mbox{t\_a}) = \mbox{c\_UNITY\_OInit}(\mbox{v\_G},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_conjecture}_0,\mbox{negated\_conjecture})$

$\mbox{c\_UNITY\_OActs}(\mbox{v\_F},\mbox{t\_a}) = \mbox{c\_UNITY\_OActs}(\mbox{v\_G},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_conjecture}_1,\mbox{negated\_conjecture})$

$\mbox{c\_UNITY\_OAllowedActs}(\mbox{v\_F},\mbox{t\_a}) = \mbox{c\_UNITY\_OAllowedActs}(\mbox{v\_G},\mbox{t\_a})\qquad\mbox{cnf}(\mbox{cls\_conjecture}_2,\mbox{negated\_conjecture})$

$\mbox{v\_F}\ne \mbox{v\_G}\qquad\mbox{cnf}(\mbox{cls\_conjecture}_3,\mbox{negated\_conjecture})$

\medskip\textbf{COM147+1.p} T-Progress-T-abs step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vT}{:}\;( ( \mbox{vtcheck}(\mbox{vempty},\mbox{ve}_1,\mbox{vT})\mbox{ and }\neg\,\mbox{visValue}(\mbox{ve}_1) ) \ \Rightarrow \ \exists \mbox{veout}{:}\;\mbox{vreduce}(\mbox{ve}_1) = \mbox{vsomeExp}(\mbox{veout}) )\qquad\mbox{fof}(\mbox{'T-Progress-T-abs-IH'},\mbox{axiom})$

$\forall \mbox{vTin},\mbox{vx},\mbox{vS}{:}\;( ( \mbox{vtcheck}(\mbox{vempty},\mbox{vabs}(\mbox{vx},\mbox{vS},\mbox{ve}_1),\mbox{vTin})\mbox{ and }\neg\,\mbox{visValue}(\mbox{vabs}(\mbox{vx},\mbox{vS},\mbox{ve}_1)) ) \ \Rightarrow \ \exists \mbox{veout}{:}\;\mbox{vreduce}(\mbox{vabs}(\mbox{vx},\mbox{vS},\mbox{ve}_1)) = \mbox{vsomeExp}(\mbox{veout}) )\qquad\mbox{fof}(\mbox{'T-Progress-T-abs'},\mbox{conjecture})$

\medskip\textbf{COM003+3.p} The halting problem is undecidable






$\exists x{:}\;( \mbox{algorithm}(x)\mbox{ and }\forall y{:}\;( \mbox{program}(y) \ \Rightarrow \ \forall z{:}\;\mbox{decides}(x,y,z) ) ) \ \Rightarrow \ \exists w{:}\;( \mbox{program}(w)\mbox{ and }\forall y{:}\;( \mbox{program}(y) \ \Rightarrow \ \forall z{:}\;\mbox{decides}(w,y,z) ) )\qquad\mbox{fof}(p_1,\mbox{axiom})$

$\forall w{:}\;( ( \mbox{program}(w)\mbox{ and }\forall y{:}\;( \mbox{program}(y) \ \Rightarrow \ \forall z{:}\;\mbox{decides}(w,y,z) ) ) \ \Rightarrow \ \forall y,z{:}\;( ( ( \mbox{program}(y)\mbox{ and }\mbox{halts}_2(y,z) ) \ \Rightarrow \ ( \mbox{halts}_3(w,y,z)\mbox{ and }\mbox{outputs}(w,\mbox{good}) ) )\mbox{ and }( ( \mbox{program}(y)\mbox{ and }\neg\,\mbox{halts}_2(y,z) ) \ \Rightarrow \ ( \mbox{halts}_3(w,y,z)\mbox{ and }\mbox{outputs}(w,\mbox{bad}) ) ) ) )\qquad\mbox{fof}(p_2,\mbox{axiom})$

$\forall w{:}\;( ( \mbox{program}(w)\mbox{ and }\forall y,z{:}\;( ( ( \mbox{program}(y)\mbox{ and }\mbox{halts}_2(y,z) ) \ \Rightarrow \ ( \mbox{halts}_3(w,y,z)\mbox{ and }\mbox{outputs}(w,\mbox{good}) ) )\mbox{ and }( ( \mbox{program}(y)\mbox{ and }\neg\,\mbox{halts}_2(y,z) ) \ \Rightarrow \ ( \mbox{halts}_3(w,y,z)\mbox{ and }\mbox{outputs}(w,\mbox{bad}) ) ) ) ) \ \Rightarrow \ \exists v{:}\;( \mbox{program}(v)\mbox{ and }\forall y{:}\;( ( ( \mbox{program}(y)\mbox{ and }\mbox{halts}_3(w,y,y)\mbox{ and }\mbox{outputs}(w,\mbox{good}) ) \ \Rightarrow \ \neg\,\mbox{halts}_2(v,y) )\mbox{ and }( ( \mbox{program}(y)\mbox{ and }\mbox{halts}_3(w,y,y)\mbox{ and }\mbox{outputs}(w,\mbox{bad}) ) \ \Rightarrow \ ( \mbox{halts}_2(v,y)\mbox{ and }\mbox{outputs}(v,\mbox{bad}) ) ) ) ) )\qquad\mbox{fof}(p_3,\mbox{axiom})$

$\neg\,\exists x_1{:}\;( \mbox{algorithm}(x_1)\mbox{ and }\forall y_1{:}\;( \mbox{program}(y_1) \ \Rightarrow \ \forall z_1{:}\;\mbox{decides}(x_1,y_1,z_1) ) )\qquad\mbox{fof}(\mbox{prove\_this},\mbox{conjecture})$

\medskip\textbf{COM125+1.p} T-Weak-FreeVar-abs step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{veabs})\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{veabs},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{veabs},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar-abs-IH'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vy},\mbox{vS}_1,\mbox{vT}{:}\;( ( \mbox{vx}\ne \mbox{vy}\mbox{ and }\neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}))\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar-abs-1'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vy},\mbox{vS}_1,\mbox{vT}{:}\;( ( \mbox{vx} = \mbox{vy}\mbox{ and }\neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}))\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar-abs-2'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vy},\mbox{vS}_1,\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}))\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar-abs'},\mbox{conjecture})$

\medskip\textbf{COM143+1.p} T-Weak-var step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vy},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vvar}(\mbox{vy}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vvar}(\mbox{vy}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-var'},\mbox{conjecture})$

\medskip\textbf{COM127+1.p} T-Weak-FreeVar-var step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{ve},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{ve})\mbox{ and }\mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{ve},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vC},\mbox{ve},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Strong'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vy},\mbox{vT}{:}\;( ( \neg\,\mbox{visFreeVar}(\mbox{vx},\mbox{vvar}(\mbox{vy}))\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vvar}(\mbox{vy}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vvar}(\mbox{vy}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-FreeVar-var'},\mbox{conjecture})$

\medskip\textbf{COM140+1.p} T-Weak-abs-2 step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\mbox{include}(\mbox{'Axioms/COM001+1.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vy},\mbox{vS}_1,\mbox{ve}_1,\mbox{vT}{:}\;( ( \mbox{vx}\ne \mbox{vy}\mbox{ and }\mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{ve}_1),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{ve}_1),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-abs-1-gen'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vy},\mbox{vS}_1,\mbox{vT}{:}\;( ( \mbox{vx} = \mbox{vy}\mbox{ and }\mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-abs-2'},\mbox{conjecture})$

\medskip\textbf{COM139+1.p} T-Weak-abs-1 step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{veabs},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{veabs},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-abs-IH'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vy},\mbox{vS}_1,\mbox{vT}{:}\;( ( \mbox{vx}\ne \mbox{vy}\mbox{ and }\mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-abs-1'},\mbox{conjecture})$

\medskip\textbf{COM141+1.p} T-Weak-abs step in progress/preservation proof

This problem is a step within the proof of progress and 
 preservation for the standard type system for the simply-typed 
 lambda calculus.




$\mbox{include}(\mbox{'Axioms/COM001+0.ax'})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{veabs},\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{veabs},\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-abs-IH'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vy},\mbox{vS}_1,\mbox{vT}{:}\;( ( \mbox{vx}\ne \mbox{vy}\mbox{ and }\mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-abs-1'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vy},\mbox{vS}_1,\mbox{vT}{:}\;( ( \mbox{vx} = \mbox{vy}\mbox{ and }\mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-abs-2'},\mbox{axiom})$

$\forall \mbox{vx},\mbox{vS},\mbox{vC},\mbox{vy},\mbox{vS}_1,\mbox{vT}{:}\;( ( \mbox{vlookup}(\mbox{vx},\mbox{vC}) = \mbox{vnoType}\mbox{ and }\mbox{vtcheck}(\mbox{vC},\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) ) \ \Rightarrow \ \mbox{vtcheck}(\mbox{vbind}(\mbox{vx},\mbox{vS},\mbox{vC}),\mbox{vabs}(\mbox{vy},\mbox{vS}_1,\mbox{veabs}),\mbox{vT}) )\qquad\mbox{fof}(\mbox{'T-Weak-abs'},\mbox{conjecture})$

\medskip
\end{document}