\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{DAT004=0.ax} Array data types






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

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

$\mbox{mkarray}{:}\;\mbox{array}\qquad\mbox{tff}(\mbox{mkarray\_type},\mbox{type})$

$\mbox{none}{:}\;\mbox{data}\qquad\mbox{tff}(\mbox{none\_type},\mbox{type})$

$\mbox{put}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{data} )\to \mbox{array}\qquad\mbox{tff}(\mbox{put\_type},\mbox{type})$

$\mbox{get}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{data}\qquad\mbox{tff}(\mbox{get\_type},\mbox{type})$

$\forall m{:}\;\mbox{\$int}{:}\;\mbox{get}(\mbox{mkarray},m) = \mbox{none}\qquad\mbox{tff}(\mbox{ax}_{17},\mbox{axiom})$

$\forall \mbox{ar}{:}\;\mbox{array},m{:}\;\mbox{\$int},d{:}\;\mbox{data}{:}\;\mbox{get}(\mbox{put}(\mbox{ar},m,d),m) = d\qquad\mbox{tff}(\mbox{ax}_{18},\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},d{:}\;\mbox{data},\mbox{ar}{:}\;\mbox{array},m{:}\;\mbox{\$int}{:}\;( m\ne n \ \Rightarrow \ \mbox{get}(\mbox{put}(\mbox{ar},n,d),m) = \mbox{get}(\mbox{ar},m) )\qquad\mbox{tff}(\mbox{ax}_{19},\mbox{axiom})$

$\forall d_2{:}\;\mbox{data},\mbox{ar}{:}\;\mbox{array},m{:}\;\mbox{\$int},d_1{:}\;\mbox{data}{:}\;\mbox{put}(\mbox{put}(\mbox{ar},m,d_2),m,d_1) = \mbox{put}(\mbox{ar},m,d_1)\qquad\mbox{tff}(\mbox{ax}_{20},\mbox{axiom})$

$\forall \mbox{ar}{:}\;\mbox{array},\mbox{ar}_0{:}\;\mbox{array}{:}\;( \mbox{ar} = \mbox{ar}_0\iff \forall n{:}\;\mbox{\$int}{:}\;\mbox{get}(\mbox{ar},n) = \mbox{get}(\mbox{ar}_0,n) )\qquad\mbox{tff}(\mbox{ax}_{21},\mbox{axiom})$

\medskip\textbf{DAT001=0.ax} Integer arrays






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

$\mbox{read}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{read\_type},\mbox{type})$

$\mbox{write}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{write\_type},\mbox{type})$

$\forall u{:}\;\mbox{array},v{:}\;\mbox{\$int},w{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{write}(u,v,w),v) = w\qquad\mbox{tff}(\mbox{ax}_1,\mbox{axiom})$

$\forall x{:}\;\mbox{array},y{:}\;\mbox{\$int},z{:}\;\mbox{\$int},x_1{:}\;\mbox{\$int}{:}\;( y = z\mbox{ or }\mbox{read}(\mbox{write}(x,y,x_1),z) = \mbox{read}(x,z) )\qquad\mbox{tff}(\mbox{ax}_2,\mbox{axiom})$

\medskip\textbf{DAT003=0.ax} Pointer data types






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

$\mbox{length}{:}\;\mbox{record}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{length\_type},\mbox{type})$

$\mbox{next}{:}\;\mbox{record}\to \mbox{record}\qquad\mbox{tff}(\mbox{next\_type},\mbox{type})$

$\mbox{data}{:}\;\mbox{record}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{data\_type},\mbox{type})$

$\mbox{split}_1{:}\;\mbox{record}\to \mbox{record}\qquad\mbox{tff}(\mbox{split1\_type},\mbox{type})$

$\mbox{split}_2{:}\;\mbox{record}\to \mbox{record}\qquad\mbox{tff}(\mbox{split2\_type},\mbox{type})$

$\mbox{isrecord}{:}\;\mbox{record}\to \mbox{\$o}\qquad\mbox{tff}(\mbox{isrecord\_type},\mbox{type})$

$\forall u{:}\;\mbox{record}{:}\;( \neg\,\mbox{isrecord}(u) \ \Rightarrow \ \mbox{length}(u) = 0 )\qquad\mbox{tff}(\mbox{ax}_1,\mbox{axiom})$

$\forall u{:}\;\mbox{record}{:}\;( \mbox{isrecord}(u) \ \Rightarrow \ \mbox{\$greatereq}(\mbox{length}(u),1) )\qquad\mbox{tff}(\mbox{ax}_2,\mbox{axiom})$

$\forall u{:}\;\mbox{record}{:}\;( \mbox{isrecord}(u) \ \Rightarrow \ \mbox{length}(u) = \mbox{\$sum}(\mbox{length}(\mbox{next}(u)),1) )\qquad\mbox{tff}(\mbox{ax}_3,\mbox{axiom})$

$\forall u{:}\;\mbox{record}{:}\;( \neg\,\mbox{isrecord}(u) \ \Rightarrow \ \neg\,\mbox{isrecord}(\mbox{split}_1(u)) )\qquad\mbox{tff}(\mbox{ax}_4,\mbox{axiom})$

$\forall u{:}\;\mbox{record}{:}\;( \mbox{isrecord}(u) \ \Rightarrow \ \mbox{isrecord}(\mbox{split}_1(u)) )\qquad\mbox{tff}(\mbox{ax}_5,\mbox{axiom})$

$\forall u{:}\;\mbox{record}{:}\;( \mbox{isrecord}(u) \ \Rightarrow \ \mbox{data}(\mbox{split}_1(u)) = \mbox{data}(u) )\qquad\mbox{tff}(\mbox{ax}_6,\mbox{axiom})$

$\forall u{:}\;\mbox{record}{:}\;( ( \mbox{isrecord}(u)\mbox{ and }\neg\,\mbox{isrecord}(\mbox{next}(u)) ) \ \Rightarrow \ \neg\,\mbox{isrecord}(\mbox{next}(\mbox{split}_1(u))) )\qquad\mbox{tff}(\mbox{ax}_7,\mbox{axiom})$

$\forall u{:}\;\mbox{record}{:}\;( ( \mbox{isrecord}(u)\mbox{ and }\mbox{isrecord}(\mbox{next}(u)) ) \ \Rightarrow \ \mbox{next}(\mbox{split}_1(u)) = \mbox{split}_1(\mbox{next}(\mbox{next}(u))) )\qquad\mbox{tff}(\mbox{ax}_8,\mbox{axiom})$

$\forall u{:}\;\mbox{record}{:}\;( \neg\,\mbox{isrecord}(u) \ \Rightarrow \ \neg\,\mbox{isrecord}(\mbox{split}_2(u)) )\qquad\mbox{tff}(\mbox{ax}_9,\mbox{axiom})$

$\forall u{:}\;\mbox{record}{:}\;( \neg\,\mbox{isrecord}(\mbox{next}(u)) \ \Rightarrow \ \neg\,\mbox{isrecord}(\mbox{split}_2(u)) )\qquad\mbox{tff}(\mbox{ax}_{10},\mbox{axiom})$

$\forall u{:}\;\mbox{record}{:}\;( ( \mbox{isrecord}(u)\mbox{ and }\mbox{isrecord}(\mbox{next}(u)) ) \ \Rightarrow \ \mbox{isrecord}(\mbox{split}_2(u)) )\qquad\mbox{tff}(\mbox{ax}_{11},\mbox{axiom})$

$\forall u{:}\;\mbox{record}{:}\;( ( \mbox{isrecord}(u)\mbox{ and }\mbox{isrecord}(\mbox{next}(u)) ) \ \Rightarrow \ \mbox{data}(\mbox{split}_2(u)) = \mbox{data}(\mbox{next}(u)) )\qquad\mbox{tff}(\mbox{ax}_{12},\mbox{axiom})$

$\forall u{:}\;\mbox{record}{:}\;( ( \mbox{isrecord}(u)\mbox{ and }\mbox{isrecord}(\mbox{next}(u)) ) \ \Rightarrow \ \mbox{next}(\mbox{split}_2(u)) = \mbox{split}_2(\mbox{next}(\mbox{next}(u))) )\qquad\mbox{tff}(\mbox{ax}_{13},\mbox{axiom})$

\medskip\textbf{DAT002=1.ax} Integer collections with counting






$\mbox{count}{:}\;\mbox{collection}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{count\_type},\mbox{type})$

$\forall x_6{:}\;\mbox{collection}{:}\;\mbox{\$greatereq}(\mbox{count}(x_6),0)\qquad\mbox{tff}(\mbox{ax}_1,\mbox{axiom})$

$\forall x_7{:}\;\mbox{collection}{:}\;( x_7 = \mbox{empty}\iff \mbox{count}(x_7) = 0 )\qquad\mbox{tff}(\mbox{ax}_2,\mbox{axiom})$

$\forall x_8{:}\;\mbox{\$int},x_9{:}\;\mbox{collection}{:}\;( \neg\,\mbox{in}(x_8,x_9)\iff \mbox{count}(x_8 + x_9) = \mbox{\$sum}(\mbox{count}(x_9),1) )\qquad\mbox{tff}(\mbox{ax}_3,\mbox{axiom})$

$\forall x_{10}{:}\;\mbox{\$int},x_{11}{:}\;\mbox{collection}{:}\;( \mbox{in}(x_{10},x_{11})\iff \mbox{count}(x_{10} + x_{11}) = \mbox{count}(x_{11}) )\qquad\mbox{tff}(\mbox{ax}_4,\mbox{axiom})$

$\forall x_{12}{:}\;\mbox{\$int},x_{13}{:}\;\mbox{collection}{:}\;( \mbox{in}(x_{12},x_{13})\iff \mbox{count}(\mbox{remove}(x_{12},x_{13})) = \mbox{\$difference}(\mbox{count}(x_{13}),1) )\qquad\mbox{tff}(\mbox{ax}_5,\mbox{axiom})$

$\forall x_{14}{:}\;\mbox{\$int},x_{15}{:}\;\mbox{collection}{:}\;( \neg\,\mbox{in}(x_{14},x_{15})\iff \mbox{count}(\mbox{remove}(x_{14},x_{15})) = \mbox{count}(x_{15}) )\qquad\mbox{tff}(\mbox{ax}_6,\mbox{axiom})$

$\forall x_{16}{:}\;\mbox{\$int},x_{17}{:}\;\mbox{collection}{:}\;( \mbox{in}(x_{16},x_{17}) \ \Rightarrow \ x_{17} = x_{16} + \mbox{remove}(x_{16},x_{17}) )\qquad\mbox{tff}(\mbox{ax}_7,\mbox{axiom})$

\medskip\textbf{DAT005=0.ax} Heap data types






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

$\mbox{empty}{:}\;\mbox{heap}\qquad\mbox{tff}(\mbox{empty\_type},\mbox{type})$

$\mbox{get}{:}\;\mbox{heap}\to \mbox{heap}\qquad\mbox{tff}(\mbox{get\_type},\mbox{type})$

$\mbox{app}{:}\;( \mbox{heap}\times \mbox{\$int} )\to \mbox{heap}\qquad\mbox{tff}(\mbox{app\_type},\mbox{type})$

$\mbox{toop}{:}\;\mbox{heap}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{toop\_type},\mbox{type})$

$\mbox{length}{:}\;\mbox{heap}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{length\_type},\mbox{type})$

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

$\forall n{:}\;\mbox{\$int},h{:}\;\mbox{heap}{:}\;\mbox{get}(\mbox{app}(h,n)) = h\qquad\mbox{tff}(\mbox{ax}_{17},\mbox{axiom})$

$\forall h{:}\;\mbox{heap},n{:}\;\mbox{\$int}{:}\;\mbox{toop}(\mbox{app}(h,n)) = n\qquad\mbox{tff}(\mbox{ax}_{18},\mbox{axiom})$

$\forall h{:}\;\mbox{heap},h_0{:}\;\mbox{heap},n{:}\;\mbox{\$int},n_0{:}\;\mbox{\$int}{:}\;( \mbox{app}(h,n) = \mbox{app}(h_0,n_0)\iff ( h = h_0\mbox{ and }n = n_0 ) )\qquad\mbox{tff}(\mbox{ax}_{19},\mbox{axiom})$

$\forall h{:}\;\mbox{heap},n{:}\;\mbox{\$int}{:}\;\mbox{empty}\ne \mbox{app}(h,n)\qquad\mbox{tff}(\mbox{ax}_{20},\mbox{axiom})$

$\forall h{:}\;\mbox{heap}{:}\;( h = \mbox{empty}\mbox{ or }h = \mbox{app}(\mbox{get}(h),\mbox{toop}(h)) )\qquad\mbox{tff}(\mbox{ax}_{21},\mbox{axiom})$

$\mbox{length}(\mbox{empty}) = 0\qquad\mbox{tff}(\mbox{ax}_{22},\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},h{:}\;\mbox{heap}{:}\;\mbox{length}(\mbox{app}(h,n)) = \mbox{\$sum}(1,\mbox{length}(h))\qquad\mbox{tff}(\mbox{ax}_{23},\mbox{axiom})$

$\forall h{:}\;\mbox{heap}{:}\;\neg\,\mbox{lsls}(h,h)\qquad\mbox{tff}(\mbox{ax}_{24},\mbox{axiom})$

$\forall h_0{:}\;\mbox{heap},h{:}\;\mbox{heap},h_1{:}\;\mbox{heap}{:}\;( ( \mbox{lsls}(h,h_0)\mbox{ and }\mbox{lsls}(h_0,h_1) ) \ \Rightarrow \ \mbox{lsls}(h,h_1) )\qquad\mbox{tff}(\mbox{ax}_{25},\mbox{axiom})$

$\forall h{:}\;\mbox{heap}{:}\;\neg\,\mbox{lsls}(h,\mbox{empty})\qquad\mbox{tff}(\mbox{ax}_{26},\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},h_0{:}\;\mbox{heap},h{:}\;\mbox{heap}{:}\;( \mbox{lsls}(h_0,\mbox{app}(h,n))\iff ( h_0 = h\mbox{ or }\mbox{lsls}(h_0,h) ) )\qquad\mbox{tff}(\mbox{ax}_{27},\mbox{axiom})$

\medskip\textbf{DAT006=0.ax} Tree-heap data types






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

