\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{NUN025$\wedge$1.p} Function h s.t. h(0) = 1, h(1) = 0, h(2) = 1, no witness

Using an axiomatiztion of if-then-else, find the if-then-else
 term that expresses the function H.




$0{:}\;\mbox{\$i}\qquad\mbox{thf}(n_6,\mbox{type})$

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

$\mbox{ite}{:}\;\mbox{\$o}\to \mbox{\$i}\to \mbox{\$i}\to \mbox{\$i}\qquad\mbox{thf}(n_8,\mbox{type})$

$( \forall x_{100}{:}\;\mbox{\$o},u{:}\;\mbox{\$i},v{:}\;\mbox{\$i}{:}\;( x_{100} \ \Rightarrow \ ( \mbox{ite}@ x_{100}@ u@ v ) = u )\mbox{ and }\forall x_{100}{:}\;\mbox{\$o},u{:}\;\mbox{\$i},v{:}\;\mbox{\$i}{:}\;( \neg\,x_{100} \ \Rightarrow \ ( \mbox{ite}@ x_{100}@ u@ v ) = v )\mbox{ and }\forall x{:}\;\mbox{\$i}{:}\;( s@ x )\ne x ) \ \Rightarrow \ \exists h{:}\;\mbox{\$i}\to \mbox{\$i}{:}\;( ( h@ 0 ) = ( s@ 0 )\mbox{ and }( h@ ( s@ 0 ) ) = 0\mbox{ and }( h@ ( s@ ( s@ 0 ) ) ) = ( s@ 0 ) )\qquad\mbox{thf}(n_9,\mbox{conjecture})$

\medskip\textbf{NUN024$\wedge$1.p} Function h s.t. h(0) = 1, h(1) = 0, h(2) = 0, no witness

Using an axiomatiztion of if-then-else, find the if-then-else
 term that expresses the function H.




$0{:}\;\mbox{\$i}\qquad\mbox{thf}(n_6,\mbox{type})$

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

$\mbox{ite}{:}\;\mbox{\$o}\to \mbox{\$i}\to \mbox{\$i}\to \mbox{\$i}\qquad\mbox{thf}(n_8,\mbox{type})$

$( \forall x_{100}{:}\;\mbox{\$o},u{:}\;\mbox{\$i},v{:}\;\mbox{\$i}{:}\;( x_{100} \ \Rightarrow \ ( \mbox{ite}@ x_{100}@ u@ v ) = u )\mbox{ and }\forall x_{100}{:}\;\mbox{\$o},u{:}\;\mbox{\$i},v{:}\;\mbox{\$i}{:}\;( \neg\,x_{100} \ \Rightarrow \ ( \mbox{ite}@ x_{100}@ u@ v ) = v )\mbox{ and }\forall x{:}\;\mbox{\$i}{:}\;( s@ x )\ne 0\mbox{ and }\forall x{:}\;\mbox{\$i}{:}\;( s@ x )\ne x ) \ \Rightarrow \ \exists h{:}\;\mbox{\$i}\to \mbox{\$i}{:}\;( ( h@ 0 ) = ( s@ 0 )\mbox{ and }( h@ ( s@ 0 ) ) = 0\mbox{ and }( h@ ( s@ ( s@ 0 ) ) ) = 0 )\qquad\mbox{thf}(n_9,\mbox{conjecture})$

\medskip\textbf{NUN020+1.p} Axioms for RDN arithmetic






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

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

$\mbox{include}(\mbox{'Axioms/NUM005+2.ax'})$

\medskip\textbf{NUN025$\wedge$3.p} Function h s.t. h(0) = 1, h(1) = 0, h(2) = 1, with witness

Using an axiomatiztion of if-then-else, find the if-then-else
 term that expresses the function H.




$0{:}\;\mbox{\$i}\qquad\mbox{thf}(n_6,\mbox{type})$

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

$\mbox{ite}{:}\;\mbox{\$o}\to \mbox{\$i}\to \mbox{\$i}\to \mbox{\$i}\qquad\mbox{thf}(n_8,\mbox{type})$

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

