Twelf 1.5R3, Aug 30, 2005 (%trustme) %% OK %% [Opening file /home/www/twelf/hcode/8caf100c13b3177f77b521a6ab54362d] void : type. %freeze void. unit : type. unit/ : unit. %freeze unit. comp : type. less : comp. greater : comp. equal : comp. %freeze comp. bool : type. true : bool. false : bool. %freeze bool. eq : bool -> bool -> type. eq/ : {B:bool} eq B B. ne : bool -> bool -> type. ne/TF : ne true false. ne/FT : ne false true. eq? : bool -> bool -> bool -> type. eq?/yes : {B:bool} eq? B B true. eq?/no : {B1:bool} {B2:bool} ne B1 B2 -> eq? B1 B2 false. %theorem false-implies-eq : {X1:bool} {X2:bool} void -> eq X1 X2 -> type. %worlds () (false-implies-eq _ _). %total {} (false-implies-eq _ _). %theorem meta-eq : {X1:bool} {X2:bool} eq X1 X2 -> type. - : {X1:bool} meta-eq X1 X1 eq/. %worlds () (meta-eq _ _ _). %total {} (meta-eq _ _ _). %reduces X = Y (meta-eq X Y _). %theorem eq-reflexive : {X:bool} eq X X -> type. - : {X1:bool} eq-reflexive X1 eq/. %worlds () (eq-reflexive _ _). %total {} (eq-reflexive _ _). %theorem eq-symmetric : {X:bool} {Y:bool} eq X Y -> eq Y X -> type. - : {X1:bool} eq-symmetric eq/ eq/. %worlds () (eq-symmetric _ _). %total {} (eq-symmetric _ _). %theorem eq-transitive : {X:bool} {Y:bool} {Z:bool} eq X Y -> eq Y Z -> eq X Z -> type. - : {X1:bool} eq-transitive eq/ eq/ eq/. %worlds () (eq-transitive _ _ _). %total {} (eq-transitive _ _ _). %theorem false-implies-ne : {X1:bool} {X2:bool} void -> ne X1 X2 -> type. %worlds () (false-implies-ne _ _). %total {} (false-implies-ne _ _). %theorem ne-respects-eq : {X1:bool} {X2:bool} {Y1:bool} {Y2:bool} ne X1 X2 -> eq X1 Y1 -> eq X2 Y2 -> ne Y1 Y2 -> type. - : {X1:bool} {X2:bool} {X1<>X2:ne X1 X2} ne-respects-eq X1<>X2 eq/ eq/ X1<>X2. %worlds () (ne-respects-eq _ _ _ _). %total {} (ne-respects-eq _ _ _ _). %theorem ne-anti-reflexive : {B:bool} ne B B -> void -> type. %worlds () (ne-anti-reflexive _ _). %total {} (ne-anti-reflexive _ _). %theorem ne-symmetric : {B1:bool} {B2:bool} ne B1 B2 -> ne B2 B1 -> type. - : ne-symmetric ne/TF ne/FT. - : ne-symmetric ne/FT ne/TF. %worlds () (ne-symmetric _ _). %total {} (ne-symmetric _ _). %theorem eq-ne-implies-false : {B1:bool} {B2:bool} eq B1 B2 -> ne B1 B2 -> void -> type. %worlds () (eq-ne-implies-false _ _ _). %total {} (eq-ne-implies-false _ _ _). %theorem eq?-total* : {B1:bool} {B2:bool} {B:bool} eq? B1 B2 B -> type. - : eq?-total* true true true eq?/yes. - : eq?-total* false false true eq?/yes. - : eq?-total* true false false (eq?/no ne/TF). - : eq?-total* false true false (eq?/no ne/FT). %worlds () (eq?-total* _ _ _ _). %total {} (eq?-total* _ _ _ _). eq?-total : {X1:bool} {X2:bool} {X3:bool} eq? X1 X2 X3 -> type = [X1:bool] [X2:bool] [X3:bool] [EQ?:eq? X1 X2 X3] eq?-total* X1 X2 X3 EQ?. bool`bool : type = bool. bool`true : bool = true. bool`false : bool = false. bool`eq : bool -> bool -> type = [x:bool] [x1:bool] eq x x1. bool`eq/ : {X1:bool} eq X1 X1 = [X1:bool] eq/. bool`ne : bool -> bool -> type = [x:bool] [x1:bool] ne x x1. bool`ne/TF : ne true false = ne/TF. bool`ne/FT : ne false true = ne/FT. bool`eq? : bool -> bool -> bool -> type = [x:bool] [x1:bool] [x2:bool] eq? x x1 x2. bool`eq?/yes : {X1:bool} eq? X1 X1 true = [X1:bool] eq?/yes. bool`eq?/no : {X1:bool} {X2:bool} ne X1 X2 -> eq? X1 X2 false = [X1:bool] [X2:bool] [x:ne X1 X2] eq?/no x. bool`false-implies-eq : {X1:bool} {X2:bool} void -> eq X1 X2 -> type = [X1:bool] [X2:bool] [F:void] [E:eq X1 X2] false-implies-eq F E. bool`meta-eq : {X1:bool} {X2:bool} eq X1 X2 -> type = [X1:bool] [X2:bool] [E:eq X1 X2] meta-eq X1 X2 E. bool`eq-reflexive : {X:bool} eq X X -> type = [X:bool] [E:eq X X] eq-reflexive X E. bool`eq-symmetric : {X1:bool} {X2:bool} eq X1 X2 -> eq X2 X1 -> type = [X1:bool] [X2:bool] [E:eq X1 X2] [F:eq X2 X1] eq-symmetric E F. bool`eq-transitive : {X1:bool} {X2:bool} {X3:bool} eq X1 X2 -> eq X2 X3 -> eq X1 X3 -> type = [X1:bool] [X2:bool] [X3:bool] [E1:eq X1 X2] [E2:eq X2 X3] [F:eq X1 X3] eq-transitive E1 E2 F. bool`false-implies-ne : {X1:bool} {X2:bool} void -> ne X1 X2 -> type = [X1:bool] [X2:bool] [F:void] [G:ne X1 X2] false-implies-ne F G. bool`ne-respects-eq : {X1:bool} {X2:bool} {X3:bool} {X4:bool} ne X1 X2 -> eq X1 X3 -> eq X2 X4 -> ne X3 X4 -> type = [X1:bool] [X2:bool] [X3:bool] [X4:bool] [D1:ne X1 X2] [E1:eq X1 X3] [E2:eq X2 X4] [D2:ne X3 X4] ne-respects-eq D1 E1 E2 D2. bool`ne-anti-reflexive : {X1:bool} ne X1 X1 -> void -> type = [X1:bool] [R:ne X1 X1] [F:void] ne-anti-reflexive R F. bool`ne-symmetric : {X1:bool} {X2:bool} ne X1 X2 -> ne X2 X1 -> type = [X1:bool] [X2:bool] [R1:ne X1 X2] [R2:ne X2 X1] ne-symmetric R1 R2. bool`eq-ne-implies-false : {X1:bool} {X2:bool} eq X1 X2 -> ne X1 X2 -> void -> type = [X1:bool] [X2:bool] [D1:eq X1 X2] [D2:ne X1 X2] [F:void] eq-ne-implies-false D1 D2 F. bool`eq?-total* : {B1:bool} {B2:bool} {B:bool} eq? B1 B2 B -> type = [B1:bool] [B2:bool] [B:bool] [EQ?:eq? B1 B2 B] eq?-total* B1 B2 B EQ?. bool`eq?-total : {X1:bool} {X2:bool} {X3:bool} eq? X1 X2 X3 -> type = [X1:bool] [X2:bool] [X3:bool] [EQ?:eq? X1 X2 X3] eq?-total* X1 X2 X3 EQ?. nat : type. z : nat. s : nat -> nat. %freeze nat. plus : nat -> nat -> nat -> type. plus/z : {Y:nat} plus z Y Y. plus/s : {X:nat} {Y:nat} {Z:nat} plus X Y Z -> plus (s X) Y (s Z). times : nat -> nat -> nat -> type. times/z : {X:nat} times z X z. times/s : {X:nat} {Y:nat} {T:nat} {Z:nat} times X Y T -> plus T Y Z -> times (s X) Y Z. eq : nat -> nat -> type. eq/ : {N:nat} eq N N. gt : nat -> nat -> type. gt/1 : {M:nat} gt (s M) M. gt/> : {M:nat} {N:nat} gt M N -> gt (s M) N. compare : nat -> nat -> comp -> type. compare/= : {N:nat} compare N N equal. compare/< : {N:nat} {M:nat} gt N M -> compare M N less. compare/> : {M:nat} {N:nat} gt M N -> compare M N greater. %reduces X = Y (eq X Y). %theorem meta-eq : {M:nat} {N:nat} eq M N -> type. - : {N:nat} meta-eq N N eq/. %worlds () (meta-eq _ _ _). %total {} (meta-eq _ _ _). %reduces X = Y (meta-eq X Y _). %theorem false-implies-eq : {M:nat} {N:nat} void -> eq M N -> type. %worlds () (false-implies-eq _ M=N). %total {} (false-implies-eq _ _). %theorem eq-symmetric : {M:nat} {N:nat} eq M N -> eq N M -> type. - : {N1:nat} eq-symmetric eq/ eq/. %worlds () (eq-symmetric M>N N>M). %total {} (eq-symmetric _ _). %theorem eq-transitive : {M:nat} {N:nat} {P:nat} eq M N -> eq N P -> eq M P -> type. - : {N1:nat} eq-transitive eq/ eq/ eq/. %worlds () (eq-transitive M>N N>P M>P). %total {} (eq-transitive _ _ _). %theorem succ-deterministic : {N1:nat} {N2:nat} eq N1 N2 -> eq (s N1) (s N2) -> type. - : {N1:nat} succ-deterministic eq/ eq/. %worlds () (succ-deterministic N1=N2 N1+1=N2+1). %total {} (succ-deterministic E _). %theorem succ-cancels : {N1:nat} {N2:nat} eq (s N1) (s N2) -> eq N1 N2 -> type. - : {N1:nat} succ-cancels eq/ eq/. %worlds () (succ-cancels N1+1=N2+1 N1=N2). %total {} (succ-cancels E _). %theorem eq-contradiction : {N:nat} eq z (s N) -> void -> type. %worlds () (eq-contradiction ZERO=N+1 _). %total {} (eq-contradiction _ _). %reduces M < N (gt N M). %theorem meta-gt : {M:nat} {N:nat} gt M N -> type. - : {M:nat} meta-gt (s M) M gt/1. - : {M:nat} {N:nat} {G:gt M N} meta-gt M N G -> meta-gt (s M) N (gt/> G). %worlds () (meta-gt _ _ _). %total M (meta-gt M _ _). %reduces M < N (meta-gt N M _). %theorem false-implies-gt : {M:nat} {N:nat} void -> gt M N -> type. %worlds () (false-implies-gt _ M>N). %total {} (false-implies-gt _ _). %theorem gt-respects-eq : {M1:nat} {M2:nat} {N1:nat} {N2:nat} gt M1 N1 -> eq M1 M2 -> eq N1 N2 -> gt M2 N2 -> type. - : {N1:nat} {N2:nat} {M1>N1:gt N1 N2} gt-respects-eq M1>N1 eq/ eq/ M1>N1. %worlds () (gt-respects-eq M1>N1 M1=M2 N1=N2 M2>N2). %total {} (gt-respects-eq _ _ _ _). %theorem succ-implies-gt : {X:nat} {X':nat} eq X (s X') -> gt X X' -> type. - : {N1:nat} succ-implies-gt eq/ gt/1. %worlds () (succ-implies-gt X=sX' X>X'). %total {} (succ-implies-gt _ _). %theorem succ-implies-gt-zero : {M:nat} gt (s M) z -> type. - : succ-implies-gt-zero z gt/1. - : {M:nat} {SM>0:gt (s M) z} succ-implies-gt-zero M SM>0 -> succ-implies-gt-zero (s M) (gt/> SM>0). %worlds () (succ-implies-gt-zero M SM>0). %total M (succ-implies-gt-zero M _). %theorem succ-preserves-gt : {M:nat} {N:nat} gt M N -> gt (s M) (s N) -> type. - : {N1:nat} succ-preserves-gt gt/1 gt/1. - : {N1:nat} {N2:nat} {M>N:gt N1 N2} {SM>SN:gt (s N1) (s N2)} succ-preserves-gt M>N SM>SN -> succ-preserves-gt (gt/> M>N) (gt/> SM>SN). %worlds () (succ-preserves-gt M>N SM>SN). %total G1 (succ-preserves-gt G1 _). %theorem succ-preserves-gt-converse : {M:nat} {N:nat} gt (s M) (s N) -> gt M N -> type. - : {N1:nat} succ-preserves-gt-converse gt/1 gt/1. - : {N1:nat} {N2:nat} {SM>SN:gt (s N1) (s N2)} {M>N:gt N1 N2} succ-preserves-gt-converse SM>SN M>N -> succ-preserves-gt-converse (gt/> SM>SN) (gt/> M>N). %worlds () (succ-preserves-gt-converse SM>SN M>N). %total G1 (succ-preserves-gt-converse G1 _). %theorem gt-implies-positive : {M:nat} {N:nat} gt M N -> ({M':nat} eq M (s M') -> type). - : {M:nat} gt-implies-positive gt/1 M eq/. - : {M:nat} {N:nat} {G:gt M N} gt-implies-positive (gt/> G) M eq/. %worlds () (gt-implies-positive M>N M' M=sM'). %total {} (gt-implies-positive _ _ _). %theorem gt-anti-reflexive* : {M:nat} gt M M -> void -> type. - : {M:nat} {G':gt M M} {F:void} {G:gt (s M) (s M)} gt-anti-reflexive* M G' F -> succ-preserves-gt-converse G G' -> gt-anti-reflexive* (s M) G F. %worlds () (gt-anti-reflexive* M M>M _). %total M (gt-anti-reflexive* M _ _). gt-anti-reflexive : {N1:nat} gt N1 N1 -> void -> type = [N1:nat] [G:gt N1 N1] [F:void] gt-anti-reflexive* N1 G F. %theorem gt-transitive : {M:nat} {N:nat} {P:nat} gt M N -> gt N P -> gt M P -> type. - : {N1:nat} {N2:nat} {G:gt N1 N2} gt-transitive gt/1 G (gt/> G). - : {N1:nat} {N2:nat} {N3:nat} {M>N:gt N1 N2} {N>P:gt N2 N3} {M>P:gt N1 N3} gt-transitive M>N N>P M>P -> gt-transitive (gt/> M>N) N>P (gt/> M>P). %worlds () (gt-transitive M>N N>P M>P). %total G1 (gt-transitive G1 _ _). %theorem gt-anti-symmetric : {M:nat} {N:nat} gt M N -> gt N M -> void -> type. - : {N1:nat} {M>M:gt N1 N1} {F:void} {N2:nat} {M>N:gt N1 N2} {N>M:gt N2 N1} gt-anti-reflexive* N1 M>M F -> gt-transitive M>N N>M M>M -> gt-anti-symmetric M>N N>M F. %worlds () (gt-anti-symmetric M>N N>M _). %total {} (gt-anti-symmetric _ _ _). %theorem gt-implies-plus : {M:nat} {N:nat} gt M N -> ({D:nat} plus (s D) N M -> type). - : {N1:nat} gt-implies-plus gt/1 z (plus/s plus/z). - : {N1:nat} {N2:nat} {M>N:gt N1 N2} {D:nat} {SD+N=M:plus (s D) N2 N1} gt-implies-plus M>N D SD+N=M -> gt-implies-plus (gt/> M>N) (s D) (plus/s SD+N=M). %worlds () (gt-implies-plus M>N D SD+N=M). %total G (gt-implies-plus G _ _). %theorem gt-contradiction : {M:nat} gt z M -> void -> type. %worlds () (gt-contradiction ZERO>N _). %total {} (gt-contradiction _ _). %theorem false-implies-compare : {M:nat} {N:nat} {C:comp} void -> compare M N C -> type. %worlds () (false-implies-compare _ _). %total {} (false-implies-compare _ _). %theorem succ-preserves-compare : {M:nat} {N:nat} {C:comp} compare M N C -> compare (s M) (s N) C -> type. - : {N1:nat} succ-preserves-compare compare/= compare/=. - : {N1:nat} {N2:nat} {M>N:gt N1 N2} {M+1>N+1:gt (s N1) (s N2)} succ-preserves-gt M>N M+1>N+1 -> succ-preserves-compare (compare/< M>N) (compare/< M+1>N+1). - : {N1:nat} {N2:nat} {M>N:gt N1 N2} {M+1>N+1:gt (s N1) (s N2)} succ-preserves-gt M>N M+1>N+1 -> succ-preserves-compare (compare/> M>N) (compare/> M+1>N+1). %worlds () (succ-preserves-compare _ _). %total {} (succ-preserves-compare _ _). %theorem compare-total* : {M:nat} {N:nat} {CMP:comp} compare M N CMP -> type. - : compare-total* z z equal compare/=. - : {M:nat} {M+1>0:gt (s M) z} succ-implies-gt-zero M M+1>0 -> compare-total* z (s M) less (compare/< M+1>0). - : {M:nat} {M+1>0:gt (s M) z} succ-implies-gt-zero M M+1>0 -> compare-total* (s M) z greater (compare/> M+1>0). - : {M:nat} {N:nat} {R:comp} {M-R-N:compare M N R} {M+1-R-N+1:compare (s M) (s N) R} succ-preserves-compare M-R-N M+1-R-N+1 -> compare-total* M N R M-R-N -> compare-total* (s M) (s N) R M+1-R-N+1. %worlds () (compare-total* _ _ _ _). %total M (compare-total* M _ _ _). compare-total : {N1:nat} {N2:nat} {X1:comp} compare N1 N2 X1 -> type = [N1:nat] [N2:nat] [X1:comp] [P:compare N1 N2 X1] compare-total* N1 N2 X1 P. %theorem greater-implies-gt : {M:nat} {N:nat} compare M N greater -> gt M N -> type. - : {N1:nat} {N2:nat} {G:gt N1 N2} greater-implies-gt (compare/> G) G. %worlds () (greater-implies-gt M>N M-gt-N). %total C (greater-implies-gt C _). %theorem less-is-reverse-greater : {M:nat} {N:nat} compare M N less -> compare N M greater -> type. - : {N1:nat} {N2:nat} {G:gt N2 N1} less-is-reverse-greater (compare/< G) (compare/> G). %worlds () (less-is-reverse-greater MM). %total C (less-is-reverse-greater C _). %theorem less-implies-lt : {M:nat} {N:nat} compare M N less -> gt N M -> type. - : {N1:nat} {N2:nat} {G:gt N2 N1} less-implies-lt (compare/< G) G. %worlds () (less-implies-lt M eq M N -> type. - : {N1:nat} equal-implies-eq compare/= eq/. %worlds () (equal-implies-eq M=N M-eq-N). %total C (equal-implies-eq C _). %theorem false-implies-plus : {M:nat} {N:nat} {O:nat} void -> plus M N O -> type. %worlds () (false-implies-plus _ _). %total {} (false-implies-plus _ _). %theorem plus-respects-eq : {M1:nat} {M2:nat} {N1:nat} {N2:nat} {P1:nat} {P2:nat} plus M1 N1 P1 -> eq M1 M2 -> eq N1 N2 -> eq P1 P2 -> plus M2 N2 P2 -> type. - : {N1:nat} {N2:nat} {N3:nat} {M1+N1=P1:plus N1 N2 N3} plus-respects-eq M1+N1=P1 eq/ eq/ eq/ M1+N1=P1. %worlds () (plus-respects-eq M1+N1=P1 M1=M2 N1=N2 P1=P2 M2+N2=P2). %total {} (plus-respects-eq _ _ _ _ _). %theorem plus-total* : {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> type. - : {N1:nat} plus-total* z N1 N1 plus/z. - : {N1':nat} {N2:nat} {N3:nat} {P:plus N1' N2 N3} plus-total* N1' N2 N3 P -> plus-total* (s N1') N2 (s N3) (plus/s P). %worlds () (plus-total* N1 N2 N3 N1+N2=N3). %total N1 (plus-total* N1 _ _ _). plus-total : {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> type = [N1:nat] [N2:nat] [N3:nat] [P:plus N1 N2 N3] plus-total* N1 N2 N3 P. %theorem plus-deterministic : {N1:nat} {N1':nat} {N2:nat} {N2':nat} {N3:nat} {N3':nat} plus N1 N2 N3 -> plus N1' N2' N3' -> eq N1 N1' -> eq N2 N2' -> eq N3 N3' -> type. - : {N1:nat} plus-deterministic plus/z plus/z eq/ eq/ eq/. - : {N3:nat} {N3':nat} {E':eq N3 N3'} {E:eq (s N3) (s N3')} {N1:nat} {N1':nat} {N2:nat} {N2':nat} {P:plus N1 N2 N3} {P':plus N1' N2' N3'} {E1':eq N1 N1'} {E2:eq N2 N2'} {E1:eq (s N1) (s N1')} succ-deterministic E' E -> plus-deterministic P P' E1' E2 E' -> succ-cancels E1 E1' -> plus-deterministic (plus/s P) (plus/s P') E1 E2 E. %worlds () (plus-deterministic _ _ _ _ _). %total P (plus-deterministic P _ _ _ _). %theorem plus-left-identity : {N:nat} plus z N N -> type. - : {N:nat} plus-left-identity N plus/z. %worlds () (plus-left-identity N Z+N=N). %total {} (plus-left-identity _ _). %theorem plus-left-increase : {M:nat} {N:nat} {O:nat} plus M N O -> plus (s M) N (s O) -> type. - : {N1:nat} {N2:nat} {N3:nat} {P:plus N1 N2 N3} plus-left-increase P (plus/s P). %worlds () (plus-left-increase M+N=O SM+N=sO). %total {} (plus-left-increase _ _). %theorem plus-right-identity : {N:nat} plus N z N -> type. - : plus-right-identity z plus/z. - : {N:nat} {N+0=N:plus N z N} plus-right-identity N N+0=N -> plus-right-identity (s N) (plus/s N+0=N). %worlds () (plus-right-identity N N+0=N). %total N (plus-right-identity N _). %theorem plus-right-increase : {M:nat} {N:nat} {O:nat} plus M N O -> plus M (s N) (s O) -> type. - : {N1:nat} plus-right-increase plus/z plus/z. - : {N1:nat} {N2:nat} {N3:nat} {M+N=O:plus N1 N2 N3} {M+sN=sO:plus N1 (s N2) (s N3)} plus-right-increase M+N=O M+sN=sO -> plus-right-increase (plus/s M+N=O) (plus/s M+sN=sO). %worlds () (plus-right-increase M+N=O M+sN=sO). %total P (plus-right-increase P _). %theorem plus-left-decrease : {M:nat} {N:nat} {O':nat} plus (s M) N O' -> ({O:nat} eq O' (s O) -> plus M N O -> type). - : {N1:nat} {N2:nat} {O:nat} {M+N=O:plus N1 N2 O} plus-left-decrease (plus/s M+N=O) O eq/ M+N=O. %worlds () (plus-left-decrease SM+N=O' O O'=sO M+N=O). %total {} (plus-left-decrease _ _ _ _). %theorem plus-right-decrease : {M:nat} {N:nat} {O':nat} plus M (s N) O' -> ({O:nat} eq O' (s O) -> plus M N O -> type). - : {N:nat} plus-right-decrease plus/z N eq/ plus/z. - : {M:nat} {N:nat} {O:nat} {X:nat} {X=O:eq X O} {O=X:eq O X} {O':nat} {O=sO':eq O (s O')} {SO'=X:eq (s O') X} {M+N=O':plus M N O'} {M+sN=O:plus M (s N) O} {sM+N=O:plus (s M) N O} {sM+N=X:plus (s M) N X} plus-respects-eq sM+N=X eq/ eq/ X=O sM+N=O -> eq-symmetric O=X X=O -> eq-transitive O=sO' SO'=X O=X -> plus-deterministic (plus/s M+N=O') sM+N=X eq/ eq/ SO'=X -> plus-total* (s M) N X sM+N=X -> plus-right-decrease M+sN=O O' O=sO' M+N=O' -> plus-right-decrease (plus/s M+sN=O) O eq/ sM+N=O. %worlds () (plus-right-decrease M+sN=O' O O'=sO M+N=O). %total P (plus-right-decrease P _ _ _). %theorem plus-swap-succ : {N1:nat} {N2:nat} {N3:nat} plus (s N1) N2 N3 -> plus N1 (s N2) N3 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N1+N2=N3-:plus N1 N2 N3} {N1+sN2=N3:plus N1 (s N2) (s N3)} plus-right-increase N1+N2=N3- N1+sN2=N3 -> plus-swap-succ (plus/s N1+N2=N3-) N1+sN2=N3. %worlds () (plus-swap-succ SN1+N2=N3 N1+sN2=N3). %total {} (plus-swap-succ _ _). %theorem plus-swap-succ-converse : {N1:nat} {N2:nat} {N3:nat} plus N1 (s N2) N3 -> plus (s N1) N2 N3 -> type. - : {N1:nat} {N2:nat} {N3-:nat} {N3:nat} {N1+N2=N3-:plus N1 N2 N3-} {SN3-=N3:eq (s N3-) N3} {SN1+N2=N3:plus (s N1) N2 N3} {N3=sN3-:eq N3 (s N3-)} {N1+sN2=N3:plus N1 (s N2) N3} plus-respects-eq (plus/s N1+N2=N3-) eq/ eq/ SN3-=N3 SN1+N2=N3 -> eq-symmetric N3=sN3- SN3-=N3 -> plus-right-decrease N1+sN2=N3 N3- N3=sN3- N1+N2=N3- -> plus-swap-succ-converse N1+sN2=N3 SN1+N2=N3. %worlds () (plus-swap-succ-converse N1+sN2=N3 SN1+N2=N3). %total {} (plus-swap-succ-converse _ _). %theorem plus-left-preserves-positive : {N1:nat} {N2:nat} {N3:nat} {N1-:nat} plus N1 N2 N3 -> eq N1 (s N1-) -> ({N3-:nat} eq N3 (s N3-) -> type). - : {N1:nat} {N2:nat} {N3:nat} {N1-+N2=N3-:plus N1 N2 N3} plus-left-preserves-positive (plus/s N1-+N2=N3-) eq/ N3 eq/. %worlds () (plus-left-preserves-positive N1+N2=N3 N1=sN1- N3- N3=sN3-). %total {} (plus-left-preserves-positive _ _ _ _). %theorem plus-right-preserves-positive : {N1:nat} {N2:nat} {N3:nat} {N2-:nat} plus N1 N2 N3 -> eq N2 (s N2-) -> ({N3-:nat} eq N3 (s N3-) -> type). - : {N1:nat} {N2:nat} {N3:nat} {N1+sN2-=N3:plus N1 (s N2) N3} {N3-:nat} {N3=sN3-:eq N3 (s N3-)} {X1:plus N1 N2 N3-} {N4:nat} {N1+N2=N3:plus N1 N4 N3} {N2=sN2-:eq N4 (s N2)} plus-right-decrease N1+sN2-=N3 N3- N3=sN3- X1 -> plus-respects-eq N1+N2=N3 eq/ N2=sN2- eq/ N1+sN2-=N3 -> plus-right-preserves-positive N1+N2=N3 N2=sN2- N3- N3=sN3-. %worlds () (plus-right-preserves-positive N1+N2=N3 N2+ N3- N3+). %total {} (plus-right-preserves-positive _ _ _ _). %theorem plus-is-zero-implies-zero : {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> eq N3 z -> eq N1 z -> eq N2 z -> type. - : plus-is-zero-implies-zero plus/z eq/ eq/ eq/. %worlds () (plus-is-zero-implies-zero X+Y=Z Z=0 X=0 Y=0). %total {} (plus-is-zero-implies-zero _ _ _ _). %theorem plus-commutative : {N1:nat} {N2:nat} {N12:nat} plus N1 N2 N12 -> plus N2 N1 N12 -> type. - : {N2:nat} {N2+z=N2:plus N2 z N2} plus-right-identity N2 N2+z=N2 -> plus-commutative plus/z N2+z=N2. - : {N1:nat} {N2:nat} {N3:nat} {N2+N1=N3:plus N1 N2 N3} {N2+sN1=sN3:plus N1 (s N2) (s N3)} {N1+N2=N3:plus N2 N1 N3} plus-right-increase N2+N1=N3 N2+sN1=sN3 -> plus-commutative N1+N2=N3 N2+N1=N3 -> plus-commutative (plus/s N1+N2=N3) N2+sN1=sN3. %worlds () (plus-commutative N1+N2=N3 N2+N1=N3). %total P (plus-commutative P _). %theorem plus-associative : {X:nat} {Y:nat} {Z:nat} {X':nat} {Z':nat} plus X Y X' -> plus X' Z Z' -> ({Y':nat} plus Y Z Y' -> plus X Y' Z' -> type). - : {N2:nat} {N3:nat} {N23:nat} {P2:plus N2 N3 N23} plus-associative plus/z P2 N23 P2 plus/z. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N1+N2=N12:plus N1 N2 N4} {N12+N3=N123:plus N4 N3 N5} {N23:nat} {N2+N3=N23:plus N2 N3 N23} {N1+N23=N123:plus N1 N23 N5} plus-associative N1+N2=N12 N12+N3=N123 N23 N2+N3=N23 N1+N23=N123 -> plus-associative (plus/s N1+N2=N12) (plus/s N12+N3=N123) N23 N2+N3=N23 (plus/s N1+N23=N123). %worlds () (plus-associative _ _ _ _ _). %total P1 (plus-associative P1 _ _ _ _). %theorem plus-associative* : {X1:nat} {X2:nat} {X12:nat} {X3:nat} {X23:nat} {X123:nat} plus X1 X2 X12 -> plus X12 X3 X123 -> plus X2 X3 X23 -> plus X1 X23 X123 -> type. - : {N1:nat} {Y6:nat} {N2:nat} {N3:nat} {X1+Y6=X7:plus N1 Y6 N3} {Y6=X6:eq Y6 N2} {X1+X6=X7:plus N1 N2 N3} {N4:nat} {N5:nat} {X2+X4=Y6:plus N4 N5 Y6} {X2+X4=X6:plus N4 N5 N2} {N6:nat} {X1+X2=X3:plus N1 N4 N6} {X3+X4=X7:plus N6 N5 N3} plus-respects-eq X1+Y6=X7 eq/ Y6=X6 eq/ X1+X6=X7 -> plus-deterministic X2+X4=Y6 X2+X4=X6 eq/ eq/ Y6=X6 -> plus-associative X1+X2=X3 X3+X4=X7 Y6 X2+X4=Y6 X1+Y6=X7 -> plus-associative* X1+X2=X3 X3+X4=X7 X2+X4=X6 X1+X6=X7. %worlds () (plus-associative* _ _ _ _). %total {} (plus-associative* _ _ _ _). %theorem plus-associative-converse : {X1:nat} {X2:nat} {X4:nat} {X6:nat} {X7:nat} plus X2 X4 X6 -> plus X1 X6 X7 -> ({X3:nat} plus X1 X2 X3 -> plus X3 X4 X7 -> type). - : {N1:nat} {N2:nat} {N3:nat} {X4+X3=X7:plus N1 N2 N3} {X3+X4=X7:plus N2 N1 N3} {N4:nat} {N5:nat} {X2+X1=X3:plus N4 N5 N2} {X1+X2=X3:plus N5 N4 N2} {N6:nat} {X4+X2=X6:plus N1 N4 N6} {X6+X1=X7:plus N6 N5 N3} {X1+X6=X7:plus N5 N6 N3} {X2+X4=X6:plus N4 N1 N6} plus-commutative X4+X3=X7 X3+X4=X7 -> plus-commutative X2+X1=X3 X1+X2=X3 -> plus-associative X4+X2=X6 X6+X1=X7 N2 X2+X1=X3 X4+X3=X7 -> plus-commutative X1+X6=X7 X6+X1=X7 -> plus-commutative X2+X4=X6 X4+X2=X6 -> plus-associative-converse X2+X4=X6 X1+X6=X7 N2 X1+X2=X3 X3+X4=X7. %worlds () (plus-associative-converse X2+X4=X6 X1+X6=X7 X3 X1+X2=X3 X3+X4=X7). %total {} (plus-associative-converse _ _ _ _ _). %theorem plus-associative-converse* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X6:nat} {X7:nat} plus X2 X4 X6 -> plus X1 X6 X7 -> plus X1 X2 X3 -> plus X3 X4 X7 -> type. - : {X3P:nat} {N1:nat} {N2:nat} {N3:nat} {X3P+X4=X7:plus X3P N2 N3} {X3P=X3:eq X3P N1} {X3+X4=X7:plus N1 N2 N3} {N4:nat} {N5:nat} {X1+X2=X3P:plus N4 N5 X3P} {X1+X2=X3:plus N4 N5 N1} {N6:nat} {X2+X4=X6:plus N5 N2 N6} {X1+X6=X7:plus N4 N6 N3} plus-respects-eq X3P+X4=X7 X3P=X3 eq/ eq/ X3+X4=X7 -> plus-deterministic X1+X2=X3P X1+X2=X3 eq/ eq/ X3P=X3 -> plus-associative-converse X2+X4=X6 X1+X6=X7 X3P X1+X2=X3P X3P+X4=X7 -> plus-associative-converse* X2+X4=X6 X1+X6=X7 X1+X2=X3 X3+X4=X7. %worlds () (plus-associative-converse* X2+X4=X6 X1+X6=X7 X1+X2=X3 X3+X4=X7). %total {} (plus-associative-converse* _ _ _ _). %theorem plus-assoc-commutative* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X7:nat} plus X1 X2 X3 -> plus X3 X4 X7 -> plus X1 X4 X5 -> plus X5 X2 X7 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {X6:nat} {N5:nat} {X4+X2=X6:plus N2 N4 X6} {X1+X6=X7:plus N1 X6 N5} {X1+X4=X5:plus N1 N2 N3} {X5+X2=X7:plus N3 N4 N5} {X2+X4=X6:plus N4 N2 X6} {N6:nat} {X1+X2=X3:plus N1 N4 N6} {X3+X4=X7:plus N6 N2 N5} plus-associative-converse* X4+X2=X6 X1+X6=X7 X1+X4=X5 X5+X2=X7 -> plus-commutative X2+X4=X6 X4+X2=X6 -> plus-associative X1+X2=X3 X3+X4=X7 X6 X2+X4=X6 X1+X6=X7 -> plus-assoc-commutative* X1+X2=X3 X3+X4=X7 X1+X4=X5 X5+X2=X7. %worlds () (plus-assoc-commutative* X1+X2=X3 X3+X4=X7 X1+X4=X5 X5+X2=X7). %total {} (plus-assoc-commutative* _ _ _ _). %theorem plus-assoc-commutative : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X7:nat} plus X1 X2 X3 -> plus X3 X4 X7 -> ({X5:nat} plus X1 X4 X5 -> plus X5 X2 X7 -> type). - : {N1:nat} {N2:nat} {N3:nat} {X6:nat} {N4:nat} {X4+X2=X6:plus N2 N3 X6} {X1+X6=X7:plus N1 X6 N4} {X5:nat} {X1+X4=X5:plus N1 N2 X5} {X5+X2=X7:plus X5 N3 N4} {X2+X4=X6:plus N3 N2 X6} {N5:nat} {X1+X2=X3:plus N1 N3 N5} {X3+X4=X7:plus N5 N2 N4} plus-associative-converse X4+X2=X6 X1+X6=X7 X5 X1+X4=X5 X5+X2=X7 -> plus-commutative X2+X4=X6 X4+X2=X6 -> plus-associative X1+X2=X3 X3+X4=X7 X6 X2+X4=X6 X1+X6=X7 -> plus-assoc-commutative X1+X2=X3 X3+X4=X7 X5 X1+X4=X5 X5+X2=X7. %worlds () (plus-assoc-commutative X1+X2=X3 X3+X4=X7 X5 X1+X4=X5 X5+X2=X7). %total {} (plus-assoc-commutative _ _ _ _ _). %theorem plus-double-associative* : {A:nat} {B:nat} {C:nat} {D:nat} {A+B:nat} {C+D:nat} {A+C:nat} {B+D:nat} {X:nat} plus A B A+B -> plus C D C+D -> plus A+B C+D X -> plus A C A+C -> plus B D B+D -> plus A+C B+D X -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {XE:nat} {N5:nat} {X4+XA=XE:plus N2 N4 XE} {X1+XE=XF:plus N1 XE N5} {X1+X4=X5:plus N1 N2 N3} {X5+XA=XF:plus N3 N4 N5} {XA+X4=XE:plus N4 N2 XE} {N6:nat} {N7:nat} {N8:nat} {X8+X4=XC:plus N7 N2 N8} {X2+XC=XE:plus N6 N8 XE} {X2+X8=XA:plus N6 N7 N4} {X4+X8=XC:plus N2 N7 N8} {N9:nat} {X1+X2=X3:plus N1 N6 N9} {X3+XC=XF:plus N9 N8 N5} plus-associative-converse* X4+XA=XE X1+XE=XF X1+X4=X5 X5+XA=XF -> plus-commutative XA+X4=XE X4+XA=XE -> plus-associative-converse* X8+X4=XC X2+XC=XE X2+X8=XA XA+X4=XE -> plus-commutative X4+X8=XC X8+X4=XC -> plus-associative X1+X2=X3 X3+XC=XF XE X2+XC=XE X1+XE=XF -> plus-double-associative* X1+X2=X3 X4+X8=XC X3+XC=XF X1+X4=X5 X2+X8=XA X5+XA=XF. %worlds () (plus-double-associative* X1+X2=X3 X4+X8=XC X3+XC=XF X1+X4=X5 X2+X8=XA X5+XA=XF). %total {} (plus-double-associative* _ _ _ _ _ _). %theorem plus-double-associative : {A:nat} {B:nat} {C:nat} {D:nat} {A+B:nat} {C+D:nat} {X:nat} plus A B A+B -> plus C D C+D -> plus A+B C+D X -> ({A+C:nat} {B+D:nat} plus A C A+C -> plus B D B+D -> plus A+C B+D X -> type). - : {N1:nat} {N2:nat} {XA:nat} {XE:nat} {N3:nat} {X4+XA=XE:plus N2 XA XE} {X1+XE=XF:plus N1 XE N3} {X5:nat} {X1+X4=X5:plus N1 N2 X5} {X5+XA=XF:plus X5 XA N3} {XA+X4=XE:plus XA N2 XE} {N4:nat} {N5:nat} {N6:nat} {X8+X4=XC:plus N5 N2 N6} {X2+XC=XE:plus N4 N6 XE} {X2+X8=XA:plus N4 N5 XA} {X4+X8=XC:plus N2 N5 N6} {N7:nat} {X1+X2=X3:plus N1 N4 N7} {X3+XC=XF:plus N7 N6 N3} plus-associative-converse X4+XA=XE X1+XE=XF X5 X1+X4=X5 X5+XA=XF -> plus-commutative XA+X4=XE X4+XA=XE -> plus-associative-converse X8+X4=XC X2+XC=XE XA X2+X8=XA XA+X4=XE -> plus-commutative X4+X8=XC X8+X4=XC -> plus-associative X1+X2=X3 X3+XC=XF XE X2+XC=XE X1+XE=XF -> plus-double-associative X1+X2=X3 X4+X8=XC X3+XC=XF X5 XA X1+X4=X5 X2+X8=XA X5+XA=XF. %worlds () (plus-double-associative _ _ _ _ _ _ _ _). %total {} (plus-double-associative _ _ _ _ _ _ _ _). %theorem plus-left-cancels : {X1:nat} {X2:nat} {Y:nat} {Z:nat} {S1:nat} {S2:nat} plus X1 Y S1 -> plus X2 Z S2 -> eq X1 X2 -> eq S1 S2 -> eq Y Z -> type. - : {N1:nat} plus-left-cancels plus/z plus/z eq/ eq/ eq/. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {X+Y1=Z:plus N1 N2 N4} {X+Y2=Z:plus N1 N3 N4} {Y1=Y2:eq N2 N3} plus-left-cancels X+Y1=Z X+Y2=Z eq/ eq/ Y1=Y2 -> plus-left-cancels (plus/s X+Y1=Z) (plus/s X+Y2=Z) eq/ eq/ Y1=Y2. %worlds () (plus-left-cancels X1+Y1=Z1 X2+Y2=Z2 X1=X2 Z1=Z2 Y1=Y2). %total P1 (plus-left-cancels P1 _ _ _ _). %theorem plus-right-cancels* : {X:nat} {Y:nat} {Z1:nat} {Z2:nat} {S1:nat} {S2:nat} plus X Z1 S1 -> plus Y Z2 S2 -> eq Z1 Z2 -> eq S1 S2 -> eq X Y -> type. - : {X1:nat} {Z:nat} {X2:nat} {X1=Z:eq X1 Z} {Z=X2:eq Z X2} {X1=X2:eq X1 X2} {X2=Z:eq X2 Z} {X2+0=X2:plus X2 z X2} {X2+0=Z:plus X2 z Z} {X1+0=X1:plus X1 z X1} {X1+0=Z:plus X1 z Z} eq-transitive X1=Z Z=X2 X1=X2 -> eq-symmetric X2=Z Z=X2 -> plus-deterministic X2+0=X2 X2+0=Z eq/ eq/ X2=Z -> plus-right-identity X2 X2+0=X2 -> plus-deterministic X1+0=X1 X1+0=Z eq/ eq/ X1=Z -> plus-right-identity X1 X1+0=X1 -> plus-right-cancels* Z Z X1+0=Z X2+0=Z eq/ eq/ X1=X2. - : {Z':nat} {Z:nat} {Z'':nat} {N1:nat} {N2:nat} {N3:nat} {X1+Y=Z':plus N1 N3 Z'} {X2+Y=Z'':plus N2 N3 Z''} {Z'=Z'':eq Z' Z''} {X1=X2:eq N1 N2} {Z=sZ':eq Z (s Z')} {Z=sZ'':eq Z (s Z'')} {X2+sY=Z:plus N2 (s N3) Z} {X1+sY=Z:plus N1 (s N3) Z} {sZ'=Z:eq (s Z') Z} {sZ'=sZ'':eq (s Z') (s Z'')} plus-right-cancels* Z' Z'' X1+Y=Z' X2+Y=Z'' eq/ Z'=Z'' X1=X2 -> meta-eq Z (s Z') Z=sZ' -> succ-cancels sZ'=sZ'' Z'=Z'' -> eq-transitive sZ'=Z Z=sZ'' sZ'=sZ'' -> eq-symmetric Z=sZ' sZ'=Z -> plus-right-decrease X2+sY=Z Z'' Z=sZ'' X2+Y=Z'' -> plus-right-decrease X1+sY=Z Z' Z=sZ' X1+Y=Z' -> plus-right-cancels* Z Z X1+sY=Z X2+sY=Z eq/ eq/ X1=X2. %worlds () (plus-right-cancels* Z1 Z2 X1+Y1=Z1 X2+Y2=Z2 Y1=Y2 Z1=Z2 X1=X2). %total Z (plus-right-cancels* Z _ _ _ _ _ _). plus-right-cancels : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} plus N1 N2 N3 -> plus N4 N5 N6 -> eq N2 N5 -> eq N3 N6 -> eq N1 N4 -> type = [N1:nat] [N2:nat] [N3:nat] [N4:nat] [N5:nat] [N6:nat] [P1:plus N1 N2 N3] [P2:plus N4 N5 N6] [EZ:eq N2 N5] [ES:eq N3 N6] [F:eq N1 N4] plus-right-cancels* N3 N6 P1 P2 EZ ES F. %theorem plus-left-preserves-gt* : {M:nat} {N1:nat} {N2:nat} {O1:nat} {O2:nat} gt N1 N2 -> plus M N1 O1 -> plus M N2 O2 -> gt O1 O2 -> type. - : {N1:nat} {N2:nat} {N1>N2:gt N1 N2} plus-left-preserves-gt* N1>N2 plus/z plus/z N1>N2. - : {N1:nat} {N2:nat} {O1>O2:gt N1 N2} {SO1>SO2:gt (s N1) (s N2)} {N3:nat} {N4:nat} {N5:nat} {N1>N2:gt N4 N5} {M+N1=O1:plus N3 N4 N1} {M+N2=O2:plus N3 N5 N2} succ-preserves-gt O1>O2 SO1>SO2 -> plus-left-preserves-gt* N1>N2 M+N1=O1 M+N2=O2 O1>O2 -> plus-left-preserves-gt* N1>N2 (plus/s M+N1=O1) (plus/s M+N2=O2) SO1>SO2. %worlds () (plus-left-preserves-gt* N1>N2 M+N1=O1 M+N2=O2 O1>O2). %total P1 (plus-left-preserves-gt* _ P1 _ _). %theorem plus-left-cancels-gt : {X1:nat} {X2:nat} {Y:nat} {Z:nat} {S1:nat} {S2:nat} plus X1 Y S1 -> plus X2 Z S2 -> eq X1 X2 -> gt S1 S2 -> gt Y Z -> type. - : {N1:nat} {N2:nat} {G:gt N1 N2} plus-left-cancels-gt plus/z plus/z eq/ G G. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X+Y1=Z1:plus N1 N2 N4} {X+Y2=Z2:plus N1 N3 N5} {Z1>Z2:gt N4 N5} {Y1>Y2:gt N2 N3} {SZ1>SZ2:gt (s N4) (s N5)} plus-left-cancels-gt X+Y1=Z1 X+Y2=Z2 eq/ Z1>Z2 Y1>Y2 -> succ-preserves-gt-converse SZ1>SZ2 Z1>Z2 -> plus-left-cancels-gt (plus/s X+Y1=Z1) (plus/s X+Y2=Z2) eq/ SZ1>SZ2 Y1>Y2. %worlds () (plus-left-cancels-gt X1+Y1=Z1 X2+Y2=Z2 X1=X2 Z1>Z2 Y1>Y2). %total P1 (plus-left-cancels-gt P1 _ _ _ _). %theorem plus-left-preserves-gt : {X1:nat} {X2:nat} {X4:nat} gt X2 X4 -> ({X3:nat} {X5:nat} plus X1 X2 X3 -> plus X1 X4 X5 -> gt X3 X5 -> type). - : {N1:nat} {N2:nat} {N3:nat} {X3:nat} {X5:nat} {X2>X4:gt N2 N3} {X1+X2=A3:plus N1 N2 X3} {X1+X4=X5:plus N1 N3 X5} {X3>X5:gt X3 X5} plus-left-preserves-gt* X2>X4 X1+X2=A3 X1+X4=X5 X3>X5 -> plus-total* N1 N3 X5 X1+X4=X5 -> plus-total* N1 N2 X3 X1+X2=A3 -> plus-left-preserves-gt X2>X4 X3 X5 X1+X2=A3 X1+X4=X5 X3>X5. %worlds () (plus-left-preserves-gt X2>X4 X3 X5 X1+X2=A3 X1+X4=X5 X3>X5). %total {} (plus-left-preserves-gt _ _ _ _ _ _). %theorem plus-right-preserves-gt* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} gt X1 X2 -> plus X1 X3 X4 -> plus X2 X3 X5 -> gt X4 X5 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X1>X2:gt N2 N3} {X3+X1=X4:plus N1 N2 N4} {X3+X2=X5:plus N1 N3 N5} {X4>X5:gt N4 N5} {X2+X3=X5:plus N3 N1 N5} {X1+X3=X4:plus N2 N1 N4} plus-left-preserves-gt* X1>X2 X3+X1=X4 X3+X2=X5 X4>X5 -> plus-commutative X2+X3=X5 X3+X2=X5 -> plus-commutative X1+X3=X4 X3+X1=X4 -> plus-right-preserves-gt* X1>X2 X1+X3=X4 X2+X3=X5 X4>X5. %worlds () (plus-right-preserves-gt* X1>X2 X1+X3=X4 X2+X3=X5 X4>X5). %total {} (plus-right-preserves-gt* _ _ _ _). %theorem plus-right-preserves-gt : {X1:nat} {X2:nat} {X3:nat} gt X1 X2 -> ({X4:nat} {X5:nat} plus X1 X3 X4 -> plus X2 X3 X5 -> gt X4 X5 -> type). - : {N1:nat} {N2:nat} {N3:nat} {X4:nat} {X5:nat} {X1>X2:gt N1 N2} {X1+X3=X4:plus N1 N3 X4} {X2+X3=X5:plus N2 N3 X5} {X4>X5:gt X4 X5} plus-right-preserves-gt* X1>X2 X1+X3=X4 X2+X3=X5 X4>X5 -> plus-total* N2 N3 X5 X2+X3=X5 -> plus-total* N1 N3 X4 X1+X3=X4 -> plus-right-preserves-gt X1>X2 X4 X5 X1+X3=X4 X2+X3=X5 X4>X5. %worlds () (plus-right-preserves-gt X1>X2 X4 X5 X1+X3=X4 X2+X3=X5 X4>X5). %total {} (plus-right-preserves-gt _ _ _ _ _ _). %theorem plus-preserves-gt* : {X1:nat} {X2:nat} {X3:nat} {Y1:nat} {Y2:nat} {Y3:nat} gt X1 Y1 -> gt X2 Y2 -> plus X1 X2 X3 -> plus Y1 Y2 Y3 -> gt X3 Y3 -> type. - : {N1:nat} {N2:nat} {N3:nat} {X3>X:gt N1 N2} {X>Y3:gt N2 N3} {X3>Y3:gt N1 N3} {N4:nat} {N5:nat} {N6:nat} {X2>Y2:gt N5 N6} {Y1+X2=X:plus N4 N5 N2} {Y1+Y2=Y3:plus N4 N6 N3} {N7:nat} {X1>Y1:gt N7 N4} {X1+X2=X3:plus N7 N5 N1} gt-transitive X3>X X>Y3 X3>Y3 -> plus-left-preserves-gt* X2>Y2 Y1+X2=X Y1+Y2=Y3 X>Y3 -> plus-right-preserves-gt* X1>Y1 X1+X2=X3 Y1+X2=X X3>X -> plus-total* N4 N5 N2 Y1+X2=X -> plus-preserves-gt* X1>Y1 X2>Y2 X1+X2=X3 Y1+Y2=Y3 X3>Y3. %worlds () (plus-preserves-gt* X1>Y1 X2>Y2 X1+X2=X3 Y1+Y2=Y3 X3>Y3). %total {} (plus-preserves-gt* _ _ _ _ _). %theorem plus-preserves-gt : {X1:nat} {X2:nat} {Y1:nat} {Y2:nat} gt X1 Y1 -> gt X2 Y2 -> ({X3:nat} {Y3:nat} plus X1 X2 X3 -> plus Y1 Y2 Y3 -> gt X3 Y3 -> type). - : {N1:nat} {N2:nat} {X3:nat} {N3:nat} {N4:nat} {Y3:nat} {X1>Y1:gt N1 N3} {X2>Y2:gt N2 N4} {X1+X2=X3:plus N1 N2 X3} {Y1+Y2=Y3:plus N3 N4 Y3} {X3>Y3:gt X3 Y3} plus-preserves-gt* X1>Y1 X2>Y2 X1+X2=X3 Y1+Y2=Y3 X3>Y3 -> plus-total* N3 N4 Y3 Y1+Y2=Y3 -> plus-total* N1 N2 X3 X1+X2=X3 -> plus-preserves-gt X1>Y1 X2>Y2 X3 Y3 X1+X2=X3 Y1+Y2=Y3 X3>Y3. %worlds () (plus-preserves-gt X1>Y1 X2>Y2 X3 Y3 X1+X2=X3 Y1+Y2=Y3 X3>Y3). %total {} (plus-preserves-gt _ _ _ _ _ _ _). %theorem plus-right-cancels-gt : {X1:nat} {X2:nat} {X3:nat} {Y1:nat} {Y2:nat} {Y3:nat} plus X1 X2 X3 -> plus Y1 Y2 Y3 -> eq X2 Y2 -> gt X3 Y3 -> gt X1 Y1 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {X2+X1=X3:plus N1 N3 N5} {Y2+Y1=Y3:plus N2 N4 N6} {X2=Y2:eq N1 N2} {X3>Y3:gt N5 N6} {X1>Y1:gt N3 N4} {Y1+Y2=Y3:plus N4 N2 N6} {X1+X2=X3:plus N3 N1 N5} plus-left-cancels-gt X2+X1=X3 Y2+Y1=Y3 X2=Y2 X3>Y3 X1>Y1 -> plus-commutative Y1+Y2=Y3 Y2+Y1=Y3 -> plus-commutative X1+X2=X3 X2+X1=X3 -> plus-right-cancels-gt X1+X2=X3 Y1+Y2=Y3 X2=Y2 X3>Y3 X1>Y1. %worlds () (plus-right-cancels-gt X1+X2=X3 Y1+Y2=Y3 X2=Y2 X3>Y3 X1>Y1). %total {} (plus-right-cancels-gt _ _ _ _ _). %theorem plus-implies-gt : {M:nat} {N:nat} {O:nat} {M':nat} plus M N O -> eq M (s M') -> gt O N -> type. - : {N1:nat} {N2:nat} {N3:nat} {X>0:gt (s N1) z} {X+Y=Z:plus (s N1) N2 N3} {Z>Y:gt N3 N2} plus-right-preserves-gt* X>0 X+Y=Z plus/z Z>Y -> succ-implies-gt-zero N1 X>0 -> plus-implies-gt X+Y=Z eq/ Z>Y. %worlds () (plus-implies-gt X+Y=Z X=sX' Z>Y). %total {} (plus-implies-gt _ _ _). %theorem plus-gt-contradiction : {M:nat} {N:nat} {O:nat} plus M N O -> gt M O -> void -> type. - : {N1:nat} {M>M:gt N1 N1} {F:void} {N2:nat} {M>O:gt N1 N2} {O=M:eq N2 N1} {M+0=O:plus N1 z N2} {M+0=M:plus N1 z N1} gt-anti-reflexive* N1 M>M F -> gt-respects-eq M>O eq/ O=M M>M -> plus-deterministic M+0=O M+0=M eq/ eq/ O=M -> plus-right-identity N1 M+0=M -> plus-gt-contradiction M+0=O M>O F. - : {N1:nat} {N2:nat} {M>O:gt N1 N2} {O>M:gt N2 N1} {F:void} {N3:nat} {N+M=O:plus (s N3) N1 N2} {M+N=O:plus N1 (s N3) N2} gt-anti-symmetric M>O O>M F -> plus-implies-gt N+M=O eq/ O>M -> plus-commutative M+N=O N+M=O -> plus-gt-contradiction M+N=O M>O F. %worlds () (plus-gt-contradiction M+N=O M>O _). %total {} (plus-gt-contradiction _ _ _). %theorem false-implies-times : {M:nat} {N:nat} {O:nat} void -> times M N O -> type. %worlds () (false-implies-times _ _). %total {} (false-implies-times _ _). %theorem times-respects-eq : {M1:nat} {M2:nat} {N1:nat} {N2:nat} {P1:nat} {P2:nat} times M1 N1 P1 -> eq M1 M2 -> eq N1 N2 -> eq P1 P2 -> times M2 N2 P2 -> type. - : {N1:nat} {N2:nat} {N3:nat} {M1*N1=P1:times N1 N2 N3} times-respects-eq M1*N1=P1 eq/ eq/ eq/ M1*N1=P1. %worlds () (times-respects-eq M1*N1=P1 M1=M2 N1=N2 P1=P2 M2*N2=P2). %total {} (times-respects-eq _ _ _ _ _). %theorem times-total* : {N1:nat} {N2:nat} {N3:nat} times N1 N2 N3 -> type. - : {N2:nat} times-total* z N2 z times/z. - : {Z':nat} {Y:nat} {Z:nat} {Z'+Y=Z:plus Z' Y Z} {X:nat} {X*Y=Z':times X Y Z'} plus-total* Z' Y Z Z'+Y=Z -> times-total* X Y Z' X*Y=Z' -> times-total* (s X) Y Z (times/s X*Y=Z' Z'+Y=Z). %worlds () (times-total* N1 N2 N3 N1*N2=N3). %total N1 (times-total* N1 _ _ _). times-total : {N1:nat} {N2:nat} {N3:nat} times N1 N2 N3 -> type = [N1:nat] [N2:nat] [N3:nat] [T:times N1 N2 N3] times-total* N1 N2 N3 T. %theorem times-deterministic : {N1:nat} {N1':nat} {N2:nat} {N2':nat} {N3:nat} {N3':nat} times N1 N2 N3 -> times N1' N2' N3' -> eq N1 N1' -> eq N2 N2' -> eq N3 N3' -> type. - : {N1:nat} times-deterministic times/z times/z eq/ eq/ eq/. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {Z1+Y=Z1':plus N1 N3 N4} {Z2+Y=Z2':plus N2 N3 N5} {Z1=Z2:eq N1 N2} {Z1'=Z2':eq N4 N5} {N6:nat} {X*Y=Z1:times N6 N3 N1} {X*Y=Z2:times N6 N3 N2} plus-deterministic Z1+Y=Z1' Z2+Y=Z2' Z1=Z2 eq/ Z1'=Z2' -> times-deterministic X*Y=Z1 X*Y=Z2 eq/ eq/ Z1=Z2 -> times-deterministic (times/s X*Y=Z1 Z1+Y=Z1') (times/s X*Y=Z2 Z2+Y=Z2') eq/ eq/ Z1'=Z2'. %worlds () (times-deterministic X1*Y1=Z1 X2*Y2=Z2 X1=X2 Y1=Y2 Z1=Z2). %total P (times-deterministic P _ _ _ _). %theorem times-left-identity : {N:nat} times (s z) N N -> type. - : {N:nat} times-left-identity N (times/s times/z plus/z). %worlds () (times-left-identity N ONE*N=N). %total {} (times-left-identity _ _). %theorem times-right-identity : {N:nat} times N (s z) N -> type. - : times-right-identity z times/z. - : {M:nat} {M+0=M:plus M z M} {M+1=sM:plus M (s z) (s M)} {M*1=M:times M (s z) M} plus-right-increase M+0=M M+1=sM -> plus-right-identity M M+0=M -> times-right-identity M M*1=M -> times-right-identity (s M) (times/s M*1=M M+1=sM). %worlds () (times-right-identity N N*1=N). %total M (times-right-identity M _). %theorem times-right-zero : {N:nat} times N z z -> type. - : times-right-zero z times/z. - : {M:nat} {M*0=0:times M z z} times-right-zero M M*0=0 -> times-right-zero (s M) (times/s M*0=0 plus/z). %worlds () (times-right-zero N N*0=0). %total M (times-right-zero M _). %theorem times-preserves-positive : {M:nat} {N:nat} {P:nat} times (s M) (s N) (s P) -> type. - : {M:nat} {N:nat} {O:nat} {P:nat} {T1:times M (s N) O} {P1:plus O (s N) (s P)} {P2:plus O N P} plus-right-increase P2 P1 -> plus-total* O N P P2 -> times-total* M (s N) O T1 -> times-preserves-positive M N P (times/s T1 P1). %worlds () (times-preserves-positive M N P SM*SN=SP). %total {} (times-preserves-positive _ _ _ _). %theorem times-preserves-positive* : {M:nat} {N:nat} {P:nat} {M':nat} {N':nat} times M N P -> eq M (s M') -> eq N (s N') -> ({P':nat} eq P (s P') -> type). - : {N1:nat} {N2:nat} {N3:nat} {O'+sN'=P:plus N1 (s N2) N3} {P':nat} {P=sP':eq N3 (s P')} {X1:plus N1 N2 P'} {N4:nat} {N5:nat} {N6:nat} {M*N=P:times N4 N6 N3} {M=sM':eq N4 (s N5)} {N=sN':eq N6 (s N2)} {M'*sN'=O':times N5 (s N2) N1} plus-right-decrease O'+sN'=P P' P=sP' X1 -> times-respects-eq M*N=P M=sM' N=sN' eq/ (times/s M'*sN'=O' O'+sN'=P) -> times-preserves-positive* M*N=P M=sM' N=sN' P' P=sP'. %worlds () (times-preserves-positive* M*N=P M=sM' N=sN' P' P=sP'). %total {} (times-preserves-positive* _ _ _ _ _). %theorem times-positive-implies-positive : {M:nat} {N:nat} {P:nat} {P':nat} times M N P -> eq P (s P') -> ({M':nat} eq M (s M') -> ({N':nat} eq N (s N') -> type)). - : {M':nat} {P':nat} {M'*N=T:times M' (s P') z} times-positive-implies-positive (times/s M'*N=T plus/z) eq/ M' eq/ P' eq/. - : {M':nat} {N1:nat} {N2:nat} {M'*N=sT':times M' N1 (s N2)} {N3:nat} {X1:eq M' (s N3)} {N':nat} {N=sN':eq N1 (s N')} {N4:nat} {T'+N=P':plus N2 N1 N4} times-positive-implies-positive M'*N=sT' eq/ N3 X1 N' N=sN' -> times-positive-implies-positive (times/s M'*N=sT' (plus/s T'+N=P')) eq/ M' eq/ N' N=sN'. %worlds () (times-positive-implies-positive M*N=P P=sP' M' M=sM' N' N=sN'). %total T (times-positive-implies-positive T _ _ _ _ _). %theorem times-left-increase : {M:nat} {N:nat} {O:nat} {X:nat} times M N O -> plus O N X -> times (s M) N X -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {T:times N1 N2 N3} {P:plus N3 N2 N4} times-left-increase T P (times/s T P). %worlds () (times-left-increase M*N=O O+N=X SM*N=X). %total {} (times-left-increase _ _ _). %theorem times-right-increase : {M:nat} {N:nat} {O:nat} {X:nat} times M N O -> plus M O X -> times M (s N) X -> type. - : {N1:nat} times-right-increase times/z plus/z times/z. - : {M:nat} {N:nat} {O:nat} {Z:nat} {N1:nat} {Z+N=Y:plus Z N N1} {Z+sN=sY:plus Z (s N) (s N1)} {M*sN=Z:times M (s N) Z} {N2:nat} {O+N=O1:plus O N N2} {M+O1=Y:plus M N2 N1} {M*N=O:times M N O} {M+O=Z:plus M O Z} plus-right-increase Z+N=Y Z+sN=sY -> times-right-increase M*N=O M+O=Z M*sN=Z -> plus-associative-converse O+N=O1 M+O1=Y Z M+O=Z Z+N=Y -> times-right-increase (times/s M*N=O O+N=O1) (plus/s M+O1=Y) (times/s M*sN=Z Z+sN=sY). %worlds () (times-right-increase M*N=O M+O=X M*sN=X). %total T (times-right-increase T _ _). %theorem times-left-decrease : {X:nat} {Y:nat} {Z:nat} times (s X) Y Z -> ({Z1:nat} times X Y Z1 -> plus Z1 Y Z -> type). - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {T:times N1 N2 N4} {P:plus N4 N2 N3} times-left-decrease (times/s T P) N4 T P. %worlds () (times-left-decrease SX*Y=Z Z1 X*Y=Z1 Z1+Y=Z). %total {} (times-left-decrease _ _ _ _). %theorem times-right-decrease : {M:nat} {N:nat} {X:nat} times M (s N) X -> ({O:nat} times M N O -> plus M O X -> type). - : {N1:nat} times-right-decrease times/z z times/z plus/z. - : {N1:nat} {O:nat} {N2:nat} {M+sO=X:plus N1 (s O) N2} {SM+O=X:plus (s N1) O N2} {P:nat} {N3:nat} {N4:nat} {M+P=Y:plus N1 P N3} {Y+sN=X:plus N3 (s N4) N2} {P+sN=sO:plus P (s N4) (s O)} {P+N=O:plus P N4 O} {M*sN=Y:times N1 (s N4) N3} {M*N=P:times N1 N4 P} plus-swap-succ-converse M+sO=X SM+O=X -> plus-associative* M+P=Y Y+sN=X P+sN=sO M+sO=X -> plus-right-increase P+N=O P+sN=sO -> plus-total* P N4 O P+N=O -> times-right-decrease M*sN=Y P M*N=P M+P=Y -> times-right-decrease (times/s M*sN=Y Y+sN=X) O (times/s M*N=P P+N=O) SM+O=X. %worlds () (times-right-decrease M*sN=X O M*N=O M+O=X). %total T (times-right-decrease T _ _ _). %theorem times-commutative : {N1:nat} {N2:nat} {N3:nat} times N1 N2 N3 -> times N2 N1 N3 -> type. - : {N2:nat} {T:times N2 z z} times-right-zero N2 T -> times-commutative times/z T. - : {N1':nat} {N2:nat} {N3':nat} {N3:nat} {T1:times N1' N2 N3'} {P2:plus N3' N2 N3} {T1c:times N2 N1' N3'} {P2c:plus N2 N3' N3} {Tc:times N2 (s N1') N3} times-right-increase T1c P2c Tc -> times-commutative T1 T1c -> plus-commutative P2 P2c -> times-commutative (times/s T1 P2) Tc. %worlds () (times-commutative N1*N2=N3 N2*N1=N3). %total T (times-commutative T _). %theorem times-right-distributes-over-plus : {N1:nat} {N2:nat} {N3:nat} {N12:nat} {N123:nat} plus N1 N2 N12 -> times N12 N3 N123 -> ({N13:nat} {N23:nat} times N1 N3 N13 -> times N2 N3 N23 -> plus N13 N23 N123 -> type). - : {N1:nat} {N2:nat} {YZ:nat} {Y*Z=YZ:times N1 N2 YZ} times-right-distributes-over-plus plus/z Y*Z=YZ z YZ times/z Y*Z=YZ plus/z. - : {YZ:nat} {SXZ:nat} {N1:nat} {YZ+SXZ=SXYZ:plus YZ SXZ N1} {SXZ+YZ=SXYZ:plus SXZ YZ N1} {XZ:nat} {N2:nat} {N3:nat} {YZ+XZ=XYZ:plus YZ XZ N3} {XYZ+Z=SXYZ:plus N3 N2 N1} {XZ+Z=SXZ:plus XZ N2 SXZ} {XZ+YZ=XYZ:plus XZ YZ N3} {N4:nat} {N5:nat} {N6:nat} {X+Y=XY:plus N4 N5 N6} {XY*Z=XYZ:times N6 N2 N3} {X*Z=XZ:times N4 N2 XZ} {Y*Z=YZ:times N5 N2 YZ} plus-commutative YZ+SXZ=SXYZ SXZ+YZ=SXYZ -> plus-associative YZ+XZ=XYZ XYZ+Z=SXYZ SXZ XZ+Z=SXZ YZ+SXZ=SXYZ -> plus-commutative XZ+YZ=XYZ YZ+XZ=XYZ -> times-right-distributes-over-plus X+Y=XY XY*Z=XYZ XZ YZ X*Z=XZ Y*Z=YZ XZ+YZ=XYZ -> times-right-distributes-over-plus (plus/s X+Y=XY) (times/s XY*Z=XYZ XYZ+Z=SXYZ) SXZ YZ (times/s X*Z=XZ XZ+Z=SXZ) Y*Z=YZ SXZ+YZ=SXYZ. %worlds () (times-right-distributes-over-plus X+Y=XY XY*Z=XYZ XZ YZ X*Z=XZ Y*Z=YZ XZ+YZ=XYZ). %total P (times-right-distributes-over-plus P _ _ _ _ _ _). %theorem times-right-distributes-over-plus* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X6:nat} {X7:nat} plus X1 X2 X3 -> times X3 X4 X7 -> times X1 X4 X5 -> times X2 X4 X6 -> plus X5 X6 X7 -> type. - : {Y5:nat} {N1:nat} {Y6:nat} {N2:nat} {N3:nat} {Y5+Y6=X7:plus Y5 Y6 N3} {Y5=X5:eq Y5 N1} {Y6=X6:eq Y6 N2} {X5+X6=X7:plus N1 N2 N3} {N4:nat} {N5:nat} {X2*X4=Y6:times N4 N5 Y6} {X2*X4=X6:times N4 N5 N2} {N6:nat} {X1*X4=Y5:times N6 N5 Y5} {X1*X4=X5:times N6 N5 N1} {N7:nat} {X1+X2=X3:plus N6 N4 N7} {X3*X4=X7:times N7 N5 N3} plus-respects-eq Y5+Y6=X7 Y5=X5 Y6=X6 eq/ X5+X6=X7 -> times-deterministic X2*X4=Y6 X2*X4=X6 eq/ eq/ Y6=X6 -> times-deterministic X1*X4=Y5 X1*X4=X5 eq/ eq/ Y5=X5 -> times-right-distributes-over-plus X1+X2=X3 X3*X4=X7 Y5 Y6 X1*X4=Y5 X2*X4=Y6 Y5+Y6=X7 -> times-right-distributes-over-plus* X1+X2=X3 X3*X4=X7 X1*X4=X5 X2*X4=X6 X5+X6=X7. %worlds () (times-right-distributes-over-plus* X1+X2=X3 X3*X4=X7 X1*X4=X5 X2*X4=X6 X5+X6=X7). %total {} (times-right-distributes-over-plus* _ _ _ _ _). %theorem times-left-distributes-over-plus* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X6:nat} {X7:nat} plus X2 X4 X6 -> times X1 X6 X7 -> times X1 X2 X3 -> times X1 X4 X5 -> plus X3 X5 X7 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {N7:nat} {X2+X4=X6:plus N1 N2 N3} {X6*X1=X7:times N3 N4 N7} {X2*X1=X3:times N1 N4 N5} {X4*X1=X5:times N2 N4 N6} {X3+X5=X7:plus N5 N6 N7} {X1*X4=X5:times N4 N2 N6} {X1*X2=X3:times N4 N1 N5} {X1*X6=X7:times N4 N3 N7} times-right-distributes-over-plus* X2+X4=X6 X6*X1=X7 X2*X1=X3 X4*X1=X5 X3+X5=X7 -> times-commutative X1*X4=X5 X4*X1=X5 -> times-commutative X1*X2=X3 X2*X1=X3 -> times-commutative X1*X6=X7 X6*X1=X7 -> times-left-distributes-over-plus* X2+X4=X6 X1*X6=X7 X1*X2=X3 X1*X4=X5 X3+X5=X7. %worlds () (times-left-distributes-over-plus* X2+X4=X6 X1*X6=X7 X1*X2=X3 X1*X4=X5 X3+X5=X7). %total {} (times-left-distributes-over-plus* _ _ _ _ _). %theorem times-left-distributes-over-plus : {X1:nat} {X2:nat} {X4:nat} {X6:nat} {X7:nat} plus X2 X4 X6 -> times X1 X6 X7 -> ({X3:nat} {X5:nat} times X1 X2 X3 -> times X1 X4 X5 -> plus X3 X5 X7 -> type). - : {N1:nat} {N2:nat} {X3:nat} {N3:nat} {X5:nat} {N4:nat} {N5:nat} {X2+X4=X6:plus N2 N3 N4} {X1*X6=X7:times N1 N4 N5} {X1*X2=X3:times N1 N2 X3} {X1*X4=X5:times N1 N3 X5} {X3+X5=X7:plus X3 X5 N5} times-left-distributes-over-plus* X2+X4=X6 X1*X6=X7 X1*X2=X3 X1*X4=X5 X3+X5=X7 -> times-total* N1 N3 X5 X1*X4=X5 -> times-total* N1 N2 X3 X1*X2=X3 -> times-left-distributes-over-plus X2+X4=X6 X1*X6=X7 X3 X5 X1*X2=X3 X1*X4=X5 X3+X5=X7. %worlds () (times-left-distributes-over-plus X2+X4=X6 X1*X6=X7 X3 X5 X1*X2=X3 X1*X4=X5 X3+X5=X7). %total {} (times-left-distributes-over-plus _ _ _ _ _ _ _). %theorem times-right-factors-over-plus : {X1:nat} {X2:nat} {X4:nat} {X5:nat} {X6:nat} {X7:nat} times X1 X4 X5 -> times X2 X4 X6 -> plus X5 X6 X7 -> ({X3:nat} plus X1 X2 X3 -> times X3 X4 X7 -> type). - : {X3:nat} {N1:nat} {N2:nat} {N3:nat} {X3*X4=Y7:times X3 N1 N2} {Y7=X7:eq N2 N3} {X3*X4=X7:times X3 N1 N3} {N4:nat} {N5:nat} {X5+X6=Y7:plus N4 N5 N2} {X5+X6=X7:plus N4 N5 N3} {N6:nat} {N7:nat} {X1+X2=X3:plus N6 N7 X3} {X1*X4=X5:times N6 N1 N4} {X2*X4=X6:times N7 N1 N5} times-respects-eq X3*X4=Y7 eq/ eq/ Y7=X7 X3*X4=X7 -> plus-deterministic X5+X6=Y7 X5+X6=X7 eq/ eq/ Y7=X7 -> times-right-distributes-over-plus* X1+X2=X3 X3*X4=Y7 X1*X4=X5 X2*X4=X6 X5+X6=Y7 -> times-total* X3 N1 N2 X3*X4=Y7 -> plus-total* N6 N7 X3 X1+X2=X3 -> times-right-factors-over-plus X1*X4=X5 X2*X4=X6 X5+X6=X7 X3 X1+X2=X3 X3*X4=X7. %worlds () (times-right-factors-over-plus X1*X4=X5 X2*X4=X6 X5+X6=X7 X3 X1+X2=X3 X3*X4=X7). %total {} (times-right-factors-over-plus _ _ _ _ _ _). %theorem times-right-factors-over-plus* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X6:nat} {X7:nat} times X1 X4 X5 -> times X2 X4 X6 -> plus X5 X6 X7 -> plus X1 X2 X3 -> times X3 X4 X7 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {X3*X4=Y7:times N1 N2 N3} {Y7=X7:eq N3 N4} {X3*X4=X7:times N1 N2 N4} {N5:nat} {N6:nat} {X5+X6=Y7:plus N5 N6 N3} {X5+X6=X7:plus N5 N6 N4} {N7:nat} {N8:nat} {X1+X2=X3:plus N7 N8 N1} {X1*X4=X5:times N7 N2 N5} {X2*X4=X6:times N8 N2 N6} times-respects-eq X3*X4=Y7 eq/ eq/ Y7=X7 X3*X4=X7 -> plus-deterministic X5+X6=Y7 X5+X6=X7 eq/ eq/ Y7=X7 -> times-right-distributes-over-plus* X1+X2=X3 X3*X4=Y7 X1*X4=X5 X2*X4=X6 X5+X6=Y7 -> times-total* N1 N2 N3 X3*X4=Y7 -> times-right-factors-over-plus* X1*X4=X5 X2*X4=X6 X5+X6=X7 X1+X2=X3 X3*X4=X7. %worlds () (times-right-factors-over-plus* X1*X4=X5 X2*X4=X6 X5+X6=X7 X1+X2=X3 X3*X4=X7). %total {} (times-right-factors-over-plus* _ _ _ _ _). %theorem times-left-factors-over-plus : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X7:nat} times X1 X2 X3 -> times X1 X4 X5 -> plus X3 X5 X7 -> ({X6:nat} plus X2 X4 X6 -> times X1 X6 X7 -> type). - : {X6:nat} {N1:nat} {N2:nat} {X6*X1=X7:times X6 N1 N2} {X1*X6=X7:times N1 X6 N2} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {X2*X1=X3:times N3 N1 N5} {X4*X1=X5:times N4 N1 N6} {X3+X5=X7:plus N5 N6 N2} {X2+X4=X6:plus N3 N4 X6} {X1*X4=X5:times N1 N4 N6} {X1*X2=X3:times N1 N3 N5} times-commutative X6*X1=X7 X1*X6=X7 -> times-right-factors-over-plus X2*X1=X3 X4*X1=X5 X3+X5=X7 X6 X2+X4=X6 X6*X1=X7 -> times-commutative X1*X4=X5 X4*X1=X5 -> times-commutative X1*X2=X3 X2*X1=X3 -> times-left-factors-over-plus X1*X2=X3 X1*X4=X5 X3+X5=X7 X6 X2+X4=X6 X1*X6=X7. %worlds () (times-left-factors-over-plus X1*X2=X3 X1*X4=X5 X3+X5=X7 X6 X2+X4=X6 X1*X6=X7). %total {} (times-left-factors-over-plus _ _ _ _ _ _). %theorem times-left-factors-over-plus* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X6:nat} {X7:nat} times X1 X2 X3 -> times X1 X4 X5 -> plus X3 X5 X7 -> plus X2 X4 X6 -> times X1 X6 X7 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {X1*X6=Y7:times N1 N2 N3} {Y7=X7:eq N3 N4} {X1*X6=X7:times N1 N2 N4} {N5:nat} {N6:nat} {X3+X5=Y7:plus N5 N6 N3} {X3+X5=X7:plus N5 N6 N4} {N7:nat} {N8:nat} {X2+X4=X6:plus N7 N8 N2} {X1*X2=X3:times N1 N7 N5} {X1*X4=X5:times N1 N8 N6} times-respects-eq X1*X6=Y7 eq/ eq/ Y7=X7 X1*X6=X7 -> plus-deterministic X3+X5=Y7 X3+X5=X7 eq/ eq/ Y7=X7 -> times-left-distributes-over-plus* X2+X4=X6 X1*X6=Y7 X1*X2=X3 X1*X4=X5 X3+X5=Y7 -> times-total* N1 N2 N3 X1*X6=Y7 -> times-left-factors-over-plus* X1*X2=X3 X1*X4=X5 X3+X5=X7 X2+X4=X6 X1*X6=X7. %worlds () (times-left-factors-over-plus* X1*X2=X3 X1*X4=X5 X3+X5=X7 X2+X4=X6 X1*X6=X7). %total {} (times-left-factors-over-plus* _ _ _ _ _). %theorem times-associative : {N1:nat} {N2:nat} {N3:nat} {N12:nat} {N123:nat} times N1 N2 N12 -> times N12 N3 N123 -> ({N23:nat} times N2 N3 N23 -> times N1 N23 N123 -> type). - : {N2:nat} {N3:nat} {N23:nat} {T2:times N2 N3 N23} times-total* N2 N3 N23 T2 -> times-associative times/z times/z N23 T2 times/z. - : {N1':nat} {N2:nat} {N1'2:nat} {N12:nat} {N3:nat} {N123:nat} {N23:nat} {N1'23:nat} {N23':nat} {T5':times N1' N23' N1'23} {N23'=N23:eq N23' N23} {T4':times N2 N3 N23'} {T1:times N1' N2 N1'2} {P2:plus N1'2 N2 N12} {T3:times N12 N3 N123} {T4:times N2 N3 N23} {T5:times N1' N23 N1'23} {P6:plus N1'23 N23 N123} {T7:times N1'2 N3 N1'23} times-respects-eq T5' eq/ N23'=N23 eq/ T5 -> times-deterministic T4' T4 eq/ eq/ N23'=N23 -> times-associative T1 T7 N23' T4' T5' -> times-right-distributes-over-plus P2 T3 N1'23 N23 T7 T4 P6 -> times-associative (times/s T1 P2) T3 N23 T4 (times/s T5 P6). %worlds () (times-associative _ _ _ _ _). %total T1 (times-associative T1 _ _ _ _). %theorem times-associative* : {X1:nat} {X2:nat} {X12:nat} {X3:nat} {X23:nat} {X123:nat} times X1 X2 X12 -> times X12 X3 X123 -> times X2 X3 X23 -> times X1 X23 X123 -> type. - : {N1:nat} {Y6:nat} {N2:nat} {N3:nat} {X1*Y6=X7:times N1 Y6 N3} {Y6=X6:eq Y6 N2} {X1*X6=X7:times N1 N2 N3} {N4:nat} {N5:nat} {X2*X4=Y6:times N4 N5 Y6} {X2*X4=X6:times N4 N5 N2} {N6:nat} {X1*X2=X3:times N1 N4 N6} {X3*X4=X7:times N6 N5 N3} times-respects-eq X1*Y6=X7 eq/ Y6=X6 eq/ X1*X6=X7 -> times-deterministic X2*X4=Y6 X2*X4=X6 eq/ eq/ Y6=X6 -> times-associative X1*X2=X3 X3*X4=X7 Y6 X2*X4=Y6 X1*Y6=X7 -> times-associative* X1*X2=X3 X3*X4=X7 X2*X4=X6 X1*X6=X7. %worlds () (times-associative* _ _ _ _). %total {} (times-associative* _ _ _ _). %theorem times-associative-converse : {X1:nat} {X2:nat} {X4:nat} {X6:nat} {X7:nat} times X2 X4 X6 -> times X1 X6 X7 -> ({X3:nat} times X1 X2 X3 -> times X3 X4 X7 -> type). - : {N1:nat} {N2:nat} {N3:nat} {X4*X3=X7:times N1 N2 N3} {X3*X4=X7:times N2 N1 N3} {N4:nat} {N5:nat} {X2*X1=X3:times N4 N5 N2} {X1*X2=X3:times N5 N4 N2} {N6:nat} {X4*X2=X6:times N1 N4 N6} {X6*X1=X7:times N6 N5 N3} {X1*X6=X7:times N5 N6 N3} {X2*X4=X6:times N4 N1 N6} times-commutative X4*X3=X7 X3*X4=X7 -> times-commutative X2*X1=X3 X1*X2=X3 -> times-associative X4*X2=X6 X6*X1=X7 N2 X2*X1=X3 X4*X3=X7 -> times-commutative X1*X6=X7 X6*X1=X7 -> times-commutative X2*X4=X6 X4*X2=X6 -> times-associative-converse X2*X4=X6 X1*X6=X7 N2 X1*X2=X3 X3*X4=X7. %worlds () (times-associative-converse X2*X4=X6 X1*X6=X7 X3 X1*X2=X3 X3*X4=X7). %total {} (times-associative-converse _ _ _ _ _). %theorem times-associative-converse* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X6:nat} {X7:nat} times X2 X4 X6 -> times X1 X6 X7 -> times X1 X2 X3 -> times X3 X4 X7 -> type. - : {X3P:nat} {N1:nat} {N2:nat} {N3:nat} {X3P*X4=X7:times X3P N2 N3} {X3P=X3:eq X3P N1} {X3*X4=X7:times N1 N2 N3} {N4:nat} {N5:nat} {X1*X2=X3P:times N4 N5 X3P} {X1*X2=X3:times N4 N5 N1} {N6:nat} {X2*X4=X6:times N5 N2 N6} {X1*X6=X7:times N4 N6 N3} times-respects-eq X3P*X4=X7 X3P=X3 eq/ eq/ X3*X4=X7 -> times-deterministic X1*X2=X3P X1*X2=X3 eq/ eq/ X3P=X3 -> times-associative-converse X2*X4=X6 X1*X6=X7 X3P X1*X2=X3P X3P*X4=X7 -> times-associative-converse* X2*X4=X6 X1*X6=X7 X1*X2=X3 X3*X4=X7. %worlds () (times-associative-converse* X2*X4=X6 X1*X6=X7 X1*X2=X3 X3*X4=X7). %total {} (times-associative-converse* _ _ _ _). %theorem times-assoc-commutative* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X7:nat} times X1 X2 X3 -> times X3 X4 X7 -> times X1 X4 X5 -> times X5 X2 X7 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {X6:nat} {N5:nat} {X4*X2=X6:times N2 N4 X6} {X1*X6=X7:times N1 X6 N5} {X1*X4=X5:times N1 N2 N3} {X5*X2=X7:times N3 N4 N5} {X2*X4=X6:times N4 N2 X6} {N6:nat} {X1*X2=X3:times N1 N4 N6} {X3*X4=X7:times N6 N2 N5} times-associative-converse* X4*X2=X6 X1*X6=X7 X1*X4=X5 X5*X2=X7 -> times-commutative X2*X4=X6 X4*X2=X6 -> times-associative X1*X2=X3 X3*X4=X7 X6 X2*X4=X6 X1*X6=X7 -> times-assoc-commutative* X1*X2=X3 X3*X4=X7 X1*X4=X5 X5*X2=X7. %worlds () (times-assoc-commutative* X1*X2=X3 X3*X4=X7 X1*X4=X5 X5*X2=X7). %total {} (times-assoc-commutative* _ _ _ _). %theorem times-assoc-commutative : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X7:nat} times X1 X2 X3 -> times X3 X4 X7 -> ({X5:nat} times X1 X4 X5 -> times X5 X2 X7 -> type). - : {N1:nat} {N2:nat} {N3:nat} {X6:nat} {N4:nat} {X4*X2=X6:times N2 N3 X6} {X1*X6=X7:times N1 X6 N4} {X5:nat} {X1*X4=X5:times N1 N2 X5} {X5*X2=X7:times X5 N3 N4} {X2*X4=X6:times N3 N2 X6} {N5:nat} {X1*X2=X3:times N1 N3 N5} {X3*X4=X7:times N5 N2 N4} times-associative-converse X4*X2=X6 X1*X6=X7 X5 X1*X4=X5 X5*X2=X7 -> times-commutative X2*X4=X6 X4*X2=X6 -> times-associative X1*X2=X3 X3*X4=X7 X6 X2*X4=X6 X1*X6=X7 -> times-assoc-commutative X1*X2=X3 X3*X4=X7 X5 X1*X4=X5 X5*X2=X7. %worlds () (times-assoc-commutative X1*X2=X3 X3*X4=X7 X5 X1*X4=X5 X5*X2=X7). %total {} (times-assoc-commutative _ _ _ _ _). %theorem times-double-associative* : {A:nat} {B:nat} {C:nat} {D:nat} {A+B:nat} {C+D:nat} {A+C:nat} {B+D:nat} {X:nat} times A B A+B -> times C D C+D -> times A+B C+D X -> times A C A+C -> times B D B+D -> times A+C B+D X -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {XE:nat} {N5:nat} {X4*XA=XE:times N2 N4 XE} {X1*XE=XF:times N1 XE N5} {X1*X4=X5:times N1 N2 N3} {X5*XA=XF:times N3 N4 N5} {XA*X4=XE:times N4 N2 XE} {N6:nat} {N7:nat} {N8:nat} {X8*X4=XC:times N7 N2 N8} {X2*XC=XE:times N6 N8 XE} {X2*X8=XA:times N6 N7 N4} {X4*X8=XC:times N2 N7 N8} {N9:nat} {X1*X2=X3:times N1 N6 N9} {X3*XC=XF:times N9 N8 N5} times-associative-converse* X4*XA=XE X1*XE=XF X1*X4=X5 X5*XA=XF -> times-commutative XA*X4=XE X4*XA=XE -> times-associative-converse* X8*X4=XC X2*XC=XE X2*X8=XA XA*X4=XE -> times-commutative X4*X8=XC X8*X4=XC -> times-associative X1*X2=X3 X3*XC=XF XE X2*XC=XE X1*XE=XF -> times-double-associative* X1*X2=X3 X4*X8=XC X3*XC=XF X1*X4=X5 X2*X8=XA X5*XA=XF. %worlds () (times-double-associative* X1*X2=X3 X4*X8=XC X3*XC=XF X1*X4=X5 X2*X8=XA X5*XA=XF). %total {} (times-double-associative* _ _ _ _ _ _). %theorem times-double-associative : {A:nat} {B:nat} {C:nat} {D:nat} {A+B:nat} {C+D:nat} {X:nat} times A B A+B -> times C D C+D -> times A+B C+D X -> ({A+C:nat} {B+D:nat} times A C A+C -> times B D B+D -> times A+C B+D X -> type). - : {N1:nat} {N2:nat} {XA:nat} {XE:nat} {N3:nat} {X4*XA=XE:times N2 XA XE} {X1*XE=XF:times N1 XE N3} {X5:nat} {X1*X4=X5:times N1 N2 X5} {X5*XA=XF:times X5 XA N3} {XA*X4=XE:times XA N2 XE} {N4:nat} {N5:nat} {N6:nat} {X8*X4=XC:times N5 N2 N6} {X2*XC=XE:times N4 N6 XE} {X2*X8=XA:times N4 N5 XA} {X4*X8=XC:times N2 N5 N6} {N7:nat} {X1*X2=X3:times N1 N4 N7} {X3*XC=XF:times N7 N6 N3} times-associative-converse X4*XA=XE X1*XE=XF X5 X1*X4=X5 X5*XA=XF -> times-commutative XA*X4=XE X4*XA=XE -> times-associative-converse X8*X4=XC X2*XC=XE XA X2*X8=XA XA*X4=XE -> times-commutative X4*X8=XC X8*X4=XC -> times-associative X1*X2=X3 X3*XC=XF XE X2*XC=XE X1*XE=XF -> times-double-associative X1*X2=X3 X4*X8=XC X3*XC=XF X5 XA X1*X4=X5 X2*X8=XA X5*XA=XF. %worlds () (times-double-associative _ _ _ _ _ _ _ _). %total {} (times-double-associative _ _ _ _ _ _ _ _). %theorem times-right-cancels : {X1:nat} {Y1:nat} {Z1:nat} {X2:nat} {Y2:nat} {Z2:nat} times X1 (s Y1) Z1 -> times X2 (s Y2) Z2 -> eq Y1 Y2 -> eq Z1 Z2 -> eq X1 X2 -> type. - : {N1:nat} {N2:nat} {EY:eq N1 N2} times-right-cancels times/z times/z EY eq/ eq/. - : {X1:nat} {Y1:nat} {Z1':nat} {Z1:nat} {X2:nat} {Y2:nat} {Z2':nat} {Z2:nat} {EX':eq (s X1) (s X2)} {EZ':eq Z1' Z2'} {EY':eq (s Y1) (s Y2)} {T1:times X1 (s Y1) Z1'} {P1:plus Z1' (s Y1) Z1} {T2:times X2 (s Y2) Z2'} {P2:plus Z2' (s Y2) Z2} {EY:eq Y1 Y2} {EZ:eq Z1 Z2} {EX:eq X1 X2} succ-deterministic EX EX' -> times-right-cancels T1 T2 EY EZ' EX -> plus-right-cancels* Z1 Z2 P1 P2 EY' EZ EZ' -> succ-deterministic EY EY' -> times-right-cancels (times/s T1 P1) (times/s T2 P2) EY EZ EX'. %worlds () (times-right-cancels X1*sY1=Z1 X2*sY2=Z2 Y1=Y2 Z1=Z2 X1=X2). %total T1 (times-right-cancels T1 _ _ _ _). %theorem times-right-cancels* : {X1:nat} {Y:nat} {Y-1:nat} {Z1:nat} {X2:nat} {Z2:nat} times X1 Y Z1 -> times X2 Y Z2 -> eq Y (s Y-1) -> eq Z1 Z2 -> eq X1 X2 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X1*Y+=Z1:times N1 (s N2) N3} {X2*Y+=Z2:times N4 (s N2) N5} {Z1=Z2:eq N3 N5} {X1=X2:eq N1 N4} {N6:nat} {X2*Y=Z2:times N4 N6 N5} {Y+:eq N6 (s N2)} {X1*Y=Z1:times N1 N6 N3} times-right-cancels X1*Y+=Z1 X2*Y+=Z2 eq/ Z1=Z2 X1=X2 -> times-respects-eq X2*Y=Z2 eq/ Y+ eq/ X2*Y+=Z2 -> times-respects-eq X1*Y=Z1 eq/ Y+ eq/ X1*Y+=Z1 -> times-right-cancels* X1*Y=Z1 X2*Y=Z2 Y+ Z1=Z2 X1=X2. %worlds () (times-right-cancels* X1*Y=Z1 X2*Y=Z2 Y+ Z1=Z2 X1=X2). %total {} (times-right-cancels* _ _ _ _ _). %theorem times-right-cancels** : {X1:nat} {Y1:nat} {Z:nat} {X2:nat} {Y2:nat} {Z-:nat} times X1 Y1 Z -> times X2 Y2 Z -> eq Y1 Y2 -> eq Z (s Z-) -> eq X1 X2 -> type. - : {N1:nat} {N2:nat} {F:void} {X1=X2:eq N1 N2} {N3:nat} {ZERO>sZ:gt z N3} {ZERO=sZ:eq z (s N3)} {X1*0=0:times N1 z z} {X1*0=sZ:times N1 z (s N3)} {X2*0=sZ:times N2 z (s N3)} false-implies-eq F X1=X2 -> gt-contradiction ZERO>sZ F -> succ-implies-gt ZERO=sZ ZERO>sZ -> times-deterministic X1*0=0 X1*0=sZ eq/ eq/ ZERO=sZ -> times-right-zero N1 X1*0=0 -> times-right-cancels** X1*0=sZ X2*0=sZ eq/ eq/ X1=X2. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {X1*Y1-=sZ:times N1 (s N2) (s N3)} {X2*Y1-=sZ:times N4 (s N2) (s N3)} {X1=X2:eq N1 N4} times-right-cancels X1*Y1-=sZ X2*Y1-=sZ eq/ eq/ X1=X2 -> times-right-cancels** X1*Y1-=sZ X2*Y1-=sZ eq/ eq/ X1=X2. %worlds () (times-right-cancels** X1*Y1=Z X2*Y2=Z Y1=Y2 Z+ X1=X2). %total {} (times-right-cancels** _ _ _ _ _). %theorem times-left-cancels : {X1:nat} {Y1:nat} {Z1:nat} {X2:nat} {Y2:nat} {Z2:nat} times (s X1) Y1 Z1 -> times (s X2) Y2 Z2 -> eq X1 X2 -> eq Z1 Z2 -> eq Y1 Y2 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {Y1*sX1=Z1:times N1 (s N2) N3} {Y2*sX2=Z2:times N4 (s N5) N6} {X1=X2:eq N2 N5} {Z1=Z2:eq N3 N6} {Y1=Y2:eq N1 N4} {SX2*Y2=Z2:times (s N5) N4 N6} {SX1*Y1=Z1:times (s N2) N1 N3} times-right-cancels Y1*sX1=Z1 Y2*sX2=Z2 X1=X2 Z1=Z2 Y1=Y2 -> times-commutative SX2*Y2=Z2 Y2*sX2=Z2 -> times-commutative SX1*Y1=Z1 Y1*sX1=Z1 -> times-left-cancels SX1*Y1=Z1 SX2*Y2=Z2 X1=X2 Z1=Z2 Y1=Y2. %worlds () (times-left-cancels SX1*Y1=Z1 SX2*Y2=Z2 X1=X2 Z1=Z2 Y1=Y2). %total {} (times-left-cancels _ _ _ _ _). %theorem times-left-cancels* : {X:nat} {Y1:nat} {Z1:nat} {X-:nat} {Y2:nat} {Z2:nat} times X Y1 Z1 -> times X Y2 Z2 -> eq X (s X-) -> eq Z1 Z2 -> eq Y1 Y2 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {Y1*X=Z1:times N1 N2 N4} {Y2*X=Z2:times N5 N2 N6} {X+:eq N2 (s N3)} {Z1=Z2:eq N4 N6} {Y1=Y2:eq N1 N5} {X*Y2=Z2:times N2 N5 N6} {X*Y1=Z1:times N2 N1 N4} times-right-cancels* Y1*X=Z1 Y2*X=Z2 X+ Z1=Z2 Y1=Y2 -> times-commutative X*Y2=Z2 Y2*X=Z2 -> times-commutative X*Y1=Z1 Y1*X=Z1 -> times-left-cancels* X*Y1=Z1 X*Y2=Z2 X+ Z1=Z2 Y1=Y2. %worlds () (times-left-cancels* X*Y1=Z1 X*Y2=Z2 X+ Z1=Z2 Y1=Y2). %total {} (times-left-cancels* _ _ _ _ _). %theorem times-left-preserves-gt : {M:nat} {N1:nat} {N2:nat} {P1:nat} {P2:nat} gt N1 N2 -> times (s M) N1 P1 -> times (s M) N2 P2 -> gt P1 P2 -> type. - : {N1:nat} {N2:nat} {N1>N2:gt N1 N2} times-left-preserves-gt N1>N2 (times/s times/z plus/z) (times/s times/z plus/z) N1>N2. - : {X1:nat} {N1:nat} {N2:nat} {X2:nat} {N3:nat} {N4:nat} {X1>X2:gt X1 X2} {N1>N2:gt N1 N3} {X1+N1=O1:plus X1 N1 N2} {X2+N2=O2:plus X2 N3 N4} {O1>O2:gt N2 N4} {M:nat} {T1:times (s M) N1 X1} {T2:times (s M) N3 X2} plus-preserves-gt* X1>X2 N1>N2 X1+N1=O1 X2+N2=O2 O1>O2 -> times-left-preserves-gt N1>N2 T1 T2 X1>X2 -> times-left-preserves-gt N1>N2 (times/s T1 X1+N1=O1) (times/s T2 X2+N2=O2) O1>O2. %worlds () (times-left-preserves-gt N1>N2 SM*N1=P1 SM*N2=P2 P1>P2). %total T1 (times-left-preserves-gt _ T1 _ _). %theorem times-left-preserves-gt* : {M:nat} {M-:nat} {N1:nat} {N2:nat} {P1:nat} {P2:nat} gt N1 N2 -> times M N1 P1 -> times M N2 P2 -> eq M (s M-) -> gt P1 P2 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N1>N2:gt N2 N3} {SM-*N1=P1:times (s N1) N2 N4} {SM-*N2=P2:times (s N1) N3 N5} {P1>P2:gt N4 N5} {N6:nat} {M*N2=P2:times N6 N3 N5} {M+:eq N6 (s N1)} {M*N1=P1:times N6 N2 N4} times-left-preserves-gt N1>N2 SM-*N1=P1 SM-*N2=P2 P1>P2 -> times-respects-eq M*N2=P2 M+ eq/ eq/ SM-*N2=P2 -> times-respects-eq M*N1=P1 M+ eq/ eq/ SM-*N1=P1 -> times-left-preserves-gt* N1>N2 M*N1=P1 M*N2=P2 M+ P1>P2. %worlds () (times-left-preserves-gt* N1>N2 M*N1=P1 M*N2=P2 M+ P1>P2). %total {} (times-left-preserves-gt* _ _ _ _ _). %theorem times-right-preserves-gt : {M1:nat} {M2:nat} {N:nat} {P1:nat} {P2:nat} gt M1 M2 -> times M1 (s N) P1 -> times M2 (s N) P2 -> gt P1 P2 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {M1>M2:gt N2 N3} {SN*M1=P1:times (s N1) N2 N4} {SN*M2=P2:times (s N1) N3 N5} {P1>P2:gt N4 N5} {M2*sN=P2:times N3 (s N1) N5} {M1*sN=P1:times N2 (s N1) N4} times-left-preserves-gt M1>M2 SN*M1=P1 SN*M2=P2 P1>P2 -> times-commutative M2*sN=P2 SN*M2=P2 -> times-commutative M1*sN=P1 SN*M1=P1 -> times-right-preserves-gt M1>M2 M1*sN=P1 M2*sN=P2 P1>P2. %worlds () (times-right-preserves-gt M1>M2 M1*sN=P1 M2*sN=P2 P1>P2). %total {} (times-right-preserves-gt _ _ _ _). %theorem times-right-preserves-gt* : {M1:nat} {M2:nat} {N:nat} {N-1:nat} {P1:nat} {P2:nat} gt M1 M2 -> times M1 N P1 -> times M2 N P2 -> eq N (s N-1) -> gt P1 P2 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {M1>M2:gt N1 N2} {M1*N+=P1:times N1 (s N3) N4} {M2*N+=P2:times N2 (s N3) N5} {P1>P2:gt N4 N5} {N6:nat} {M2*N=P2:times N2 N6 N5} {N=sN-1:eq N6 (s N3)} {M1*N=P1:times N1 N6 N4} times-right-preserves-gt M1>M2 M1*N+=P1 M2*N+=P2 P1>P2 -> times-respects-eq M2*N=P2 eq/ N=sN-1 eq/ M2*N+=P2 -> times-respects-eq M1*N=P1 eq/ N=sN-1 eq/ M1*N+=P1 -> times-right-preserves-gt* M1>M2 M1*N=P1 M2*N=P2 N=sN-1 P1>P2. %worlds () (times-right-preserves-gt* M1>M2 M1*N=P1 M2*N=P2 N=sN-1 P1>P2). %total {} (times-right-preserves-gt* _ _ _ _ _). %theorem times-preserves-gt : {M1:nat} {N1:nat} {P1:nat} {M2:nat} {N2:nat} {P2:nat} gt M1 M2 -> gt N1 N2 -> times M1 N1 P1 -> times M2 N2 P2 -> gt P1 P2 -> type. - : {N1:nat} {P1:nat} {P1>0:gt P1 z} {P1>0':gt P1 N1} {M1':nat} {N2:nat} {N1>0:gt N2 z} {SM1'*N1=P1:times (s M1') N2 P1} {SM1'*0=0:times (s M1') z z} {M2:nat} {M2*0=0:times M2 z z} {M2*0=0':times M2 z N1} {M1:nat} {M1*N1=P1:times M1 N2 P1} {M1=sM1':eq M1 (s M1')} {M1>M2:gt M1 M2} {0=0':eq z N1} gt-respects-eq P1>0 eq/ 0=0' P1>0' -> times-left-preserves-gt N1>0 SM1'*N1=P1 SM1'*0=0 P1>0 -> times-right-zero (s M1') SM1'*0=0 -> times-deterministic M2*0=0 M2*0=0' eq/ eq/ 0=0' -> times-right-zero M2 M2*0=0 -> times-respects-eq M1*N1=P1 M1=sM1' eq/ eq/ SM1'*N1=P1 -> gt-implies-positive M1>M2 M1' M1=sM1' -> times-preserves-gt M1>M2 N1>0 M1*N1=P1 M2*0=0' P1>0'. - : {N1:nat} {N2:nat} {N3:nat} {P1>PX:gt N1 N2} {PX>P2:gt N2 N3} {P1>P2:gt N1 N3} {N4:nat} {N5:nat} {N2':nat} {M1>M2:gt N4 N5} {M1*sN2'=PX:times N4 (s N2') N2} {M2*sN2'=P2:times N5 (s N2') N3} {M1':nat} {SM1'*sN2'=PX:times (s M1') (s N2') N2} {SM1'=M1:eq (s M1') N4} {M1=sM1':eq N4 (s M1')} {N6:nat} {N1>sN2':gt N6 (s N2')} {SM1'*N1=P1:times (s M1') N6 N1} {M1*N1=P1:times N4 N6 N1} gt-transitive P1>PX PX>P2 P1>P2 -> times-right-preserves-gt M1>M2 M1*sN2'=PX M2*sN2'=P2 PX>P2 -> times-respects-eq SM1'*sN2'=PX SM1'=M1 eq/ eq/ M1*sN2'=PX -> eq-symmetric M1=sM1' SM1'=M1 -> times-left-preserves-gt N1>sN2' SM1'*N1=P1 SM1'*sN2'=PX P1>PX -> times-total* (s M1') (s N2') N2 SM1'*sN2'=PX -> times-respects-eq M1*N1=P1 M1=sM1' eq/ eq/ SM1'*N1=P1 -> gt-implies-positive M1>M2 M1' M1=sM1' -> times-preserves-gt M1>M2 N1>sN2' M1*N1=P1 M2*sN2'=P2 P1>P2. %worlds () (times-preserves-gt M1>M2 N1>N2 M1*N1=P1 M2*N2=P2 P1>P2). %total {} (times-preserves-gt _ _ _ _ _). %theorem times-right-cancels-gt : {X1:nat} {X2:nat} {Y1:nat} {Y2:nat} {Z1:nat} {Z2:nat} times X1 Y1 Z1 -> times X2 Y2 Z2 -> eq Y1 Y2 -> gt Z1 Z2 -> gt X1 X2 -> type. - : {N1:nat} {SX1>0:gt (s N1) z} {N2:nat} {N3:nat} {N4:nat} {X1*Y=N1:times N1 N2 N4} {N1+Y=Z1:plus N4 N2 N3} {Z1>0:gt N3 z} succ-implies-gt-zero N1 SX1>0 -> times-right-cancels-gt (times/s X1*Y=N1 N1+Y=Z1) times/z eq/ Z1>0 SX1>0. - : {N1:nat} {N2:nat} {X1>X2:gt N1 N2} {SX1>SX2:gt (s N1) (s N2)} {N3:nat} {N4:nat} {N5:nat} {X1*Y=N1:times N1 N3 N4} {X2*Y=N2:times N2 N3 N5} {N1>N2:gt N4 N5} {N6:nat} {N7:nat} {N1+Y=Z1:plus N4 N3 N6} {N2+Y=Z2:plus N5 N3 N7} {Z1>Z2:gt N6 N7} succ-preserves-gt X1>X2 SX1>SX2 -> times-right-cancels-gt X1*Y=N1 X2*Y=N2 eq/ N1>N2 X1>X2 -> plus-right-cancels-gt N1+Y=Z1 N2+Y=Z2 eq/ Z1>Z2 N1>N2 -> times-right-cancels-gt (times/s X1*Y=N1 N1+Y=Z1) (times/s X2*Y=N2 N2+Y=Z2) eq/ Z1>Z2 SX1>SX2. %worlds () (times-right-cancels-gt X1*Y1=Z1 X2*Y2=Z2 Y1=Y2 Z1>Z2 X1>X2). %total [P1 P2] (times-right-cancels-gt P1 P2 _ _ _). %theorem times-left-cancels-gt : {X1:nat} {X2:nat} {Y1:nat} {Y2:nat} {Z1:nat} {Z2:nat} times X1 Y1 Z1 -> times X2 Y2 Z2 -> eq X1 X2 -> gt Z1 Z2 -> gt Y1 Y2 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {Y1*X1=Z1:times N1 N3 N5} {Y2*X2=Z2:times N2 N4 N6} {X1=X2:eq N3 N4} {Z1>Z2:gt N5 N6} {Y1>Y2:gt N1 N2} {X2*Y2=Z2:times N4 N2 N6} {X1*Y1=Z1:times N3 N1 N5} times-right-cancels-gt Y1*X1=Z1 Y2*X2=Z2 X1=X2 Z1>Z2 Y1>Y2 -> times-commutative X2*Y2=Z2 Y2*X2=Z2 -> times-commutative X1*Y1=Z1 Y1*X1=Z1 -> times-left-cancels-gt X1*Y1=Z1 X2*Y2=Z2 X1=X2 Z1>Z2 Y1>Y2. %worlds () (times-left-cancels-gt X1*Y1=Z1 X2*Y2=Z2 X1=X2 Z1>Z2 Y1>Y2). %total P1 (times-left-cancels-gt P1 _ _ _ _). minus : nat -> nat -> nat -> type = [X1:nat] [X2:nat] [X3:nat] plus X3 X2 X1. false-implies-minus : {N1:nat} {N2:nat} {N3:nat} void -> plus N1 N2 N3 -> type = [N1:nat] [N2:nat] [N3:nat] [P:void] [Q:plus N1 N2 N3] false-implies-plus P Q. %theorem minus-respects-eq : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X6:nat} plus X3 X2 X1 -> eq X1 X4 -> eq X2 X5 -> eq X3 X6 -> plus X6 X5 X4 -> type. - : {N1:nat} {N2:nat} {N3:nat} {S:plus N3 N2 N1} minus-respects-eq S eq/ eq/ eq/ S. %worlds () (minus-respects-eq _ _ _ _ _). %total {} (minus-respects-eq _ _ _ _ _). %theorem minus-deterministic : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X6:nat} plus X3 X2 X1 -> plus X6 X5 X4 -> eq X1 X4 -> eq X2 X5 -> eq X3 X6 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {X3+X2=X1:plus N1 N3 N5} {X6+X5=X4:plus N2 N4 N6} {X2=X5:eq N3 N4} {X1=X4:eq N5 N6} {X3=X6:eq N1 N2} plus-right-cancels* N5 N6 X3+X2=X1 X6+X5=X4 X2=X5 X1=X4 X3=X6 -> minus-deterministic X3+X2=X1 X6+X5=X4 X1=X4 X2=X5 X3=X6. %worlds () (minus-deterministic X1-X2=X3 X4-X5=X6 X1=X4 X2=X5 X3=X6). %total {} (minus-deterministic _ _ _ _ _). %theorem plus-associates-with-minus* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X6:nat} {X7:nat} plus X1 X2 X3 -> plus X7 X4 X3 -> plus X6 X4 X2 -> plus X1 X6 X7 -> type. - : {N1:nat} {N2:nat} {X7P:nat} {N3:nat} {X1+X6=X7P:plus N1 N2 X7P} {X7P=X7:eq X7P N3} {X1+X6=X7:plus N1 N2 N3} {N4:nat} {N5:nat} {X7P+X4=X3:plus X7P N4 N5} {X7+X4=X3:plus N3 N4 N5} {N6:nat} {X6+X4=X2:plus N2 N4 N6} {X1+X2=X3:plus N1 N6 N5} plus-respects-eq X1+X6=X7P eq/ eq/ X7P=X7 X1+X6=X7 -> plus-right-cancels* N5 N5 X7P+X4=X3 X7+X4=X3 eq/ eq/ X7P=X7 -> plus-associative-converse X6+X4=X2 X1+X2=X3 X7P X1+X6=X7P X7P+X4=X3 -> plus-associates-with-minus* X1+X2=X3 X7+X4=X3 X6+X4=X2 X1+X6=X7. %worlds () (plus-associates-with-minus* X1+X2=X3 X3-X4=X7 X2-X4=X6 X1+X6=X7). %total {} (plus-associates-with-minus* _ _ _ _). %theorem plus-associates-with-minus-converse* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X6:nat} {X7:nat} plus X6 X4 X2 -> plus X1 X6 X7 -> plus X1 X2 X3 -> plus X7 X4 X3 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {X6+X4=X2:plus N2 N4 N5} {X1+X2=X3:plus N1 N5 N6} {X1+X6=X7:plus N1 N2 N3} {X7+X4=X3:plus N3 N4 N6} plus-associative-converse* X6+X4=X2 X1+X2=X3 X1+X6=X7 X7+X4=X3 -> plus-associates-with-minus-converse* X6+X4=X2 X1+X6=X7 X1+X2=X3 X7+X4=X3. %worlds () (plus-associates-with-minus-converse* X2-X4=X6 X1+X6=X7 X1+X2=X3 X3-X4=X7). %total {} (plus-associates-with-minus-converse* _ _ _ _). %theorem plus-associates-with-minus-converse : {X1:nat} {X2:nat} {X4:nat} {X6:nat} {X7:nat} plus X6 X4 X2 -> plus X1 X6 X7 -> ({X3:nat} plus X1 X2 X3 -> plus X7 X4 X3 -> type). - : {N1:nat} {N2:nat} {X3:nat} {N3:nat} {N4:nat} {N5:nat} {X6+X4=X2:plus N4 N3 N2} {X1+X6=X7:plus N1 N4 N5} {X1+X2=X3:plus N1 N2 X3} {X7+X4=X3:plus N5 N3 X3} plus-associates-with-minus-converse* X6+X4=X2 X1+X6=X7 X1+X2=X3 X7+X4=X3 -> plus-total* N1 N2 X3 X1+X2=X3 -> plus-associates-with-minus-converse X6+X4=X2 X1+X6=X7 X3 X1+X2=X3 X7+X4=X3. %worlds () (plus-associates-with-minus-converse X2-X4=X6 X1+X6=X7 X3 X1+X2=X3 X3-X4=X7). %total {} (plus-associates-with-minus-converse _ _ _ _ _). %theorem minus-associates-from-plus* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X6:nat} {X7:nat} plus X3 X2 X1 -> plus X3 X4 X7 -> plus X6 X4 X2 -> plus X7 X6 X1 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {X4+X6=X2:plus N2 N4 N5} {X3+X2=X1:plus N1 N5 N6} {X3+X4=X7:plus N1 N2 N3} {X7+X6=X1:plus N3 N4 N6} {X6+X4=X2:plus N4 N2 N5} plus-associative-converse* X4+X6=X2 X3+X2=X1 X3+X4=X7 X7+X6=X1 -> plus-commutative X6+X4=X2 X4+X6=X2 -> minus-associates-from-plus* X3+X2=X1 X3+X4=X7 X6+X4=X2 X7+X6=X1. %worlds () (minus-associates-from-plus* X1-X2=X3 X3+X4=X7 X2-X4=X6 X1-X6=X7). %total {} (minus-associates-from-plus* _ _ _ _). %theorem minus-associates-from-plus-converse* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X6:nat} {X7:nat} plus X6 X4 X2 -> plus X7 X6 X1 -> plus X3 X2 X1 -> plus X3 X4 X7 -> type. - : {N1:nat} {N2:nat} {X7P:nat} {N3:nat} {X3+X4=X7P:plus N1 N2 X7P} {X7P=X7:eq X7P N3} {X3+X4=X7:plus N1 N2 N3} {N4:nat} {N5:nat} {X7P+X6=X1:plus X7P N4 N5} {X7+X6=X1:plus N3 N4 N5} {N6:nat} {X4+X6=X2:plus N2 N4 N6} {X3+X2=X1:plus N1 N6 N5} {X6+X4=X2:plus N4 N2 N6} plus-respects-eq X3+X4=X7P eq/ eq/ X7P=X7 X3+X4=X7 -> plus-right-cancels* N5 N5 X7P+X6=X1 X7+X6=X1 eq/ eq/ X7P=X7 -> plus-associative-converse X4+X6=X2 X3+X2=X1 X7P X3+X4=X7P X7P+X6=X1 -> plus-commutative X6+X4=X2 X4+X6=X2 -> minus-associates-from-plus-converse* X6+X4=X2 X7+X6=X1 X3+X2=X1 X3+X4=X7. %worlds () (minus-associates-from-plus-converse* X2-X4=X6 X1-X6=X7 X1-X2=X3 X3+X4=X7). %total {} (minus-associates-from-plus-converse* _ _ _ _). %theorem minus-associates-to-plus* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X6:nat} {X7:nat} plus X3 X2 X1 -> plus X7 X4 X3 -> plus X2 X4 X6 -> plus X7 X6 X1 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {X7+X4=X3:plus N1 N2 N3} {X3+X2=X1:plus N3 N4 N6} {X4+X2=X6:plus N2 N4 N5} {X7+X6=X1:plus N1 N5 N6} {X2+X4=X6:plus N4 N2 N5} plus-associative* X7+X4=X3 X3+X2=X1 X4+X2=X6 X7+X6=X1 -> plus-commutative X2+X4=X6 X4+X2=X6 -> minus-associates-to-plus* X3+X2=X1 X7+X4=X3 X2+X4=X6 X7+X6=X1. %worlds () (minus-associates-to-plus* X1-X2=X3 X3-X4=X7 X2+X4=X6 X1-X6=X7). %total {} (minus-associates-to-plus* _ _ _ _). %theorem minus-associates-to-plus : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X7:nat} plus X3 X2 X1 -> plus X7 X4 X3 -> ({X6:nat} plus X2 X4 X6 -> plus X7 X6 X1 -> type). - : {N1:nat} {N2:nat} {X6:nat} {X4+X2=X6:plus N1 N2 X6} {X2+X4=X6:plus N2 N1 X6} {N3:nat} {N4:nat} {N5:nat} {X7+X4=X3:plus N3 N1 N4} {X3+X2=X1:plus N4 N2 N5} {X7+X6=X1:plus N3 X6 N5} plus-commutative X4+X2=X6 X2+X4=X6 -> plus-associative X7+X4=X3 X3+X2=X1 X6 X4+X2=X6 X7+X6=X1 -> minus-associates-to-plus X3+X2=X1 X7+X4=X3 X6 X2+X4=X6 X7+X6=X1. %worlds () (minus-associates-to-plus X1-X2=X3 X3-X4=X7 X6 X2+X4=X6 X1-X6=X7). %total {} (minus-associates-to-plus _ _ _ _ _). %theorem minus-associates-to-plus-converse* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X6:nat} {X7:nat} plus X2 X4 X6 -> plus X7 X6 X1 -> plus X3 X2 X1 -> plus X7 X4 X3 -> type. - : {N1:nat} {N2:nat} {X3P:nat} {N3:nat} {X7+X4=X3P:plus N1 N2 X3P} {X3P=X3:eq X3P N3} {X7+X4=X3:plus N1 N2 N3} {N4:nat} {N5:nat} {X3P+X2=X1:plus X3P N4 N5} {X3+X2=X1:plus N3 N4 N5} {N6:nat} {X4+X2=X6:plus N2 N4 N6} {X7+X6=X1:plus N1 N6 N5} {X2+X4=X6:plus N4 N2 N6} plus-respects-eq X7+X4=X3P eq/ eq/ X3P=X3 X7+X4=X3 -> plus-right-cancels* N5 N5 X3P+X2=X1 X3+X2=X1 eq/ eq/ X3P=X3 -> plus-associative-converse X4+X2=X6 X7+X6=X1 X3P X7+X4=X3P X3P+X2=X1 -> plus-commutative X2+X4=X6 X4+X2=X6 -> minus-associates-to-plus-converse* X2+X4=X6 X7+X6=X1 X3+X2=X1 X7+X4=X3. %worlds () (minus-associates-to-plus-converse* X2+X4=X6 X1-X6=X7 X1-X2=X3 X3-X4=X7). %total {} (minus-associates-to-plus-converse* _ _ _ _). %theorem minus-associates-to-plus-converse : {X1:nat} {X2:nat} {X4:nat} {X6:nat} {X7:nat} plus X2 X4 X6 -> plus X7 X6 X1 -> ({X3:nat} plus X3 X2 X1 -> plus X7 X4 X3 -> type). - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X4+X2=X6:plus N2 N3 N4} {X7+X6=X1:plus N1 N4 N5} {X3:nat} {X7+X4=X3:plus N1 N2 X3} {X3+X2=X1:plus X3 N3 N5} {X2+X4=X6:plus N3 N2 N4} plus-associative-converse X4+X2=X6 X7+X6=X1 X3 X7+X4=X3 X3+X2=X1 -> plus-commutative X2+X4=X6 X4+X2=X6 -> minus-associates-to-plus-converse X2+X4=X6 X7+X6=X1 X3 X3+X2=X1 X7+X4=X3. %worlds () (minus-associates-to-plus-converse X2+X4=X6 X1-X6=X7 X3 X1-X2=X3 X3-X4=X7). %total {} (minus-associates-to-plus-converse _ _ _ _ _). %theorem minus-is-zero-implies-eq : {N1:nat} {N2:nat} {N3:nat} plus N3 N2 N1 -> eq N3 z -> eq N1 N2 -> type. - : {N1:nat} minus-is-zero-implies-eq plus/z eq/ eq/. %worlds () (minus-is-zero-implies-eq X-Y=Z Z=0 X=Y). %total {} (minus-is-zero-implies-eq _ _ _). minus-implies-gt : {N1:nat} {N2:nat} {N3:nat} {N4:nat} plus N1 N2 N3 -> eq N1 (s N4) -> gt N3 N2 -> type = [N1:nat] [N2:nat] [N3:nat] [N4:nat] [P:plus N1 N2 N3] [E:eq N1 (s N4)] [G:gt N3 N2] plus-implies-gt P E G. %theorem minus-left-cancels : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X6:nat} plus X3 X2 X1 -> plus X6 X5 X4 -> eq X1 X4 -> eq X3 X6 -> eq X2 X5 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {X3+X2=X1:plus N1 N3 N5} {X6+X5=X4:plus N2 N4 N6} {X3=X6:eq N1 N2} {X1=X4:eq N5 N6} {X2=X5:eq N3 N4} plus-left-cancels X3+X2=X1 X6+X5=X4 X3=X6 X1=X4 X2=X5 -> minus-left-cancels X3+X2=X1 X6+X5=X4 X1=X4 X3=X6 X2=X5. %worlds () (minus-left-cancels X1-X2=X3 X4-X5=X6 X1=X4 X3=X6 X2=X5). %total {} (minus-left-cancels _ _ _ _ _). %theorem minus-right-cancels : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X6:nat} plus X3 X2 X1 -> plus X6 X5 X4 -> eq X2 X5 -> eq X3 X6 -> eq X1 X4 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {X3+X2=X1:plus N1 N3 N5} {X6+X5=X4:plus N2 N4 N6} {X3=X6:eq N1 N2} {X2=X5:eq N3 N4} {X1=X4:eq N5 N6} plus-deterministic X3+X2=X1 X6+X5=X4 X3=X6 X2=X5 X1=X4 -> minus-right-cancels X3+X2=X1 X6+X5=X4 X2=X5 X3=X6 X1=X4. %worlds () (minus-right-cancels X1-X2=X3 X4-X5=X6 X2=X5 X3=X6 X1=X4). %total {} (minus-right-cancels _ _ _ _ _). %theorem minus-left-inverts-gt* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} gt X2 X4 -> plus X3 X2 X1 -> plus X5 X4 X1 -> gt X5 X3 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X5+X4=X1:plus N1 N2 N3} {X3+X4=X7:plus N4 N2 N5} {X1>X7:gt N3 N5} {X5>X3:gt N1 N4} {N6:nat} {X2>X4:gt N6 N2} {X3+X2=X1:plus N4 N6 N3} plus-right-cancels-gt X5+X4=X1 X3+X4=X7 eq/ X1>X7 X5>X3 -> plus-left-preserves-gt* X2>X4 X3+X2=X1 X3+X4=X7 X1>X7 -> plus-total* N4 N2 N5 X3+X4=X7 -> minus-left-inverts-gt* X2>X4 X3+X2=X1 X5+X4=X1 X5>X3. %worlds () (minus-left-inverts-gt* X2>X4 X1-X2=X3 X1-X4=X5 X5>X3). %total {} (minus-left-inverts-gt* _ _ _ _). %theorem minus-right-preserves-gt* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} gt X1 X2 -> plus X4 X3 X1 -> plus X5 X3 X2 -> gt X4 X5 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X4+X3=X1:plus N1 N2 N3} {X5+X3=X2:plus N4 N2 N5} {X1>X2:gt N3 N5} {X4>X5:gt N1 N4} plus-right-cancels-gt X4+X3=X1 X5+X3=X2 eq/ X1>X2 X4>X5 -> minus-right-preserves-gt* X1>X2 X4+X3=X1 X5+X3=X2 X4>X5. %worlds () (minus-right-preserves-gt* X1>X2 X1-X3=X4 X2-X3=X5 X4>X5). %total {} (minus-right-preserves-gt* _ _ _ _). %theorem minus-left-cancels-inverts-gt : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X6:nat} plus X3 X2 X1 -> plus X6 X5 X4 -> eq X1 X4 -> gt X3 X6 -> gt X5 X2 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X6+X5=X1:plus N1 N2 N4} {X6+X2=X7:plus N1 N3 N5} {X1>X7:gt N4 N5} {X5>X2:gt N2 N3} {N6:nat} {X6+X5=X4:plus N1 N2 N6} {X4=X1:eq N6 N4} {X1=X4:eq N4 N6} {N7:nat} {X3>X6:gt N7 N1} {X3+X2=X1:plus N7 N3 N4} plus-left-cancels-gt X6+X5=X1 X6+X2=X7 eq/ X1>X7 X5>X2 -> plus-respects-eq X6+X5=X4 eq/ eq/ X4=X1 X6+X5=X1 -> eq-symmetric X1=X4 X4=X1 -> plus-right-preserves-gt* X3>X6 X3+X2=X1 X6+X2=X7 X1>X7 -> plus-total* N1 N3 N5 X6+X2=X7 -> minus-left-cancels-inverts-gt X3+X2=X1 X6+X5=X4 X1=X4 X3>X6 X5>X2. %worlds () (minus-left-cancels-inverts-gt X1-X2=X3 X4-X5=X6 X1=X4 X3>X6 X5>X2). %total {} (minus-left-cancels-inverts-gt _ _ _ _ _). %theorem minus-right-cancels-gt : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X6:nat} plus X3 X2 X1 -> plus X6 X5 X4 -> eq X2 X5 -> gt X3 X6 -> gt X1 X4 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X3>X6:gt N1 N2} {X3+X5=X1:plus N1 N3 N4} {X6+X5=X4:plus N2 N3 N5} {X1>X4:gt N4 N5} {N6:nat} {X3+X2=X1:plus N1 N6 N4} {X2=X5:eq N6 N3} plus-right-preserves-gt* X3>X6 X3+X5=X1 X6+X5=X4 X1>X4 -> plus-respects-eq X3+X2=X1 eq/ X2=X5 eq/ X3+X5=X1 -> minus-right-cancels-gt X3+X2=X1 X6+X5=X4 X2=X5 X3>X6 X1>X4. %worlds () (minus-right-cancels-gt X1-X2=X3 X4-X5=X6 X2=X5 X3>X6 X1>X4). %total {} (minus-right-cancels-gt _ _ _ _ _). %theorem times-right-distributes-over-minus : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X7:nat} plus X3 X2 X1 -> times X3 X4 X7 -> ({X5:nat} {X6:nat} times X1 X4 X5 -> times X2 X4 X6 -> plus X7 X6 X5 -> type). - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {Y7+X6=X5:plus N1 N3 N4} {Y7=X7:eq N1 N2} {X7+X6=X5:plus N2 N3 N4} {N5:nat} {N6:nat} {X3*X4=Y7:times N5 N6 N1} {X3*X4=X7:times N5 N6 N2} {N7:nat} {N8:nat} {X3+X2=X1:plus N5 N7 N8} {X1*X4=X5:times N8 N6 N4} {X2*X4=X6:times N7 N6 N3} plus-respects-eq Y7+X6=X5 Y7=X7 eq/ eq/ X7+X6=X5 -> times-deterministic X3*X4=Y7 X3*X4=X7 eq/ eq/ Y7=X7 -> times-right-distributes-over-plus X3+X2=X1 X1*X4=X5 N1 N3 X3*X4=Y7 X2*X4=X6 Y7+X6=X5 -> times-total* N8 N6 N4 X1*X4=X5 -> times-right-distributes-over-minus X3+X2=X1 X3*X4=X7 N4 N3 X1*X4=X5 X2*X4=X6 X7+X6=X5. %worlds () (times-right-distributes-over-minus X1-X2=X3 X3*X4=X7 X5 X6 X1*X4=X5 X2*X4=X6 X5-X6=X7). %total {} (times-right-distributes-over-minus _ _ _ _ _ _ _). %theorem times-right-distributes-over-minus* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X6:nat} {X7:nat} plus X3 X2 X1 -> times X3 X4 X7 -> times X1 X4 X5 -> times X2 X4 X6 -> plus X7 X6 X5 -> type. - : {Y5:nat} {Y6:nat} {N1:nat} {N2:nat} {N3:nat} {Y5-Y6=X7:plus N1 Y6 Y5} {Y5=X5:eq Y5 N2} {Y6=X6:eq Y6 N3} {X5-X6=X7:plus N1 N3 N2} {N4:nat} {N5:nat} {X2*X4=Y6:times N4 N5 Y6} {X2*X4=X6:times N4 N5 N3} {N6:nat} {X1*X4=Y5:times N6 N5 Y5} {X1*X4=X5:times N6 N5 N2} {N7:nat} {X1-X2=X3:plus N7 N4 N6} {X3*X4=X7:times N7 N5 N1} minus-respects-eq Y5-Y6=X7 Y5=X5 Y6=X6 eq/ X5-X6=X7 -> times-deterministic X2*X4=Y6 X2*X4=X6 eq/ eq/ Y6=X6 -> times-deterministic X1*X4=Y5 X1*X4=X5 eq/ eq/ Y5=X5 -> times-right-distributes-over-minus X1-X2=X3 X3*X4=X7 Y5 Y6 X1*X4=Y5 X2*X4=Y6 Y5-Y6=X7 -> times-right-distributes-over-minus* X1-X2=X3 X3*X4=X7 X1*X4=X5 X2*X4=X6 X5-X6=X7. %worlds () (times-right-distributes-over-minus* X1-X2=X3 X3*X4=X7 X1*X4=X5 X2*X4=X6 X5-X6=X7). %total {} (times-right-distributes-over-minus* _ _ _ _ _). %theorem times-left-distributes-over-minus* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X6:nat} {X7:nat} plus X6 X4 X2 -> times X1 X6 X7 -> times X1 X2 X3 -> times X1 X4 X5 -> plus X7 X5 X3 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {N7:nat} {X2-X4=X6:plus N3 N2 N1} {X6*X1=X7:times N3 N4 N7} {X2*X1=X3:times N1 N4 N5} {X4*X1=X5:times N2 N4 N6} {X3-X5=X7:plus N7 N6 N5} {X1*X4=X5:times N4 N2 N6} {X1*X2=X3:times N4 N1 N5} {X1*X6=X7:times N4 N3 N7} times-right-distributes-over-minus* X2-X4=X6 X6*X1=X7 X2*X1=X3 X4*X1=X5 X3-X5=X7 -> times-commutative X1*X4=X5 X4*X1=X5 -> times-commutative X1*X2=X3 X2*X1=X3 -> times-commutative X1*X6=X7 X6*X1=X7 -> times-left-distributes-over-minus* X2-X4=X6 X1*X6=X7 X1*X2=X3 X1*X4=X5 X3-X5=X7. %worlds () (times-left-distributes-over-minus* X2-X4=X6 X1*X6=X7 X1*X2=X3 X1*X4=X5 X3-X5=X7). %total {} (times-left-distributes-over-minus* _ _ _ _ _). %theorem times-left-distributes-over-minus : {X1:nat} {X2:nat} {X4:nat} {X6:nat} {X7:nat} plus X6 X4 X2 -> times X1 X6 X7 -> ({X3:nat} {X5:nat} times X1 X2 X3 -> times X1 X4 X5 -> plus X7 X5 X3 -> type). - : {N1:nat} {N2:nat} {X3:nat} {N3:nat} {X5:nat} {N4:nat} {N5:nat} {X2-X4=X6:plus N4 N3 N2} {X1*X6=X7:times N1 N4 N5} {X1*X2=X3:times N1 N2 X3} {X1*X4=X5:times N1 N3 X5} {X3-X5=X7:plus N5 X5 X3} times-left-distributes-over-minus* X2-X4=X6 X1*X6=X7 X1*X2=X3 X1*X4=X5 X3-X5=X7 -> times-total* N1 N3 X5 X1*X4=X5 -> times-total* N1 N2 X3 X1*X2=X3 -> times-left-distributes-over-minus X2-X4=X6 X1*X6=X7 X3 X5 X1*X2=X3 X1*X4=X5 X3-X5=X7. %worlds () (times-left-distributes-over-minus X2-X4=X6 X1*X6=X7 X3 X5 X1*X2=X3 X1*X4=X5 X3-X5=X7). %total {} (times-left-distributes-over-minus _ _ _ _ _ _ _). %theorem times-right-factors-over-minus* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X6:nat} {X7:nat} times X1 X4 X5 -> times X2 X4 X6 -> plus X7 X6 X5 -> plus X3 X2 X1 -> times X3 X4 X7 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {X3*X4=Y7:times N1 N2 N3} {Y7=X7:eq N3 N4} {X3*X4=X7:times N1 N2 N4} {N5:nat} {N6:nat} {X5-X6=Y7:plus N3 N6 N5} {X5-X6=X7:plus N4 N6 N5} {N7:nat} {N8:nat} {X1-X2=X3:plus N1 N8 N7} {X1*X4=X5:times N7 N2 N5} {X2*X4=X6:times N8 N2 N6} times-respects-eq X3*X4=Y7 eq/ eq/ Y7=X7 X3*X4=X7 -> minus-deterministic X5-X6=Y7 X5-X6=X7 eq/ eq/ Y7=X7 -> times-right-distributes-over-minus* X1-X2=X3 X3*X4=Y7 X1*X4=X5 X2*X4=X6 X5-X6=Y7 -> times-total* N1 N2 N3 X3*X4=Y7 -> times-right-factors-over-minus* X1*X4=X5 X2*X4=X6 X5-X6=X7 X1-X2=X3 X3*X4=X7. %worlds () (times-right-factors-over-minus* X1*X4=X5 X2*X4=X6 X5-X6=X7 X1-X2=X3 X3*X4=X7). %total {} (times-right-factors-over-minus* _ _ _ _ _). %theorem times-left-factors-over-minus* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} {X6:nat} {X7:nat} times X1 X2 X3 -> times X1 X4 X5 -> plus X7 X5 X3 -> plus X6 X4 X2 -> times X1 X6 X7 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {X1*X6=Y7:times N1 N2 N3} {Y7=X7:eq N3 N4} {X1*X6=X7:times N1 N2 N4} {N5:nat} {N6:nat} {X3-X5=Y7:plus N3 N6 N5} {X3-X5=X7:plus N4 N6 N5} {N7:nat} {N8:nat} {X2-X4=X6:plus N2 N8 N7} {X1*X2=X3:times N1 N7 N5} {X1*X4=X5:times N1 N8 N6} times-respects-eq X1*X6=Y7 eq/ eq/ Y7=X7 X1*X6=X7 -> minus-deterministic X3-X5=Y7 X3-X5=X7 eq/ eq/ Y7=X7 -> times-left-distributes-over-minus* X2-X4=X6 X1*X6=Y7 X1*X2=X3 X1*X4=X5 X3-X5=Y7 -> times-total* N1 N2 N3 X1*X6=Y7 -> times-left-factors-over-minus* X1*X2=X3 X1*X4=X5 X3-X5=X7 X2-X4=X6 X1*X6=X7. %worlds () (times-left-factors-over-minus* X1*X2=X3 X1*X4=X5 X3-X5=X7 X2-X4=X6 X1*X6=X7). %total {} (times-left-factors-over-minus* _ _ _ _ _). %theorem times-right-factors-over-minus : {Y:nat} {Z:nat} {XY:nat} {XZ:nat} {YZ:nat} {XYZ:nat} {Z-:nat} times XY Z XYZ -> times Y Z YZ -> plus XZ YZ XYZ -> eq Z (s Z-) -> ({X:nat} plus X Y XY -> times X Z XZ -> type). - : {N1:nat} {N2:nat} {XY=Y:eq N1 N2} {ZERO+Y=XY:plus z N2 N1} {N3:nat} {N4:nat} {XY*Z=YZ:times N1 (s N3) N4} {Y*Z=YZ:times N2 (s N3) N4} plus-respects-eq plus/z eq/ XY=Y eq/ ZERO+Y=XY -> times-right-cancels* XY*Z=YZ Y*Z=YZ eq/ eq/ XY=Y -> times-right-factors-over-minus XY*Z=YZ Y*Z=YZ plus/z eq/ z ZERO+Y=XY times/z. - : {N1:nat} {N2:nat} {X-:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {XY*Z=XYZ:times N1 N3 N4} {Y*Z=YZ:times N2 N3 N5} {XZ+YZ=XYZ:plus (s N6) N5 N4} {X+Y=XY:plus (s X-) N2 N1} {X*Z=XZ:times (s X-) N3 (s N6)} {XY>Y:gt N1 N2} {XYZ>YZ:gt N4 N5} {N7:nat} {X1:eq N3 (s N7)} times-right-factors-over-minus* XY*Z=XYZ Y*Z=YZ XZ+YZ=XYZ X+Y=XY X*Z=XZ -> gt-implies-plus XY>Y X- X+Y=XY -> times-right-cancels-gt XY*Z=XYZ Y*Z=YZ eq/ XYZ>YZ XY>Y -> plus-implies-gt XZ+YZ=XYZ eq/ XYZ>YZ -> times-right-factors-over-minus XY*Z=XYZ Y*Z=YZ XZ+YZ=XYZ X1 (s X-) X+Y=XY X*Z=XZ. %worlds () (times-right-factors-over-minus XY*Z=XYZ Y*Z=YZ XYZ-YZ=XZ Z+ X XY-Y=X X*Z=XZ). %total {} (times-right-factors-over-minus _ _ _ _ _ _ _). %theorem times-left-factors-over-minus : {X:nat} {Y:nat} {Z:nat} {XY:nat} {XZ:nat} {XYZ:nat} {X-:nat} times X Y XY -> times X Z XZ -> plus XYZ XZ XY -> eq X (s X-) -> ({YZ:nat} plus YZ Z Y -> times X YZ XYZ -> type). - : {YZ:nat} {N1:nat} {N2:nat} {YZ*X=XYZ:times YZ N1 N2} {X*YZ=XYZ:times N1 YZ N2} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {N7:nat} {Y*X=XY:times N4 N1 N6} {Z*X=XZ:times N3 N1 N5} {XY-XZ=XYZ:plus N2 N5 N6} {X=sX-:eq N1 (s N7)} {Y-Z=YZ:plus YZ N3 N4} {X*Z=XZ:times N1 N3 N5} {X*Y=XY:times N1 N4 N6} times-commutative YZ*X=XYZ X*YZ=XYZ -> times-right-factors-over-minus Y*X=XY Z*X=XZ XY-XZ=XYZ X=sX- YZ Y-Z=YZ YZ*X=XYZ -> times-commutative X*Z=XZ Z*X=XZ -> times-commutative X*Y=XY Y*X=XY -> times-left-factors-over-minus X*Y=XY X*Z=XZ XY-XZ=XYZ X=sX- YZ Y-Z=YZ X*YZ=XYZ. %worlds () (times-left-factors-over-minus X*Y=XY X*Z=XZ XY-XZ=XYZ X=sX- YZ Y-Z=YZ X*YZ=XYZ). %total {} (times-left-factors-over-minus _ _ _ _ _ _ _). ge : nat -> nat -> type. ge/= : {X:nat} {Y:nat} eq X Y -> ge X Y. ge/> : {X:nat} {Y:nat} gt X Y -> ge X Y. %theorem false-implies-ge : {X1:nat} {X2:nat} void -> ge X1 X2 -> type. %worlds () (false-implies-ge _ _). %total {} (false-implies-ge _ _). %theorem ge-respects-eq : {X1:nat} {X2:nat} {Y1:nat} {Y2:nat} ge X1 X2 -> eq X1 Y1 -> eq X2 Y2 -> ge Y1 Y2 -> type. - : {N1:nat} {N2:nat} {X1>=X2:ge N1 N2} ge-respects-eq X1>=X2 eq/ eq/ X1>=X2. %worlds () (ge-respects-eq _ _ _ _). %total {} (ge-respects-eq _ _ _ _). %theorem ge-reflexive : {X:nat} ge X X -> type. - : {N1:nat} ge-reflexive N1 (ge/= eq/). %worlds () (ge-reflexive X X>=X). %total {} (ge-reflexive _ _). %theorem ge-transitive : {X1:nat} {X2:nat} {X3:nat} ge X1 X2 -> ge X2 X3 -> ge X1 X3 -> type. - : {N1:nat} ge-transitive (ge/= eq/) (ge/= eq/) (ge/= eq/). - : {N1:nat} {N2:nat} {X>X3:gt N1 N2} ge-transitive (ge/= eq/) (ge/> X>X3) (ge/> X>X3). - : {N1:nat} {N2:nat} {X1>X:gt N1 N2} ge-transitive (ge/> X1>X) (ge/= eq/) (ge/> X1>X). - : {N1:nat} {N2:nat} {N3:nat} {X1>X2:gt N1 N2} {X2>X3:gt N2 N3} {X1>X3:gt N1 N3} gt-transitive X1>X2 X2>X3 X1>X3 -> ge-transitive (ge/> X1>X2) (ge/> X2>X3) (ge/> X1>X3). %worlds () (ge-transitive X1>=X2 X2>=X3 X1>=X3). %total {} (ge-transitive _ _ _). %theorem ge-anti-symmetric : {X1:nat} {X2:nat} ge X1 X2 -> ge X2 X1 -> eq X1 X2 -> type. - : {N1:nat} {X1:ge N1 N1} ge-anti-symmetric (ge/= eq/) X1 eq/. - : {N1:nat} {X1:ge N1 N1} ge-anti-symmetric X1 (ge/= eq/) eq/. - : {N1:nat} {N2:nat} {F:void} {X1=X2:eq N1 N2} {X1>X2:gt N1 N2} {X2>X1:gt N2 N1} false-implies-eq F X1=X2 -> gt-anti-symmetric X1>X2 X2>X1 F -> ge-anti-symmetric (ge/> X1>X2) (ge/> X2>X1) X1=X2. %worlds () (ge-anti-symmetric X1>=X2 X2>=X1 X1=X2). %total {} (ge-anti-symmetric _ _ _). %theorem ge-transitive-gt : {X1:nat} {X2:nat} {X3:nat} ge X1 X2 -> gt X2 X3 -> gt X1 X3 -> type. - : {N1:nat} {N2:nat} {X>X3:gt N1 N2} ge-transitive-gt (ge/= eq/) X>X3 X>X3. - : {N1:nat} {N2:nat} {N3:nat} {X1>X2:gt N1 N2} {X2>X3:gt N2 N3} {X1>X3:gt N1 N3} gt-transitive X1>X2 X2>X3 X1>X3 -> ge-transitive-gt (ge/> X1>X2) X2>X3 X1>X3. %worlds () (ge-transitive-gt X1>=X2 X2>X3 X1>X3). %total {} (ge-transitive-gt _ _ _). %theorem gt-transitive-ge : {X1:nat} {X2:nat} {X3:nat} gt X1 X2 -> ge X2 X3 -> gt X1 X3 -> type. - : {N1:nat} {N2:nat} {X1>X2:gt N1 N2} gt-transitive-ge X1>X2 (ge/= eq/) X1>X2. - : {N1:nat} {N2:nat} {N3:nat} {X1>X2:gt N1 N2} {X2>X3:gt N2 N3} {X1>X3:gt N1 N3} gt-transitive X1>X2 X2>X3 X1>X3 -> gt-transitive-ge X1>X2 (ge/> X2>X3) X1>X3. %worlds () (gt-transitive-ge X1>X2 X2>=X3 X1>X3). %total {} (gt-transitive-ge _ _ _). %theorem meta-ge : {M:nat} {N:nat} ge M N -> type. - : {N1:nat} meta-ge N1 N1 (ge/= eq/). - : {N1:nat} {N2:nat} {M>N:gt N1 N2} meta-gt N1 N2 M>N -> meta-ge N1 N2 (ge/> M>N). %worlds () (meta-ge _ _ _). %total {} (meta-ge _ _ _). %reduces N <= M (meta-ge M N _). %theorem succ-preserves-ge : {M:nat} {N:nat} ge M N -> ge (s M) (s N) -> type. - : {N1:nat} succ-preserves-ge (ge/= eq/) (ge/= eq/). - : {N1:nat} {N2:nat} {N>M:gt N1 N2} {N+1>M+1:gt (s N1) (s N2)} succ-preserves-gt N>M N+1>M+1 -> succ-preserves-ge (ge/> N>M) (ge/> N+1>M+1). %worlds () (succ-preserves-ge M>=N M+1>=N+1). %total {} (succ-preserves-ge _ _). %theorem succ-preserves-ge-converse : {M:nat} {N:nat} ge (s M) (s N) -> ge M N -> type. - : {N1:nat} succ-preserves-ge-converse (ge/= eq/) (ge/= eq/). - : {N1:nat} {N2:nat} {N+1>M+1:gt (s N1) (s N2)} {N>M:gt N1 N2} succ-preserves-gt-converse N+1>M+1 N>M -> succ-preserves-ge-converse (ge/> N+1>M+1) (ge/> N>M). %worlds () (succ-preserves-ge-converse M+1>=N+1 M>=N). %total {} (succ-preserves-ge-converse _ _). %theorem ge-succ-implies-gt : {N1:nat} {N2:nat} ge N1 (s N2) -> gt N1 N2 -> type. - : {N1:nat} ge-succ-implies-gt (ge/= eq/) gt/1. - : {N1:nat} {N2:nat} {N1>sN2:gt N1 (s N2)} {N1>N2:gt N1 N2} gt-transitive N1>sN2 gt/1 N1>N2 -> ge-succ-implies-gt (ge/> N1>sN2) N1>N2. %worlds () (ge-succ-implies-gt _ _). %total {} (ge-succ-implies-gt _ _). %theorem ge-implies-succ-gt : {N1:nat} {N2:nat} ge N1 N2 -> gt (s N1) N2 -> type. - : {N1:nat} {N2:nat} {N1+1>=N2+1:ge (s N1) (s N2)} {N1+1>N2:gt (s N1) N2} {N1>=N2:ge N1 N2} ge-succ-implies-gt N1+1>=N2+1 N1+1>N2 -> succ-preserves-ge N1>=N2 N1+1>=N2+1 -> ge-implies-succ-gt N1>=N2 N1+1>N2. %worlds () (ge-implies-succ-gt _ _). %total {} (ge-implies-succ-gt _ _). %theorem succ-gt-implies-ge : {N1:nat} {N2:nat} gt (s N1) N2 -> ge N1 N2 -> type. - : {N1:nat} succ-gt-implies-ge gt/1 (ge/= eq/). - : {N1:nat} {N2:nat} {N1>N2:gt N1 N2} succ-gt-implies-ge (gt/> N1>N2) (ge/> N1>N2). %worlds () (succ-gt-implies-ge _ _). %total {} (succ-gt-implies-ge _ _). %theorem gt-implies-ge-succ : {N1:nat} {N2:nat} gt N1 N2 -> ge N1 (s N2) -> type. - : {N1:nat} {N2:nat} {N1+1>N2+1:gt (s N1) (s N2)} {N1>=N2+1:ge N1 (s N2)} {N1>N2:gt N1 N2} succ-gt-implies-ge N1+1>N2+1 N1>=N2+1 -> succ-preserves-gt N1>N2 N1+1>N2+1 -> gt-implies-ge-succ N1>N2 N1>=N2+1. %worlds () (gt-implies-ge-succ _ _). %total {} (gt-implies-ge-succ _ _). %theorem ge-implies-plus : {N1:nat} {N2:nat} ge N2 N1 -> ({N0:nat} plus N0 N1 N2 -> type). - : {N1:nat} ge-implies-plus (ge/= eq/) z plus/z. - : {N1:nat} {N2:nat} {N2>N1:gt N1 N2} {N0:nat} {P:plus (s N0) N2 N1} gt-implies-plus N2>N1 N0 P -> ge-implies-plus (ge/> N2>N1) (s N0) P. %worlds () (ge-implies-plus N2>=N1 N0 N0+N1=N2). %total {} (ge-implies-plus _ _ _). %theorem plus-implies-ge : {N0:nat} {N1:nat} {N2:nat} plus N0 N1 N2 -> ge N2 N1 -> type. - : {N1:nat} plus-implies-ge plus/z (ge/= eq/). - : {N1:nat} {N2:nat} {N3:nat} {P:plus (s N1) N2 N3} {N2>N1:gt N3 N2} plus-implies-gt P eq/ N2>N1 -> plus-implies-ge P (ge/> N2>N1). %worlds () (plus-implies-ge N0+N1=N2 N2>=N1). %total {} (plus-implies-ge _ _). %theorem ge-zero-always : {N:nat} ge N z -> type. - : {N1:nat} {N+0=N:plus N1 z N1} {N>=0:ge N1 z} plus-implies-ge N+0=N N>=0 -> plus-right-identity N1 N+0=N -> ge-zero-always N1 N>=0. %worlds () (ge-zero-always _ _). %total {} (ge-zero-always _ _). %theorem nonzero-times-implies-ge : {N0:nat} {N1:nat} {N2:nat} times (s N0) N1 N2 -> ge N2 N1 -> type. - : {N1:nat} {N2:nat} {N3:nat} {X+N1=N2:plus N1 N2 N3} {N2>=N1:ge N3 N2} {N4:nat} {X1:times N4 N2 N1} plus-implies-ge X+N1=N2 N2>=N1 -> nonzero-times-implies-ge (times/s X1 X+N1=N2) N2>=N1. %worlds () (nonzero-times-implies-ge N0*N1=N2 N2>=N1). %total {} (nonzero-times-implies-ge _ _). %theorem times-nonzero-implies-ge : {N0:nat} {N1:nat} {N2:nat} times N0 (s N1) N2 -> ge N2 N0 -> type. - : {N1:nat} {N2:nat} {N3:nat} {B*A=C:times (s N1) N2 N3} {C>=A:ge N3 N2} {A*B=C:times N2 (s N1) N3} nonzero-times-implies-ge B*A=C C>=A -> times-commutative A*B=C B*A=C -> times-nonzero-implies-ge A*B=C C>=A. %worlds () (times-nonzero-implies-ge _ _). %total {} (times-nonzero-implies-ge _ _). %theorem non-trivial-times-implies-much-gt* : {N1:nat} {N2:nat} {N3:nat} times (s (s N1)) (s (s N2)) N3 -> gt N3 (s (s (s N1))) -> type. - : {N1:nat} {N2:nat} {N3:nat} {N3>sP2:gt N1 (s N2)} {SP2>=sssN1:ge (s N2) (s (s (s N3)))} {N3>sssN1:gt N1 (s (s (s N3)))} {N4:nat} {SN2+sP2=N3:plus (s N4) (s N2) N1} {SSN2+P2=N3:plus (s (s N4)) N2 N1} {P2+ssN2=N3:plus N2 (s (s N4)) N1} {SP2>ssN1:gt (s N2) (s (s N3))} {P2>sN1:gt N2 (s N3)} {N5:nat} {P2>sP1:gt N2 (s N5)} {SP1>=sN1:ge (s N5) (s N3)} {SN2+sP1=P2:plus (s N4) (s N5) N2} {SP1+sN2=P2:plus (s N5) (s N4) N2} {P1+ssN2=P2:plus N5 (s (s N4)) N2} {P1>=N1:ge N5 N3} {N1*ssN2=P1:times N3 (s (s N4)) N5} gt-transitive-ge N3>sP2 SP2>=sssN1 N3>sssN1 -> plus-implies-gt SN2+sP2=N3 eq/ N3>sP2 -> plus-swap-succ SSN2+P2=N3 SN2+sP2=N3 -> plus-commutative P2+ssN2=N3 SSN2+P2=N3 -> gt-implies-ge-succ SP2>ssN1 SP2>=sssN1 -> succ-preserves-gt P2>sN1 SP2>ssN1 -> gt-transitive-ge P2>sP1 SP1>=sN1 P2>sN1 -> plus-implies-gt SN2+sP1=P2 eq/ P2>sP1 -> plus-commutative SP1+sN2=P2 SN2+sP1=P2 -> plus-swap-succ-converse P1+ssN2=P2 SP1+sN2=P2 -> succ-preserves-ge P1>=N1 SP1>=sN1 -> times-nonzero-implies-ge N1*ssN2=P1 P1>=N1 -> non-trivial-times-implies-much-gt* (times/s (times/s N1*ssN2=P1 P1+ssN2=P2) P2+ssN2=N3) N3>sssN1. %worlds () (non-trivial-times-implies-much-gt* _ _). %total {} (non-trivial-times-implies-much-gt* _ _). %theorem non-trivial-times-implies-much-gt : {N1:nat} {N2:nat} {N3:nat} times (s (s N1)) (s (s N2)) N3 -> gt N3 (s (s (s N1))) -> gt N3 (s (s (s N2))) -> type. - : {N1:nat} {N2:nat} {N3:nat} {Tc:times (s (s N1)) (s (s N2)) N3} {G2:gt N3 (s (s (s N1)))} {T:times (s (s N2)) (s (s N1)) N3} {G1:gt N3 (s (s (s N2)))} non-trivial-times-implies-much-gt* Tc G2 -> times-commutative T Tc -> non-trivial-times-implies-much-gt* T G1 -> non-trivial-times-implies-much-gt T G1 G2. %worlds () (non-trivial-times-implies-much-gt _ _ _). %total {} (non-trivial-times-implies-much-gt _ _ _). %theorem plus-left-preserves-ge* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} ge X2 X4 -> plus X1 X2 X3 -> plus X1 X4 X5 -> ge X3 X5 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {X1+X2=X3:plus N1 N2 N3} {X1+X2=X5:plus N1 N2 N4} {X3=X5:eq N3 N4} plus-deterministic X1+X2=X3 X1+X2=X5 eq/ eq/ X3=X5 -> plus-left-preserves-ge* (ge/= eq/) X1+X2=X3 X1+X2=X5 (ge/= X3=X5). - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X2>X4:gt N2 N3} {X1+X2=X3:plus N1 N2 N4} {X1+X4=X5:plus N1 N3 N5} {X3>X5:gt N4 N5} plus-left-preserves-gt* X2>X4 X1+X2=X3 X1+X4=X5 X3>X5 -> plus-left-preserves-ge* (ge/> X2>X4) X1+X2=X3 X1+X4=X5 (ge/> X3>X5). %worlds () (plus-left-preserves-ge* X2>=X4 X1+X2=X3 X1+X4=X5 X3>=X5). %total {} (plus-left-preserves-ge* _ _ _ _). %theorem plus-left-cancels-ge : {X1:nat} {X2:nat} {X3:nat} {Y1:nat} {Y2:nat} {Y3:nat} plus X1 X2 X3 -> plus Y1 Y2 Y3 -> eq X1 Y1 -> ge X3 Y3 -> ge X2 Y2 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {X1+X2=X3:plus N1 N2 N4} {X1+Y2=X3:plus N1 N3 N4} {X2=Y2:eq N2 N3} plus-left-cancels X1+X2=X3 X1+Y2=X3 eq/ eq/ X2=Y2 -> plus-left-cancels-ge X1+X2=X3 X1+Y2=X3 eq/ (ge/= eq/) (ge/= X2=Y2). - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X1+X2=X3:plus N1 N2 N4} {X1+Y2=Y3:plus N1 N3 N5} {X3>Y3:gt N4 N5} {X2>Y2:gt N2 N3} plus-left-cancels-gt X1+X2=X3 X1+Y2=Y3 eq/ X3>Y3 X2>Y2 -> plus-left-cancels-ge X1+X2=X3 X1+Y2=Y3 eq/ (ge/> X3>Y3) (ge/> X2>Y2). %worlds () (plus-left-cancels-ge X1+X2=X3 Y1+Y2=Y3 X1=Y1 X3>=Y3 X2>=Y2). %total {} (plus-left-cancels-ge _ _ _ _ _). %theorem plus-left-preserves-ge : {X1:nat} {X2:nat} {X4:nat} ge X2 X4 -> ({X3:nat} {X5:nat} plus X1 X2 X3 -> plus X1 X4 X5 -> ge X3 X5 -> type). - : {N1:nat} {N2:nat} {X3:nat} {N3:nat} {X5:nat} {X2>=X4:ge N2 N3} {X1+X2=A3:plus N1 N2 X3} {X1+X4=X5:plus N1 N3 X5} {X3>=X5:ge X3 X5} plus-left-preserves-ge* X2>=X4 X1+X2=A3 X1+X4=X5 X3>=X5 -> plus-total* N1 N3 X5 X1+X4=X5 -> plus-total* N1 N2 X3 X1+X2=A3 -> plus-left-preserves-ge X2>=X4 X3 X5 X1+X2=A3 X1+X4=X5 X3>=X5. %worlds () (plus-left-preserves-ge X2>=X4 X3 X5 X1+X2=A3 X1+X4=X5 X3>=X5). %total {} (plus-left-preserves-ge _ _ _ _ _ _). %theorem plus-right-preserves-ge* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} ge X1 X2 -> plus X1 X3 X4 -> plus X2 X3 X5 -> ge X4 X5 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X1>=X2:ge N2 N4} {X3+X1=X4:plus N1 N2 N3} {X3+X2=X5:plus N1 N4 N5} {X4>=X5:ge N3 N5} {X2+X3=X5:plus N4 N1 N5} {X1+X3=X4:plus N2 N1 N3} plus-left-preserves-ge* X1>=X2 X3+X1=X4 X3+X2=X5 X4>=X5 -> plus-commutative X2+X3=X5 X3+X2=X5 -> plus-commutative X1+X3=X4 X3+X1=X4 -> plus-right-preserves-ge* X1>=X2 X1+X3=X4 X2+X3=X5 X4>=X5. %worlds () (plus-right-preserves-ge* X1>=X2 X1+X3=X4 X2+X3=X5 X4>=X5). %total {} (plus-right-preserves-ge* _ _ _ _). %theorem plus-right-preserves-ge : {X1:nat} {X2:nat} {X3:nat} ge X1 X2 -> ({X4:nat} {X5:nat} plus X1 X3 X4 -> plus X2 X3 X5 -> ge X4 X5 -> type). - : {N1:nat} {N2:nat} {N3:nat} {X4:nat} {X5:nat} {X1>=X2:ge N1 N2} {X1+X3=X4:plus N1 N3 X4} {X2+X3=X5:plus N2 N3 X5} {X4>=X5:ge X4 X5} plus-right-preserves-ge* X1>=X2 X1+X3=X4 X2+X3=X5 X4>=X5 -> plus-total* N2 N3 X5 X2+X3=X5 -> plus-total* N1 N3 X4 X1+X3=X4 -> plus-right-preserves-ge X1>=X2 X4 X5 X1+X3=X4 X2+X3=X5 X4>=X5. %worlds () (plus-right-preserves-ge X1>=X2 X4 X5 X1+X3=X4 X2+X3=X5 X4>=X5). %total {} (plus-right-preserves-ge _ _ _ _ _ _). %theorem plus-preserves-ge* : {X1:nat} {X2:nat} {X3:nat} {Y1:nat} {Y2:nat} {Y3:nat} ge X1 Y1 -> ge X2 Y2 -> plus X1 X2 X3 -> plus Y1 Y2 Y3 -> ge X3 Y3 -> type. - : {N1:nat} {N2:nat} {N3:nat} {X3>=X:ge N1 N2} {X>=Y3:ge N2 N3} {X3>=Y3:ge N1 N3} {N4:nat} {N5:nat} {N6:nat} {X2>=Y2:ge N5 N6} {Y1+X2=X:plus N4 N5 N2} {Y1+Y2=Y3:plus N4 N6 N3} {N7:nat} {X1>=Y1:ge N7 N4} {X1+X2=X3:plus N7 N5 N1} ge-transitive X3>=X X>=Y3 X3>=Y3 -> plus-left-preserves-ge* X2>=Y2 Y1+X2=X Y1+Y2=Y3 X>=Y3 -> plus-right-preserves-ge* X1>=Y1 X1+X2=X3 Y1+X2=X X3>=X -> plus-total* N4 N5 N2 Y1+X2=X -> plus-preserves-ge* X1>=Y1 X2>=Y2 X1+X2=X3 Y1+Y2=Y3 X3>=Y3. %worlds () (plus-preserves-ge* X1>=Y1 X2>=Y2 X1+X2=X3 Y1+Y2=Y3 X3>=Y3). %total {} (plus-preserves-ge* _ _ _ _ _). %theorem plus-preserves-ge : {X1:nat} {X2:nat} {Y1:nat} {Y2:nat} ge X1 Y1 -> ge X2 Y2 -> ({X3:nat} {Y3:nat} plus X1 X2 X3 -> plus Y1 Y2 Y3 -> ge X3 Y3 -> type). - : {N1:nat} {N2:nat} {X3:nat} {N3:nat} {N4:nat} {Y3:nat} {X1>=Y1:ge N1 N3} {X2>=Y2:ge N2 N4} {X1+X2=X3:plus N1 N2 X3} {Y1+Y2=Y3:plus N3 N4 Y3} {X3>=Y3:ge X3 Y3} plus-preserves-ge* X1>=Y1 X2>=Y2 X1+X2=X3 Y1+Y2=Y3 X3>=Y3 -> plus-total* N3 N4 Y3 Y1+Y2=Y3 -> plus-total* N1 N2 X3 X1+X2=X3 -> plus-preserves-ge X1>=Y1 X2>=Y2 X3 Y3 X1+X2=X3 Y1+Y2=Y3 X3>=Y3. %worlds () (plus-preserves-ge X1>=Y1 X2>=Y2 X3 Y3 X1+X2=X3 Y1+Y2=Y3 X3>=Y3). %total {} (plus-preserves-ge _ _ _ _ _ _ _). %theorem plus-right-cancels-ge : {X1:nat} {X2:nat} {X3:nat} {Y1:nat} {Y2:nat} {Y3:nat} plus X1 X2 X3 -> plus Y1 Y2 Y3 -> eq X2 Y2 -> ge X3 Y3 -> ge X1 Y1 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {X2+X1=X3:plus N1 N2 N3} {Y2+Y1=Y3:plus N4 N5 N6} {X2=Y2:eq N1 N4} {X3>=Y3:ge N3 N6} {X1>=Y1:ge N2 N5} {Y1+Y2=Y3:plus N5 N4 N6} {X1+X2=X3:plus N2 N1 N3} plus-left-cancels-ge X2+X1=X3 Y2+Y1=Y3 X2=Y2 X3>=Y3 X1>=Y1 -> plus-commutative Y1+Y2=Y3 Y2+Y1=Y3 -> plus-commutative X1+X2=X3 X2+X1=X3 -> plus-right-cancels-ge X1+X2=X3 Y1+Y2=Y3 X2=Y2 X3>=Y3 X1>=Y1. %worlds () (plus-right-cancels-ge X1+X2=X3 Y1+Y2=Y3 X2=Y2 X3>=Y3 X1>=Y1). %total {} (plus-right-cancels-ge _ _ _ _ _). %theorem times-left-preserves-ge* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} ge X2 X4 -> times X1 X2 X3 -> times X1 X4 X5 -> ge X3 X5 -> type. - : {N1:nat} {N2:nat} {X1:ge N1 N2} times-left-preserves-ge* X1 times/z times/z (ge/= eq/). - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {X1*X2=X3:times N1 N2 N3} {X1*X2=X5:times N1 N2 N4} {X3=X5:eq N3 N4} times-deterministic X1*X2=X3 X1*X2=X5 eq/ eq/ X3=X5 -> times-left-preserves-ge* (ge/= eq/) X1*X2=X3 X1*X2=X5 (ge/= X3=X5). - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X2>X4:gt N2 N3} {X1*X2=X3:times (s N1) N2 N4} {X1*X4=X5:times (s N1) N3 N5} {X3>X5:gt N4 N5} times-left-preserves-gt X2>X4 X1*X2=X3 X1*X4=X5 X3>X5 -> times-left-preserves-ge* (ge/> X2>X4) X1*X2=X3 X1*X4=X5 (ge/> X3>X5). %worlds () (times-left-preserves-ge* X2>=X4 X1*X2=X3 X1*X4=X5 X3>=X5). %total {} (times-left-preserves-ge* _ _ _ _). %theorem times-left-preserves-ge : {X1:nat} {X2:nat} {X4:nat} ge X2 X4 -> ({X3:nat} {X5:nat} times X1 X2 X3 -> times X1 X4 X5 -> ge X3 X5 -> type). - : {N1:nat} {N2:nat} {X3:nat} {N3:nat} {X5:nat} {X2>=X4:ge N2 N3} {X1*X2=A3:times N1 N2 X3} {X1*X4=X5:times N1 N3 X5} {X3>=X5:ge X3 X5} times-left-preserves-ge* X2>=X4 X1*X2=A3 X1*X4=X5 X3>=X5 -> times-total* N1 N3 X5 X1*X4=X5 -> times-total* N1 N2 X3 X1*X2=A3 -> times-left-preserves-ge X2>=X4 X3 X5 X1*X2=A3 X1*X4=X5 X3>=X5. %worlds () (times-left-preserves-ge X2>=X4 X3 X5 X1*X2=A3 X1*X4=X5 X3>=X5). %total {} (times-left-preserves-ge _ _ _ _ _ _). %theorem times-right-preserves-ge* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} ge X1 X2 -> times X1 X3 X4 -> times X2 X3 X5 -> ge X4 X5 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X1>=X2:ge N2 N4} {X3*X1=X4:times N1 N2 N3} {X3*X2=X5:times N1 N4 N5} {X4>=X5:ge N3 N5} {X2*X3=X5:times N4 N1 N5} {X1*X3=X4:times N2 N1 N3} times-left-preserves-ge* X1>=X2 X3*X1=X4 X3*X2=X5 X4>=X5 -> times-commutative X2*X3=X5 X3*X2=X5 -> times-commutative X1*X3=X4 X3*X1=X4 -> times-right-preserves-ge* X1>=X2 X1*X3=X4 X2*X3=X5 X4>=X5. %worlds () (times-right-preserves-ge* X1>=X2 X1*X3=X4 X2*X3=X5 X4>=X5). %total {} (times-right-preserves-ge* _ _ _ _). %theorem times-right-preserves-ge : {X1:nat} {X2:nat} {X3:nat} ge X1 X2 -> ({X4:nat} {X5:nat} times X1 X3 X4 -> times X2 X3 X5 -> ge X4 X5 -> type). - : {N1:nat} {N2:nat} {N3:nat} {X4:nat} {X5:nat} {X1>=X2:ge N1 N2} {X1*X3=X4:times N1 N3 X4} {X2*X3=X5:times N2 N3 X5} {X4>=X5:ge X4 X5} times-right-preserves-ge* X1>=X2 X1*X3=X4 X2*X3=X5 X4>=X5 -> times-total* N2 N3 X5 X2*X3=X5 -> times-total* N1 N3 X4 X1*X3=X4 -> times-right-preserves-ge X1>=X2 X4 X5 X1*X3=X4 X2*X3=X5 X4>=X5. %worlds () (times-right-preserves-ge X1>=X2 X4 X5 X1*X3=X4 X2*X3=X5 X4>=X5). %total {} (times-right-preserves-ge _ _ _ _ _ _). ne : nat -> nat -> type. ne/< : {Y:nat} {X:nat} gt Y X -> ne X Y. ne/> : {X:nat} {Y:nat} gt X Y -> ne X Y. eq? : nat -> nat -> bool -> type. eq?/yes : {X:nat} eq? X X true. eq?/no : {X:nat} {Y:nat} ne X Y -> eq? X Y false. %theorem false-implies-ne : {X1:nat} {X2:nat} void -> ne X1 X2 -> type. %worlds () (false-implies-ne _ _). %total {} (false-implies-ne _ _). %theorem ne-respects-eq : {X1:nat} {X2:nat} {Y1:nat} {Y2:nat} ne X1 X2 -> eq X1 Y1 -> eq X2 Y2 -> ne Y1 Y2 -> type. - : {N1:nat} {N2:nat} {X1<>X2:ne N1 N2} ne-respects-eq X1<>X2 eq/ eq/ X1<>X2. %worlds () (ne-respects-eq _ _ _ _). %total {} (ne-respects-eq _ _ _ _). %theorem ne-anti-reflexive : {X:nat} ne X X -> void -> type. - : {N1:nat} {X ne-anti-reflexive (ne/< XX:gt N1 N1} {F:void} gt-anti-reflexive* N1 X>X F -> ne-anti-reflexive (ne/> X>X) F. %worlds () (ne-anti-reflexive X<>X _). %total {} (ne-anti-reflexive _ _). %theorem ne-symmetric : {X:nat} {Y:nat} ne X Y -> ne Y X -> type. - : {N1:nat} {N2:nat} {X XY:gt N1 N2} ne-symmetric (ne/> X>Y) (ne/< X>Y). %worlds () (ne-symmetric X<>Y Y<>X). %total {} (ne-symmetric _ _). %theorem eq-ne-implies-false : {X:nat} {Y:nat} eq X Y -> ne X Y -> void -> type. - : {N1:nat} {X<>X:ne N1 N1} {F:void} ne-anti-reflexive X<>X F -> eq-ne-implies-false eq/ X<>X F. %worlds () (eq-ne-implies-false X=Y X<>Y _). %total {} (eq-ne-implies-false _ _ _). %theorem ge-ne-implies-gt : {X:nat} {Y:nat} ge X Y -> ne X Y -> gt X Y -> type. - : {N1:nat} {N2:nat} {X>Y:gt N1 N2} {X1:ne N1 N2} ge-ne-implies-gt (ge/> X>Y) X1 X>Y. - : {N1:nat} {F:void} {X>X:gt N1 N1} {X<>X:ne N1 N1} false-implies-gt F X>X -> ne-anti-reflexive X<>X F -> ge-ne-implies-gt (ge/= eq/) X<>X X>X. %worlds () (ge-ne-implies-gt X>=Y X<>Y X>Y). %total {} (ge-ne-implies-gt _ _ _). %theorem eq?-total* : {M:nat} {N:nat} {B:bool} eq? M N B -> type. %theorem eq?-total*/L : {M:nat} {N:nat} {C:comp} compare M N C -> ({B:bool} eq? M N B -> type). - : {N1:nat} eq?-total*/L compare/= true eq?/yes. - : {N1:nat} {N2:nat} {XY:gt N1 N2} eq?-total*/L (compare/> X>Y) false (eq?/no (ne/> X>Y)). %worlds () (eq?-total*/L _ _ _). %total {} (eq?-total*/L _ _ _). - : {M:nat} {N:nat} {X1:comp} {CMP:compare M N X1} {B:bool} {T:eq? M N B} eq?-total*/L CMP B T -> compare-total* M N X1 CMP -> eq?-total* M N B T. %worlds () (eq?-total* _ _ _ _). %total {} (eq?-total* _ _ _ _). eq?-total : {N1:nat} {N2:nat} {X1:bool} eq? N1 N2 X1 -> type = [N1:nat] [N2:nat] [X1:bool] [T:eq? N1 N2 X1] eq?-total* N1 N2 X1 T. %theorem succ-preserves-ne : {M:nat} {N:nat} ne M N -> ne (s M) (s N) -> type. - : {N1:nat} {N2:nat} {N>M:gt N1 N2} {N+1>M+1:gt (s N1) (s N2)} succ-preserves-gt N>M N+1>M+1 -> succ-preserves-ne (ne/< N>M) (ne/< N+1>M+1). - : {N1:nat} {N2:nat} {N>M:gt N1 N2} {N+1>M+1:gt (s N1) (s N2)} succ-preserves-gt N>M N+1>M+1 -> succ-preserves-ne (ne/> N>M) (ne/> N+1>M+1). %worlds () (succ-preserves-ne M<>N M+1<>N+1). %total {} (succ-preserves-ne _ _). %theorem succ-preserves-ne-converse : {M:nat} {N:nat} ne (s M) (s N) -> ne M N -> type. - : {N1:nat} {N2:nat} {N+1>M+1:gt (s N1) (s N2)} {N>M:gt N1 N2} succ-preserves-gt-converse N+1>M+1 N>M -> succ-preserves-ne-converse (ne/< N+1>M+1) (ne/< N>M). - : {N1:nat} {N2:nat} {N+1>M+1:gt (s N1) (s N2)} {N>M:gt N1 N2} succ-preserves-gt-converse N+1>M+1 N>M -> succ-preserves-ne-converse (ne/> N+1>M+1) (ne/> N>M). %worlds () (succ-preserves-ne-converse M+1<>N+1 M<>N). %total {} (succ-preserves-ne-converse _ _). %theorem plus-left-preserves-ne* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} ne X2 X4 -> plus X1 X2 X3 -> plus X1 X4 X5 -> ne X3 X5 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X4>X2:gt N2 N3} {X1+X4=X5:plus N1 N2 N4} {X1+X2=X3:plus N1 N3 N5} {X5>X3:gt N4 N5} plus-left-preserves-gt* X4>X2 X1+X4=X5 X1+X2=X3 X5>X3 -> plus-left-preserves-ne* (ne/< X4>X2) X1+X2=X3 X1+X4=X5 (ne/< X5>X3). - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X2>X4:gt N2 N3} {X1+X2=X3:plus N1 N2 N4} {X1+X4=X5:plus N1 N3 N5} {X3>X5:gt N4 N5} plus-left-preserves-gt* X2>X4 X1+X2=X3 X1+X4=X5 X3>X5 -> plus-left-preserves-ne* (ne/> X2>X4) X1+X2=X3 X1+X4=X5 (ne/> X3>X5). %worlds () (plus-left-preserves-ne* X2<>X4 X1+X2=X3 X1+X4=X5 X3<>X5). %total {} (plus-left-preserves-ne* _ _ _ _). %theorem plus-left-cancels-ne : {X1:nat} {X2:nat} {X3:nat} {Y1:nat} {Y2:nat} {Y3:nat} plus X1 X2 X3 -> plus Y1 Y2 Y3 -> eq X1 Y1 -> ne X3 Y3 -> ne X2 Y2 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X1+Y2=Y3:plus N1 N2 N4} {X1+X2=X3:plus N1 N3 N5} {Y3>X3:gt N4 N5} {Y2>X2:gt N2 N3} plus-left-cancels-gt X1+Y2=Y3 X1+X2=X3 eq/ Y3>X3 Y2>X2 -> plus-left-cancels-ne X1+X2=X3 X1+Y2=Y3 eq/ (ne/< Y3>X3) (ne/< Y2>X2). - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X1+X2=X3:plus N1 N2 N4} {X1+Y2=Y3:plus N1 N3 N5} {X3>Y3:gt N4 N5} {X2>Y2:gt N2 N3} plus-left-cancels-gt X1+X2=X3 X1+Y2=Y3 eq/ X3>Y3 X2>Y2 -> plus-left-cancels-ne X1+X2=X3 X1+Y2=Y3 eq/ (ne/> X3>Y3) (ne/> X2>Y2). %worlds () (plus-left-cancels-ne X1+X2=X3 Y1+Y2=Y3 X1=Y1 X3<>Y3 X2<>Y2). %total {} (plus-left-cancels-ne _ _ _ _ _). %theorem plus-left-preserves-ne : {X1:nat} {X2:nat} {X4:nat} ne X2 X4 -> ({X3:nat} {X5:nat} plus X1 X2 X3 -> plus X1 X4 X5 -> ne X3 X5 -> type). - : {N1:nat} {N2:nat} {X3:nat} {N3:nat} {X5:nat} {X2<>X4:ne N2 N3} {X1+X2=A3:plus N1 N2 X3} {X1+X4=X5:plus N1 N3 X5} {X3<>X5:ne X3 X5} plus-left-preserves-ne* X2<>X4 X1+X2=A3 X1+X4=X5 X3<>X5 -> plus-total* N1 N3 X5 X1+X4=X5 -> plus-total* N1 N2 X3 X1+X2=A3 -> plus-left-preserves-ne X2<>X4 X3 X5 X1+X2=A3 X1+X4=X5 X3<>X5. %worlds () (plus-left-preserves-ne X2<>X4 X3 X5 X1+X2=A3 X1+X4=X5 X3<>X5). %total {} (plus-left-preserves-ne _ _ _ _ _ _). %theorem plus-right-preserves-ne* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} ne X1 X2 -> plus X1 X3 X4 -> plus X2 X3 X5 -> ne X4 X5 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X1<>X2:ne N2 N4} {X3+X1=X4:plus N1 N2 N3} {X3+X2=X5:plus N1 N4 N5} {X4<>X5:ne N3 N5} {X2+X3=X5:plus N4 N1 N5} {X1+X3=X4:plus N2 N1 N3} plus-left-preserves-ne* X1<>X2 X3+X1=X4 X3+X2=X5 X4<>X5 -> plus-commutative X2+X3=X5 X3+X2=X5 -> plus-commutative X1+X3=X4 X3+X1=X4 -> plus-right-preserves-ne* X1<>X2 X1+X3=X4 X2+X3=X5 X4<>X5. %worlds () (plus-right-preserves-ne* X1<>X2 X1+X3=X4 X2+X3=X5 X4<>X5). %total {} (plus-right-preserves-ne* _ _ _ _). %theorem plus-right-preserves-ne : {X1:nat} {X2:nat} {X3:nat} ne X1 X2 -> ({X4:nat} {X5:nat} plus X1 X3 X4 -> plus X2 X3 X5 -> ne X4 X5 -> type). - : {N1:nat} {N2:nat} {N3:nat} {X4:nat} {X5:nat} {X1<>X2:ne N1 N2} {X1+X3=X4:plus N1 N3 X4} {X2+X3=X5:plus N2 N3 X5} {X4<>X5:ne X4 X5} plus-right-preserves-ne* X1<>X2 X1+X3=X4 X2+X3=X5 X4<>X5 -> plus-total* N2 N3 X5 X2+X3=X5 -> plus-total* N1 N3 X4 X1+X3=X4 -> plus-right-preserves-ne X1<>X2 X4 X5 X1+X3=X4 X2+X3=X5 X4<>X5. %worlds () (plus-right-preserves-ne X1<>X2 X4 X5 X1+X3=X4 X2+X3=X5 X4<>X5). %total {} (plus-right-preserves-ne _ _ _ _ _ _). %theorem plus-right-cancels-ne : {X1:nat} {X2:nat} {X3:nat} {Y1:nat} {Y2:nat} {Y3:nat} plus X1 X2 X3 -> plus Y1 Y2 Y3 -> eq X2 Y2 -> ne X3 Y3 -> ne X1 Y1 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {X2+X1=X3:plus N1 N2 N3} {Y2+Y1=Y3:plus N4 N5 N6} {X2=Y2:eq N1 N4} {X3<>Y3:ne N3 N6} {X1<>Y1:ne N2 N5} {Y1+Y2=Y3:plus N5 N4 N6} {X1+X2=X3:plus N2 N1 N3} plus-left-cancels-ne X2+X1=X3 Y2+Y1=Y3 X2=Y2 X3<>Y3 X1<>Y1 -> plus-commutative Y1+Y2=Y3 Y2+Y1=Y3 -> plus-commutative X1+X2=X3 X2+X1=X3 -> plus-right-cancels-ne X1+X2=X3 Y1+Y2=Y3 X2=Y2 X3<>Y3 X1<>Y1. %worlds () (plus-right-cancels-ne X1+X2=X3 Y1+Y2=Y3 X2=Y2 X3<>Y3 X1<>Y1). %total {} (plus-right-cancels-ne _ _ _ _ _). lt : nat -> nat -> type = [X:nat] [Y:nat] gt Y X. %theorem false-implies-lt : {X1:nat} {X2:nat} void -> gt X2 X1 -> type. %worlds () (false-implies-lt _ _). %total {} (false-implies-lt _ _). %theorem lt-respects-eq : {X1:nat} {X2:nat} {Y1:nat} {Y2:nat} gt X2 X1 -> eq X1 Y1 -> eq X2 Y2 -> gt Y2 Y1 -> type. - : {N1:nat} {N2:nat} {X1 gt X1 X2 -> void -> type. - : {N1:nat} {N2:nat} {X1>X2:gt N1 N2} {X2>X1:gt N2 N1} {R:void} gt-anti-symmetric X1>X2 X2>X1 R -> lt-anti-symmetric X2>X1 X1>X2 R. %worlds () (lt-anti-symmetric _ _ _). %total {} (lt-anti-symmetric _ _ _). %theorem lt-transitive : {X1:nat} {X2:nat} {X3:nat} gt X2 X1 -> gt X3 X2 -> gt X3 X1 -> type. - : {N1:nat} {N2:nat} {N3:nat} {X2 lt-transitive X1 void -> type = [N1:nat] [G:gt N1 N1] [F:void] gt-anti-reflexive* N1 G F. %theorem plus-left-preserves-lt* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} gt X4 X2 -> plus X1 X2 X3 -> plus X1 X4 X5 -> gt X5 X3 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X4>X2:gt N2 N3} {X1+X4=X5:plus N1 N2 N4} {X1+X2=X3:plus N1 N3 N5} {X5>X3:gt N4 N5} plus-left-preserves-gt* X4>X2 X1+X4=X5 X1+X2=X3 X5>X3 -> plus-left-preserves-lt* X4>X2 X1+X2=X3 X1+X4=X5 X5>X3. %worlds () (plus-left-preserves-lt* X2 plus Y1 Y2 Y3 -> eq X1 Y1 -> gt Y3 X3 -> gt Y2 X2 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X1+Y2=X3:plus N1 N2 N4} {X1+X2=X3:plus N1 N3 N5} {Y3>X3:gt N4 N5} {Y2>X2:gt N2 N3} plus-left-cancels-gt X1+Y2=X3 X1+X2=X3 eq/ Y3>X3 Y2>X2 -> plus-left-cancels-lt X1+X2=X3 X1+Y2=X3 eq/ Y3>X3 Y2>X2. %worlds () (plus-left-cancels-lt X1+X2=X3 Y1+Y2=Y3 X1=Y1 X3 ({X3:nat} {X5:nat} plus X1 X2 X3 -> plus X1 X4 X5 -> gt X5 X3 -> type). - : {N1:nat} {N2:nat} {X3:nat} {N3:nat} {X5:nat} {X2 plus-total* N1 N3 X5 X1+X4=X5 -> plus-total* N1 N2 X3 X1+X2=A3 -> plus-left-preserves-lt X2 plus X1 X3 X4 -> plus X2 X3 X5 -> gt X5 X4 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X1 plus-commutative X2+X3=X5 X3+X2=X5 -> plus-commutative X1+X3=X4 X3+X1=X4 -> plus-right-preserves-lt* X1 ({X4:nat} {X5:nat} plus X1 X3 X4 -> plus X2 X3 X5 -> gt X5 X4 -> type). - : {N1:nat} {N2:nat} {N3:nat} {X4:nat} {X5:nat} {X1 plus-total* N2 N3 X5 X2+X3=X5 -> plus-total* N1 N3 X4 X1+X3=X4 -> plus-right-preserves-lt X1 gt Y2 X2 -> plus X1 X2 X3 -> plus Y1 Y2 Y3 -> gt Y3 X3 -> type. - : {N1:nat} {N2:nat} {N3:nat} {X3 plus-left-preserves-lt* X2 plus-right-preserves-lt* X1 plus-total* N4 N5 N2 Y1+X2=X -> plus-preserves-lt* X1 gt Y2 X2 -> ({X3:nat} {Y3:nat} plus X1 X2 X3 -> plus Y1 Y2 Y3 -> gt Y3 X3 -> type). - : {N1:nat} {N2:nat} {X3:nat} {N3:nat} {N4:nat} {Y3:nat} {X1 plus-total* N3 N4 Y3 Y1+Y2=Y3 -> plus-total* N1 N2 X3 X1+X2=X3 -> plus-preserves-lt X1 plus Y1 Y2 Y3 -> eq X2 Y2 -> gt Y3 X3 -> gt Y1 X1 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {N6:nat} {X2+X1=X3:plus N1 N2 N3} {Y2+Y1=Y3:plus N4 N5 N6} {X2=Y2:eq N1 N4} {X3 plus-commutative Y1+Y2=Y3 Y2+Y1=Y3 -> plus-commutative X1+X2=X3 X2+X1=X3 -> plus-right-cancels-lt X1+X2=X3 Y1+Y2=Y3 X2=Y2 X3 nat -> type = [X:nat] [Y:nat] ge Y X. %theorem false-implies-le : {X1:nat} {X2:nat} void -> ge X2 X1 -> type. %worlds () (false-implies-le _ _). %total {} (false-implies-le _ _). %theorem le-respects-eq : {X1:nat} {X2:nat} {Y1:nat} {Y2:nat} ge X2 X1 -> eq X1 Y1 -> eq X2 Y2 -> ge Y2 Y1 -> type. - : {N1:nat} {N2:nat} {X1<=X2:ge N2 N1} le-respects-eq X1<=X2 eq/ eq/ X1<=X2. %worlds () (le-respects-eq _ _ _ _). %total {} (le-respects-eq _ _ _ _). %theorem le-anti-symmetric : {X1:nat} {X2:nat} ge X2 X1 -> ge X1 X2 -> eq X1 X2 -> type. - : {N1:nat} {N2:nat} {X1>=X2:ge N1 N2} {X2>=X1:ge N2 N1} {R:eq N1 N2} ge-anti-symmetric X1>=X2 X2>=X1 R -> le-anti-symmetric X2>=X1 X1>=X2 R. %worlds () (le-anti-symmetric _ _ _). %total {} (le-anti-symmetric _ _ _). %theorem le-transitive : {X1:nat} {X2:nat} {X3:nat} ge X2 X1 -> ge X3 X2 -> ge X3 X1 -> type. - : {N1:nat} {N2:nat} {N3:nat} {X2<=X3:ge N1 N2} {X1<=X2:ge N2 N3} {X1<=X3:ge N1 N3} ge-transitive X2<=X3 X1<=X2 X1<=X3 -> le-transitive X1<=X2 X2<=X3 X1<=X3. %worlds () (le-transitive X1<=X2 X2<=X3 X1<=X3). %total {} (le-transitive _ _ _). le-reflexive : {X:nat} ge X X -> type = [X:nat] [G:ge X X] ge-reflexive X G. %theorem le-transitive-lt : {X1:nat} {X2:nat} {X3:nat} ge X2 X1 -> gt X3 X2 -> gt X3 X1 -> type. - : {N1:nat} {N2:nat} {N3:nat} {X3>X2:gt N1 N2} {X2>=X1:ge N2 N3} {X3>X1:gt N1 N3} gt-transitive-ge X3>X2 X2>=X1 X3>X1 -> le-transitive-lt X2>=X1 X3>X2 X3>X1. %worlds () (le-transitive-lt X1<=X2 X2 ge X3 X2 -> gt X3 X1 -> type. - : {N1:nat} {N2:nat} {N3:nat} {X3>=X2:ge N1 N2} {X2>X1:gt N2 N3} {X3>X1:gt N1 N3} ge-transitive-gt X3>=X2 X2>X1 X3>X1 -> lt-transitive-le X2>X1 X3>=X2 X3>X1. %worlds () (lt-transitive-le X1 plus X1 X2 X3 -> plus X1 X4 X5 -> ge X5 X3 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X4>=X2:ge N2 N4} {X1+X4=X5:plus N1 N2 N3} {X1+X2=X3:plus N1 N4 N5} {X5>=X3:ge N3 N5} plus-left-preserves-ge* X4>=X2 X1+X4=X5 X1+X2=X3 X5>=X3 -> plus-left-preserves-le* X4>=X2 X1+X2=X3 X1+X4=X5 X5>=X3. %worlds () (plus-left-preserves-le* X2<=X4 X1+X2=X3 X1+X4=X5 X3<=X5). %total {} (plus-left-preserves-le* _ _ _ _). %theorem plus-left-cancels-le : {X1:nat} {X2:nat} {X3:nat} {Y1:nat} {Y2:nat} {Y3:nat} plus X1 X2 X3 -> plus Y1 Y2 Y3 -> eq X1 Y1 -> ge Y3 X3 -> ge Y2 X2 -> type. - : {N1:nat} {N2:nat} {N3:nat} {N4:nat} {N5:nat} {X1+Y2=X3:plus N1 N2 N3} {X1+X2=X3:plus N1 N4 N5} {Y3>=X3:ge N3 N5} {Y2>=X2:ge N2 N4} plus-left-cancels-ge X1+Y2=X3 X1+X2=X3 eq/ Y3>=X3 Y2>=X2 -> plus-left-cancels-le X1+X2=X3 X1+Y2=X3 eq/ Y3>=X3 Y2>=X2. %worlds () (plus-left-cancels-le X1+X2=X3 Y1+Y2=Y3 X1=Y1 X3<=Y3 X2<=Y2). %total {} (plus-left-cancels-le _ _ _ _ _). %theorem plus-left-preserves-le : {X1:nat} {X2:nat} {X4:nat} ge X4 X2 -> ({X3:nat} {X5:nat} plus X1 X2 X3 -> plus X1 X4 X5 -> ge X5 X3 -> type). - : {N1:nat} {N2:nat} {X3:nat} {N3:nat} {X5:nat} {X2<=X4:ge N3 N2} {X1+X2=A3:plus N1 N2 X3} {X1+X4=X5:plus N1 N3 X5} {X3<=X5:ge X5 X3} plus-left-preserves-le* X2<=X4 X1+X2=A3 X1+X4=X5 X3<=X5 -> plus-total* N1 N3 X5 X1+X4=X5 -> plus-total* N1 N2 X3 X1+X2=A3 -> plus-left-preserves-le X2<=X4 X3 X5 X1+X2=A3 X1+X4=X5 X3<=X5. %worlds () (plus-left-preserves-le X2<=X4 X3 X5 X1+X2=A3 X1+X4=X5 X3<=X5). %total {} (plus-left-preserves-le _ _ _ _ _ _). %theorem plus-right-preserves-le* : {X1:nat} {X2:nat} {X3:nat} {X4:nat} {X5:nat} ge X2 X1 -> plus X1 X3 X4 -> plus X2 X3 X5 -> ge X5 X4 -> type. - :