$\mbox{empty}{:}\;\mbox{heap}\qquad\mbox{tff}(\mbox{empty\_type},\mbox{type})$

$\mbox{toop}{:}\;\mbox{heap}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{toop\_type},\mbox{type})$

$\mbox{sel}{:}\;( \mbox{heap}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{sel\_type},\mbox{type})$

$\mbox{length}{:}\;\mbox{heap}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{length\_type},\mbox{type})$

$\mbox{app}{:}\;( \mbox{heap}\times \mbox{\$int} )\to \mbox{heap}\qquad\mbox{tff}(\mbox{app\_type},\mbox{type})$

$\mbox{get}{:}\;\mbox{heap}\to \mbox{heap}\qquad\mbox{tff}(\mbox{get\_type},\mbox{type})$

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

$\forall m{:}\;\mbox{\$int}{:}\;\mbox{sel}(\mbox{empty},m) = 0\qquad\mbox{tff}(\mbox{ax}_1,\mbox{axiom})$

$\forall h{:}\;\mbox{heap},m{:}\;\mbox{\$int},n{:}\;\mbox{\$int}{:}\;( m = \mbox{\$sum}(1,\mbox{length}(h)) \ \Rightarrow \ \mbox{sel}(\mbox{app}(h,n),m) = n )\qquad\mbox{tff}(\mbox{ax}_2,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},h{:}\;\mbox{heap},m{:}\;\mbox{\$int}{:}\;( m\ne \mbox{\$sum}(1,\mbox{length}(h)) \ \Rightarrow \ \mbox{sel}(\mbox{app}(h,n),m) = \mbox{sel}(h,m) )\qquad\mbox{tff}(\mbox{ax}_3,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},h{:}\;\mbox{heap}{:}\;\mbox{get}(\mbox{app}(h,n)) = h\qquad\mbox{tff}(\mbox{ax}_{20},\mbox{axiom})$

$\forall h{:}\;\mbox{heap},n{:}\;\mbox{\$int}{:}\;\mbox{toop}(\mbox{app}(h,n)) = n\qquad\mbox{tff}(\mbox{ax}_{21},\mbox{axiom})$

$\forall h{:}\;\mbox{heap},h_0{:}\;\mbox{heap},n{:}\;\mbox{\$int},n_0{:}\;\mbox{\$int}{:}\;( \mbox{app}(h,n) = \mbox{app}(h_0,n_0)\iff ( h = h_0\mbox{ and }n = n_0 ) )\qquad\mbox{tff}(\mbox{ax}_{22},\mbox{axiom})$

$\forall h{:}\;\mbox{heap},n{:}\;\mbox{\$int}{:}\;\mbox{empty}\ne \mbox{app}(h,n)\qquad\mbox{tff}(\mbox{ax}_{23},\mbox{axiom})$

$\forall h{:}\;\mbox{heap}{:}\;( h = \mbox{empty}\mbox{ or }h = \mbox{app}(\mbox{get}(h),\mbox{toop}(h)) )\qquad\mbox{tff}(\mbox{ax}_{24},\mbox{axiom})$

$\mbox{length}(\mbox{empty}) = 0\qquad\mbox{tff}(\mbox{ax}_{25},\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},h{:}\;\mbox{heap}{:}\;\mbox{length}(\mbox{app}(h,n)) = \mbox{\$sum}(1,\mbox{length}(h))\qquad\mbox{tff}(\mbox{ax}_{26},\mbox{axiom})$

$\forall h{:}\;\mbox{heap}{:}\;\neg\,\mbox{lsls}(h,h)\qquad\mbox{tff}(\mbox{ax}_{27},\mbox{axiom})$

$\forall h_0{:}\;\mbox{heap},h{:}\;\mbox{heap},h_1{:}\;\mbox{heap}{:}\;( ( \mbox{lsls}(h,h_0)\mbox{ and }\mbox{lsls}(h_0,h_1) ) \ \Rightarrow \ \mbox{lsls}(h,h_1) )\qquad\mbox{tff}(\mbox{ax}_{28},\mbox{axiom})$

$\forall h{:}\;\mbox{heap}{:}\;\neg\,\mbox{lsls}(h,\mbox{empty})\qquad\mbox{tff}(\mbox{ax}_{29},\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},h_0{:}\;\mbox{heap},h{:}\;\mbox{heap}{:}\;( \mbox{lsls}(h_0,\mbox{app}(h,n))\iff ( h_0 = h\mbox{ or }\mbox{lsls}(h_0,h) ) )\qquad\mbox{tff}(\mbox{ax}_{30},\mbox{axiom})$

\medskip\textbf{DAT002=0.ax} Integer collections






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

$\mbox{empty}{:}\;\mbox{collection}\qquad\mbox{tff}(\mbox{empty\_type},\mbox{type})$

$ + {:}\;( \mbox{\$int}\times \mbox{collection} )\to \mbox{collection}\qquad\mbox{tff}(\mbox{add\_type},\mbox{type})$

$\mbox{remove}{:}\;( \mbox{\$int}\times \mbox{collection} )\to \mbox{collection}\qquad\mbox{tff}(\mbox{remove\_type},\mbox{type})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{collection} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in\_type},\mbox{type})$

$\forall u{:}\;\mbox{\$int}{:}\;\neg\,\mbox{in}(u,\mbox{empty})\qquad\mbox{tff}(\mbox{ax}_1,\mbox{axiom})$

$\forall v{:}\;\mbox{\$int},w{:}\;\mbox{collection}{:}\;\mbox{in}(v,v + w)\qquad\mbox{tff}(\mbox{ax}_2,\mbox{axiom})$

$\forall x{:}\;\mbox{\$int},y{:}\;\mbox{collection}{:}\;\neg\,\mbox{in}(x,\mbox{remove}(x,y))\qquad\mbox{tff}(\mbox{ax}_3,\mbox{axiom})$

$\forall z{:}\;\mbox{\$int},x_1{:}\;\mbox{collection},x_2{:}\;\mbox{\$int}{:}\;( ( \mbox{in}(z,x_1)\mbox{ or }z = x_2 )\iff \mbox{in}(z,x_2 + x_1) )\qquad\mbox{tff}(\mbox{ax}_4,\mbox{axiom})$

$\forall x_3{:}\;\mbox{\$int},x_4{:}\;\mbox{collection},x_5{:}\;\mbox{\$int}{:}\;( ( \mbox{in}(x_3,x_4)\mbox{ and }x_3\ne x_5 )\iff \mbox{in}(x_3,\mbox{remove}(x_5,x_4)) )\qquad\mbox{tff}(\mbox{ax}_5,\mbox{axiom})$

\medskip\textbf{DAT092=1.p} Lists by functions problem 14






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\neg\,\forall k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{append}(k,l)) = \mbox{length}(k)\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT037=1.p} If 2 is the only element, there are not 5 elements






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\forall u{:}\;\mbox{collection}{:}\;( ( \mbox{in}(2,u)\mbox{ and }\mbox{count}(u) = 1 ) \ \Rightarrow \ \neg\,\mbox{in}(5,u) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT068=1.p} Can select from only within a tree-heap






$\mbox{include}(\mbox{'Axioms/DAT006=0.ax'})$

$\forall n{:}\;\mbox{\$int},m{:}\;\mbox{\$int},h{:}\;\mbox{heap}{:}\;( \mbox{sel}(\mbox{app}(h,n),m) = \mbox{sel}(h,m)\mbox{ or }\neg\,\mbox{\$less}(m,\mbox{length}(h)) )\qquad\mbox{tff}(\mbox{th}_3,\mbox{conjecture})$

\medskip\textbf{DAT097=1.p} Lists by functions problem 18






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\neg\,\forall m{:}\;\mbox{\$int},n{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list},l_1{:}\;\mbox{list}{:}\;( ( \mbox{in}(n,l)\mbox{ and }\neg\,\mbox{in}(m,k)\mbox{ and }l_1 = \mbox{append}(l,\mbox{cons}(m,k)) ) \ \Rightarrow \ \mbox{count}(n,l_1) = \mbox{count}(n,l) )\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT056$\wedge$1.p} List operation requiring induction






$\mbox{lst}{:}\;\mbox{\$tType}\qquad\mbox{thf}(\mbox{ty\_n\_tc\_\_Foo\_\_Olst\_It\_\_J},\mbox{type})$

$a{:}\;\mbox{\$tType}\qquad\mbox{thf}(\mbox{ty\_n\_t\_},\mbox{type})$

$\mbox{ap}{:}\;\mbox{lst}\to \mbox{lst}\to \mbox{lst}\qquad\mbox{thf}(\mbox{sy\_c\_Foo\_Oap\_001t\_},\mbox{type})$

$\mbox{cns}{:}\;a\to \mbox{lst}\to \mbox{lst}\qquad\mbox{thf}(\mbox{sy\_c\_Foo\_Olst\_OCns\_001t\_},\mbox{type})$

$\mbox{nl}{:}\;\mbox{lst}\qquad\mbox{thf}(\mbox{sy\_c\_Foo\_Olst\_ONl\_001t\_},\mbox{type})$

$\mbox{xs}{:}\;\mbox{lst}\qquad\mbox{thf}(\mbox{sy\_v\_xs},\mbox{type})$

$\forall \mbox{lst}{:}\;\mbox{lst}{:}\;( \forall \mbox{ys}{:}\;\mbox{lst},\mbox{zs}{:}\;\mbox{lst}{:}\;( \mbox{ap}@ \mbox{nl}@ ( \mbox{ap}@ \mbox{ys}@ \mbox{zs} ) ) = ( \mbox{ap}@ ( \mbox{ap}@ \mbox{nl}@ \mbox{ys} )@ \mbox{zs} ) \ \Rightarrow \ ( \forall a{:}\;a,\mbox{lst}_2{:}\;\mbox{lst}{:}\;( \forall \mbox{ys}_3{:}\;\mbox{lst},\mbox{zs}_2{:}\;\mbox{lst}{:}\;( \mbox{ap}@ \mbox{lst}_2@ ( \mbox{ap}@ \mbox{ys}_3@ \mbox{zs}_2 ) ) = ( \mbox{ap}@ ( \mbox{ap}@ \mbox{lst}_2@ \mbox{ys}_3 )@ \mbox{zs}_2 ) \ \Rightarrow \ \forall \mbox{ys}{:}\;\mbox{lst},\mbox{zs}{:}\;\mbox{lst}{:}\;( \mbox{ap}@ ( \mbox{cns}@ a@ \mbox{lst}_2 )@ ( \mbox{ap}@ \mbox{ys}@ \mbox{zs} ) ) = ( \mbox{ap}@ ( \mbox{ap}@ ( \mbox{cns}@ a@ \mbox{lst}_2 )@ \mbox{ys} )@ \mbox{zs} ) ) \ \Rightarrow \ \forall \mbox{ys}_3{:}\;\mbox{lst},\mbox{zs}_2{:}\;\mbox{lst}{:}\;( \mbox{ap}@ \mbox{lst}@ ( \mbox{ap}@ \mbox{ys}_3@ \mbox{zs}_2 ) ) = ( \mbox{ap}@ ( \mbox{ap}@ \mbox{lst}@ \mbox{ys}_3 )@ \mbox{zs}_2 ) ) )\qquad\mbox{thf}(\mbox{fact\_0\_lst\_Oinduct\_091where\_AP\_A\_061\_A\_C\_Fxs\_O\_AALL\_Ays\_Azs\_O\_Aap\_Axs\_A\_Iap\_Ays\_Azs\_J\_A\_061\_Aap\_A\_Iap\_Axs\_Ays\_J\_Azs\_C}_{093},\mbox{axiom})$

$\forall \mbox{ys}_2{:}\;\mbox{lst},\mbox{xs}{:}\;\mbox{lst},x{:}\;a{:}\;( \mbox{ap}@ ( \mbox{cns}@ x@ \mbox{xs} )@ \mbox{ys}_2 ) = ( \mbox{cns}@ x@ ( \mbox{ap}@ \mbox{xs}@ \mbox{ys}_2 ) )\qquad\mbox{thf}(\mbox{fact\_1p\_Osimps\_I2\_J},\mbox{axiom})$

$\forall \mbox{ys}_2{:}\;\mbox{lst}{:}\;( \mbox{ap}@ \mbox{nl}@ \mbox{ys}_2 ) = \mbox{ys}_2\qquad\mbox{thf}(\mbox{fact\_2p\_Osimps\_I1\_J},\mbox{axiom})$

$\forall \mbox{ys}{:}\;\mbox{lst},\mbox{zs}{:}\;\mbox{lst}{:}\;( \mbox{ap}@ \mbox{xs}@ ( \mbox{ap}@ \mbox{ys}@ \mbox{zs} ) ) = ( \mbox{ap}@ ( \mbox{ap}@ \mbox{xs}@ \mbox{ys} )@ \mbox{zs} )\qquad\mbox{thf}(\mbox{conj}_0,\mbox{conjecture})$

\medskip\textbf{DAT100=1.p} Lists by relations problem 3






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\neg\,\mbox{inRange}(4,\mbox{cons}(1,\mbox{cons}(5,\mbox{cons}(2,\mbox{nil}))))\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT077=1.p} Arrays problem 7






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

$\mbox{read}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{read\_type},\mbox{type})$

$\mbox{write}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{write\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},i{:}\;\mbox{\$int},v{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{write}(a,i,v),i) = v\qquad\mbox{tff}(\mbox{ax}_1,\mbox{axiom})$

$\forall a{:}\;\mbox{array},i{:}\;\mbox{\$int},j{:}\;\mbox{\$int},v{:}\;\mbox{\$int}{:}\;( i = j\mbox{ or }\mbox{read}(\mbox{write}(a,i,v),j) = \mbox{read}(a,j) )\qquad\mbox{tff}(\mbox{ax}_2,\mbox{axiom})$

$\forall a{:}\;\mbox{array},b{:}\;\mbox{array}{:}\;( \forall i{:}\;\mbox{\$int}{:}\;\mbox{read}(a,i) = \mbox{read}(b,i) \ \Rightarrow \ a = b )\qquad\mbox{tff}(\mbox{ext},\mbox{axiom})$

$\mbox{init}{:}\;\mbox{\$int}\to \mbox{array}\qquad\mbox{tff}(\mbox{init\_type},\mbox{type})$