$( \forall x_{100}{:}\;\mbox{\$o},u{:}\;\mbox{\$i},v{:}\;\mbox{\$i}{:}\;( x_{100} \ \Rightarrow \ ( \mbox{ite}@ x_{100}@ u@ v ) = u )\mbox{ and }\forall x_{100}{:}\;\mbox{\$o},u{:}\;\mbox{\$i},v{:}\;\mbox{\$i}{:}\;( \neg\,x_{100} \ \Rightarrow \ ( \mbox{ite}@ x_{100}@ u@ v ) = v )\mbox{ and }\forall x{:}\;\mbox{\$i}{:}\;( s@ x )\ne 0\mbox{ and }\forall x{:}\;\mbox{\$i}{:}\;( s@ x )\ne x\mbox{ and }\forall x{:}\;\mbox{\$i}{:}\;( h@ x ) = ( \mbox{ite}@ x = 0@ ( s@ 0 )@ ( \mbox{ite}@ x = ( s@ 0 )@ 0@ ( s@ 0 ) ) ) ) \ \Rightarrow \ \exists h{:}\;\mbox{\$i}\to \mbox{\$i}{:}\;( ( h@ 0 ) = ( s@ 0 )\mbox{ and }( h@ ( s@ 0 ) ) = 0\mbox{ and }( h@ ( s@ ( s@ 0 ) ) ) = ( s@ 0 ) )\qquad\mbox{thf}(n_{10},\mbox{conjecture})$

\medskip\textbf{NUN021$\wedge$1.p} Axioms for Church Numerals in Simple Type Theory






$\mbox{include}(\mbox{'Axioms/NUM006\string^0.ax'})$

\medskip\textbf{NUN024$\wedge$2.p} Function h s.t. h(0) = 1, h(1) = 0, h(2) = 0, with witness

Using an axiomatiztion of if-then-else, find the if-then-else
 term that expresses the function H.




$0{:}\;\mbox{\$i}\qquad\mbox{thf}(n_6,\mbox{type})$

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

$\mbox{ite}{:}\;\mbox{\$o}\to \mbox{\$i}\to \mbox{\$i}\to \mbox{\$i}\qquad\mbox{thf}(n_8,\mbox{type})$

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

$( \forall x_{100}{:}\;\mbox{\$o},u{:}\;\mbox{\$i},v{:}\;\mbox{\$i}{:}\;( x_{100} \ \Rightarrow \ ( \mbox{ite}@ x_{100}@ u@ v ) = u )\mbox{ and }\forall x_{100}{:}\;\mbox{\$o},u{:}\;\mbox{\$i},v{:}\;\mbox{\$i}{:}\;( \neg\,x_{100} \ \Rightarrow \ ( \mbox{ite}@ x_{100}@ u@ v ) = v )\mbox{ and }\forall x{:}\;\mbox{\$i}{:}\;( s@ x )\ne 0\mbox{ and }\forall x{:}\;\mbox{\$i}{:}\;( s@ x )\ne x\mbox{ and }\forall x{:}\;\mbox{\$i}{:}\;( h@ x ) = ( \mbox{ite}@ x = 0@ ( s@ 0 )@ 0 ) ) \ \Rightarrow \ \exists h{:}\;\mbox{\$i}\to \mbox{\$i}{:}\;( ( h@ 0 ) = ( s@ 0 )\mbox{ and }( h@ ( s@ 0 ) ) = 0\mbox{ and }( h@ ( s@ ( s@ 0 ) ) ) = 0 )\qquad\mbox{thf}(n_{10},\mbox{conjecture})$

\medskip\textbf{NUN025$\wedge$2.p} Function h s.t. h(0) = 1, h(1) = 0, h(2) = 1, with witness

Using an axiomatiztion of if-then-else, find the if-then-else
 term that expresses the function H.




$0{:}\;\mbox{\$i}\qquad\mbox{thf}(n_6,\mbox{type})$

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

$\mbox{ite}{:}\;\mbox{\$o}\to \mbox{\$i}\to \mbox{\$i}\to \mbox{\$i}\qquad\mbox{thf}(n_8,\mbox{type})$

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

$( \forall x_{100}{:}\;\mbox{\$o},u{:}\;\mbox{\$i},v{:}\;\mbox{\$i}{:}\;( x_{100} \ \Rightarrow \ ( \mbox{ite}@ x_{100}@ u@ v ) = u )\mbox{ and }\forall x_{100}{:}\;\mbox{\$o},u{:}\;\mbox{\$i},v{:}\;\mbox{\$i}{:}\;( \neg\,x_{100} \ \Rightarrow \ ( \mbox{ite}@ x_{100}@ u@ v ) = v )\mbox{ and }\forall x{:}\;\mbox{\$i}{:}\;( s@ x )\ne x\mbox{ and }\forall x{:}\;\mbox{\$i}{:}\;( h@ x ) = ( \mbox{ite}@ x = ( s@ 0 )@ 0@ ( s@ 0 ) ) ) \ \Rightarrow \ \exists h{:}\;\mbox{\$i}\to \mbox{\$i}{:}\;( ( h@ 0 ) = ( s@ 0 )\mbox{ and }( h@ ( s@ 0 ) ) = 0\mbox{ and }( h@ ( s@ ( s@ 0 ) ) ) = ( s@ 0 ) )\qquad\mbox{thf}(n_{10},\mbox{conjecture})$

