THM	discrete__Formula	Discrete{Formula}
THM	discrete__Formula_term	x.rec_ind(x;f,x1.case x1: x (y.case y: x4 case ext{decidable__equal_V ar} x x4 of inl(l) => inl Ax | inr(r) => inr (z.any (r Ax)) ; x4 (inr (z.Ax) ); x2x3 (inr (z.Ax) ); x2x3 (inr (z.Ax) ); y6y7 (inr (z.Ax) );); x (y.case y: x1 (inr (z.Ax) ); x1 case f x x1 of inl(l) => inl Ax | inr(r) => inr (z.any (r Ax)) ; x2x3 (inr (z.Ax) ); x2x3 (inr (z.Ax) ); y2y3 (inr (z.Ax) );); x1x2 (y.case y: x (inr (x.Ax) ); x (inr (z.Ax) ); x3x4 case f x1 x3 of inl(l) => case f x2 x4 of inl(l1) => inl Ax | inr(r) => inr  (z.any (r  Ax)) | inr(r) => inr (z.any (r Ax)) ; x3x4 (inr (%3.Ax) ); y2y3 (inr (%3.Ax) );); x1x2 (y.case y: x (inr (z.Ax) ); x (inr (z.Ax) ); x3x4 (inr (z.Ax) ); x3x4 case f x1 x3 of inl(l) => case f x2 x4 of inl(l1) => inl Ax | inr(r) => inr  (z.any (r  Ax)) | inr(r) => inr (z.any (r Ax)) ; y2y3 (inr (z.Ax) );); y2y3 (y.case y: x (inr (z.Ax) ); x (inr (z.Ax) ); x1x2 (inr (z.Ax) ); x1x2 (inr (z.Ax) ); y5y6 case f y2 y5 of inl(l) => case f y3 y6 of inl(l1) => in l Ax | inr(r) => inr (z.any (r  Ax)) | inr(r) => inr (z.any (r Ax)) ;); )
THM	discrete__Formula__with_rank	Discrete{Formula}
THM	discrete__Formula__with_rank_term	x.(%1.%1 ( x) x Ax) (x1.(%1.%1 (x1 + 1) x1 Ax) (zz.(%1.(%1.(%.(%2.%2 %1) I(%) where I() = when zzj = < 0, % = I(+1). %2.Ax when = 0. %,x1,%.(%1.Ax) x1 when zzj = > 0, % = I(-1). %2,x1,%@0. (%3,x,%. (%4.(%5.%5 %4) case x of inl(x2) => %,y. case y of inl(x3) => ( %1.case %1  of inl(%) => inl Ax  | inr(%2) => inr (%.any (%2  Ax)) ) (( %1.%1  x2  x3) ex t{decidable__equal_Var}) | inr(y2) => ca se y2 of inl(x3) => inr (%.(%1.Ax)  Ax) | inr(y3) => case y3  of inl(x3) => let <x4,x5> = x3  in  inr (%.(%1.Ax)  Ax)  | inr(y4) => case y4  of inl(x3) => let <x4,x5> = x3  in  inr (%.(%1.Ax)  Ax)  | inr(y5) => let <y6,y7> = y5  in  inr (%.(%1.Ax)  Ax) | inr(y) => case y of inl(x1) => %,y @0. cas e y@0 of  inl(x2) => inr (%1.(%2.Ax)  Ax) |  inr(y) => case y  of inl(x2) => case %  x1  Ax  x2  of inl(%) => inl Ax  | inr(%2) => inr (%.any (%2  Ax))  | inr(y1) => case y1  of inl(x2) => let <x3,x4> = x2  in  inr (%1.(%2.Ax)  Ax)  | inr(y) => case y  of inl(x2) => let <x3,x4> = x2  in  inr (%1.(%2.Ax)  Ax)  | inr(y1) => let <y2,y3> = y1  in  inr (%1.(%2.Ax)  Ax) | inr(y1) => case y1 of i nl(x1) => let <x2,x3> = x1  in  %.(%1,y@0.  case y@0  of inl(x4) => inr (%4.(%5.Ax)  Ax)  | inr(y) => case y  of inl(x4) => inr (%4.(%5.Ax)  Ax)  | inr(y1) => case y1  of inl(x4) => let <x5,x6> =  x4  in  case %1  x2  Ax  x5  of inl(%@0) => case %   x3   Ax   x6   of inl(%6) => inl Ax   | inr(%7) => inr (%8.any (%7   Ax))  | inr(%6) =>  inr (%.any (%6   Ax))  | inr(y) => case y  of inl(x4) => l et <x5,x6> = x4  i n  i nr (%4.(%5.Ax)   Ax)  | inr(y1) => l et <y2,y3> = y1  i n  i nr (%4.(%5.Ax)   Ax) )  % | i nr(y) => case y  of inl(x1) => let <x2,x3> = x1  in  %.(%1,y@0.  case y@0  of inl(x4) => inr (%4.(%5.Ax)  Ax)  | inr(y) => case y  of inl(x4) => inr (%4.(%5.A x)  Ax)  | inr(y1) => case y1  of inl(x4) => l et <x5,x6> = x4  i n  i nr (%4.(%5.Ax)   Ax)  | inr(y) => ca se y  of inl(x4) => let <x5,x6> = x4   in   case %1   x2   Ax   x5   of inl(%@0) => case %   x3   Ax   x6   of inl(%6) => inl Ax   | inr(%7) => inr (%8.any (%7   Ax))   | inr(%6) => inr (%.any (%6   Ax))  | inr(y1) => let <y2,y3> = y1   in   inr (%4.(%5.Ax)   Ax) )  %  | inr(y1) => let <y2,y3> = y1  in  %.(%1,y@0.  case y@0  of inl(x1) => inr (%4.(%5.Ax)  Ax)  | inr(y) => case y  of inl(x1) => inr (%4.(%5.A x)  Ax)  | inr(y3@0) => case y3@0  of inl(x1) => let <x2,x3> = x1   in   inr (%4.(%5.Ax)   Ax)  | inr(y) =>  case y   of inl(x1) => let <x2,x3> = x1   in   inr (%4.(%5.Ax)   Ax)   | inr(y3@0) => let <y4,y5> = y3@0   in   case %1   y2   Ax   y4   of inl(%@0) => case %   y3   Ax   y5   of inl(%6) => inl Ax   | inr(%7) => inr (%8.any (%7   Ax))   | inr(%6) => inr (%.any (%6   Ax)) )  %) (x2,%4.%3 ( x2) Ax x2 Ax)) (x2,%3.% (.Ax) x2 Ax) end where ) zz) (%1 zz)) ext{nat_properties}))
THM	decidable__equal_Formula	F,F':Formula. Dec(F = F')

the other theories