$\forall v{:}\;\mbox{\$int},i{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{init}(v),i) = v\qquad\mbox{tff}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{max}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{max},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int},w{:}\;\mbox{\$int}{:}\;( \mbox{max}(a,n) = w \ \Leftarrow \ ( \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),w) )\mbox{ and }\exists i{:}\;\mbox{\$int}{:}\;( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0)\mbox{ and }\mbox{read}(a,i) = w ) ) )\qquad\mbox{tff}(a,\mbox{axiom})$

$\mbox{sorted}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{sorted\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{sorted}(a,n)\iff \forall i{:}\;\mbox{\$int},j{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(0,i)\mbox{ and }\mbox{\$less}(i,n)\mbox{ and }\mbox{\$less}(i,j)\mbox{ and }\mbox{\$less}(j,n) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),\mbox{read}(a,j)) ) )\qquad\mbox{tff}(\mbox{sorted}_1,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},r{:}\;\mbox{\$int},n{:}\;\mbox{\$int}{:}\;( \mbox{inRange}(a,r,n)\iff \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ ( \mbox{\$greatereq}(r,\mbox{read}(a,i))\mbox{ and }\mbox{\$greatereq}(\mbox{read}(a,i),0) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{distinct}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{distinct\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{distinct}(a,n)\iff \forall i{:}\;\mbox{\$int},j{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greater}(n,j)\mbox{ and }\mbox{\$greatereq}(j,0)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ ( \mbox{read}(a,i) = \mbox{read}(a,j) \ \Rightarrow \ i = j ) ) )\qquad\mbox{tff}(\mbox{distinct},\mbox{axiom})$

$\mbox{rev}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{rev\_n},\mbox{type})$

$\forall a{:}\;\mbox{array},b{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{rev}(a,n) = b \ \Leftarrow \ \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greatereq}(i,0)\mbox{ and }\mbox{\$greater}(n,i)\mbox{ and }\mbox{read}(b,i) = \mbox{read}(a,\mbox{\$difference}(n,\mbox{\$sum}(i,1))) )\mbox{ or }( ( \mbox{\$greater}(0,i)\mbox{ or }\mbox{\$greatereq}(i,n) )\mbox{ and }\mbox{read}(b,i) = \mbox{read}(a,i) ) ) )\qquad\mbox{tff}(\mbox{rev\_n1\_proper},\mbox{axiom})$

$\neg\,\forall m{:}\;\mbox{\$int}{:}\;\exists n{:}\;\mbox{\$int}{:}\;\neg\,\mbox{sorted}(\mbox{rev}(\mbox{init}(n),m),m)\qquad\mbox{tff}(c_5,\mbox{conjecture})$

\medskip\textbf{DAT054=1.p} Decreasing pointer list






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

$\mbox{data}{:}\;\mbox{element}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{data\_type},\mbox{type})$

$\mbox{next}{:}\;\mbox{element}\to \mbox{element}\qquad\mbox{tff}(\mbox{next\_type},\mbox{type})$

$\mbox{iselem}{:}\;\mbox{element}\to \mbox{\$o}\qquad\mbox{tff}(\mbox{iselem\_type},\mbox{type})$

$a{:}\;\mbox{element}\qquad\mbox{tff}(\mbox{a\_type},\mbox{type})$

$( \forall x{:}\;\mbox{element},z{:}\;\mbox{\$int}{:}\;( \neg\,\mbox{iselem}(x)\mbox{ or }\mbox{data}(x)\ne z\mbox{ or }\mbox{\$less}(0,z) )\mbox{ and }\forall x{:}\;\mbox{element},y{:}\;\mbox{element}{:}\;( \neg\,\mbox{iselem}(x)\mbox{ or }\neg\,\mbox{iselem}(\mbox{next}(y))\mbox{ or }\mbox{next}(x)\ne y\mbox{ or }\mbox{\$less}(\mbox{data}(y),\mbox{data}(x)) )\mbox{ and }\mbox{iselem}(a)\mbox{ and }\mbox{iselem}(\mbox{next}(a))\mbox{ and }\mbox{iselem}(\mbox{next}(\mbox{next}(a))) ) \ \Rightarrow \ \mbox{\$lesseq}(3,\mbox{data}(a))\qquad\mbox{tff}(\mbox{decreasing\_pointer\_list},\mbox{conjecture})$

\medskip\textbf{DAT058=1.p} Add nothing to an array






$\mbox{include}(\mbox{'Axioms/DAT004=0.ax'})$

$\forall m{:}\;\mbox{\$int}{:}\;\mbox{put}(\mbox{mkarray},m,\mbox{none}) = \mbox{mkarray}\qquad\mbox{tff}(\mbox{th\_lem}_2,\mbox{conjecture})$

\medskip\textbf{DAT107=1.p} Integer arrays






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

\medskip\textbf{DAT066=1.p} Cannot select after end of tree-heap






$\mbox{include}(\mbox{'Axioms/DAT006=0.ax'})$

$\forall n{:}\;\mbox{\$int},m{:}\;\mbox{\$int},h{:}\;\mbox{heap}{:}\;( \mbox{sel}(\mbox{app}(h,n),m) = n\mbox{ or }m\ne \mbox{\$sum}(1,\mbox{length}(h)) )\qquad\mbox{tff}(\mbox{th}_1,\mbox{conjecture})$

\medskip\textbf{DAT014=1.p} Compare elements 4






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

$\forall u{:}\;\mbox{array}{:}\;( ( \forall v{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(1,v)\mbox{ and }\mbox{\$lesseq}(v,10) ) \ \Rightarrow \ \mbox{\$greater}(\mbox{read}(u,v),v) )\mbox{ and }\forall w{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(11,w)\mbox{ and }\mbox{\$lesseq}(w,20) ) \ \Rightarrow \ \mbox{\$greater}(\mbox{read}(u,w),\mbox{\$difference}(20,w)) ) ) \ \Rightarrow \ \forall x{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(6,x)\mbox{ and }\mbox{\$lesseq}(x,15) ) \ \Rightarrow \ \mbox{\$greater}(\mbox{read}(u,x),5) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT095=1.p} Lists by functions problem 17






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\neg\,\forall m{:}\;\mbox{\$int},n{:}\;\mbox{\$int},l{:}\;\mbox{list},l_1{:}\;\mbox{list}{:}\;( ( \mbox{in}(n,l)\mbox{ and }l_1 = \mbox{cons}(m,l) ) \ \Rightarrow \ \mbox{count}(n,l_1) = \mbox{count}(n,l) )\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT021=1.p} Sum of two elements is less than 9






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{\$int},w{:}\;\mbox{\$int}{:}\;( ( u = 5 + ( 3 + ( 1 + \mbox{empty} ) )\mbox{ and }\mbox{in}(v,u)\mbox{ and }\mbox{in}(w,u)\mbox{ and }v\ne w ) \ \Rightarrow \ \mbox{\$less}(\mbox{\$sum}(v,w),9) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT061=1.p} get-put on self lemma






$\mbox{include}(\mbox{'Axioms/DAT004=0.ax'})$

$\forall d{:}\;\mbox{data},\mbox{ar}{:}\;\mbox{array},m{:}\;\mbox{\$int},n{:}\;\mbox{\$int}{:}\;( \mbox{get}(\mbox{put}(\mbox{ar},m,d),n) = \mbox{get}(\mbox{ar},n)\mbox{ or }\neg\,\mbox{\$less}(m,n) )\qquad\mbox{tff}(\mbox{th\_lem}_7,\mbox{conjecture})$

\medskip\textbf{DAT013=1.p} Compare elements 3






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

$\forall u{:}\;\mbox{array},v{:}\;\mbox{\$int},w{:}\;\mbox{\$int}{:}\;( \forall x{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(v,x)\mbox{ and }\mbox{\$lesseq}(x,w) ) \ \Rightarrow \ \mbox{\$greater}(\mbox{read}(u,x),0) ) \ \Rightarrow \ \forall y{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(\mbox{\$sum}(v,3),y)\mbox{ and }\mbox{\$lesseq}(y,w) ) \ \Rightarrow \ \mbox{\$greater}(\mbox{read}(u,y),0) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT080=1.p} Lists by functions problem 2






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\neg\,\mbox{in}(4,\mbox{cons}(1,\mbox{cons}(2,\mbox{cons}(3,\mbox{nil}))))\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT036=1.p} Adding an element greater than 0 - 2






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{\$int},w{:}\;\mbox{\$int}{:}\;( \mbox{\$greater}(w,0) \ \Rightarrow \ \mbox{\$greatereq}(\mbox{\$sum}(\mbox{count}(u),w),\mbox{count}(v + ( v + u ))) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT045=1.p} Adding a larger element to the collection 2






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{\$int}{:}\;( \forall w{:}\;\mbox{\$int}{:}\;( \mbox{in}(w,u) \ \Rightarrow \ \mbox{\$greater}(v,w) ) \ \Rightarrow \ \mbox{\$greater}(\mbox{count}(v + u),\mbox{count}(u)) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT018=1.p} Compare elements 5






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

$\forall u{:}\;\mbox{array},v{:}\;\mbox{array},w{:}\;\mbox{\$int},x{:}\;\mbox{\$int}{:}\;( ( u = \mbox{write}(\mbox{write}(\mbox{write}(v,w,3),\mbox{\$sum}(w,2),2),\mbox{\$sum}(w,4),1)\mbox{ and }\mbox{\$lesseq}(w,x)\mbox{ and }\mbox{\$lesseq}(x,\mbox{\$sum}(w,3)) ) \ \Rightarrow \ \exists y{:}\;\mbox{\$int}{:}\;( \mbox{\$lesseq}(x,y)\mbox{ and }\mbox{\$lesseq}(y,\mbox{\$sum}(x,3))\mbox{ and }\mbox{\$lesseq}(\mbox{read}(u,y),3) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT047=1.p} Adding and removing 3 leaves size 1






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\mbox{count}(5 + \mbox{remove}(3,3 + \mbox{empty})) = 1\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT046=1.p} The collection of 1 and 2 has size 2






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\mbox{count}(1 + ( 3 + \mbox{empty} )) = 2\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT048=1.p} Removing an non-existent element from collection of size 3






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\mbox{count}(1 + ( 5 + \mbox{remove}(3,2 + \mbox{empty}) )) = 3\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT063=1.p} Empty heap length






$\mbox{include}(\mbox{'Axioms/DAT005=0.ax'})$

$\forall h{:}\;\mbox{heap}{:}\;( \mbox{lsls}(h,\mbox{empty}) \ \Rightarrow \ \mbox{\$less}(\mbox{length}(h),\mbox{length}(\mbox{empty})) )\qquad\mbox{tff}(\mbox{th\_lem\_1b},\mbox{conjecture})$

\medskip\textbf{DAT086=1.p} Lists by functions problem 8






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\neg\,\forall l{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greatereq}(n,3)\mbox{ and }\mbox{\$greatereq}(\mbox{length}(l),4) ) \ \Rightarrow \ \mbox{inRange}(n,l) )\qquad\mbox{tff}(a_9,\mbox{conjecture})$

\medskip\textbf{DAT040=1.p} Only elements less than 3 or greater than 6






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{\$int},w{:}\;\mbox{\$int}{:}\;( ( \mbox{\$less}(v,3)\mbox{ and }\mbox{\$less}(6,w)\mbox{ and }\mbox{in}(v,u)\mbox{ and }\mbox{in}(w,u)\mbox{ and }\mbox{count}(u) = 2 ) \ \Rightarrow \ \neg\,\mbox{in}(5,u) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT007=1.p} Element between 30 and 40






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

$\forall u{:}\;\mbox{array},v{:}\;\mbox{array}{:}\;( u = \mbox{write}(\mbox{write}(\mbox{write}(\mbox{write}(v,3,33),4,444),5,55),4,44) \ \Rightarrow \ \exists w{:}\;\mbox{\$int}{:}\;( \mbox{\$less}(\mbox{read}(u,w),40)\mbox{ and }\mbox{\$less}(30,\mbox{read}(u,w)) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT053=1.p} Sublist of odd numbered elements






$\mbox{include}(\mbox{'Axioms/DAT003=0.ax'})$

$a{:}\;\mbox{record}\qquad\mbox{tff}(\mbox{a\_type},\mbox{type})$

$b{:}\;\mbox{record}\qquad\mbox{tff}(\mbox{b\_type},\mbox{type})$

$( \mbox{isrecord}(b)\mbox{ and }\mbox{isrecord}(\mbox{next}(b))\mbox{ and }\mbox{next}(\mbox{next}(b)) = a\mbox{ and }( \mbox{\$product}(2,\mbox{length}(\mbox{split}_1(a))) = \mbox{\$sum}(\mbox{length}(a),1)\mbox{ or }\mbox{\$product}(2,\mbox{length}(\mbox{split}_1(a))) = \mbox{length}(a) ) ) \ \Rightarrow \ ( \mbox{\$product}(2,\mbox{length}(\mbox{split}_1(b))) = \mbox{\$sum}(\mbox{length}(b),1)\mbox{ or }\mbox{\$product}(2,\mbox{length}(\mbox{split}_1(b))) = \mbox{length}(b) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT043=1.p} Three different elements






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{\$int},w{:}\;\mbox{\$int},x{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(v,w)\mbox{ and }\mbox{\$greater}(w,x)\mbox{ and }\mbox{in}(v,u)\mbox{ and }\mbox{in}(w,u)\mbox{ and }\mbox{in}(x,u) ) \ \Rightarrow \ \mbox{\$greater}(\mbox{count}(u),2) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT024=1.p} Without 0 or 1 all elements are greater or equal to 2






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\forall u{:}\;\mbox{collection}{:}\;( ( \forall v{:}\;\mbox{\$int}{:}\;( \mbox{in}(v,u) \ \Rightarrow \ \mbox{\$greatereq}(v,0) )\mbox{ and }\neg\,\mbox{in}(0,u)\mbox{ and }\neg\,\mbox{in}(1,u) ) \ \Rightarrow \ \forall w{:}\;\mbox{\$int}{:}\;( \mbox{in}(w,u) \ \Rightarrow \ \mbox{\$greatereq}(w,2) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT075=1.p} Arrays problem 5






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

$\mbox{read}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{read\_type},\mbox{type})$