\medskip\textbf{NUN023$\wedge$2.p} Function h s.t. h(0) = 1, h(1) = 0, with witness

Using an axiomatiztion of if-then-else, find the if-then-else
 term that expresses the function H.




$0{:}\;\mbox{\$i}\qquad\mbox{thf}(n_6,\mbox{type})$

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

$\mbox{ite}{:}\;\mbox{\$o}\to \mbox{\$i}\to \mbox{\$i}\to \mbox{\$i}\qquad\mbox{thf}(n_8,\mbox{type})$

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

$( \forall x_{100}{:}\;\mbox{\$o},u{:}\;\mbox{\$i},v{:}\;\mbox{\$i}{:}\;( x_{100} \ \Rightarrow \ ( \mbox{ite}@ x_{100}@ u@ v ) = u )\mbox{ and }\forall x_{100}{:}\;\mbox{\$o},u{:}\;\mbox{\$i},v{:}\;\mbox{\$i}{:}\;( \neg\,x_{100} \ \Rightarrow \ ( \mbox{ite}@ x_{100}@ u@ v ) = v )\mbox{ and }\forall x{:}\;\mbox{\$i}{:}\;( h@ x ) = ( \mbox{ite}@ x = 0@ ( s@ 0 )@ 0 ) ) \ \Rightarrow \ \exists h{:}\;\mbox{\$i}\to \mbox{\$i}{:}\;( ( h@ 0 ) = ( s@ 0 )\mbox{ and }( h@ ( s@ 0 ) ) = 0 )\qquad\mbox{thf}(n_{10},\mbox{conjecture})$

\medskip\textbf{NUN022$\wedge$1.p} Find this function

Does there exist a function f from reals to reals such that 
 for all x and y, f(x + y * y) - f(x) $>$= y?




$\exists f{:}\;\mbox{\$real}\to \mbox{\$real}{:}\;\forall x{:}\;\mbox{\$real},y{:}\;\mbox{\$real}{:}\;( \mbox{\$lesseq}@ ( \mbox{\$difference}@ ( f@ ( \mbox{\$sum}@ x@ ( \mbox{\$product}@ y@ y ) ) )@ ( f@ x ) )@ y )\qquad\mbox{thf}(\mbox{jasmin},\mbox{conjecture})$

\medskip\textbf{NUN023$\wedge$1.p} Function h s.t. h(0) = 1, h(1) = 0, no witness

Using an axiomatiztion of if-then-else, find the if-then-else
 term that expresses the function H.




$0{:}\;\mbox{\$i}\qquad\mbox{thf}(n_5,\mbox{type})$

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

$\mbox{ite}{:}\;\mbox{\$o}\to \mbox{\$i}\to \mbox{\$i}\to \mbox{\$i}\qquad\mbox{thf}(n_7,\mbox{type})$

$( \forall x{:}\;\mbox{\$o},u{:}\;\mbox{\$i},v{:}\;\mbox{\$i}{:}\;( x \ \Rightarrow \ ( \mbox{ite}@ x@ u@ v ) = u )\mbox{ and }\forall x{:}\;\mbox{\$o},u{:}\;\mbox{\$i},v{:}\;\mbox{\$i}{:}\;( \neg\,x \ \Rightarrow \ ( \mbox{ite}@ x@ u@ v ) = v ) ) \ \Rightarrow \ \exists h{:}\;\mbox{\$i}\to \mbox{\$i}{:}\;( ( h@ 0 ) = ( s@ 0 )\mbox{ and }( h@ ( s@ 0 ) ) = 0 )\qquad\mbox{thf}(n_8,\mbox{conjecture})$

\medskip\textbf{NUN019+1.p} Peano greater and unequal






$\forall x{:}\;\mbox{greater}(s(x),x)\qquad\mbox{fof}(\mbox{greater}_0,\mbox{axiom})$

$\forall x,y{:}\;( \mbox{greater}(x,y) \ \Rightarrow \ \mbox{greater}(s(x),y) )\qquad\mbox{fof}(\mbox{greater}_1,\mbox{axiom})$

$\forall x,y{:}\;( \mbox{greater}(x,y) \ \Rightarrow \ x\ne y )\qquad\mbox{fof}(\mbox{not\_equal}_0,\mbox{axiom})$

\medskip
\end{document}