$\mbox{write}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{write\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},i{:}\;\mbox{\$int},v{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{write}(a,i,v),i) = v\qquad\mbox{tff}(\mbox{ax}_1,\mbox{axiom})$

$\forall a{:}\;\mbox{array},i{:}\;\mbox{\$int},j{:}\;\mbox{\$int},v{:}\;\mbox{\$int}{:}\;( i = j\mbox{ or }\mbox{read}(\mbox{write}(a,i,v),j) = \mbox{read}(a,j) )\qquad\mbox{tff}(\mbox{ax}_2,\mbox{axiom})$

$\forall a{:}\;\mbox{array},b{:}\;\mbox{array}{:}\;( \forall i{:}\;\mbox{\$int}{:}\;\mbox{read}(a,i) = \mbox{read}(b,i) \ \Rightarrow \ a = b )\qquad\mbox{tff}(\mbox{ext},\mbox{axiom})$

$\mbox{init}{:}\;\mbox{\$int}\to \mbox{array}\qquad\mbox{tff}(\mbox{init\_type},\mbox{type})$

$\forall v{:}\;\mbox{\$int},i{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{init}(v),i) = v\qquad\mbox{tff}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{max}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{max},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int},w{:}\;\mbox{\$int}{:}\;( \mbox{max}(a,n) = w \ \Leftarrow \ ( \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),w) )\mbox{ and }\exists i{:}\;\mbox{\$int}{:}\;( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0)\mbox{ and }\mbox{read}(a,i) = w ) ) )\qquad\mbox{tff}(a,\mbox{axiom})$

$\mbox{sorted}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{sorted\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{sorted}(a,n)\iff \forall i{:}\;\mbox{\$int},j{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(0,i)\mbox{ and }\mbox{\$less}(i,n)\mbox{ and }\mbox{\$less}(i,j)\mbox{ and }\mbox{\$less}(j,n) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),\mbox{read}(a,j)) ) )\qquad\mbox{tff}(\mbox{sorted}_1,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},r{:}\;\mbox{\$int},n{:}\;\mbox{\$int}{:}\;( \mbox{inRange}(a,r,n)\iff \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ ( \mbox{\$greatereq}(r,\mbox{read}(a,i))\mbox{ and }\mbox{\$greatereq}(\mbox{read}(a,i),0) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{distinct}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{distinct\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{distinct}(a,n)\iff \forall i{:}\;\mbox{\$int},j{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greater}(n,j)\mbox{ and }\mbox{\$greatereq}(j,0)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ ( \mbox{read}(a,i) = \mbox{read}(a,j) \ \Rightarrow \ i = j ) ) )\qquad\mbox{tff}(\mbox{distinct},\mbox{axiom})$

$\mbox{rev}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{rev\_n},\mbox{type})$

$\forall a{:}\;\mbox{array},b{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{rev}(a,n) = b \ \Leftarrow \ \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greatereq}(i,0)\mbox{ and }\mbox{\$greater}(n,i)\mbox{ and }\mbox{read}(b,i) = \mbox{read}(a,\mbox{\$difference}(n,\mbox{\$sum}(i,1))) )\mbox{ or }( ( \mbox{\$greater}(0,i)\mbox{ or }\mbox{\$greatereq}(i,n) )\mbox{ and }\mbox{read}(b,i) = \mbox{read}(a,i) ) ) )\qquad\mbox{tff}(\mbox{rev\_n1\_proper},\mbox{axiom})$

$\neg\,\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{rev}(a,\mbox{\$sum}(n,1)),0) = \mbox{read}(a,n)\qquad\mbox{tff}(c_3,\mbox{conjecture})$

\medskip\textbf{DAT035=1.p} Adding an element greater than 0 - 1






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{\$int},w{:}\;\mbox{\$int}{:}\;( \mbox{\$greater}(w,0) \ \Rightarrow \ \mbox{\$greatereq}(\mbox{\$sum}(\mbox{count}(u),w),\mbox{count}(v + u)) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT002=1.p} Recursive list Fibonacci sort

A list is Fibonacci sorted if it is sorted, and every element is
 greater of equal to the sum of its two predecessors (from the
 third element onwards).




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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{mycons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{mycons\_type},\mbox{type})$

$\mbox{fib\_sorted}{:}\;\mbox{list}\to \mbox{\$o}\qquad\mbox{tff}(\mbox{sorted\_type},\mbox{type})$

$\mbox{fib\_sorted}(\mbox{nil})\qquad\mbox{tff}(\mbox{empty\_fib\_sorted},\mbox{axiom})$

$\forall x{:}\;\mbox{\$int}{:}\;\mbox{fib\_sorted}(\mbox{mycons}(x,\mbox{nil}))\qquad\mbox{tff}(\mbox{single\_is\_fib\_sorted},\mbox{axiom})$

$\forall x{:}\;\mbox{\$int},y{:}\;\mbox{\$int}{:}\;( \mbox{\$less}(x,y) \ \Rightarrow \ \mbox{fib\_sorted}(\mbox{mycons}(x,\mbox{mycons}(y,\mbox{nil}))) )\qquad\mbox{tff}(\mbox{double\_is\_fib\_sorted\_if\_ordered},\mbox{axiom})$

$\forall x{:}\;\mbox{\$int},y{:}\;\mbox{\$int},z{:}\;\mbox{\$int},r{:}\;\mbox{list}{:}\;( ( \mbox{\$less}(x,y)\mbox{ and }\mbox{\$greatereq}(z,\mbox{\$sum}(x,y))\mbox{ and }\mbox{fib\_sorted}(\mbox{mycons}(y,\mbox{mycons}(z,r))) ) \ \Rightarrow \ \mbox{fib\_sorted}(\mbox{mycons}(x,\mbox{mycons}(y,\mbox{mycons}(z,r)))) )\qquad\mbox{tff}(\mbox{recursive\_fib\_sort},\mbox{axiom})$

$\mbox{fib\_sorted}(\mbox{mycons}(1,\mbox{mycons}(2,\mbox{mycons}(4,\mbox{mycons}(7,\mbox{mycons}(100,\mbox{nil}))))))\qquad\mbox{tff}(\mbox{check\_list},\mbox{conjecture})$

\medskip\textbf{DAT023=1.p} Removing 1 and 2 ensures elements are greater than 2






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{collection}{:}\;( ( \forall w{:}\;\mbox{\$int}{:}\;( \mbox{in}(w,v) \ \Rightarrow \ \mbox{\$greater}(w,0) )\mbox{ and }u = \mbox{remove}(4,\mbox{remove}(1,\mbox{remove}(2,v))) ) \ \Rightarrow \ \forall x{:}\;\mbox{\$int}{:}\;( \mbox{in}(x,u) \ \Rightarrow \ \mbox{\$greater}(x,2) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT089=1.p} Lists by functions problem 11






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\neg\,\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{\$greatereq}(\mbox{count}(n,l),\mbox{length}(l))\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT102=1.p} Lists by relations problem 5






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\neg\,\forall l{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{inRange}(n,\mbox{tail}(l)) \ \Rightarrow \ \mbox{inRange}(n,l) )\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT012=1.p} Compare elements 2






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

$\forall u{:}\;\mbox{array},v{:}\;\mbox{array},w{:}\;\mbox{\$int},x{:}\;\mbox{\$int}{:}\;( ( \forall y{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(w,y)\mbox{ and }\mbox{\$lesseq}(y,x) ) \ \Rightarrow \ \mbox{\$greater}(\mbox{read}(u,y),0) )\mbox{ and }v = \mbox{write}(u,\mbox{\$sum}(w,2),\mbox{\$sum}(\mbox{read}(u,\mbox{\$sum}(w,1)),1)) ) \ \Rightarrow \ \forall z{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(w,z)\mbox{ and }\mbox{\$lesseq}(z,x) ) \ \Rightarrow \ \mbox{\$greater}(\mbox{read}(v,z),0) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT041=1.p} Adding an element makes list longer






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\exists u{:}\;\mbox{collection},v{:}\;\mbox{\$int}{:}\;\mbox{\$greater}(\mbox{\$sum}(\mbox{count}(u),1),\mbox{count}(v + u))\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT076=1.p} Arrays problem 6






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

$\mbox{read}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{read\_type},\mbox{type})$

$\mbox{write}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{write\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},i{:}\;\mbox{\$int},v{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{write}(a,i,v),i) = v\qquad\mbox{tff}(\mbox{ax}_1,\mbox{axiom})$

$\forall a{:}\;\mbox{array},i{:}\;\mbox{\$int},j{:}\;\mbox{\$int},v{:}\;\mbox{\$int}{:}\;( i = j\mbox{ or }\mbox{read}(\mbox{write}(a,i,v),j) = \mbox{read}(a,j) )\qquad\mbox{tff}(\mbox{ax}_2,\mbox{axiom})$

$\forall a{:}\;\mbox{array},b{:}\;\mbox{array}{:}\;( \forall i{:}\;\mbox{\$int}{:}\;\mbox{read}(a,i) = \mbox{read}(b,i) \ \Rightarrow \ a = b )\qquad\mbox{tff}(\mbox{ext},\mbox{axiom})$

$\mbox{init}{:}\;\mbox{\$int}\to \mbox{array}\qquad\mbox{tff}(\mbox{init\_type},\mbox{type})$

$\forall v{:}\;\mbox{\$int},i{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{init}(v),i) = v\qquad\mbox{tff}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{max}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{max},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int},w{:}\;\mbox{\$int}{:}\;( \mbox{max}(a,n) = w \ \Leftarrow \ ( \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),w) )\mbox{ and }\exists i{:}\;\mbox{\$int}{:}\;( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0)\mbox{ and }\mbox{read}(a,i) = w ) ) )\qquad\mbox{tff}(a,\mbox{axiom})$

$\mbox{sorted}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{sorted\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{sorted}(a,n)\iff \forall i{:}\;\mbox{\$int},j{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(0,i)\mbox{ and }\mbox{\$less}(i,n)\mbox{ and }\mbox{\$less}(i,j)\mbox{ and }\mbox{\$less}(j,n) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),\mbox{read}(a,j)) ) )\qquad\mbox{tff}(\mbox{sorted}_1,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},r{:}\;\mbox{\$int},n{:}\;\mbox{\$int}{:}\;( \mbox{inRange}(a,r,n)\iff \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ ( \mbox{\$greatereq}(r,\mbox{read}(a,i))\mbox{ and }\mbox{\$greatereq}(\mbox{read}(a,i),0) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{distinct}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{distinct\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{distinct}(a,n)\iff \forall i{:}\;\mbox{\$int},j{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greater}(n,j)\mbox{ and }\mbox{\$greatereq}(j,0)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ ( \mbox{read}(a,i) = \mbox{read}(a,j) \ \Rightarrow \ i = j ) ) )\qquad\mbox{tff}(\mbox{distinct},\mbox{axiom})$

$\mbox{rev}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{rev\_n},\mbox{type})$

$\forall a{:}\;\mbox{array},b{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{rev}(a,n) = b \ \Leftarrow \ \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greatereq}(i,0)\mbox{ and }\mbox{\$greater}(n,i)\mbox{ and }\mbox{read}(b,i) = \mbox{read}(a,\mbox{\$difference}(n,\mbox{\$sum}(i,1))) )\mbox{ or }( ( \mbox{\$greater}(0,i)\mbox{ or }\mbox{\$greatereq}(i,n) )\mbox{ and }\mbox{read}(b,i) = \mbox{read}(a,i) ) ) )\qquad\mbox{tff}(\mbox{rev\_n1\_proper},\mbox{axiom})$

$\neg\,\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{sorted}(a,n) \ \Rightarrow \ \neg\,\mbox{sorted}(\mbox{rev}(a,n),n) )\qquad\mbox{tff}(c_4,\mbox{conjecture})$

\medskip\textbf{DAT029=1.p} Comparing elements in two collections 2






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{collection}{:}\;( ( \forall w{:}\;\mbox{\$int}{:}\;( \mbox{in}(w,v) \ \Rightarrow \ \mbox{\$greater}(w,0) )\mbox{ and }\forall x{:}\;\mbox{\$int}{:}\;( \mbox{in}(x,u) \ \Rightarrow \ \exists y{:}\;\mbox{\$int}{:}\;( \mbox{in}(y,v)\mbox{ and }\mbox{\$greater}(\mbox{\$difference}(\mbox{\$product}(2,x),\mbox{\$product}(5,y)),0) ) ) ) \ \Rightarrow \ \forall z{:}\;\mbox{\$int}{:}\;( \mbox{in}(z,u) \ \Rightarrow \ \mbox{\$greater}(z,2) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT101=1.p} Lists by relations problem 4






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\neg\,\forall n{:}\;\mbox{\$int}{:}\;( \mbox{\$greatereq}(n,4) \ \Rightarrow \ \mbox{inRange}(n,\mbox{cons}(1,\mbox{cons}(5,\mbox{cons}(2,\mbox{nil})))) )\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT078=1.p} Arrays problem 8






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

$\mbox{read}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{read\_type},\mbox{type})$

$\mbox{write}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{write\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},i{:}\;\mbox{\$int},v{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{write}(a,i,v),i) = v\qquad\mbox{tff}(\mbox{ax}_1,\mbox{axiom})$

$\forall a{:}\;\mbox{array},i{:}\;\mbox{\$int},j{:}\;\mbox{\$int},v{:}\;\mbox{\$int}{:}\;( i = j\mbox{ or }\mbox{read}(\mbox{write}(a,i,v),j) = \mbox{read}(a,j) )\qquad\mbox{tff}(\mbox{ax}_2,\mbox{axiom})$

$\forall a{:}\;\mbox{array},b{:}\;\mbox{array}{:}\;( \forall i{:}\;\mbox{\$int}{:}\;\mbox{read}(a,i) = \mbox{read}(b,i) \ \Rightarrow \ a = b )\qquad\mbox{tff}(\mbox{ext},\mbox{axiom})$

$\mbox{init}{:}\;\mbox{\$int}\to \mbox{array}\qquad\mbox{tff}(\mbox{init\_type},\mbox{type})$

$\forall v{:}\;\mbox{\$int},i{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{init}(v),i) = v\qquad\mbox{tff}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{max}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{max},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int},w{:}\;\mbox{\$int}{:}\;( \mbox{max}(a,n) = w \ \Leftarrow \ ( \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),w) )\mbox{ and }\exists i{:}\;\mbox{\$int}{:}\;( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0)\mbox{ and }\mbox{read}(a,i) = w ) ) )\qquad\mbox{tff}(a,\mbox{axiom})$

$\mbox{sorted}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{sorted\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{sorted}(a,n)\iff \forall i{:}\;\mbox{\$int},j{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(0,i)\mbox{ and }\mbox{\$less}(i,n)\mbox{ and }\mbox{\$less}(i,j)\mbox{ and }\mbox{\$less}(j,n) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),\mbox{read}(a,j)) ) )\qquad\mbox{tff}(\mbox{sorted}_1,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},r{:}\;\mbox{\$int},n{:}\;\mbox{\$int}{:}\;( \mbox{inRange}(a,r,n)\iff \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ ( \mbox{\$greatereq}(r,\mbox{read}(a,i))\mbox{ and }\mbox{\$greatereq}(\mbox{read}(a,i),0) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{distinct}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{distinct\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{distinct}(a,n)\iff \forall i{:}\;\mbox{\$int},j{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greater}(n,j)\mbox{ and }\mbox{\$greatereq}(j,0)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ ( \mbox{read}(a,i) = \mbox{read}(a,j) \ \Rightarrow \ i = j ) ) )\qquad\mbox{tff}(\mbox{distinct},\mbox{axiom})$

$\mbox{rev}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{rev\_n},\mbox{type})$

$\forall a{:}\;\mbox{array},b{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{rev}(a,n) = b \ \Leftarrow \ \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greatereq}(i,0)\mbox{ and }\mbox{\$greater}(n,i)\mbox{ and }\mbox{read}(b,i) = \mbox{read}(a,\mbox{\$difference}(n,\mbox{\$sum}(i,1))) )\mbox{ or }( ( \mbox{\$greater}(0,i)\mbox{ or }\mbox{\$greatereq}(i,n) )\mbox{ and }\mbox{read}(b,i) = \mbox{read}(a,i) ) ) )\qquad\mbox{tff}(\mbox{rev\_n1\_proper},\mbox{axiom})$

$\neg\,\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( ( \mbox{sorted}(a,n)\mbox{ and }\mbox{\$greater}(n,0) ) \ \Rightarrow \ \mbox{distinct}(a,n) )\qquad\mbox{tff}(c_6,\mbox{conjecture})$

\medskip\textbf{DAT020=1.p} 4 is not in the collection






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\neg\,\mbox{in}(4,1 + ( 3 + ( 5 + \mbox{empty} ) ))\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT005=1.p} Element between 33 and 44






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

$\forall u{:}\;\mbox{array},v{:}\;\mbox{array},w{:}\;\mbox{\$int}{:}\;( ( u = \mbox{write}(\mbox{write}(\mbox{write}(\mbox{write}(v,3,33),4,444),5,55),4,44)\mbox{ and }\mbox{\$lesseq}(3,w)\mbox{ and }\mbox{\$lesseq}(w,4) ) \ \Rightarrow \ ( \mbox{\$lesseq}(33,\mbox{read}(u,w))\mbox{ and }\mbox{\$lesseq}(\mbox{read}(u,w),44) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT069=1.p} Can select from only within a tree-heap






$\mbox{include}(\mbox{'Axioms/DAT006=0.ax'})$

$\forall n{:}\;\mbox{\$int},h{:}\;\mbox{heap},m{:}\;\mbox{\$int}{:}\;( \mbox{sel}(\mbox{app}(h,n),m) = \mbox{sel}(h,m)\mbox{ or }\mbox{\$less}(\mbox{length}(h),m) )\qquad\mbox{tff}(\mbox{th}_4,\mbox{conjecture})$

\medskip\textbf{DAT106=1.p} Lists by relations problem 9






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\neg\,\forall n{:}\;\mbox{\$int},l_0{:}\;\mbox{list},l_1{:}\;\mbox{list}{:}\;( ( \mbox{\$greater}(n,0)\mbox{ and }\mbox{inRange}(n,l_0)\mbox{ and }l_1 = \mbox{cons}(\mbox{\$difference}(n,2),l_0) ) \ \Rightarrow \ \mbox{inRange}(n,l_1) )\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT087=1.p} Lists by functions problem 9






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\neg\,\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{count}(n,l) = \mbox{count}(n,\mbox{cons}(1,l))\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT064=1.p} Impossible heap






$\mbox{include}(\mbox{'Axioms/DAT005=0.ax'})$

$\forall h_1{:}\;\mbox{heap},h{:}\;\mbox{heap}{:}\;( ( \mbox{lsls}(h,h_1)\mbox{ and }\mbox{\$less}(\mbox{length}(h_1),\mbox{length}(h)) ) \ \Rightarrow \ \mbox{\$false} )\qquad\mbox{tff}(\mbox{th\_lem}_2,\mbox{conjecture})$

\medskip\textbf{DAT103=1.p} Lists by relations problem 6






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\neg\,\exists l{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( l\ne \mbox{nil}\mbox{ and }\mbox{inRange}(n,l)\mbox{ and }\mbox{\$less}(\mbox{\$difference}(n,\mbox{head}(l)),1) )\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT001=1.p} Recursive list sort






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{mycons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{mycons\_type},\mbox{type})$

$\mbox{sorted}{:}\;\mbox{list}\to \mbox{\$o}\qquad\mbox{tff}(\mbox{sorted\_type},\mbox{type})$

$\mbox{sorted}(\mbox{nil})\qquad\mbox{tff}(\mbox{empty\_is\_sorted},\mbox{axiom})$

$\forall x{:}\;\mbox{\$int}{:}\;\mbox{sorted}(\mbox{mycons}(x,\mbox{nil}))\qquad\mbox{tff}(\mbox{single\_is\_sorted},\mbox{axiom})$

$\forall x{:}\;\mbox{\$int},y{:}\;\mbox{\$int},r{:}\;\mbox{list}{:}\;( ( \mbox{\$less}(x,y)\mbox{ and }\mbox{sorted}(\mbox{mycons}(y,r)) ) \ \Rightarrow \ \mbox{sorted}(\mbox{mycons}(x,\mbox{mycons}(y,r))) )\qquad\mbox{tff}(\mbox{recursive\_sort},\mbox{axiom})$

$\mbox{sorted}(\mbox{mycons}(1,\mbox{mycons}(2,\mbox{mycons}(4,\mbox{mycons}(7,\mbox{mycons}(100,\mbox{nil}))))))\qquad\mbox{tff}(\mbox{check\_list},\mbox{conjecture})$

\medskip\textbf{DAT031=1.p} Some element is betweeb 20 and 40






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\forall u{:}\;\mbox{collection}{:}\;( u = 10 + ( 30 + ( 50 + \mbox{empty} ) ) \ \Rightarrow \ \exists v{:}\;\mbox{\$int}{:}\;( \mbox{\$lesseq}(20,v)\mbox{ and }\mbox{\$lesseq}(v,40)\mbox{ and }\mbox{in}(v,u) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT025=1.p} With 0 and 1 removed all elements are greater or equal to 2






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\forall u{:}\;\mbox{collection}{:}\;( ( \forall v{:}\;\mbox{\$int}{:}\;( \mbox{in}(v,u) \ \Rightarrow \ \mbox{\$greatereq}(v,0) )\mbox{ and }\forall w{:}\;\mbox{\$int}{:}\;( \mbox{in}(w,u)\iff \mbox{in}(w,\mbox{remove}(0,\mbox{remove}(1,u))) ) ) \ \Rightarrow \ \forall x{:}\;\mbox{\$int}{:}\;( \mbox{in}(x,u) \ \Rightarrow \ \mbox{\$greatereq}(x,2) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT022=1.p} Elements stay positive






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{collection}{:}\;( ( \forall w{:}\;\mbox{\$int}{:}\;( \mbox{in}(w,v) \ \Rightarrow \ \mbox{\$greater}(w,0) )\mbox{ and }u = 2 + \mbox{remove}(7,v) ) \ \Rightarrow \ \forall x{:}\;\mbox{\$int}{:}\;( \mbox{in}(x,u) \ \Rightarrow \ \mbox{\$greater}(x,0) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT015=1.p} Some element is 50






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

$\forall u{:}\;\mbox{array}{:}\;( \forall v{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(20,v)\mbox{ and }\mbox{\$lesseq}(v,30) ) \ \Rightarrow \ \mbox{read}(u,v) = \mbox{\$sum}(v,25) ) \ \Rightarrow \ \exists w{:}\;\mbox{\$int}{:}\;\mbox{read}(u,w) = 50 )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT032=1.p} Removing one elements changes count by one






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\forall u{:}\;\mbox{collection}{:}\;( \mbox{\$greatereq}(\mbox{count}(\mbox{remove}(5,u)),7) \ \Rightarrow \ \mbox{\$greatereq}(\mbox{count}(\mbox{remove}(4,u)),6) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT110=1.p} Array data types






$\mbox{include}(\mbox{'Axioms/DAT004=0.ax'})$

\medskip\textbf{DAT073=1.p} Arrays problem 3






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

$\mbox{read}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{read\_type},\mbox{type})$

$\mbox{write}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{write\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},i{:}\;\mbox{\$int},v{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{write}(a,i,v),i) = v\qquad\mbox{tff}(\mbox{ax}_1,\mbox{axiom})$

$\forall a{:}\;\mbox{array},i{:}\;\mbox{\$int},j{:}\;\mbox{\$int},v{:}\;\mbox{\$int}{:}\;( i = j\mbox{ or }\mbox{read}(\mbox{write}(a,i,v),j) = \mbox{read}(a,j) )\qquad\mbox{tff}(\mbox{ax}_2,\mbox{axiom})$

$\forall a{:}\;\mbox{array},b{:}\;\mbox{array}{:}\;( \forall i{:}\;\mbox{\$int}{:}\;\mbox{read}(a,i) = \mbox{read}(b,i) \ \Rightarrow \ a = b )\qquad\mbox{tff}(\mbox{ext},\mbox{axiom})$

$\mbox{init}{:}\;\mbox{\$int}\to \mbox{array}\qquad\mbox{tff}(\mbox{init\_type},\mbox{type})$

$\forall v{:}\;\mbox{\$int},i{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{init}(v),i) = v\qquad\mbox{tff}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{max}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{max},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int},w{:}\;\mbox{\$int}{:}\;( \mbox{max}(a,n) = w \ \Leftarrow \ ( \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),w) )\mbox{ and }\exists i{:}\;\mbox{\$int}{:}\;( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0)\mbox{ and }\mbox{read}(a,i) = w ) ) )\qquad\mbox{tff}(a,\mbox{axiom})$

$\mbox{sorted}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{sorted\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{sorted}(a,n)\iff \forall i{:}\;\mbox{\$int},j{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(0,i)\mbox{ and }\mbox{\$less}(i,n)\mbox{ and }\mbox{\$less}(i,j)\mbox{ and }\mbox{\$less}(j,n) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),\mbox{read}(a,j)) ) )\qquad\mbox{tff}(\mbox{sorted}_1,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},r{:}\;\mbox{\$int},n{:}\;\mbox{\$int}{:}\;( \mbox{inRange}(a,r,n)\iff \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ ( \mbox{\$greatereq}(r,\mbox{read}(a,i))\mbox{ and }\mbox{\$greatereq}(\mbox{read}(a,i),0) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{distinct}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{distinct\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{distinct}(a,n)\iff \forall i{:}\;\mbox{\$int},j{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greater}(n,j)\mbox{ and }\mbox{\$greatereq}(j,0)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ ( \mbox{read}(a,i) = \mbox{read}(a,j) \ \Rightarrow \ i = j ) ) )\qquad\mbox{tff}(\mbox{distinct},\mbox{axiom})$

$\mbox{rev}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{rev\_n},\mbox{type})$

$\forall a{:}\;\mbox{array},b{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{rev}(a,n) = b \ \Leftarrow \ \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greatereq}(i,0)\mbox{ and }\mbox{\$greater}(n,i)\mbox{ and }\mbox{read}(b,i) = \mbox{read}(a,\mbox{\$difference}(n,\mbox{\$sum}(i,1))) )\mbox{ or }( ( \mbox{\$greater}(0,i)\mbox{ or }\mbox{\$greatereq}(i,n) )\mbox{ and }\mbox{read}(b,i) = \mbox{read}(a,i) ) ) )\qquad\mbox{tff}(\mbox{rev\_n1\_proper},\mbox{axiom})$

$\neg\,\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{\$greatereq}(n,0) \ \Rightarrow \ \mbox{inRange}(a,\mbox{max}(a,n),n) )\qquad\mbox{tff}(c_1,\mbox{conjecture})$

\medskip\textbf{DAT050=1.p} Adding 0 to equal size results






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{\$int}{:}\;\mbox{count}(0 + \mbox{remove}(v,v + u)) = \mbox{count}(0 + \mbox{remove}(v,u))\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT004=1.p} Element 4 is 44 or 66






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

$\forall u{:}\;\mbox{array},v{:}\;\mbox{array},w{:}\;\mbox{\$int}{:}\;( u = \mbox{write}(\mbox{write}(\mbox{write}(\mbox{write}(v,3,33),4,44),5,55),w,66) \ \Rightarrow \ ( \mbox{read}(u,4) = 44\mbox{ or }\mbox{read}(u,4) = 66 ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT079=1.p} Lists by functions problem 1






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\mbox{in}(2,\mbox{cons}(1,\mbox{cons}(2,\mbox{cons}(3,\mbox{nil}))))\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT051=1.p} Even and odd numbered elements 1






$\mbox{include}(\mbox{'Axioms/DAT003=0.ax'})$

$\forall u{:}\;\mbox{record},v{:}\;\mbox{record}{:}\;( ( \mbox{isrecord}(u)\mbox{ and }\mbox{isrecord}(\mbox{next}(u))\mbox{ and }v = \mbox{next}(\mbox{next}(u))\mbox{ and }( \mbox{\$product}(2,\mbox{length}(\mbox{split}_2(v))) = \mbox{\$difference}(\mbox{length}(v),1)\mbox{ or }\mbox{\$product}(2,\mbox{length}(\mbox{split}_2(v))) = \mbox{length}(v) ) ) \ \Rightarrow \ ( \mbox{\$product}(2,\mbox{length}(\mbox{split}_2(u))) = \mbox{\$difference}(\mbox{length}(u),1)\mbox{ or }\mbox{\$product}(2,\mbox{length}(\mbox{split}_2(u))) = \mbox{length}(u) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT112=1.p} Tree-heap data types






$\mbox{include}(\mbox{'Axioms/DAT006=0.ax'})$

\medskip\textbf{DAT062=1.p} Heap lengths






$\mbox{include}(\mbox{'Axioms/DAT005=0.ax'})$

$\forall h{:}\;\mbox{heap},n{:}\;\mbox{\$int}{:}\;( \neg\,\forall h_0{:}\;\mbox{heap}{:}\;( \mbox{lsls}(h_0,h) \ \Rightarrow \ \mbox{\$less}(\mbox{length}(h_0),\mbox{length}(h)) )\mbox{ or }\forall h_0{:}\;\mbox{heap}{:}\;( \mbox{lsls}(h_0,\mbox{app}(h,n)) \ \Rightarrow \ \mbox{\$less}(\mbox{length}(h_0),\mbox{length}(\mbox{app}(h,n))) ) )\qquad\mbox{tff}(\mbox{th\_lem\_1a},\mbox{conjecture})$

\medskip\textbf{DAT098=1.p} Lists by relations problem 1






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{inRange}(4,\mbox{cons}(1,\mbox{cons}(3,\mbox{cons}(2,\mbox{nil}))))\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT105=1.p} Lists by relations problem 8






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\neg\,\forall l{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( ( l\ne \mbox{nil}\mbox{ and }\mbox{inRange}(n,l) ) \ \Rightarrow \ \mbox{\$greatereq}(\mbox{\$difference}(n,\mbox{head}(l)),2) )\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT026=1.p} Replacing 2 by something larger keeps elements positive






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{collection},w{:}\;\mbox{\$int}{:}\;( ( \forall x{:}\;\mbox{\$int}{:}\;( \mbox{in}(x,v) \ \Rightarrow \ \mbox{\$greater}(x,0) )\mbox{ and }\mbox{in}(w,v)\mbox{ and }u = \mbox{\$sum}(w,2) + \mbox{remove}(w,v) ) \ \Rightarrow \ \forall y{:}\;\mbox{\$int}{:}\;( \mbox{in}(y,u) \ \Rightarrow \ \mbox{\$greater}(y,0) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT002$\wedge$1.p} Recursive list Fibonacci sort

A list is Fibonacci sorted if it is sorted, and every element is
 greater of equal to the sum of its two predecessors (from the
 third element onwards).




$\mbox{list}{:}\;\mbox{\$tType}\qquad\mbox{thf}(\mbox{list\_type},\mbox{type})$

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{thf}(\mbox{nil\_type},\mbox{type})$

$\mbox{mycons}{:}\;\mbox{\$int}\to \mbox{list}\to \mbox{list}\qquad\mbox{thf}(\mbox{mycons\_type},\mbox{type})$

$\mbox{fib\_sorted}{:}\;\mbox{list}\to \mbox{\$o}\qquad\mbox{thf}(\mbox{sorted\_type},\mbox{type})$

$\mbox{fib\_sorted}@ \mbox{nil}\qquad\mbox{thf}(\mbox{empty\_fib\_sorted},\mbox{axiom})$

$\forall x{:}\;\mbox{\$int}{:}\;( \mbox{fib\_sorted}@ ( \mbox{mycons}@ x@ \mbox{nil} ) )\qquad\mbox{thf}(\mbox{single\_is\_fib\_sorted},\mbox{axiom})$

$\forall x{:}\;\mbox{\$int},y{:}\;\mbox{\$int}{:}\;( ( \mbox{\$less}@ x@ y ) \ \Rightarrow \ ( \mbox{fib\_sorted}@ ( \mbox{mycons}@ x@ ( \mbox{mycons}@ y@ \mbox{nil} ) ) ) )\qquad\mbox{thf}(\mbox{double\_is\_fib\_sorted\_if\_ordered},\mbox{axiom})$

$\forall x{:}\;\mbox{\$int},y{:}\;\mbox{\$int},z{:}\;\mbox{\$int},r{:}\;\mbox{list}{:}\;( ( \mbox{\$less}@ x@ y\mbox{ and }\mbox{\$greatereq}@ z@ ( \mbox{\$sum}@ x@ y )\mbox{ and }\mbox{fib\_sorted}@ ( \mbox{mycons}@ y@ ( \mbox{mycons}@ z@ r ) ) ) \ \Rightarrow \ ( \mbox{fib\_sorted}@ ( \mbox{mycons}@ x@ ( \mbox{mycons}@ y@ ( \mbox{mycons}@ z@ r ) ) ) ) )\qquad\mbox{thf}(\mbox{recursive\_fib\_sort},\mbox{axiom})$

$\mbox{fib\_sorted}@ ( \mbox{mycons}@ 1@ ( \mbox{mycons}@ 2@ ( \mbox{mycons}@ 4@ ( \mbox{mycons}@ 7@ ( \mbox{mycons}@ 100@ \mbox{nil} ) ) ) ) )\qquad\mbox{thf}(\mbox{check\_list},\mbox{conjecture})$

\medskip\textbf{DAT049=1.p} Removing what you've added does change the size






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{\$int}{:}\;\mbox{count}(\mbox{remove}(v,v + u)) = \mbox{count}(\mbox{remove}(v,u))\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT108=1.p} Integer collections with counting






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

\medskip\textbf{DAT057=1.p} get-put on self






$\mbox{include}(\mbox{'Axioms/DAT004=0.ax'})$

$\forall d{:}\;\mbox{data},\mbox{ar}{:}\;\mbox{array},m{:}\;\mbox{\$int},n{:}\;\mbox{\$int}{:}\;( \mbox{get}(\mbox{put}(\mbox{ar},m,d),n) = \mbox{get}(\mbox{ar},n)\mbox{ or }m = n )\qquad\mbox{tff}(\mbox{th\_lem}_1,\mbox{conjecture})$

\medskip\textbf{DAT017=1.p} Arrays with different elements






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

$\forall u{:}\;\mbox{array},v{:}\;\mbox{array},w{:}\;\mbox{\$int},x{:}\;\mbox{\$int},y{:}\;\mbox{\$int}{:}\;( ( \mbox{read}(v,w)\ne \mbox{read}(v,x)\mbox{ and }u = \mbox{write}(\mbox{write}(\mbox{write}(v,x,0),y,\mbox{\$sum}(\mbox{read}(v,y),1)),w,0) ) \ \Rightarrow \ \exists z{:}\;\mbox{\$int}{:}\;\mbox{read}(u,z)\ne \mbox{read}(v,z) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT085=1.p} Lists by functions problem 7






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\neg\,\forall l_1{:}\;\mbox{list},l_2{:}\;\mbox{list}{:}\;( \mbox{length}(l_1) = \mbox{length}(l_2) \ \Rightarrow \ l_1 = l_2 )\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT055=1.p} Boyer-Moore min-max problem






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

$a{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{a\_type},\mbox{type})$

$l{:}\;\mbox{\$int}\qquad\mbox{tff}(\mbox{l\_type},\mbox{type})$

$k{:}\;\mbox{\$int}\qquad\mbox{tff}(\mbox{k\_type},\mbox{type})$

$\mbox{min}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{min\_type},\mbox{type})$

$\mbox{max}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{max\_type},\mbox{type})$

$( \forall x{:}\;\mbox{list}{:}\;\mbox{\$lesseq}(\mbox{min}(x),\mbox{max}(x))\mbox{ and }\mbox{\$lesseq}(l,\mbox{min}(a))\mbox{ and }\mbox{\$less}(0,k) ) \ \Rightarrow \ \mbox{\$less}(l,\mbox{\$sum}(\mbox{max}(a),k))\qquad\mbox{tff}(\mbox{boyer\_moore\_max\_min},\mbox{conjecture})$

\medskip\textbf{DAT033=1.p} Count changes are consistent with adding and removal






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\forall u{:}\;\mbox{collection}{:}\;( \mbox{count}(5 + u) = \mbox{count}(3 + u) \ \Rightarrow \ \mbox{count}(\mbox{remove}(5,u)) = \mbox{count}(\mbox{remove}(3,u)) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT109=1.p} Pointer data types






$\mbox{include}(\mbox{'Axioms/DAT003=0.ax'})$

\medskip\textbf{DAT091=1.p} Lists by functions problem 13






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\neg\,\forall l_1{:}\;\mbox{list},l_2{:}\;\mbox{list}{:}\;( l_1\ne l_2 \ \Rightarrow \ \forall n{:}\;\mbox{\$int}{:}\;\mbox{count}(n,l_1)\ne \mbox{count}(n,l_2) )\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT034=1.p} Adding an element increases the count by at least one






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{\$int}{:}\;\mbox{\$greatereq}(\mbox{\$sum}(\mbox{count}(u),1),\mbox{count}(v + u))\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT099=1.p} Lists by relations problem 2






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\forall n{:}\;\mbox{\$int}{:}\;( \mbox{\$greatereq}(n,4) \ \Rightarrow \ \mbox{inRange}(n,\mbox{cons}(1,\mbox{cons}(3,\mbox{cons}(2,\mbox{nil})))) )\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT019=1.p} 3 is in the colection






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{in}(3,1 + ( 3 + ( 5 + \mbox{empty} ) ))\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT003=1.p} Element 3 is 33






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

$\forall u{:}\;\mbox{array},v{:}\;\mbox{array}{:}\;( u = \mbox{write}(\mbox{write}(\mbox{write}(\mbox{write}(v,3,33),4,444),5,55),4,44) \ \Rightarrow \ \mbox{read}(u,3) = 33 )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT067=1.p} Add an element to a tree heap






$\mbox{include}(\mbox{'Axioms/DAT006=0.ax'})$

$\forall n{:}\;\mbox{\$int},m{:}\;\mbox{\$int},h{:}\;\mbox{heap}{:}\;( \mbox{sel}(\mbox{app}(h,n),m) = \mbox{sel}(h,m)\mbox{ or }m = \mbox{\$sum}(1,\mbox{length}(h)) )\qquad\mbox{tff}(\mbox{th}_2,\mbox{conjecture})$

\medskip\textbf{DAT090=1.p} Lists by functions problem 12






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\neg\,\exists n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{\$greater}(\mbox{count}(n,l),\mbox{length}(l))\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT072=1.p} Arrays problem 2






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

$\mbox{read}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{read\_type},\mbox{type})$

$\mbox{write}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{write\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},i{:}\;\mbox{\$int},v{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{write}(a,i,v),i) = v\qquad\mbox{tff}(\mbox{ax}_1,\mbox{axiom})$

$\forall a{:}\;\mbox{array},i{:}\;\mbox{\$int},j{:}\;\mbox{\$int},v{:}\;\mbox{\$int}{:}\;( i = j\mbox{ or }\mbox{read}(\mbox{write}(a,i,v),j) = \mbox{read}(a,j) )\qquad\mbox{tff}(\mbox{ax}_2,\mbox{axiom})$

$\forall a{:}\;\mbox{array},b{:}\;\mbox{array}{:}\;( \forall i{:}\;\mbox{\$int}{:}\;\mbox{read}(a,i) = \mbox{read}(b,i) \ \Rightarrow \ a = b )\qquad\mbox{tff}(\mbox{ext},\mbox{axiom})$

$\mbox{init}{:}\;\mbox{\$int}\to \mbox{array}\qquad\mbox{tff}(\mbox{init\_type},\mbox{type})$

$\forall v{:}\;\mbox{\$int},i{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{init}(v),i) = v\qquad\mbox{tff}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{max}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{max},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int},w{:}\;\mbox{\$int}{:}\;( \mbox{max}(a,n) = w \ \Leftarrow \ ( \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),w) )\mbox{ and }\exists i{:}\;\mbox{\$int}{:}\;( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0)\mbox{ and }\mbox{read}(a,i) = w ) ) )\qquad\mbox{tff}(a,\mbox{axiom})$

$\mbox{sorted}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{sorted\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{sorted}(a,n)\iff \forall i{:}\;\mbox{\$int},j{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(0,i)\mbox{ and }\mbox{\$less}(i,n)\mbox{ and }\mbox{\$less}(i,j)\mbox{ and }\mbox{\$less}(j,n) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),\mbox{read}(a,j)) ) )\qquad\mbox{tff}(\mbox{sorted}_1,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},r{:}\;\mbox{\$int},n{:}\;\mbox{\$int}{:}\;( \mbox{inRange}(a,r,n)\iff \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ ( \mbox{\$greatereq}(r,\mbox{read}(a,i))\mbox{ and }\mbox{\$greatereq}(\mbox{read}(a,i),0) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{distinct}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{distinct\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{distinct}(a,n)\iff \forall i{:}\;\mbox{\$int},j{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greater}(n,j)\mbox{ and }\mbox{\$greatereq}(j,0)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ ( \mbox{read}(a,i) = \mbox{read}(a,j) \ \Rightarrow \ i = j ) ) )\qquad\mbox{tff}(\mbox{distinct},\mbox{axiom})$

$\mbox{rev}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{rev\_n},\mbox{type})$

$\forall a{:}\;\mbox{array},b{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{rev}(a,n) = b \ \Leftarrow \ \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greatereq}(i,0)\mbox{ and }\mbox{\$greater}(n,i)\mbox{ and }\mbox{read}(b,i) = \mbox{read}(a,\mbox{\$difference}(n,\mbox{\$sum}(i,1))) )\mbox{ or }( ( \mbox{\$greater}(0,i)\mbox{ or }\mbox{\$greatereq}(i,n) )\mbox{ and }\mbox{read}(b,i) = \mbox{read}(a,i) ) ) )\qquad\mbox{tff}(\mbox{rev\_n1\_proper},\mbox{axiom})$

$\forall a{:}\;\mbox{array},b_1{:}\;\mbox{array},b_2{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( ( \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greatereq}(i,0)\mbox{ and }\mbox{\$greater}(n,i)\mbox{ and }\mbox{read}(b_1,i) = \mbox{read}(a,\mbox{\$difference}(n,\mbox{\$sum}(i,1))) )\mbox{ or }( ( \mbox{\$greater}(0,i)\mbox{ or }\mbox{\$greatereq}(i,n) )\mbox{ and }\mbox{read}(b_1,i) = \mbox{read}(a,i) ) )\mbox{ and }\forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greatereq}(i,0)\mbox{ and }\mbox{\$greater}(n,i)\mbox{ and }\mbox{read}(b_2,i) = \mbox{read}(a,\mbox{\$difference}(n,\mbox{\$sum}(i,1))) )\mbox{ or }( ( \mbox{\$greater}(0,i)\mbox{ or }\mbox{\$greatereq}(i,n) )\mbox{ and }\mbox{read}(b_2,i) = \mbox{read}(a,i) ) ) ) \ \Rightarrow \ b_1 = b_2 )\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT038=1.p} If 2 and 3 are the only elements, there are not 5 elements






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\forall u{:}\;\mbox{collection}{:}\;( ( \mbox{in}(2,u)\mbox{ and }\mbox{in}(3,u)\mbox{ and }\mbox{count}(u) = 2 ) \ \Rightarrow \ \neg\,\mbox{in}(5,u) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT094=1.p} Lists by functions problem 16






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\neg\,\forall k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;( ( \mbox{\$greater}(\mbox{length}(k),1)\mbox{ and }\mbox{\$greater}(\mbox{length}(l),1) ) \ \Rightarrow \ \mbox{\$greater}(\mbox{length}(\mbox{append}(k,l)),4) )\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT074=1.p} Arrays problem 4






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

$\mbox{read}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{read\_type},\mbox{type})$

$\mbox{write}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{write\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},i{:}\;\mbox{\$int},v{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{write}(a,i,v),i) = v\qquad\mbox{tff}(\mbox{ax}_1,\mbox{axiom})$

$\forall a{:}\;\mbox{array},i{:}\;\mbox{\$int},j{:}\;\mbox{\$int},v{:}\;\mbox{\$int}{:}\;( i = j\mbox{ or }\mbox{read}(\mbox{write}(a,i,v),j) = \mbox{read}(a,j) )\qquad\mbox{tff}(\mbox{ax}_2,\mbox{axiom})$

$\forall a{:}\;\mbox{array},b{:}\;\mbox{array}{:}\;( \forall i{:}\;\mbox{\$int}{:}\;\mbox{read}(a,i) = \mbox{read}(b,i) \ \Rightarrow \ a = b )\qquad\mbox{tff}(\mbox{ext},\mbox{axiom})$

$\mbox{init}{:}\;\mbox{\$int}\to \mbox{array}\qquad\mbox{tff}(\mbox{init\_type},\mbox{type})$

$\forall v{:}\;\mbox{\$int},i{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{init}(v),i) = v\qquad\mbox{tff}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{max}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{max},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int},w{:}\;\mbox{\$int}{:}\;( \mbox{max}(a,n) = w \ \Leftarrow \ ( \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),w) )\mbox{ and }\exists i{:}\;\mbox{\$int}{:}\;( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0)\mbox{ and }\mbox{read}(a,i) = w ) ) )\qquad\mbox{tff}(a,\mbox{axiom})$

$\mbox{sorted}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{sorted\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{sorted}(a,n)\iff \forall i{:}\;\mbox{\$int},j{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(0,i)\mbox{ and }\mbox{\$less}(i,n)\mbox{ and }\mbox{\$less}(i,j)\mbox{ and }\mbox{\$less}(j,n) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),\mbox{read}(a,j)) ) )\qquad\mbox{tff}(\mbox{sorted}_1,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},r{:}\;\mbox{\$int},n{:}\;\mbox{\$int}{:}\;( \mbox{inRange}(a,r,n)\iff \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ ( \mbox{\$greatereq}(r,\mbox{read}(a,i))\mbox{ and }\mbox{\$greatereq}(\mbox{read}(a,i),0) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{distinct}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{distinct\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{distinct}(a,n)\iff \forall i{:}\;\mbox{\$int},j{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greater}(n,j)\mbox{ and }\mbox{\$greatereq}(j,0)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ ( \mbox{read}(a,i) = \mbox{read}(a,j) \ \Rightarrow \ i = j ) ) )\qquad\mbox{tff}(\mbox{distinct},\mbox{axiom})$

$\mbox{rev}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{rev\_n},\mbox{type})$

$\forall a{:}\;\mbox{array},b{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{rev}(a,n) = b \ \Leftarrow \ \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greatereq}(i,0)\mbox{ and }\mbox{\$greater}(n,i)\mbox{ and }\mbox{read}(b,i) = \mbox{read}(a,\mbox{\$difference}(n,\mbox{\$sum}(i,1))) )\mbox{ or }( ( \mbox{\$greater}(0,i)\mbox{ or }\mbox{\$greatereq}(i,n) )\mbox{ and }\mbox{read}(b,i) = \mbox{read}(a,i) ) ) )\qquad\mbox{tff}(\mbox{rev\_n1\_proper},\mbox{axiom})$

$\neg\,\forall n{:}\;\mbox{\$int},i{:}\;\mbox{\$int}{:}\;\mbox{distinct}(\mbox{init}(n),i)\qquad\mbox{tff}(c_2,\mbox{conjecture})$

\medskip\textbf{DAT088=1.p} Lists by functions problem 10






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\neg\,\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( l\ne \mbox{nil} \ \Rightarrow \ \mbox{count}(n,l) = \mbox{count}(n,\mbox{tail}(l)) )\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT082=1.p} Lists by functions problem 4






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\mbox{length}(\mbox{cons}(1,\mbox{cons}(2,\mbox{nil}))) = 2\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT056$\wedge$2.p} List operation requiring induction






$\mbox{lst}{:}\;\mbox{\$tType}\qquad\mbox{thf}(\mbox{ty\_n\_tc\_\_Foo\_\_Olst\_It\_\_J},\mbox{type})$

$a{:}\;\mbox{\$tType}\qquad\mbox{thf}(\mbox{ty\_n\_t\_},\mbox{type})$

$\mbox{ap}{:}\;\mbox{lst}\to \mbox{lst}\to \mbox{lst}\qquad\mbox{thf}(\mbox{sy\_c\_Foo\_Oap\_001t\_},\mbox{type})$

$\mbox{cns}{:}\;a\to \mbox{lst}\to \mbox{lst}\qquad\mbox{thf}(\mbox{sy\_c\_Foo\_Olst\_OCns\_001t\_},\mbox{type})$

$\mbox{nl}{:}\;\mbox{lst}\qquad\mbox{thf}(\mbox{sy\_c\_Foo\_Olst\_ONl\_001t\_},\mbox{type})$

$\mbox{xs}{:}\;\mbox{lst}\qquad\mbox{thf}(\mbox{sy\_v\_xs},\mbox{type})$

$\forall \mbox{lst}{:}\;\mbox{lst},p{:}\;\mbox{lst}\to \mbox{\$o}{:}\;( ( p@ \mbox{nl} ) \ \Rightarrow \ ( \forall a{:}\;a,\mbox{lst}_2{:}\;\mbox{lst}{:}\;( ( p@ \mbox{lst}_2 ) \ \Rightarrow \ ( p@ ( \mbox{cns}@ a@ \mbox{lst}_2 ) ) ) \ \Rightarrow \ ( p@ \mbox{lst} ) ) )\qquad\mbox{thf}(\mbox{fact\_0\_lst\_Oinduct},\mbox{axiom})$

$\forall \mbox{ys}_2{:}\;\mbox{lst},\mbox{xs}{:}\;\mbox{lst},x{:}\;a{:}\;( \mbox{ap}@ ( \mbox{cns}@ x@ \mbox{xs} )@ \mbox{ys}_2 ) = ( \mbox{cns}@ x@ ( \mbox{ap}@ \mbox{xs}@ \mbox{ys}_2 ) )\qquad\mbox{thf}(\mbox{fact\_1p\_Osimps\_I2\_J},\mbox{axiom})$

$\forall \mbox{ys}_2{:}\;\mbox{lst}{:}\;( \mbox{ap}@ \mbox{nl}@ \mbox{ys}_2 ) = \mbox{ys}_2\qquad\mbox{thf}(\mbox{fact\_2p\_Osimps\_I1\_J},\mbox{axiom})$

$\forall \mbox{ys}{:}\;\mbox{lst},\mbox{zs}{:}\;\mbox{lst}{:}\;( \mbox{ap}@ \mbox{xs}@ ( \mbox{ap}@ \mbox{ys}@ \mbox{zs} ) ) = ( \mbox{ap}@ ( \mbox{ap}@ \mbox{xs}@ \mbox{ys} )@ \mbox{zs} )\qquad\mbox{thf}(\mbox{conj}_0,\mbox{conjecture})$

\medskip\textbf{DAT111=1.p} Heap data types






$\mbox{include}(\mbox{'Axioms/DAT005=0.ax'})$

\medskip\textbf{DAT093=1.p} Lists by functions problem 15






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\neg\,\forall k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{append}(k,l)) = \mbox{\$sum}(\mbox{\$sum}(\mbox{length}(k),\mbox{length}(l)),1)\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT084=1.p} Lists by functions problem 6






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\neg\,\exists l{:}\;\mbox{list}{:}\;\mbox{length}(l) = \mbox{length}(\mbox{cons}(1,l))\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT042=1.p} Some collection has 3 as an element






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\exists u{:}\;\mbox{collection}{:}\;\mbox{count}(u) = 3\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT028=1.p} Comparing elements in two collections 1






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{collection}{:}\;( ( \forall w{:}\;\mbox{\$int}{:}\;( \mbox{in}(w,v) \ \Rightarrow \ \mbox{\$greater}(w,0) )\mbox{ and }\forall x{:}\;\mbox{\$int}{:}\;( \mbox{in}(x,u) \ \Rightarrow \ \exists y{:}\;\mbox{\$int}{:}\;( \mbox{in}(y,v)\mbox{ and }\mbox{\$greater}(x,y) ) ) ) \ \Rightarrow \ \forall z{:}\;\mbox{\$int}{:}\;( \mbox{in}(z,u) \ \Rightarrow \ \mbox{\$greater}(z,1) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT044=1.p} Adding a larger element to the collection 1






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{\$int}{:}\;( \forall w{:}\;\mbox{\$int}{:}\;( \mbox{in}(w,u) \ \Rightarrow \ \mbox{\$greater}(v,w) ) \ \Rightarrow \ \mbox{\$greater}(\mbox{count}(v + u),\mbox{count}(u)) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT083=1.p} Lists by functions problem 5






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\mbox{length}(\mbox{cons}(1,\mbox{cons}(2,\mbox{nil})))\ne 3\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT027=1.p} Replacing 2 by something positive keeps elements positive






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{collection},w{:}\;\mbox{\$int},x{:}\;\mbox{\$int}{:}\;( ( \forall y{:}\;\mbox{\$int}{:}\;( \mbox{in}(y,v) \ \Rightarrow \ \mbox{\$greater}(y,0) )\mbox{ and }\mbox{in}(w,v)\mbox{ and }\mbox{\$greatereq}(x,0)\mbox{ and }u = \mbox{\$sum}(w,x) + \mbox{remove}(w,v) ) \ \Rightarrow \ \forall z{:}\;\mbox{\$int}{:}\;( \mbox{in}(z,u) \ \Rightarrow \ \mbox{\$greater}(z,0) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT071=1.p} Arrays problem 1






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

$\mbox{read}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{read\_type},\mbox{type})$

$\mbox{write}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{write\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},i{:}\;\mbox{\$int},v{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{write}(a,i,v),i) = v\qquad\mbox{tff}(\mbox{ax}_1,\mbox{axiom})$

$\forall a{:}\;\mbox{array},i{:}\;\mbox{\$int},j{:}\;\mbox{\$int},v{:}\;\mbox{\$int}{:}\;( i = j\mbox{ or }\mbox{read}(\mbox{write}(a,i,v),j) = \mbox{read}(a,j) )\qquad\mbox{tff}(\mbox{ax}_2,\mbox{axiom})$

$\forall a{:}\;\mbox{array},b{:}\;\mbox{array}{:}\;( \forall i{:}\;\mbox{\$int}{:}\;\mbox{read}(a,i) = \mbox{read}(b,i) \ \Rightarrow \ a = b )\qquad\mbox{tff}(\mbox{ext},\mbox{axiom})$

$\mbox{init}{:}\;\mbox{\$int}\to \mbox{array}\qquad\mbox{tff}(\mbox{init\_type},\mbox{type})$

$\forall v{:}\;\mbox{\$int},i{:}\;\mbox{\$int}{:}\;\mbox{read}(\mbox{init}(v),i) = v\qquad\mbox{tff}(\mbox{ax}_3,\mbox{axiom})$

$\mbox{max}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$int}\qquad\mbox{tff}(\mbox{max},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int},w{:}\;\mbox{\$int}{:}\;( \mbox{max}(a,n) = w \ \Leftarrow \ ( \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),w) )\mbox{ and }\exists i{:}\;\mbox{\$int}{:}\;( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0)\mbox{ and }\mbox{read}(a,i) = w ) ) )\qquad\mbox{tff}(a,\mbox{axiom})$

$\mbox{sorted}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{sorted\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{sorted}(a,n)\iff \forall i{:}\;\mbox{\$int},j{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(0,i)\mbox{ and }\mbox{\$less}(i,n)\mbox{ and }\mbox{\$less}(i,j)\mbox{ and }\mbox{\$less}(j,n) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),\mbox{read}(a,j)) ) )\qquad\mbox{tff}(\mbox{sorted}_1,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{array}\times \mbox{\$int}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},r{:}\;\mbox{\$int},n{:}\;\mbox{\$int}{:}\;( \mbox{inRange}(a,r,n)\iff \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ ( \mbox{\$greatereq}(r,\mbox{read}(a,i))\mbox{ and }\mbox{\$greatereq}(\mbox{read}(a,i),0) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{distinct}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{distinct\_type},\mbox{type})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{distinct}(a,n)\iff \forall i{:}\;\mbox{\$int},j{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greater}(n,j)\mbox{ and }\mbox{\$greatereq}(j,0)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ ( \mbox{read}(a,i) = \mbox{read}(a,j) \ \Rightarrow \ i = j ) ) )\qquad\mbox{tff}(\mbox{distinct},\mbox{axiom})$

$\mbox{rev}{:}\;( \mbox{array}\times \mbox{\$int} )\to \mbox{array}\qquad\mbox{tff}(\mbox{rev\_n},\mbox{type})$

$\forall a{:}\;\mbox{array},b{:}\;\mbox{array},n{:}\;\mbox{\$int}{:}\;( \mbox{rev}(a,n) = b \ \Leftarrow \ \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greatereq}(i,0)\mbox{ and }\mbox{\$greater}(n,i)\mbox{ and }\mbox{read}(b,i) = \mbox{read}(a,\mbox{\$difference}(n,\mbox{\$sum}(i,1))) )\mbox{ or }( ( \mbox{\$greater}(0,i)\mbox{ or }\mbox{\$greatereq}(i,n) )\mbox{ and }\mbox{read}(b,i) = \mbox{read}(a,i) ) ) )\qquad\mbox{tff}(\mbox{rev\_n1\_proper},\mbox{axiom})$

$\forall a{:}\;\mbox{array},n{:}\;\mbox{\$int},w_1{:}\;\mbox{\$int},w_2{:}\;\mbox{\$int}{:}\;( ( \forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),w_1) )\mbox{ and }\exists i{:}\;\mbox{\$int}{:}\;( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0)\mbox{ and }\mbox{read}(a,i) = w_1 )\mbox{ and }\forall i{:}\;\mbox{\$int}{:}\;( ( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0) ) \ \Rightarrow \ \mbox{\$lesseq}(\mbox{read}(a,i),w_2) )\mbox{ and }\exists i{:}\;\mbox{\$int}{:}\;( \mbox{\$greater}(n,i)\mbox{ and }\mbox{\$greatereq}(i,0)\mbox{ and }\mbox{read}(a,i) = w_2 ) ) \ \Rightarrow \ w_1 = w_2 )\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT059=1.p} put is commutative






$\mbox{include}(\mbox{'Axioms/DAT004=0.ax'})$

$\forall d_1{:}\;\mbox{data},\mbox{ar}{:}\;\mbox{array},m{:}\;\mbox{\$int},d_2{:}\;\mbox{data}{:}\;\mbox{put}(\mbox{put}(\mbox{ar},m,d_1),m,d_2) = \mbox{put}(\mbox{ar},m,d_2)\qquad\mbox{tff}(\mbox{th\_lem}_5,\mbox{conjecture})$

\medskip\textbf{DAT009=1.p} Every element greater than its index






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

$\forall u{:}\;\mbox{array},v{:}\;\mbox{array},w{:}\;\mbox{\$int}{:}\;( ( \forall x{:}\;\mbox{\$int}{:}\;\mbox{\$greater}(\mbox{read}(v,x),x)\mbox{ and }u = \mbox{write}(v,w,\mbox{\$sum}(w,3)) ) \ \Rightarrow \ \forall y{:}\;\mbox{\$int}{:}\;\mbox{\$greater}(\mbox{read}(u,y),y) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT030=1.p} Comparing elements in two collections 3






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{collection}{:}\;( ( \forall w{:}\;\mbox{\$int}{:}\;( \mbox{in}(w,v) \ \Rightarrow \ \mbox{\$greater}(w,0) )\mbox{ and }\forall x{:}\;\mbox{\$int}{:}\;( \mbox{in}(x,u) \ \Rightarrow \ \exists y{:}\;\mbox{\$int},z{:}\;\mbox{\$int}{:}\;( \mbox{in}(y,v)\mbox{ and }\mbox{in}(z,v)\mbox{ and }x = \mbox{\$sum}(y,z) ) ) ) \ \Rightarrow \ \forall x_1{:}\;\mbox{\$int}{:}\;( \mbox{in}(x_1,u) \ \Rightarrow \ \mbox{\$greater}(x_1,1) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT016=1.p} Some element is 53






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

$\forall u{:}\;\mbox{array}{:}\;( \forall v{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(20,v)\mbox{ and }\mbox{\$lesseq}(v,30) ) \ \Rightarrow \ \mbox{read}(u,v) = \mbox{\$sum}(\mbox{\$product}(2,v),3) ) \ \Rightarrow \ \exists w{:}\;\mbox{\$int}{:}\;\mbox{read}(u,w) = 53 )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT006=1.p} Some element is 33






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

$\forall u{:}\;\mbox{array},v{:}\;\mbox{array}{:}\;( u = \mbox{write}(\mbox{write}(\mbox{write}(\mbox{write}(v,3,33),4,444),5,55),4,44) \ \Rightarrow \ \exists w{:}\;\mbox{\$int}{:}\;\mbox{read}(u,w) = 33 )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT052=1.p} Even and odd numbered elements 2






$\mbox{include}(\mbox{'Axioms/DAT003=0.ax'})$

$\forall u{:}\;\mbox{record},v{:}\;\mbox{record}{:}\;( ( \mbox{isrecord}(u)\mbox{ and }\mbox{isrecord}(\mbox{next}(u))\mbox{ and }v = \mbox{next}(\mbox{next}(u))\mbox{ and }\mbox{\$sum}(\mbox{length}(\mbox{split}_1(v)),\mbox{length}(\mbox{split}_2(v))) = \mbox{length}(v) ) \ \Rightarrow \ \mbox{\$sum}(\mbox{length}(\mbox{split}_1(u)),\mbox{length}(\mbox{split}_2(u))) = \mbox{length}(u) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT070=1.p} Select from only within a tree-heap






$\mbox{include}(\mbox{'Axioms/DAT006=0.ax'})$

$\forall n{:}\;\mbox{\$int},m{:}\;\mbox{\$int},h{:}\;\mbox{heap}{:}\;( \mbox{sel}(\mbox{app}(h,n),m) = \mbox{sel}(h,m)\mbox{ or }\neg\,\mbox{\$less}(m,\mbox{\$sum}(1,\mbox{length}(h))) )\qquad\mbox{tff}(\mbox{th}_5,\mbox{conjecture})$

\medskip\textbf{DAT104=1.p} Lists by relations problem 7






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\neg\,\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l) \ \Rightarrow \ \mbox{inRange}(\mbox{\$difference}(n,1),l) )\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT010=1.p} All elements are less than 100






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

$\forall u{:}\;\mbox{array},v{:}\;\mbox{array}{:}\;( ( u = \mbox{write}(\mbox{write}(\mbox{write}(\mbox{write}(v,3,33),4,444),5,55),4,44)\mbox{ and }\forall w{:}\;\mbox{\$int}{:}\;\mbox{\$less}(\mbox{read}(v,w),100) ) \ \Rightarrow \ \forall x{:}\;\mbox{\$int}{:}\;\mbox{\$less}(\mbox{read}(u,x),100) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT011=1.p} Compare elements 1






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

$\forall u{:}\;\mbox{array},v{:}\;\mbox{array},w{:}\;\mbox{\$int},x{:}\;\mbox{\$int}{:}\;( ( \forall y{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(w,y)\mbox{ and }\mbox{\$lesseq}(y,x) ) \ \Rightarrow \ \mbox{\$greater}(\mbox{read}(v,y),0) )\mbox{ and }u = \mbox{write}(v,\mbox{\$sum}(x,1),3) ) \ \Rightarrow \ \forall z{:}\;\mbox{\$int}{:}\;( ( \mbox{\$lesseq}(w,z)\mbox{ and }\mbox{\$lesseq}(z,\mbox{\$sum}(x,1)) ) \ \Rightarrow \ \mbox{\$greater}(\mbox{read}(u,z),0) ) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT039=1.p} If 2 and 3 are the only elements, then no elements are larger






$\mbox{include}(\mbox{'Axioms/DAT002=0.ax'})$

$\mbox{include}(\mbox{'Axioms/DAT002=1.ax'})$

$\forall u{:}\;\mbox{collection},v{:}\;\mbox{\$int}{:}\;( ( \mbox{in}(2,u)\mbox{ and }\mbox{in}(3,u)\mbox{ and }\mbox{count}(u) = 2\mbox{ and }\mbox{\$greater}(v,3) ) \ \Rightarrow \ \neg\,\mbox{in}(v,u) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT060=1.p} get-put on self lemma






$\mbox{include}(\mbox{'Axioms/DAT004=0.ax'})$

$\forall d{:}\;\mbox{data},\mbox{ar}{:}\;\mbox{array},n{:}\;\mbox{\$int},m{:}\;\mbox{\$int}{:}\;( \mbox{get}(\mbox{put}(\mbox{ar},m,d),n) = \mbox{get}(\mbox{ar},n)\mbox{ or }\neg\,\mbox{\$less}(n,m) )\qquad\mbox{tff}(\mbox{th\_lem}_6,\mbox{conjecture})$

\medskip\textbf{DAT081=1.p} Lists by functions problem 3






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

$\mbox{nil}{:}\;\mbox{list}\qquad\mbox{tff}(\mbox{nil\_type},\mbox{type})$

$\mbox{cons}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(\mbox{cons\_type},\mbox{type})$

$\mbox{head}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(\mbox{head\_type},\mbox{type})$

$\mbox{tail}{:}\;\mbox{list}\to \mbox{list}\qquad\mbox{tff}(\mbox{tail\_type},\mbox{type})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{head}(\mbox{cons}(k,l)) = k\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{tail}(\mbox{cons}(k,l)) = l\qquad\mbox{tff}(l_2,\mbox{axiom})$

$\forall l{:}\;\mbox{list}{:}\;( l = \mbox{nil}\mbox{ or }l = \mbox{cons}(\mbox{head}(l),\mbox{tail}(l)) )\qquad\mbox{tff}(l_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;\mbox{cons}(k,l)\ne \mbox{nil}\qquad\mbox{tff}(l_4,\mbox{axiom})$

$\mbox{in}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{in},\mbox{type})$

$\forall x{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(x,l)\iff ( \exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }x = h )\mbox{ or }\exists h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(h,t)\mbox{ and }\mbox{in}(x,t) ) ) )\qquad\mbox{tff}(\mbox{in\_conv},\mbox{axiom})$

$\mbox{inRange}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$o}\qquad\mbox{tff}(\mbox{inRange\_type},\mbox{type})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{inRange}(n,l)\iff ( l = \mbox{nil}\mbox{ or }\exists k{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;( l = \mbox{cons}(k,t)\mbox{ and }\mbox{\$lesseq}(0,k)\mbox{ and }\mbox{\$less}(k,n)\mbox{ and }\mbox{inRange}(n,t) ) ) )\qquad\mbox{tff}(\mbox{inRange},\mbox{axiom})$

$\mbox{length}{:}\;\mbox{list}\to \mbox{\$int}\qquad\mbox{tff}(t,\mbox{type})$

$\mbox{length}(\mbox{nil}) = 0\qquad\mbox{tff}(l,\mbox{axiom})$

$\forall h{:}\;\mbox{\$int},t{:}\;\mbox{list}{:}\;\mbox{length}(\mbox{cons}(h,t)) = \mbox{\$sum}(1,\mbox{length}(t))\qquad\mbox{tff}(l_1,\mbox{axiom})$

$\mbox{count}{:}\;( \mbox{\$int}\times \mbox{list} )\to \mbox{\$int}\qquad\mbox{tff}(t_2,\mbox{type})$

$\forall k{:}\;\mbox{\$int}{:}\;\mbox{count}(k,\mbox{nil}) = 0\qquad\mbox{tff}(a,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{count}(k,t) \ \Leftarrow \ k\ne h )\qquad\mbox{tff}(a_3,\mbox{axiom})$

$\forall k{:}\;\mbox{\$int},h{:}\;\mbox{\$int},t{:}\;\mbox{list},n{:}\;\mbox{\$int}{:}\;( \mbox{count}(k,\mbox{cons}(h,t)) = \mbox{\$sum}(\mbox{count}(k,t),1) \ \Leftarrow \ k = h )\qquad\mbox{tff}(a_4,\mbox{axiom})$

$\mbox{append}{:}\;( \mbox{list}\times \mbox{list} )\to \mbox{list}\qquad\mbox{tff}(t_5,\mbox{type})$

$\forall l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{nil},l) = l\qquad\mbox{tff}(l_6,\mbox{axiom})$

$\forall i{:}\;\mbox{\$int},k{:}\;\mbox{list},l{:}\;\mbox{list}{:}\;\mbox{append}(\mbox{cons}(i,k),l) = \mbox{cons}(i,\mbox{append}(k,l))\qquad\mbox{tff}(l_7,\mbox{axiom})$

$\forall n{:}\;\mbox{\$int},l{:}\;\mbox{list}{:}\;( \mbox{in}(n,l)\iff \mbox{\$greater}(\mbox{count}(n,l),0) )\qquad\mbox{tff}(a_8,\mbox{axiom})$

$\forall a{:}\;\mbox{\$int}{:}\;\neg\,\mbox{in}(a,\mbox{nil})\qquad\mbox{tff}(c,\mbox{conjecture})$

\medskip\textbf{DAT008=1.p} An element greater than its index






$\mbox{include}(\mbox{'Axioms/DAT001=0.ax'})$

$\forall u{:}\;\mbox{array},v{:}\;\mbox{array}{:}\;( ( \forall w{:}\;\mbox{\$int}{:}\;\mbox{\$greater}(\mbox{read}(v,w),w)\mbox{ and }u = \mbox{write}(\mbox{write}(v,3,5),7,9) ) \ \Rightarrow \ \forall x{:}\;\mbox{\$int}{:}\;\mbox{\$greater}(\mbox{read}(u,x),x) )\qquad\mbox{tff}(\mbox{co}_1,\mbox{conjecture})$

\medskip\textbf{DAT065=1.p} Add an element to an empty heap






$\mbox{include}(\mbox{'Axioms/DAT005=0.ax'})$

$\forall h_0{:}\;\mbox{heap},n{:}\;\mbox{\$int}{:}\;( \neg\,\mbox{length}(h_0) = 0\iff h_0 = \mbox{empty}\mbox{ or }( \mbox{length}(\mbox{app}(h_0,n)) = 0\iff \mbox{app}(h_0,n) = \mbox{empty} ) )\qquad\mbox{tff}(\mbox{th\_lem\_3a},\mbox{conjecture})$

\medskip
\end{document}