%%%%% Natural numbers %%%%% John Boyland %%%%% Anyone may use, copy or modify this software without restriction %%%%% This file requires std.elf %{% The natural numbers signature comes in several pieces, all of which are concatenated in nat.elf: - nat-base.elf (basic definitions, relations and operations) - nat-comp.elf (composed orders: ge, ne) - nat-inv.elf (inverse operation: minus) - nat-less.elf (inverse orders: lt, le) - nat-inv-comp.elf (theorems about minus and composed relations) - nat-inv-less.elf (theorems about minus and inverse orders) - nat-divrem.elf (quotient/remainder operation) - nat-minmax-elf (min/max operations) With the exception of the nat-inv-XXX.elf files, all later files depend on (require) only the nat-base.elf file. The nat-inv-XXX.elf files depend also on nat-inv.elf and nat-XXX.elf. %}% %{% The theorems in this signature mostly fall into the following groups: false-implies-XXX: one can derive XXX after a contradiction XXX-respects-eq: one can substitute equal terms in a relation XXX XXX-total: effectiveness lemma for XXX XXX-deterministic: uniqueness lemma for XXX XXX-reflexive, XXX-symmetric, XXX-transitive: properties of an equivalence XXX-anti-reflexive, XXX-anti-symmetric: properties of a partial order XXX-commutative, XXX-associative: properties of a binary operation XXX-left/right-distributes-over-YYY: distribution theorem XXX-left/right-factors-over-YYY: converse of distribution theorem XXX-left/right-preserves-ORD: If X ORD Y then we can apply Z to both sides XXX-left/right-cancels: cancellation property of binary operator XXX XXX-left/right-cancels-ORD: cancellation property w.r.t. order ORD XXX-contradiction: case where XXX can never happen XXX-implies-YYY: if XXX is true, we show YYY is true TTT-converse: converse of theorem TTT Additionally there are varieties of theorems with star appended to the name. These versions of the theorems typically require more inputs. %}% %%%%% nat-base.elf %%%%% Basic definitions, operations and theorems %%%%% This file is part of the nat.elf signature %%%% Definitions %%% Natural numbers: nat : type. %name nat N. z : nat. s : nat -> nat. %freeze nat. %%% Operations on natural numbers plus : nat -> nat -> nat -> type. plus/z : plus z Y Y. plus/s : plus (s X) Y (s Z) <- plus X Y Z. times : nat -> nat -> nat -> type. times/z : times z X z. times/s : times (s X) Y Z <- plus T Y Z <- times X Y T. eq : nat -> nat -> type. eq/ : eq N N. gt : nat -> nat -> type. gt/1 : gt (s M) M. gt/> : gt (s M) N <- gt M N. %%% Using the conditional for natural numbers compare : nat -> nat -> comp -> type. compare/= : compare N N equal. compare/< : compare M N less <- gt N M. compare/> : compare M N greater <- gt M N. %%%% Theorems %%% Theorems about eq %reduces X = Y (eq X Y). %theorem meta-eq : forall {M} {N} {E:eq M N} true. - : meta-eq N N eq/. %worlds () (meta-eq _ _ _). %total {} (meta-eq _ _ _). %reduces X = Y (meta-eq X Y _). %theorem false-implies-eq : forall* {M} {N} forall {P:void} exists {Q:eq M N} true. %worlds () (false-implies-eq _ %{=>}% M=N). %total {} (false-implies-eq _ _). %theorem eq-symmetric : forall* {M:nat} {N:nat} forall {E:eq M N} exists {F:eq N M} true. - : eq-symmetric (eq/) (eq/). %worlds () (eq-symmetric M>N %{=>}% N>M). %total {} (eq-symmetric _ _). %theorem eq-transitive : forall* {M:nat} {N:nat} {P:nat} forall {E1:eq M N} {E2:eq N P} exists {F:eq M P} true. - : eq-transitive (eq/) (eq/) (eq/). %worlds () (eq-transitive M>N N>P %{=>}% M>P). %total {} (eq-transitive _ _ _). %theorem succ-deterministic : forall* {N1:nat} {N2:nat} forall {E:eq N1 N2} exists {F:eq (s N1) (s N2)} true. - : succ-deterministic eq/ eq/. %worlds () (succ-deterministic N1=N2 %{=>}% N1+1=N2+1). %total {} (succ-deterministic E _). %theorem succ-cancels : forall* {N1:nat} {N2:nat} forall {E:eq (s N1) (s N2)} exists {F:eq N1 N2} true. - : succ-cancels eq/ eq/. %worlds () (succ-cancels N1+1=N2+1 %{=>}% N1=N2). %total {} (succ-cancels E _). %theorem succ-contradiction : forall* {N} forall {E:eq N (s N)} exists {F:void} true. %worlds () (succ-contradiction _ _). %total { } (succ-contradiction _ _). %theorem eq-contradiction : forall* {N} forall {E:eq z (s N)} exists {F:void} true. %worlds () (eq-contradiction ZERO=N+1 %{=>}% _). %total {} (eq-contradiction _ _). %%% Theorems about gt %reduces M < N (gt N M). %% If we want to prove the termination of a theorem using gt, %% we need the gt relation lifted to the meta level: %theorem meta-gt : forall {M} {N} {G:gt M N} true. - : meta-gt (s M) M (gt/1). - : meta-gt (s M) N (gt/> G) <- meta-gt M N G. %worlds () (meta-gt _ _ _). %total M (meta-gt M _ _). %reduces M < N (meta-gt N M _). %theorem false-implies-gt : forall* {M} {N} forall {P:void} exists {Q:gt M N} true. %worlds () (false-implies-gt _ %{=>}% M>N). %total {} (false-implies-gt _ _). %theorem gt-respects-eq : forall* {M1:nat} {M2:nat} {N1:nat} {N2:nat} forall {P:gt M1 N1} {E1:eq M1 M2} {E2:eq N1 N2} exists {Q:gt M2 N2} true. - : 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 : forall* {X} {X'} forall {E:eq X (s X')} exists {G:gt X X'} true. - : succ-implies-gt eq/ gt/1. %worlds () (succ-implies-gt X=sX' %{=>}% X>X'). %total {} (succ-implies-gt _ _). %theorem succ-implies-gt-zero: forall {M} exists {G:gt (s M) z} true. - : succ-implies-gt-zero z gt/1. - : succ-implies-gt-zero (s M) (gt/> SM>0) <- succ-implies-gt-zero M SM>0. %worlds () (succ-implies-gt-zero M %{=>}% SM>0). %total M (succ-implies-gt-zero M _). %theorem succ-preserves-gt: forall* {M} {N} forall {G1:gt M N} exists {G2:gt (s M) (s N)} true. - : succ-preserves-gt gt/1 gt/1. - : succ-preserves-gt (gt/> M>N) (gt/> SM>SN) <- succ-preserves-gt M>N SM>SN. %worlds () (succ-preserves-gt M>N %{=>}% SM>SN). %total G1 (succ-preserves-gt G1 _). %theorem succ-preserves-gt-converse: forall* {M} {N} forall {G1:gt (s M) (s N)} exists {G2:gt M N} true. - : succ-preserves-gt-converse gt/1 gt/1. - : succ-preserves-gt-converse (gt/> SM>SN) (gt/> M>N) <- succ-preserves-gt-converse SM>SN M>N. %worlds () (succ-preserves-gt-converse SM>SN %{=>}% M>N). %total G1 (succ-preserves-gt-converse G1 _). %theorem gt-implies-positive : forall* {M} {N} forall {G:gt M N} exists {M'} {E:eq M (s M')} true. - : gt-implies-positive gt/1 M eq/. - : gt-implies-positive (gt/> (G:gt M N)) M eq/. %worlds () (gt-implies-positive M>N %{=>}% M' M=sM'). %total {} (gt-implies-positive _ _ _). %theorem gt-anti-reflexive* : forall {M} {G:gt M M} exists {F:void} true. - : gt-anti-reflexive* (s M) (G:gt (s M) (s M)) F <- succ-preserves-gt-converse G G' <- gt-anti-reflexive* M G' F. %worlds () (gt-anti-reflexive* M M>M %{=>}% _). %total M (gt-anti-reflexive* M _ _). %abbrev gt-anti-reflexive = gt-anti-reflexive* _. %theorem gt-transitive : forall* {M} {N} {P} forall {G1:gt M N} {G2:gt N P} exists {G3:gt M P} true. - : gt-transitive gt/1 G (gt/> G). - : gt-transitive (gt/> M>N) N>P (gt/> M>P) <- gt-transitive M>N N>P M>P. %worlds () (gt-transitive M>N N>P %{=>}% M>P). %total (G1) (gt-transitive G1 _ _). %theorem gt-anti-symmetric : forall* {M} {N} forall {G1:gt M N} {G2:gt N M} exists {F:void} true. - : gt-anti-symmetric M>N N>M F <- gt-transitive M>N N>M M>M <- gt-anti-reflexive M>M F. %worlds () (gt-anti-symmetric M>N N>M %{=>}% _). %total {} (gt-anti-symmetric _ _ _). %theorem gt-implies-plus : forall* {M} {N} forall {G:gt M N} exists {D} {P:plus (s D) N M} true. - : gt-implies-plus gt/1 z (plus/s plus/z). - : gt-implies-plus (gt/> M>N) (s D) (plus/s SD+N=M) <- gt-implies-plus M>N D SD+N=M. %worlds () (gt-implies-plus M>N %{=>}% D SD+N=M). %total G (gt-implies-plus G _ _). %theorem gt-contradiction : forall* {M} forall {P:gt z M} exists {Q:void} true. %worlds () (gt-contradiction ZERO>N %{=>}% _). %total {} (gt-contradiction _ _). %%% Theorems about compare %theorem false-implies-compare : forall* {M} {N} {C} forall {P:void} exists {Q:compare M N C} true. %worlds () (false-implies-compare _ _). %total {} (false-implies-compare _ _). %theorem succ-preserves-compare : forall* {M} {N} {C} forall {CMP:compare M N C} exists {CMP':compare (s M) (s N) C} true. - : succ-preserves-compare compare/= compare/=. - : succ-preserves-compare (compare/< M>N) (compare/< M+1>N+1) <- succ-preserves-gt M>N M+1>N+1. - : succ-preserves-compare (compare/> M>N) (compare/> M+1>N+1) <- succ-preserves-gt M>N M+1>N+1. %worlds () (succ-preserves-compare _ _). %total {} (succ-preserves-compare _ _). %theorem compare-total* : forall {M} {N} exists {CMP} {P:(compare M N CMP)} true. - : compare-total* z z equal compare/=. - : compare-total* z (s M) less (compare/< M+1>0) <- succ-implies-gt-zero M M+1>0. - : compare-total* (s M) z greater (compare/> M+1>0) <- succ-implies-gt-zero M M+1>0. - : compare-total* (s M) (s N) R M+1-R-N+1 <- compare-total* M N R M-R-N <- succ-preserves-compare M-R-N M+1-R-N+1. %worlds () (compare-total* _ _ _ _). %total (M) (compare-total* M _ _ _). %abbrev compare-total = compare-total* _ _ _. %theorem greater-implies-gt : forall* {M} {N} forall {C:compare M N greater} exists {G:gt M N} true. - : 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 : forall* {M} {N} forall {C1:compare M N less} exists {C2:compare N M greater} true. - : less-is-reverse-greater (compare/< G) (compare/> G). %worlds () (less-is-reverse-greater M}% N>M). %total C (less-is-reverse-greater C _). %theorem less-implies-lt : forall* {M} {N} forall {C:compare M N less} exists {G:gt N M} true. - : less-implies-lt (compare/< G) G. %worlds () (less-implies-lt M}% N-gt-M). %total {} (less-implies-lt _ _). %theorem equal-implies-eq : forall* {M} {N} forall {C:compare M N equal} exists {E:eq M N} true. - : equal-implies-eq compare/= eq/. %worlds () (equal-implies-eq M=N %{=>}% M-eq-N). %total C (equal-implies-eq C _). %%% Theorems about plus %theorem false-implies-plus : forall* {M} {N} {O} forall {P:void} exists {Q:plus M N O} true. %worlds () (false-implies-plus _ _). %total {} (false-implies-plus _ _). %theorem plus-respects-eq : forall* {M1:nat} {M2:nat} {N1:nat} {N2:nat} {P1:nat} {P2:nat} forall {P:plus M1 N1 P1} {E1:eq M1 M2} {E2:eq N1 N2} {E3:eq P1 P2} exists {Q:plus M2 N2 P2} true. - : 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*: forall {N1:nat} {N2:nat} exists {N3:nat} {P:plus N1 N2 N3} true. - : plus-total* _ _ _ plus/z. - : plus-total* (s N1') N2 (s N3) (plus/s P) <- plus-total* N1' N2 N3 P. %worlds () (plus-total* N1 N2 %{=>}% N3 N1+N2=N3). %total N1 (plus-total* N1 _ _ _). %abbrev plus-total = plus-total* _ _ _. %theorem plus-deterministic: forall* {N1:nat} {N1':nat} {N2:nat} {N2':nat} {N3:nat} {N3':nat} forall {P:plus N1 N2 N3} {P':plus N1' N2' N3'} {E1:eq N1 N1'} {E2:eq N2 N2'} exists {E3:eq N3 N3'} true. - : plus-deterministic plus/z plus/z eq/ eq/ eq/. - : plus-deterministic (plus/s (P:plus N1 N2 N3)) (plus/s (P':plus N1' N2' N3')) E1 E2 (E:eq (s N3) (s N3')) <- succ-cancels E1 E1' <- plus-deterministic P P' E1' E2 E' <- succ-deterministic E' E. %worlds () (plus-deterministic _ _ _ _ _). %total (P) (plus-deterministic P _ _ _ _). %theorem plus-left-identity : forall {N:nat} exists {P:plus z N N} true. - : plus-left-identity N plus/z. %worlds () (plus-left-identity N %{=>}% Z+N=N). %total {} (plus-left-identity _ _). %theorem plus-left-increase : forall* {M:nat} {N:nat} {O:nat} forall {P:plus M N O} exists {Q:plus (s M) N (s O)} true. - : 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 : forall {N:nat} exists {P:plus N z N} true. - : plus-right-identity z plus/z. - : plus-right-identity (s N) (plus/s N+0=N) <- plus-right-identity N N+0=N. %worlds () (plus-right-identity N %{=>}% N+0=N). %total N (plus-right-identity N _). %theorem plus-right-increase : forall* {M:nat} {N:nat} {O:nat} forall {P:plus M N O} exists {Q:plus M (s N) (s O)} true. - : plus-right-increase plus/z plus/z. - : plus-right-increase (plus/s M+N=O) (plus/s M+sN=sO) <- plus-right-increase M+N=O M+sN=sO. %worlds () (plus-right-increase M+N=O %{=>}% M+sN=sO). %total P (plus-right-increase P _). %theorem plus-left-decrease: forall* {M:nat} {N:nat} {O':nat} forall {P:plus (s M) N O'} exists {O} {E:eq O' (s O)} {Q:plus M N O} true. - : 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: forall* {M:nat} {N:nat} {O':nat} forall {P:plus M (s N) O'} exists {O} {E:eq O' (s O)} {Q:plus M N O} true. - : plus-right-decrease (plus/z) N eq/ (plus/z). - : {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-right-decrease (plus/s M+sN=O) _ eq/ sM+N=O <- plus-right-decrease M+sN=O O' O=sO' M+N=O' <- plus-total sM+N=X <- plus-deterministic (plus/s M+N=O') sM+N=X eq/ eq/ SO'=X <- eq-transitive O=sO' SO'=X O=X <- eq-symmetric O=X X=O <- plus-respects-eq sM+N=X eq/ eq/ X=O 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: forall* {N1} {N2} {N3} forall {P:plus (s N1) N2 N3} exists {P':plus N1 (s N2) N3} true. - : plus-swap-succ (plus/s N1+N2=N3-) N1+sN2=N3 <- plus-right-increase 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: forall* {N1} {N2} {N3} forall {P:plus N1 (s N2) N3} exists {P':plus (s N1) N2 N3} true. - : plus-swap-succ-converse N1+sN2=N3 SN1+N2=N3 <- plus-right-decrease N1+sN2=N3 N3- N3=sN3- N1+N2=N3- <- eq-symmetric N3=sN3- SN3-=N3 <- plus-respects-eq (plus/s N1+N2=N3-) eq/ eq/ SN3-=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: forall* {N1} {N2} {N3} {N1-} forall {P:plus N1 N2 N3} {E:eq N1 (s N1-)} exists {N3-} {E':eq N3 (s N3-)} true. - : plus-left-preserves-positive (plus/s N1-+N2=N3-) eq/ _ eq/. %worlds () (plus-left-preserves-positive N1+N2=N3 N1=sN1- %{=>}% N3- N3=sN3-). %total {} (plus-left-preserves-positive _ _ _ _). %theorem plus-right-preserves-positive: forall* {N1} {N2} {N3} {N2-} forall {P:plus N1 N2 N3} {E:eq N2 (s N2-)} exists {N3-} {E':eq N3 (s N3-)} true. - : plus-right-preserves-positive N1+N2=N3 N2=sN2- N3- N3=sN3- <- plus-respects-eq N1+N2=N3 eq/ N2=sN2- eq/ N1+sN2-=N3 <- plus-right-decrease N1+sN2-=N3 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 : forall* {N1} {N2} {N3} forall {P:plus N1 N2 N3} {E3:eq N3 z} exists {E1:eq N1 z} {E2:eq N2 z} true. - : 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: forall* {N1} {N2} {N12} forall {P:plus N1 N2 N12} exists {Q:plus N2 N1 N12} true. - : plus-commutative (plus/z) N2+z=N2 <- plus-right-identity N2 N2+z=N2. - : plus-commutative (plus/s N1+N2=N3) N2+sN1=sN3 <- plus-commutative N1+N2=N3 N2+N1=N3 <- plus-right-increase N2+N1=N3 N2+sN1=sN3. %worlds () (plus-commutative N1+N2=N3 %{=>}% N2+N1=N3). %total P (plus-commutative P _). %theorem plus-associative : forall* {X:nat} {Y:nat} {Z:nat} {X':nat} {Z':nat} forall {P1:plus X Y X'} {P2:plus X' Z Z'} exists {Y':nat} {Q1:plus Y Z Y'} {Q2:plus X Y' Z'} true. - : plus-associative plus/z (P2:plus N2 N3 N23) N23 P2 plus/z. - : plus-associative (plus/s N1+N2=N12) (plus/s N12+N3=N123) N23 N2+N3=N23 (plus/s N1+N23=N123) <- plus-associative N1+N2=N12 N12+N3=N123 N23 N2+N3=N23 N1+N23=N123. %worlds () (plus-associative _ _ _ _ _). %total P1 (plus-associative P1 _ _ _ _). %theorem plus-associative* : forall* {X1} {X2} {X12} {X3} {X23} {X123} forall {OP12:plus X1 X2 X12} {OP12-3:plus X12 X3 X123} {OP23:plus X2 X3 X23} exists {OP1-23:plus X1 X23 X123} true. - : plus-associative* X1+X2=X3 X3+X4=X7 X2+X4=X6 X1+X6=X7 <- plus-associative X1+X2=X3 X3+X4=X7 Y6 X2+X4=Y6 X1+Y6=X7 <- plus-deterministic X2+X4=Y6 X2+X4=X6 eq/ eq/ Y6=X6 <- plus-respects-eq X1+Y6=X7 eq/ Y6=X6 eq/ X1+X6=X7. %worlds () (plus-associative* _ _ _ _). %total {} (plus-associative* _ _ _ _). %theorem plus-associative-converse : forall* {X1} {X2} {X4} {X6} {X7} forall {OP24:plus X2 X4 X6} {OP16:plus X1 X6 X7} exists {X3} {OP12:plus X1 X2 X3} {OP34:plus X3 X4 X7} true. - : plus-associative-converse X2+X4=X6 X1+X6=X7 _ X1+X2=X3 X3+X4=X7 <- plus-commutative X2+X4=X6 X4+X2=X6 <- plus-commutative X1+X6=X7 X6+X1=X7 <- plus-associative X4+X2=X6 X6+X1=X7 _ X2+X1=X3 X4+X3=X7 <- plus-commutative X2+X1=X3 X1+X2=X3 <- plus-commutative X4+X3=X7 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* : forall* {X1} {X2} {X3} {X4} {X6} {X7} forall {OP24:plus X2 X4 X6} {OP16:plus X1 X6 X7} {OP12:plus X1 X2 X3} exists {OP34:plus X3 X4 X7} true. - : plus-associative-converse* X2+X4=X6 X1+X6=X7 X1+X2=X3 X3+X4=X7 <- plus-associative-converse X2+X4=X6 X1+X6=X7 X3P X1+X2=X3P X3P+X4=X7 <- plus-deterministic X1+X2=X3P X1+X2=X3 eq/ eq/ X3P=X3 <- plus-respects-eq X3P+X4=X7 X3P=X3 eq/ eq/ X3+X4=X7. %worlds () (plus-associative-converse* X2+X4=X6 X1+X6=X7 X1+X2=X3 %{=>}% X3+X4=X7). %total {} (plus-associative-converse* _ _ _ _). %% The following two theorems are useful for reordering elements %% is a left-associative sequence of operations. %theorem plus-assoc-commutative* : forall* {X1} {X2} {X3} {X4} {X5} {X7} forall {OP1:plus X1 X2 X3} {OP2:plus X3 X4 X7} {OP3:plus X1 X4 X5} exists {OP4:plus X5 X2 X7} true. - : plus-assoc-commutative* X1+X2=X3 X3+X4=X7 X1+X4=X5 X5+X2=X7 <- plus-associative X1+X2=X3 X3+X4=X7 X6 X2+X4=X6 X1+X6=X7 <- plus-commutative X2+X4=X6 X4+X2=X6 <- plus-associative-converse* X4+X2=X6 X1+X6=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 : forall* {X1} {X2} {X3} {X4} {X7} forall {OP1:plus X1 X2 X3} {OP2:plus X3 X4 X7} exists {X5} {OP3:plus X1 X4 X5} {OP4:plus X5 X2 X7} true. - : plus-assoc-commutative X1+X2=X3 X3+X4=X7 X5 X1+X4=X5 X5+X2=X7 <- plus-associative X1+X2=X3 X3+X4=X7 X6 X2+X4=X6 X1+X6=X7 <- plus-commutative X2+X4=X6 X4+X2=X6 <- plus-associative-converse X4+X2=X6 X1+X6=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 _ _ _ _ _). %% The following theorem is a useful shortcut to %% re-associate (AB)(CD) to (AC)(BD): %theorem plus-double-associative* : forall* {A} {B} {C} {D} {A+B} {C+D} {A+C} {B+D} {X} forall {AB:plus A B A+B} {CD:plus C D C+D} {ABCD:plus A+B C+D X} {AC:plus A C A+C} {BD:plus B D B+D} exists {ACBD:plus A+C B+D X} true. - : plus-double-associative* X1+X2=X3 X4+X8=XC X3+XC=XF X1+X4=X5 X2+X8=XA X5+XA=XF <- plus-associative X1+X2=X3 X3+XC=XF XE X2+XC=XE X1+XE=XF <- plus-commutative X4+X8=XC X8+X4=XC <- plus-associative-converse* X8+X4=XC X2+XC=XE X2+X8=XA XA+X4=XE <- plus-commutative XA+X4=XE X4+XA=XE <- plus-associative-converse* X4+XA=XE X1+XE=XF X1+X4=X5 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 : forall* {A} {B} {C} {D} {A+B} {C+D} {X} forall {AB:plus A B A+B} {CD:plus C D C+D} {ABCD:plus A+B C+D X} exists {A+C} {B+D} {AC:plus A C A+C} {BD:plus B D B+D} {ACBD:plus A+C B+D X} true. - : plus-double-associative X1+X2=X3 X4+X8=XC X3+XC=XF X5 XA X1+X4=X5 X2+X8=XA X5+XA=XF <- plus-associative X1+X2=X3 X3+XC=XF XE X2+XC=XE X1+XE=XF <- plus-commutative X4+X8=XC X8+X4=XC <- plus-associative-converse X8+X4=XC X2+XC=XE XA X2+X8=XA XA+X4=XE <- plus-commutative XA+X4=XE X4+XA=XE <- plus-associative-converse X4+XA=XE X1+XE=XF X5 X1+X4=X5 X5+XA=XF. %worlds () (plus-double-associative _ _ _ _ _ _ _ _). %total { } (plus-double-associative _ _ _ _ _ _ _ _). %theorem plus-left-cancels : forall* {X1:nat} {X2:nat} {Y:nat} {Z:nat} {S1:nat} {S2:nat} forall {P1:plus X1 Y S1} {P2:plus X2 Z S2} {EX:eq X1 X2} {ES:eq S1 S2} exists {F:eq Y Z} true. - : plus-left-cancels plus/z plus/z eq/ eq/ eq/. - : plus-left-cancels (plus/s X+Y1=Z) (plus/s X+Y2=Z) eq/ eq/ Y1=Y2 <- plus-left-cancels X+Y1=Z 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* : forall* {X:nat} {Y:nat} {Z1:nat} {Z2:nat} forall {S1} {S2} {P1:plus X Z1 S1} {P2:plus Y Z2 S2} {EZ:eq Z1 Z2} {ES:eq S1 S2} exists {F:eq X Y} true. - : plus-right-cancels* Z Z X1+0=Z X2+0=Z eq/ eq/ X1=X2 <- plus-right-identity X1 X1+0=X1 <- plus-deterministic X1+0=X1 X1+0=Z eq/ eq/ X1=Z <- plus-right-identity X2 X2+0=X2 <- plus-deterministic X2+0=X2 X2+0=Z eq/ eq/ X2=Z <- eq-symmetric X2=Z Z=X2 <- eq-transitive X1=Z Z=X2 X1=X2. - : {sZ'=Z:eq (s Z') Z} {sZ'=sZ'':eq (s Z') (s Z'')} plus-right-cancels* Z Z X1+sY=Z X2+sY=Z eq/ eq/ X1=X2 <- plus-right-decrease X1+sY=Z Z' Z=sZ' X1+Y=Z' <- plus-right-decrease X2+sY=Z Z'' Z=sZ'' X2+Y=Z'' <- eq-symmetric Z=sZ' sZ'=Z <- eq-transitive sZ'=Z Z=sZ'' sZ'=sZ'' <- succ-cancels sZ'=sZ'' Z'=Z'' <- meta-eq Z (s Z') Z=sZ' <- plus-right-cancels* Z' Z'' X1+Y=Z' X2+Y=Z'' eq/ Z'=Z'' 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 _ _ _ _ _ _). %abbrev plus-right-cancels = plus-right-cancels* _ _. %theorem plus-left-preserves-gt*: forall* {M} {N1} {N2} {O1} {O2} forall {G1:gt N1 N2} {P1:plus M N1 O1} {P2:plus M N2 O2} exists {G2:gt O1 O2} true. - : plus-left-preserves-gt* N1>N2 plus/z plus/z N1>N2. - : plus-left-preserves-gt* N1>N2 (plus/s M+N1=O1) (plus/s M+N2=O2) SO1>SO2 <- plus-left-preserves-gt* N1>N2 M+N1=O1 M+N2=O2 O1>O2 <- succ-preserves-gt O1>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 : forall* {X1:nat} {X2:nat} {Y:nat} {Z:nat} {S1:nat} {S2:nat} forall {P1:plus X1 Y S1} {P2:plus X2 Z S2} {EX:eq X1 X2} {G1:gt S1 S2} exists {G2:gt Y Z} true. - : plus-left-cancels-gt plus/z plus/z eq/ G G. - : plus-left-cancels-gt (plus/s X+Y1=Z1) (plus/s X+Y2=Z2) eq/ SZ1>SZ2 Y1>Y2 <- succ-preserves-gt-converse SZ1>SZ2 Z1>Z2 <- plus-left-cancels-gt X+Y1=Z1 X+Y2=Z2 eq/ Z1>Z2 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 : forall* {X1} {X2} {X4} forall {G:gt X2 X4} exists {X3} {X5} {O1:plus X1 X2 X3} {O2:plus X1 X4 X5} {G2:gt X3 X5} true. - : plus-left-preserves-gt X2>X4 X3 X5 X1+X2=A3 X1+X4=X5 X3>X5 <- plus-total X1+X2=A3 <- plus-total X1+X4=X5 <- plus-left-preserves-gt* X2>X4 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* : forall* {X1} {X2} {X3} {X4} {X5} forall {G1:gt X1 X2} {O1:plus X1 X3 X4} {O2:plus X2 X3 X5} exists {G2:gt X4 X5} true. - : plus-right-preserves-gt* X1>X2 X1+X3=X4 X2+X3=X5 X4>X5 <- plus-commutative X1+X3=X4 X3+X1=X4 <- plus-commutative X2+X3=X5 X3+X2=X5 <- plus-left-preserves-gt* X1>X2 X3+X1=X4 X3+X2=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 : forall* {X1} {X2} {X3} forall {G1:gt X1 X2} exists {X4} {X5} {O1:plus X1 X3 X4} {O2:plus X2 X3 X5} {G2:gt X4 X5} true. - : plus-right-preserves-gt X1>X2 X4 X5 X1+X3=X4 X2+X3=X5 X4>X5 <- plus-total X1+X3=X4 <- plus-total X2+X3=X5 <- plus-right-preserves-gt* X1>X2 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* : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {G1:gt X1 Y1} {G2:gt X2 Y2} {MX:plus X1 X2 X3} {MY:plus Y1 Y2 Y3} exists {G3:gt X3 Y3} true. - : plus-preserves-gt* X1>Y1 X2>Y2 X1+X2=X3 Y1+Y2=Y3 X3>Y3 <- plus-total Y1+X2=X <- plus-right-preserves-gt* X1>Y1 X1+X2=X3 Y1+X2=X X3>X <- plus-left-preserves-gt* X2>Y2 Y1+X2=X Y1+Y2=Y3 X>Y3 <- gt-transitive X3>X X>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 : forall* {X1} {X2} {Y1} {Y2} forall {G1:gt X1 Y1} {G2:gt X2 Y2} exists {X3} {Y3} {MX:plus X1 X2 X3} {MY:plus Y1 Y2 Y3} {G3:gt X3 Y3} true. - : plus-preserves-gt X1>Y1 X2>Y2 X3 Y3 X1+X2=X3 Y1+Y2=Y3 X3>Y3 <- plus-total X1+X2=X3 <- plus-total Y1+Y2=Y3 <- plus-preserves-gt* X1>Y1 X2>Y2 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 : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {OP1:plus X1 X2 X3} {OP2:plus Y1 Y2 Y3} {E2:eq X2 Y2} {G3:gt X3 Y3} exists {G1:gt X1 Y1} true. - : plus-right-cancels-gt X1+X2=X3 Y1+Y2=Y3 X2=Y2 X3>Y3 X1>Y1 <- plus-commutative X1+X2=X3 X2+X1=X3 <- plus-commutative Y1+Y2=Y3 Y2+Y1=Y3 <- plus-left-cancels-gt X2+X1=X3 Y2+Y1=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: forall* {M} {N} {O} {M'} forall {P:plus M N O} {E:eq M (s M')} exists {G:gt O N} true. - : plus-implies-gt X+Y=Z eq/ Z>Y <- succ-implies-gt-zero _ X>0 <- plus-right-preserves-gt* X>0 X+Y=Z plus/z Z>Y. %worlds () (plus-implies-gt X+Y=Z X=sX' %{=>}% Z>Y). %total {} (plus-implies-gt _ _ _). %theorem plus-gt-contradiction : forall* {M} {N} {O} forall {P:plus M N O} {G:gt M O} exists {F:void} true. - : plus-gt-contradiction M+0=O M>O F <- plus-right-identity _ M+0=M <- plus-deterministic M+0=O M+0=M eq/ eq/ O=M <- gt-respects-eq M>O eq/ O=M M>M <- gt-anti-reflexive M>M F. - : plus-gt-contradiction M+N=O M>O F % N > 0 <- plus-commutative M+N=O N+M=O <- plus-implies-gt N+M=O eq/ O>M <- gt-anti-symmetric M>O O>M F. %worlds () (plus-gt-contradiction M+N=O M>O %{=>}% _). %total {} (plus-gt-contradiction _ _ _). %%% Theorems about times %theorem false-implies-times : forall* {M} {N} {O} forall {P:void} exists {Q:times M N O} true. %worlds () (false-implies-times _ _). %total {} (false-implies-times _ _). %theorem times-respects-eq: forall* {M1:nat} {M2:nat} {N1:nat} {N2:nat} {P1:nat} {P2:nat} forall {P:times M1 N1 P1} {E1:eq M1 M2} {E2:eq N1 N2} {E3:eq P1 P2} exists {Q:times M2 N2 P2} true. - : 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* : forall {N1:nat} {N2:nat} exists {N3:nat} {T:times N1 N2 N3} true. - : times-total* z N2 z times/z. - : times-total* (s X) Y Z (times/s X*Y=Z' Z'+Y=Z) <- times-total* X Y Z' X*Y=Z' <- plus-total Z'+Y=Z. %worlds () (times-total* N1 N2 %{=>}% N3 N1*N2=N3). %total (N1) (times-total* N1 _ _ _). %abbrev times-total = times-total* _ _ _. %theorem times-deterministic : forall* {N1:nat} {N1':nat} {N2:nat} {N2':nat} {N3:nat} {N3':nat} forall {P:times N1 N2 N3} {P':times N1' N2' N3'} {E1:eq N1 N1'} {E2:eq N2 N2'} exists {E3:eq N3 N3'} true. - : times-deterministic (times/z) (times/z) eq/ eq/ eq/. - : times-deterministic (times/s X*Y=Z1 Z1+Y=Z1') (times/s X*Y=Z2 Z2+Y=Z2') eq/ eq/ Z1'=Z2' <- times-deterministic X*Y=Z1 X*Y=Z2 eq/ eq/ Z1=Z2 <- plus-deterministic Z1+Y=Z1' Z2+Y=Z2' Z1=Z2 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 : forall {N:nat} exists {T:times (s z) N N} true. - : 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 : forall {N:nat} exists {T:times N (s z) N} true. - : times-right-identity z times/z. - : times-right-identity (s M) (times/s M*1=M M+1=sM) <- times-right-identity M M*1=M <- plus-right-identity M M+0=M <- plus-right-increase M+0=M M+1=sM. %worlds () (times-right-identity N %{=>}% N*1=N). %total M (times-right-identity M _). %theorem times-right-zero : forall {N:nat} exists {T:times N z z} true. - : times-right-zero z times/z. - : times-right-zero (s M) (times/s M*0=0 plus/z) <- times-right-zero M M*0=0. %worlds () (times-right-zero N %{=>}% N*0=0). %total M (times-right-zero M _). %theorem times-preserves-positive: forall {M} {N} exists {P} {T:times (s M) (s N) (s P)} true. -: {T1:times M (s N) O} {P1:plus O (s N) (s P)} {P2:plus O N P} times-preserves-positive M N P (times/s T1 P1) <- times-total T1 <- plus-total P2 <- plus-right-increase P2 P1. %worlds () (times-preserves-positive M N %{=>}% P SM*SN=SP). %total {} (times-preserves-positive _ _ _ _). %theorem times-preserves-positive*: forall* {M} {N} {P} {M'} {N'} forall {T:times M N P} {M+:eq M (s M')} {N+:eq N (s N')} exists {P'} {P+:eq P (s P')} true. - : times-preserves-positive* M*N=P M=sM' N=sN' P' P=sP' <- times-respects-eq M*N=P M=sM' N=sN' eq/ (times/s M'*sN'=O' O'+sN'=P) <- plus-right-decrease O'+sN'=P 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 : forall* {M} {N} {P} {P'} forall {T:times M N P} {P+:eq P (s P')} exists {M'} {M+:eq M (s M')} {N'} {N+:eq N (s N')} true. - : times-positive-implies-positive (times/s M'*N=T plus/z) eq/ M' eq/ P' eq/. - : times-positive-implies-positive (times/s M'*N=sT' (plus/s T'+N=P')) eq/ M' eq/ N' N=sN' <- times-positive-implies-positive M'*N=sT' 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 : forall* {M} {N} {O} {X} forall {T:times M N O} {P:plus O N X} exists {U:times (s M) N X} true. - : 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 : forall* {M:nat} {N:nat} {O:nat} {X:nat} forall {T:times M N O} {P:plus M O X} exists {U:times M (s N) X} true. - : times-right-increase times/z plus/z times/z. - : {M*N=O:times M N O} {M+O=Z:plus M O Z} times-right-increase (times/s M*N=O O+N=O1) (plus/s M+O1=Y) (times/s M*sN=Z Z+sN=sY) <- plus-associative-converse O+N=O1 M+O1=Y Z M+O=Z Z+N=Y <- times-right-increase M*N=O M+O=Z M*sN=Z <- plus-right-increase Z+N=Y 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 : forall* {X} {Y} {Z} forall {T1:times (s X) Y Z} exists {Z1} {T2:times X Y Z1} {P:plus Z1 Y Z} true. - : times-left-decrease (times/s T P) _ T P. %worlds () (times-left-decrease SX*Y=Z Z1 X*Y=Z1 Z1+Y=Z). %total {} (times-left-decrease _ _ _ _). %theorem times-right-decrease : forall* {M} {N} {X} forall {T:times M (s N) X} exists {O} {U:times M N O} {P:plus M O X} true. - : times-right-decrease times/z z times/z plus/z. - : times-right-decrease (times/s M*sN=Y Y+sN=X) O (times/s M*N=P P+N=O) SM+O=X <- times-right-decrease M*sN=Y P M*N=P M+P=Y <- plus-total P+N=O <- plus-right-increase P+N=O P+sN=sO <- plus-associative* M+P=Y Y+sN=X P+sN=sO M+sO=X <- plus-swap-succ-converse M+sO=X 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 : forall* {N1} {N2} {N3} forall {T:times N1 N2 N3} exists {U:times N2 N1 N3} true. - : times-commutative times/z T <- (times-right-zero N2 T). - : {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-commutative (times/s T1 P2) Tc <- plus-commutative P2 P2c <- times-commutative T1 T1c <- times-right-increase T1c P2c Tc. %worlds () (times-commutative N1*N2=N3 %{=>}% N2*N1=N3). %total T (times-commutative T _). %theorem times-right-distributes-over-plus : forall* {N1} {N2} {N3} {N12} {N123} forall {P1:plus N1 N2 N12} {T1:times N12 N3 N123} exists {N13} {N23} {T13:times N1 N3 N13} {T23:times N2 N3 N23} {P123:plus N13 N23 N123} true. - : times-right-distributes-over-plus plus/z Y*Z=YZ z YZ times/z Y*Z=YZ plus/z. - : 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 <- times-right-distributes-over-plus X+Y=XY XY*Z=XYZ XZ YZ X*Z=XZ Y*Z=YZ XZ+YZ=XYZ <- plus-commutative XZ+YZ=XYZ YZ+XZ=XYZ <- plus-associative YZ+XZ=XYZ XYZ+Z=SXYZ SXZ XZ+Z=SXZ YZ+SXZ=SXYZ <- plus-commutative YZ+SXZ=SXYZ 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* : forall* {X1} {X2} {X3} {X4} {X5} {X6} {X7} forall {A12:plus X1 X2 X3} {M34:times X3 X4 X7} {M14:times X1 X4 X5} {M24:times X2 X4 X6} exists {A56:plus X5 X6 X7} true. - : times-right-distributes-over-plus* X1+X2=X3 X3*X4=X7 X1*X4=X5 X2*X4=X6 X5+X6=X7 <- times-right-distributes-over-plus X1+X2=X3 X3*X4=X7 Y5 Y6 X1*X4=Y5 X2*X4=Y6 Y5+Y6=X7 <- times-deterministic X1*X4=Y5 X1*X4=X5 eq/ eq/ Y5=X5 <- times-deterministic X2*X4=Y6 X2*X4=X6 eq/ eq/ Y6=X6 <- plus-respects-eq Y5+Y6=X7 Y5=X5 Y6=X6 eq/ 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* : forall* {X1} {X2} {X3} {X4} {X5} {X6} {X7} forall {A12:plus X2 X4 X6} {M34:times X1 X6 X7} {M14:times X1 X2 X3} {M24:times X1 X4 X5} exists {A56:plus X3 X5 X7} true. - : times-left-distributes-over-plus* X2+X4=X6 X1*X6=X7 X1*X2=X3 X1*X4=X5 X3+X5=X7 <- times-commutative X1*X6=X7 X6*X1=X7 <- times-commutative X1*X2=X3 X2*X1=X3 <- times-commutative X1*X4=X5 X4*X1=X5 <- times-right-distributes-over-plus* X2+X4=X6 X6*X1=X7 X2*X1=X3 X4*X1=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 : forall* {X1} {X2} {X4} {X6} {X7} forall {A12:plus X2 X4 X6} {M34:times X1 X6 X7} exists {X3} {X5} {M14:times X1 X2 X3} {M24:times X1 X4 X5} {A56:plus X3 X5 X7} true. - : times-left-distributes-over-plus X2+X4=X6 X1*X6=X7 X3 X5 X1*X2=X3 X1*X4=X5 X3+X5=X7 <- times-total X1*X2=X3 <- times-total X1*X4=X5 <- 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 %{=>}% X3 X5 X1*X2=X3 X1*X4=X5 X3+X5=X7). %total {} (times-left-distributes-over-plus _ _ _ _ _ _ _). %theorem times-right-factors-over-plus : forall* {X1} {X2} {X4} {X5} {X6} {X7} forall {M14:times X1 X4 X5} {M24:times X2 X4 X6} {A56:plus X5 X6 X7} exists {X3} {A12:plus X1 X2 X3} {M34:times X3 X4 X7} true. - : times-right-factors-over-plus X1*X4=X5 X2*X4=X6 X5+X6=X7 X3 X1+X2=X3 X3*X4=X7 <- plus-total X1+X2=X3 <- times-total X3*X4=Y7 <- times-right-distributes-over-plus* X1+X2=X3 X3*X4=Y7 X1*X4=X5 X2*X4=X6 X5+X6=Y7 <- plus-deterministic X5+X6=Y7 X5+X6=X7 eq/ eq/ Y7=X7 <- times-respects-eq X3*X4=Y7 eq/ eq/ Y7=X7 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* : forall* {X1} {X2} {X3} {X4} {X5} {X6} {X7} forall {M14:times X1 X4 X5} {M24:times X2 X4 X6} {A56:plus X5 X6 X7} {A12:plus X1 X2 X3} exists {M34:times X3 X4 X7} true. - : times-right-factors-over-plus* X1*X4=X5 X2*X4=X6 X5+X6=X7 X1+X2=X3 X3*X4=X7 <- times-total X3*X4=Y7 <- times-right-distributes-over-plus* X1+X2=X3 X3*X4=Y7 X1*X4=X5 X2*X4=X6 X5+X6=Y7 <- plus-deterministic X5+X6=Y7 X5+X6=X7 eq/ eq/ Y7=X7 <- times-respects-eq X3*X4=Y7 eq/ eq/ Y7=X7 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 : forall* {X1} {X2} {X3} {X4} {X5} {X7} forall {M12:times X1 X2 X3} {M14:times X1 X4 X5} {A35:plus X3 X5 X7} exists {X6} {A24:plus X2 X4 X6} {M16:times X1 X6 X7} true. - : times-left-factors-over-plus X1*X2=X3 X1*X4=X5 X3+X5=X7 X6 X2+X4=X6 X1*X6=X7 <- times-commutative X1*X2=X3 X2*X1=X3 <- times-commutative X1*X4=X5 X4*X1=X5 <- times-right-factors-over-plus X2*X1=X3 X4*X1=X5 X3+X5=X7 X6 X2+X4=X6 X6*X1=X7 <- times-commutative X6*X1=X7 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* : forall* {X1} {X2} {X3} {X4} {X5} {X6} {X7} forall {M12:times X1 X2 X3} {M14:times X1 X4 X5} {A35:plus X3 X5 X7} {A24:plus X2 X4 X6} exists {M16:times X1 X6 X7} true. - : times-left-factors-over-plus* X1*X2=X3 X1*X4=X5 X3+X5=X7 X2+X4=X6 X1*X6=X7 <- times-total X1*X6=Y7 <- times-left-distributes-over-plus* X2+X4=X6 X1*X6=Y7 X1*X2=X3 X1*X4=X5 X3+X5=Y7 <- plus-deterministic X3+X5=Y7 X3+X5=X7 eq/ eq/ Y7=X7 <- times-respects-eq X1*X6=Y7 eq/ eq/ Y7=X7 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: forall* {N1} {N2} {N3} {N12} {N123} forall {T1:times N1 N2 N12} {T12:times N12 N3 N123} exists {N23} {T2:times N2 N3 N23} {T123:times N1 N23 N123} true. - : {T2:times N2 N3 N23} times-associative times/z times/z N23 T2 times/z <- times-total T2. - : {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-associative (times/s T1 P2) T3 N23 T4 (times/s T5 P6) <- times-right-distributes-over-plus P2 T3 N1'23 N23 T7 T4 P6 <- times-associative T1 T7 N23' T4' T5' <- times-deterministic T4' T4 eq/ eq/ N23'=N23 <- times-respects-eq T5' eq/ N23'=N23 eq/ T5. %worlds () (times-associative _ _ _ _ _). %total T1 (times-associative T1 _ _ _ _). %theorem times-associative* : forall* {X1} {X2} {X12} {X3} {X23} {X123} forall {OP12:times X1 X2 X12} {OP12-3:times X12 X3 X123} {OP23:times X2 X3 X23} exists {OP1-23:times X1 X23 X123} true. - : times-associative* X1*X2=X3 X3*X4=X7 X2*X4=X6 X1*X6=X7 <- times-associative X1*X2=X3 X3*X4=X7 Y6 X2*X4=Y6 X1*Y6=X7 <- times-deterministic X2*X4=Y6 X2*X4=X6 eq/ eq/ Y6=X6 <- times-respects-eq X1*Y6=X7 eq/ Y6=X6 eq/ X1*X6=X7. %worlds () (times-associative* _ _ _ _). %total {} (times-associative* _ _ _ _). %theorem times-associative-converse : forall* {X1} {X2} {X4} {X6} {X7} forall {OP24:times X2 X4 X6} {OP16:times X1 X6 X7} exists {X3} {OP12:times X1 X2 X3} {OP34:times X3 X4 X7} true. - : times-associative-converse X2*X4=X6 X1*X6=X7 _ X1*X2=X3 X3*X4=X7 <- times-commutative X2*X4=X6 X4*X2=X6 <- times-commutative X1*X6=X7 X6*X1=X7 <- times-associative X4*X2=X6 X6*X1=X7 _ X2*X1=X3 X4*X3=X7 <- times-commutative X2*X1=X3 X1*X2=X3 <- times-commutative X4*X3=X7 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* : forall* {X1} {X2} {X3} {X4} {X6} {X7} forall {OP24:times X2 X4 X6} {OP16:times X1 X6 X7} {OP12:times X1 X2 X3} exists {OP34:times X3 X4 X7} true. - : times-associative-converse* X2*X4=X6 X1*X6=X7 X1*X2=X3 X3*X4=X7 <- times-associative-converse X2*X4=X6 X1*X6=X7 X3P X1*X2=X3P X3P*X4=X7 <- times-deterministic X1*X2=X3P X1*X2=X3 eq/ eq/ X3P=X3 <- times-respects-eq X3P*X4=X7 X3P=X3 eq/ eq/ 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* : forall* {X1} {X2} {X3} {X4} {X5} {X7} forall {OP1:times X1 X2 X3} {OP2:times X3 X4 X7} {OP3:times X1 X4 X5} exists {OP4:times X5 X2 X7} true. - : times-assoc-commutative* X1*X2=X3 X3*X4=X7 X1*X4=X5 X5*X2=X7 <- times-associative X1*X2=X3 X3*X4=X7 X6 X2*X4=X6 X1*X6=X7 <- times-commutative X2*X4=X6 X4*X2=X6 <- times-associative-converse* X4*X2=X6 X1*X6=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 : forall* {X1} {X2} {X3} {X4} {X7} forall {OP1:times X1 X2 X3} {OP2:times X3 X4 X7} exists {X5} {OP3:times X1 X4 X5} {OP4:times X5 X2 X7} true. - : times-assoc-commutative X1*X2=X3 X3*X4=X7 X5 X1*X4=X5 X5*X2=X7 <- times-associative X1*X2=X3 X3*X4=X7 X6 X2*X4=X6 X1*X6=X7 <- times-commutative X2*X4=X6 X4*X2=X6 <- times-associative-converse X4*X2=X6 X1*X6=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* : forall* {A} {B} {C} {D} {A+B} {C+D} {A+C} {B+D} {X} forall {AB:times A B A+B} {CD:times C D C+D} {ABCD:times A+B C+D X} {AC:times A C A+C} {BD:times B D B+D} exists {ACBD:times A+C B+D X} true. - : times-double-associative* X1*X2=X3 X4*X8=XC X3*XC=XF X1*X4=X5 X2*X8=XA X5*XA=XF <- times-associative X1*X2=X3 X3*XC=XF XE X2*XC=XE X1*XE=XF <- times-commutative X4*X8=XC X8*X4=XC <- times-associative-converse* X8*X4=XC X2*XC=XE X2*X8=XA XA*X4=XE <- times-commutative XA*X4=XE X4*XA=XE <- times-associative-converse* X4*XA=XE X1*XE=XF X1*X4=X5 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 : forall* {A} {B} {C} {D} {A+B} {C+D} {X} forall {AB:times A B A+B} {CD:times C D C+D} {ABCD:times A+B C+D X} exists {A+C} {B+D} {AC:times A C A+C} {BD:times B D B+D} {ACBD:times A+C B+D X} true. - : times-double-associative X1*X2=X3 X4*X8=XC X3*XC=XF X5 XA X1*X4=X5 X2*X8=XA X5*XA=XF <- times-associative X1*X2=X3 X3*XC=XF XE X2*XC=XE X1*XE=XF <- times-commutative X4*X8=XC X8*X4=XC <- times-associative-converse X8*X4=XC X2*XC=XE XA X2*X8=XA XA*X4=XE <- times-commutative XA*X4=XE X4*XA=XE <- times-associative-converse X4*XA=XE X1*XE=XF X5 X1*X4=X5 X5*XA=XF. %worlds () (times-double-associative _ _ _ _ _ _ _ _). %total { } (times-double-associative _ _ _ _ _ _ _ _). %theorem times-right-cancels: forall* {X1} {Y1} {Z1} {X2} {Y2} {Z2} forall {T1:times X1 (s Y1) Z1} {T2:times X2 (s Y2) Z2} {EY:eq Y1 Y2} {EZ:eq Z1 Z2} exists {EX:eq X1 X2} true. - : times-right-cancels times/z times/z EY eq/ eq/. - : {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} times-right-cancels (times/s T1 P1) (times/s T2 P2) EY EZ EX' <- succ-deterministic EY EY' <- plus-right-cancels P1 P2 EY' EZ EZ' <- times-right-cancels T1 T2 EY EZ' EX <- succ-deterministic EX 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*: forall* {X1} {Y} {Y-1} {Z1} {X2} {Z2} forall {T1:times X1 Y Z1} {T2:times X2 Y Z2} {EY:eq Y (s Y-1)} {EZ:eq Z1 Z2} exists {EX:eq X1 X2} true. - : times-right-cancels* X1*Y=Z1 X2*Y=Z2 Y+ Z1=Z2 X1=X2 <- times-respects-eq X1*Y=Z1 eq/ Y+ eq/ X1*Y+=Z1 <- times-respects-eq X2*Y=Z2 eq/ Y+ eq/ X2*Y+=Z2 <- times-right-cancels X1*Y+=Z1 X2*Y+=Z2 eq/ 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**: forall* {X1} {Y1} {Z} {X2} {Y2} {Z-} forall {T1:times X1 Y1 Z} {T2:times X2 Y2 Z} {EY:eq Y1 Y2} {EZ:eq Z (s Z-)} exists {EX:eq X1 X2} true. - : times-right-cancels** X1*0=sZ X2*0=sZ eq/ eq/ X1=X2 <- times-right-zero _ X1*0=0 <- times-deterministic X1*0=0 X1*0=sZ eq/ eq/ ZERO=sZ <- succ-implies-gt ZERO=sZ ZERO>sZ <- gt-contradiction ZERO>sZ F <- false-implies-eq F X1=X2. - : 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 : forall* {X1} {Y1} {Z1} {X2} {Y2} {Z2} forall {T1:times (s X1) Y1 Z1} {T2:times (s X2) Y2 Z2} {E1:eq X1 X2} {E2:eq Z1 Z2} exists {F:eq Y1 Y2} true. - : times-left-cancels SX1*Y1=Z1 SX2*Y2=Z2 X1=X2 Z1=Z2 Y1=Y2 <- times-commutative SX1*Y1=Z1 Y1*sX1=Z1 <- times-commutative SX2*Y2=Z2 Y2*sX2=Z2 <- times-right-cancels Y1*sX1=Z1 Y2*sX2=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* : forall* {X} {Y1} {Z1} {X-} {Y2} {Z2} forall {T1:times X Y1 Z1} {T2:times X Y2 Z2} {E1:eq X (s X-)} {E2:eq Z1 Z2} exists {F:eq Y1 Y2} true. - : times-left-cancels* X*Y1=Z1 X*Y2=Z2 X+ Z1=Z2 Y1=Y2 <- times-commutative X*Y1=Z1 Y1*X=Z1 <- times-commutative X*Y2=Z2 Y2*X=Z2 <- times-right-cancels* Y1*X=Z1 Y2*X=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 : forall* {M} {N1} {N2} {P1} {P2} forall {GN:gt N1 N2} {T1:times (s M) N1 P1} {T2:times (s M) N2 P2} exists {GP:gt P1 P2} true. - : times-left-preserves-gt N1>N2 (times/s times/z plus/z) (times/s times/z plus/z) N1>N2. - : times-left-preserves-gt N1>N2 (times/s (T1:times (s M) N1 X1) X1+N1=O1) (times/s (T2:times (s M) N2 X2) X2+N2=O2) O1>O2 <- times-left-preserves-gt N1>N2 T1 T2 X1>X2 <- plus-preserves-gt* X1>X2 N1>N2 X1+N1=O1 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* : forall* {M} {M-} {N1} {N2} {P1} {P2} forall {GN:gt N1 N2} {T1:times M N1 P1} {T2:times M N2 P2} {M+:eq M (s M-)} exists {GP:gt P1 P2} true. - : times-left-preserves-gt* N1>N2 M*N1=P1 M*N2=P2 M+ P1>P2 <- times-respects-eq M*N1=P1 M+ eq/ eq/ SM-*N1=P1 <- times-respects-eq M*N2=P2 M+ eq/ eq/ SM-*N2=P2 <- times-left-preserves-gt N1>N2 SM-*N1=P1 SM-*N2=P2 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 : forall* {M1} {M2} {N} {P1} {P2} forall {G1:gt M1 M2} {T1:times M1 (s N) P1} {T2:times M2 (s N) P2} exists {G2:gt P1 P2} true. - : times-right-preserves-gt M1>M2 M1*sN=P1 M2*sN=P2 P1>P2 <- times-commutative M1*sN=P1 SN*M1=P1 <- times-commutative M2*sN=P2 SN*M2=P2 <- times-left-preserves-gt M1>M2 SN*M1=P1 SN*M2=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* : forall* {M1} {M2} {N} {N-1} {P1} {P2} forall {G1:gt M1 M2} {T1:times M1 N P1} {T2:times M2 N P2} {N+:eq N (s N-1)} exists {G2:gt P1 P2} true. - : times-right-preserves-gt* M1>M2 M1*N=P1 M2*N=P2 N=sN-1 P1>P2 <- times-respects-eq M1*N=P1 eq/ N=sN-1 eq/ M1*N+=P1 <- times-respects-eq M2*N=P2 eq/ N=sN-1 eq/ M2*N+=P2 <- times-right-preserves-gt M1>M2 M1*N+=P1 M2*N+=P2 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 : forall* {M1} {N1} {P1} {M2} {N2} {P2} forall {GM:gt M1 M2} {GN:gt N1 N2} {T1:times M1 N1 P1} {T2:times M2 N2 P2} exists {GP:gt P1 P2} true. - : {0=0': eq z _} times-preserves-gt (M1>M2:gt M1 M2) (N1>0:gt N1 z) (M1*N1=P1:times M1 N1 P1) M2*0=0' P1>0' <- gt-implies-positive M1>M2 M1' M1=sM1' <- times-respects-eq M1*N1=P1 M1=sM1' eq/ eq/ SM1'*N1=P1 <- times-right-zero M2 M2*0=0 <- times-deterministic M2*0=0 M2*0=0' eq/ eq/ 0=0' <- times-right-zero (s M1') SM1'*0=0 <- times-left-preserves-gt N1>0 SM1'*N1=P1 SM1'*0=0 P1>0 <- gt-respects-eq P1>0 eq/ 0=0' P1>0'. - : times-preserves-gt M1>M2 (N1>sN2':gt N1 (s N2')) M1*N1=P1 M2*sN2'=P2 P1>P2 <- gt-implies-positive M1>M2 M1' M1=sM1' <- times-respects-eq M1*N1=P1 M1=sM1' eq/ eq/ SM1'*N1=P1 <- times-total (SM1'*sN2'=PX:times (s M1') (s N2') _) <- times-left-preserves-gt N1>sN2' SM1'*N1=P1 SM1'*sN2'=PX P1>PX <- eq-symmetric M1=sM1' SM1'=M1 <- times-respects-eq SM1'*sN2'=PX SM1'=M1 eq/ eq/ M1*sN2'=PX <- times-right-preserves-gt M1>M2 M1*sN2'=PX M2*sN2'=P2 PX>P2 <- gt-transitive P1>PX PX>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 : forall* {X1:nat} {X2:nat} {Y1:nat} {Y2:nat} {Z1:nat} {Z2:nat} forall {P1:times X1 Y1 Z1} {P2:times X2 Y2 Z2} {EY:eq Y1 Y2} {G1:gt Z1 Z2} exists {G2:gt X1 X2} true. - : times-right-cancels-gt (times/s X1*Y=N1 N1+Y=Z1) times/z eq/ Z1>0 SX1>0 <- succ-implies-gt-zero _ SX1>0. - : 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 <- plus-right-cancels-gt N1+Y=Z1 N2+Y=Z2 eq/ Z1>Z2 N1>N2 <- times-right-cancels-gt X1*Y=N1 X2*Y=N2 eq/ N1>N2 X1>X2 <- succ-preserves-gt X1>X2 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 : forall* {X1:nat} {X2:nat} {Y1:nat} {Y2:nat} {Z1:nat} {Z2:nat} forall {P1:times X1 Y1 Z1} {P2:times X2 Y2 Z2} {EX:eq X1 X2} {G1:gt Z1 Z2} exists {G2:gt Y1 Y2} true. - : times-left-cancels-gt X1*Y1=Z1 X2*Y2=Z2 X1=X2 Z1>Z2 Y1>Y2 <- times-commutative X1*Y1=Z1 Y1*X1=Z1 <- times-commutative X2*Y2=Z2 Y2*X2=Z2 <- times-right-cancels-gt Y1*X1=Z1 Y2*X2=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 _ _ _ _). %%%%% nat-inv.elf %%%%% Minus for natural numbers %%%%% This file is part of the nat.elf signature %%%% Definitions %abbrev minus = [X1] [X2] [X3] plus X3 X2 X1. %%%% Theorems %%% Theorems about minus %abbrev false-implies-minus = false-implies-plus. %theorem minus-respects-eq : forall* {X1} {X2} {X3} {X4} {X5} {X6} forall {D:minus X1 X2 X3} {E1:eq X1 X4} {E2:eq X2 X5} {E3:eq X3 X6} exists {DP:minus X4 X5 X6} true. - : minus-respects-eq S eq/ eq/ eq/ S. %worlds () (minus-respects-eq _ _ _ _ _). %total {} (minus-respects-eq _ _ _ _ _). %theorem minus-deterministic : forall* {X1} {X2} {X3} {X4} {X5} {X6} forall {S:minus X1 X2 X3} {SP:minus X4 X5 X6} {E1:eq X1 X4} {E2:eq X2 X5} exists {E3:eq X3 X6} true. - : minus-deterministic X3+X2=X1 X6+X5=X4 X1=X4 X2=X5 X3=X6 <- plus-right-cancels X3+X2=X1 X6+X5=X4 X2=X5 X1=X4 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* : forall* {X1} {X2} {X3} {X4} {X6} {X7} forall {OP1:plus X1 X2 X3} {IOP1:minus X3 X4 X7} {IOP2:minus X2 X4 X6} exists {OP2:plus X1 X6 X7} true. - : plus-associates-with-minus* X1+X2=X3 X7+X4=X3 X6+X4=X2 X1+X6=X7 <- plus-associative-converse X6+X4=X2 X1+X2=X3 X7P X1+X6=X7P X7P+X4=X3 <- plus-right-cancels X7P+X4=X3 X7+X4=X3 eq/ eq/ X7P=X7 <- plus-respects-eq X1+X6=X7P eq/ eq/ X7P=X7 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* : forall* {X1} {X2} {X3} {X4} {X6} {X7} forall {IOP2:minus X2 X4 X6} {OP2:plus X1 X6 X7} {OP1:plus X1 X2 X3} exists {IOP1:minus X3 X4 X7} true. - : plus-associates-with-minus-converse* X6+X4=X2 X1+X6=X7 X1+X2=X3 X7+X4=X3 <- plus-associative-converse* X6+X4=X2 X1+X2=X3 X1+X6=X7 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 : forall* {X1} {X2} {X4} {X6} {X7} forall {IOP2:minus X2 X4 X6} {OP2:plus X1 X6 X7} exists {X3} {OP1:plus X1 X2 X3} {IOP1:minus X3 X4 X7} true. - : plus-associates-with-minus-converse X6+X4=X2 X1+X6=X7 X3 X1+X2=X3 X7+X4=X3 <- plus-total X1+X2=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 %{=>}% X3 X1+X2=X3 X3-X4=X7). %total {} (plus-associates-with-minus-converse _ _ _ _ _). %theorem minus-associates-from-plus* : forall* {X1} {X2} {X3} {X4} {X6} {X7} forall {IOP1:minus X1 X2 X3} {OP1:plus X3 X4 X7} {IOP2:minus X2 X4 X6} exists {IOP3:minus X1 X6 X7} true. - : minus-associates-from-plus* X3+X2=X1 X3+X4=X7 X6+X4=X2 X7+X6=X1 <- plus-commutative X6+X4=X2 X4+X6=X2 <- plus-associative-converse* X4+X6=X2 X3+X2=X1 X3+X4=X7 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* : forall* {X1} {X2} {X3} {X4} {X6} {X7} forall {IOP2:minus X2 X4 X6} {IOP3:minus X1 X6 X7} {IOP1:minus X1 X2 X3} exists {OP1:plus X3 X4 X7} true. - : minus-associates-from-plus-converse* X6+X4=X2 X7+X6=X1 X3+X2=X1 X3+X4=X7 <- plus-commutative X6+X4=X2 X4+X6=X2 <- plus-associative-converse X4+X6=X2 X3+X2=X1 X7P X3+X4=X7P X7P+X6=X1 <- plus-right-cancels X7P+X6=X1 X7+X6=X1 eq/ eq/ X7P=X7 <- plus-respects-eq X3+X4=X7P eq/ eq/ X7P=X7 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* : forall* {X1} {X2} {X3} {X4} {X6} {X7} forall {IOP1:minus X1 X2 X3} {IOP2:minus X3 X4 X7} {OP1:plus X2 X4 X6} exists {IOP3:minus X1 X6 X7} true. - : minus-associates-to-plus* X3+X2=X1 X7+X4=X3 X2+X4=X6 X7+X6=X1 <- plus-commutative X2+X4=X6 X4+X2=X6 <- plus-associative* X7+X4=X3 X3+X2=X1 X4+X2=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 : forall* {X1} {X2} {X3} {X4} {X7} forall {IOP1:minus X1 X2 X3} {IOP2:minus X3 X4 X7} exists {X6} {OP1:plus X2 X4 X6} {IOP3:minus X1 X6 X7} true. - : minus-associates-to-plus X3+X2=X1 X7+X4=X3 X6 X2+X4=X6 X7+X6=X1 <- plus-associative X7+X4=X3 X3+X2=X1 X6 X4+X2=X6 X7+X6=X1 <- plus-commutative X4+X2=X6 X2+X4=X6. %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* : forall* {X1} {X2} {X3} {X4} {X6} {X7} forall {OP1:plus X2 X4 X6} {IOP3:minus X1 X6 X7} {IOP1:minus X1 X2 X3} exists {IOP2:minus X3 X4 X7} true. - : minus-associates-to-plus-converse* X2+X4=X6 X7+X6=X1 X3+X2=X1 X7+X4=X3 <- plus-commutative X2+X4=X6 X4+X2=X6 <- plus-associative-converse X4+X2=X6 X7+X6=X1 X3P X7+X4=X3P X3P+X2=X1 <- plus-right-cancels X3P+X2=X1 X3+X2=X1 eq/ eq/ X3P=X3 <- plus-respects-eq X7+X4=X3P eq/ eq/ X3P=X3 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 : forall* {X1} {X2} {X4} {X6} {X7} forall {OP1:plus X2 X4 X6} {IOP3:minus X1 X6 X7} exists {X3} {IOP1:minus X1 X2 X3} {IOP2:minus X3 X4 X7} true. - : minus-associates-to-plus-converse X2+X4=X6 X7+X6=X1 X3 X3+X2=X1 X7+X4=X3 <- plus-commutative X2+X4=X6 X4+X2=X6 <- plus-associative-converse X4+X2=X6 X7+X6=X1 X3 X7+X4=X3 X3+X2=X1. %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 : forall* {N1} {N2} {N3} forall {P:minus N1 N2 N3} {E3:eq N3 z} exists {E1:eq N1 N2} true. - : 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 _ _ _). %abbrev minus-implies-gt = plus-implies-gt. %theorem minus-left-cancels : forall* {X1} {X2} {X3} {X4} {X5} {X6} forall {IOP1:minus X1 X2 X3} {IOP2:minus X4 X5 X6} {E1:eq X1 X4} {E3:eq X3 X6} exists {E2:eq X2 X5} true. - : minus-left-cancels X3+X2=X1 X6+X5=X4 X1=X4 X3=X6 X2=X5 <- plus-left-cancels X3+X2=X1 X6+X5=X4 X3=X6 X1=X4 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 : forall* {X1} {X2} {X3} {X4} {X5} {X6} forall {IOP1:minus X1 X2 X3} {IOP2:minus X4 X5 X6} {E2:eq X2 X5} {E3:eq X3 X6} exists {E1:eq X1 X4} true. - : minus-right-cancels X3+X2=X1 X6+X5=X4 X2=X5 X3=X6 X1=X4 <- plus-deterministic X3+X2=X1 X6+X5=X4 X3=X6 X2=X5 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* : forall* {X1} {X2} {X3} {X4} {X5} forall {G:gt X2 X4} {IOP1:minus X1 X2 X3} {IOP2:minus X1 X4 X5} exists {GP:gt X5 X3} true. - : minus-left-inverts-gt* X2>X4 X3+X2=X1 X5+X4=X1 X5>X3 <- plus-total X3+X4=X7 <- plus-left-preserves-gt* X2>X4 X3+X2=X1 X3+X4=X7 X1>X7 <- plus-right-cancels-gt X5+X4=X1 X3+X4=X7 eq/ X1>X7 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* : forall* {X1} {X2} {X3} {X4} {X5} forall {G:gt X1 X2} {IOP1:minus X1 X3 X4} {IOP2:minus X2 X3 X5} exists {GP:gt X4 X5} true. - : minus-right-preserves-gt* X1>X2 X4+X3=X1 X5+X3=X2 X4>X5 <- plus-right-cancels-gt X4+X3=X1 X5+X3=X2 eq/ X1>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 : forall* {X1} {X2} {X3} {X4} {X5} {X6} forall {IOP1:minus X1 X2 X3} {IOP2:minus X4 X5 X6} {E:eq X1 X4} {G:gt X3 X6} exists {GP:gt X5 X2} true. - : minus-left-cancels-inverts-gt X3+X2=X1 X6+X5=X4 X1=X4 X3>X6 X5>X2 <- plus-total X6+X2=X7 <- plus-right-preserves-gt* X3>X6 X3+X2=X1 X6+X2=X7 X1>X7 <- eq-symmetric X1=X4 X4=X1 <- plus-respects-eq X6+X5=X4 eq/ eq/ X4=X1 X6+X5=X1 <- plus-left-cancels-gt X6+X5=X1 X6+X2=X7 eq/ X1>X7 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 : forall* {X1} {X2} {X3} {X4} {X5} {X6} forall {IOP1:minus X1 X2 X3} {IOP2:minus X4 X5 X6} {E2:eq X2 X5} {G3:gt X3 X6} exists {G1:gt X1 X4} true. - : minus-right-cancels-gt X3+X2=X1 X6+X5=X4 X2=X5 X3>X6 X1>X4 <- plus-respects-eq X3+X2=X1 eq/ X2=X5 eq/ X3+X5=X1 <- plus-right-preserves-gt* X3>X6 X3+X5=X1 X6+X5=X4 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 : forall* {X1} {X2} {X3} {X4} {X7} forall {S12:minus X1 X2 X3} {M34:times X3 X4 X7} exists {X5} {X6} {M14:times X1 X4 X5} {M24:times X2 X4 X6} {S56:minus X5 X6 X7} true. - : times-right-distributes-over-minus X3+X2=X1 X3*X4=X7 _ _ X1*X4=X5 X2*X4=X6 X7+X6=X5 <- times-total X1*X4=X5 <- times-right-distributes-over-plus X3+X2=X1 X1*X4=X5 _ _ X3*X4=Y7 X2*X4=X6 Y7+X6=X5 <- times-deterministic X3*X4=Y7 X3*X4=X7 eq/ eq/ Y7=X7 <- plus-respects-eq Y7+X6=X5 Y7=X7 eq/ eq/ 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* : forall* {X1} {X2} {X3} {X4} {X5} {X6} {X7} forall {A12:minus X1 X2 X3} {M34:times X3 X4 X7} {M14:times X1 X4 X5} {M24:times X2 X4 X6} exists {A56:minus X5 X6 X7} true. - : times-right-distributes-over-minus* X1-X2=X3 X3*X4=X7 X1*X4=X5 X2*X4=X6 X5-X6=X7 <- times-right-distributes-over-minus X1-X2=X3 X3*X4=X7 Y5 Y6 X1*X4=Y5 X2*X4=Y6 Y5-Y6=X7 <- times-deterministic X1*X4=Y5 X1*X4=X5 eq/ eq/ Y5=X5 <- times-deterministic X2*X4=Y6 X2*X4=X6 eq/ eq/ Y6=X6 <- minus-respects-eq Y5-Y6=X7 Y5=X5 Y6=X6 eq/ 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* : forall* {X1} {X2} {X3} {X4} {X5} {X6} {X7} forall {A12:minus X2 X4 X6} {M34:times X1 X6 X7} {M14:times X1 X2 X3} {M24:times X1 X4 X5} exists {A56:minus X3 X5 X7} true. - : times-left-distributes-over-minus* X2-X4=X6 X1*X6=X7 X1*X2=X3 X1*X4=X5 X3-X5=X7 <- times-commutative X1*X6=X7 X6*X1=X7 <- times-commutative X1*X2=X3 X2*X1=X3 <- times-commutative X1*X4=X5 X4*X1=X5 <- times-right-distributes-over-minus* X2-X4=X6 X6*X1=X7 X2*X1=X3 X4*X1=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 : forall* {X1} {X2} {X4} {X6} {X7} forall {A12:minus X2 X4 X6} {M34:times X1 X6 X7} exists {X3} {X5} {M14:times X1 X2 X3} {M24:times X1 X4 X5} {A56:minus X3 X5 X7} true. - : times-left-distributes-over-minus X2-X4=X6 X1*X6=X7 X3 X5 X1*X2=X3 X1*X4=X5 X3-X5=X7 <- times-total X1*X2=X3 <- times-total X1*X4=X5 <- 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 %{=>}% X3 X5 X1*X2=X3 X1*X4=X5 X3-X5=X7). %total {} (times-left-distributes-over-minus _ _ _ _ _ _ _). %theorem times-right-factors-over-minus* : forall* {X1} {X2} {X3} {X4} {X5} {X6} {X7} forall {M14:times X1 X4 X5} {M24:times X2 X4 X6} {A56:minus X5 X6 X7} {A12:minus X1 X2 X3} exists {M34:times X3 X4 X7} true. - : times-right-factors-over-minus* X1*X4=X5 X2*X4=X6 X5-X6=X7 X1-X2=X3 X3*X4=X7 <- times-total X3*X4=Y7 <- times-right-distributes-over-minus* X1-X2=X3 X3*X4=Y7 X1*X4=X5 X2*X4=X6 X5-X6=Y7 <- minus-deterministic X5-X6=Y7 X5-X6=X7 eq/ eq/ Y7=X7 <- times-respects-eq X3*X4=Y7 eq/ eq/ Y7=X7 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* : forall* {X1} {X2} {X3} {X4} {X5} {X6} {X7} forall {M12:times X1 X2 X3} {M14:times X1 X4 X5} {A35:minus X3 X5 X7} {A24:minus X2 X4 X6} exists {M16:times X1 X6 X7} true. - : times-left-factors-over-minus* X1*X2=X3 X1*X4=X5 X3-X5=X7 X2-X4=X6 X1*X6=X7 <- times-total X1*X6=Y7 <- times-left-distributes-over-minus* X2-X4=X6 X1*X6=Y7 X1*X2=X3 X1*X4=X5 X3-X5=Y7 <- minus-deterministic X3-X5=Y7 X3-X5=X7 eq/ eq/ Y7=X7 <- times-respects-eq X1*X6=Y7 eq/ eq/ Y7=X7 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 : forall* {Y} {Z} {XY} {XZ} {YZ} {XYZ} {Z-} forall {TXY:times XY Z XYZ} {TY:times Y Z YZ} {M:minus XYZ YZ XZ} {EZ:eq Z (s Z-)} exists {X} {M':minus XY Y X} {TX:times X Z XZ} true. % minus isn't total, so this is harder. - : times-right-factors-over-minus XY*Z=YZ Y*Z=YZ plus/z eq/ z ZERO+Y=XY times/z <- times-right-cancels* XY*Z=YZ Y*Z=YZ eq/ eq/ XY=Y <- plus-respects-eq plus/z eq/ XY=Y eq/ ZERO+Y=XY. - : times-right-factors-over-minus XY*Z=XYZ Y*Z=YZ XZ+YZ=XYZ _ (s X-) X+Y=XY X*Z=XZ %% we assume XZ is of the form (s XZ-) <- plus-implies-gt XZ+YZ=XYZ eq/ XYZ>YZ <- times-right-cancels-gt XY*Z=XYZ Y*Z=YZ eq/ XYZ>YZ XY>Y <- gt-implies-plus XY>Y X- X+Y=XY <- times-right-factors-over-minus* XY*Z=XYZ Y*Z=YZ XZ+YZ=XYZ 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 : forall* {X} {Y} {Z} {XY} {XZ} {XYZ} {X-} forall {TXY:times X Y XY} {TXZ:times X Z XZ} {M:minus XY XZ XYZ} {EX:eq X (s X-)} exists {YZ} {MYZ:minus Y Z YZ} {TXYZ:times X YZ XYZ} true. - : times-left-factors-over-minus X*Y=XY X*Z=XZ XY-XZ=XYZ X=sX- YZ Y-Z=YZ X*YZ=XYZ <- times-commutative X*Y=XY Y*X=XY <- times-commutative X*Z=XZ Z*X=XZ <- 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 YZ*X=XYZ 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 _ _ _ _ _ _ _). %%%%% nat-comp.elf %%%%% Composed relations for natural numbers %%%%% This file is part of the nat.elf signature %%%% Definitions ge : nat -> nat -> type. ge/= : ge X Y <- eq X Y. ge/> : ge X Y <- gt X Y. %%%% Theorems %%% Theorems about ge %theorem false-implies-ge : forall* {X1} {X2} forall {F:void} exists {G:ge X1 X2} true. %worlds () (false-implies-ge _ _). %total { } (false-implies-ge _ _). %theorem ge-respects-eq : forall* {X1} {X2} {Y1} {Y2} forall {D1:ge X1 X2} {E1:eq X1 Y1} {E2:eq X2 Y2} exists {D2:ge Y1 Y2} true. - : ge-respects-eq X1>=X2 eq/ eq/ X1>=X2. %worlds () (ge-respects-eq _ _ _ _). %total { } (ge-respects-eq _ _ _ _). %theorem ge-reflexive : forall {X} exists {G:ge X X} true. - : ge-reflexive _ (ge/= eq/). %worlds () (ge-reflexive X %{=>}% X>=X). %total {} (ge-reflexive _ _). %theorem ge-transitive: forall* {X1} {X2} {X3} forall {G1:ge X1 X2} {G2:ge X2 X3} exists {G3:ge X1 X3} true. - : ge-transitive (ge/= eq/) (ge/= eq/) (ge/= eq/). - : ge-transitive (ge/= eq/) (ge/> X>X3) (ge/> X>X3). - : ge-transitive (ge/> X1>X) (ge/= eq/) (ge/> X1>X). - : ge-transitive (ge/> X1>X2) (ge/> X2>X3) (ge/> X1>X3) <- gt-transitive X1>X2 X2>X3 X1>X3. %worlds () (ge-transitive X1>=X2 X2>=X3 %{=>}% X1>=X3). %total {} (ge-transitive _ _ _). %theorem ge-anti-symmetric : forall* {X1} {X2} forall {G1:ge X1 X2} {G2:ge X2 X1} exists {E:eq X1 X2} true. - : ge-anti-symmetric (ge/= eq/) _ eq/. - : ge-anti-symmetric _ (ge/= eq/) eq/. - : ge-anti-symmetric (ge/> X1>X2) (ge/> X2>X1) X1=X2 <- gt-anti-symmetric X1>X2 X2>X1 F <- false-implies-eq F X1=X2. %worlds () (ge-anti-symmetric X1>=X2 X2>=X1 %{=>}% X1=X2). %total {} (ge-anti-symmetric _ _ _). %theorem ge-transitive-gt: forall* {X1} {X2} {X3} forall {G1:ge X1 X2} {G2:gt X2 X3} exists {G3:gt X1 X3} true. - : ge-transitive-gt (ge/= eq/) X>X3 X>X3. - : ge-transitive-gt (ge/> X1>X2) X2>X3 X1>X3 <- gt-transitive X1>X2 X2>X3 X1>X3. %worlds () (ge-transitive-gt X1>=X2 X2>X3 %{=>}% X1>X3). %total {} (ge-transitive-gt _ _ _). %theorem gt-transitive-ge: forall* {X1} {X2} {X3} forall {G1:gt X1 X2} {G2:ge X2 X3} exists {G3:gt X1 X3} true. - : gt-transitive-ge X1>X2 (ge/= eq/) X1>X2. - : gt-transitive-ge X1>X2 (ge/> X2>X3) X1>X3 <- gt-transitive X1>X2 X2>X3 X1>X3. %worlds () (gt-transitive-ge X1>X2 X2>=X3 %{=>}% X1>X3). %total {} (gt-transitive-ge _ _ _). %theorem meta-ge : forall {M} {N} {G:ge M N} true. - : meta-ge _ _ (ge/= eq/). - : meta-ge _ _ (ge/> M>N) <- meta-gt _ _ M>N. %worlds () (meta-ge _ _ _). %total { } (meta-ge _ _ _). %reduces N <= M (meta-ge M N _). %theorem succ-preserves-ge : forall* {M} {N} forall {G:ge M N} exists {G':ge (s M) (s N)} true. - : succ-preserves-ge (ge/= eq/) (ge/= eq/). - : succ-preserves-ge (ge/> N>M) (ge/> N+1>M+1) <- succ-preserves-gt N>M N+1>M+1. %worlds () (succ-preserves-ge M>=N %{=>}% M+1>=N+1). %total {} (succ-preserves-ge _ _). %theorem succ-preserves-ge-converse : forall* {M} {N} forall {G':ge (s M) (s N)} exists {G:ge M N} true. - : succ-preserves-ge-converse (ge/= eq/) (ge/= eq/). - : succ-preserves-ge-converse (ge/> N+1>M+1) (ge/> N>M) <- succ-preserves-gt-converse N+1>M+1 N>M. %worlds () (succ-preserves-ge-converse M+1>=N+1 %{=>}% M>=N). %total {} (succ-preserves-ge-converse _ _). %theorem ge-succ-implies-gt : forall* {N1} {N2} forall {G:ge N1 (s N2)} exists {G':gt N1 N2} true. - : ge-succ-implies-gt (ge/= eq/) (gt/1). - : ge-succ-implies-gt (ge/> N1>sN2) N1>N2 <- gt-transitive N1>sN2 (gt/1) N1>N2. %worlds () (ge-succ-implies-gt _ _). %total { } (ge-succ-implies-gt _ _). %theorem ge-implies-succ-gt : forall* {N1} {N2} forall {G:ge N1 N2} exists {G':gt (s N1) N2} true. - : ge-implies-succ-gt N1>=N2 N1+1>N2 <- succ-preserves-ge N1>=N2 N1+1>=N2+1 <- ge-succ-implies-gt N1+1>=N2+1 N1+1>N2. %worlds () (ge-implies-succ-gt _ _). %total { } (ge-implies-succ-gt _ _). %theorem succ-gt-implies-ge : forall* {N1} {N2} forall {G:gt (s N1) N2} exists {G':ge N1 N2} true. - : succ-gt-implies-ge (gt/1) (ge/= eq/). - : 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 : forall* {N1} {N2} forall {G':gt N1 N2} exists {G:ge N1 (s N2)} true. - : gt-implies-ge-succ N1>N2 N1>=N2+1 <- succ-preserves-gt N1>N2 N1+1>N2+1 <- succ-gt-implies-ge N1+1>N2+1 N1>=N2+1. %worlds () (gt-implies-ge-succ _ _). %total { } (gt-implies-ge-succ _ _). %theorem ge-implies-plus: forall* {N1} {N2} forall {G:ge N2 N1} exists {N0} {P:plus N0 N1 N2} true. - : ge-implies-plus (ge/= eq/) z plus/z. - : ge-implies-plus (ge/> N2>N1) (s N0) P <- gt-implies-plus N2>N1 N0 P. %worlds () (ge-implies-plus N2>=N1 %{=>}% N0 N0+N1=N2). %total { } (ge-implies-plus _ _ _). %theorem plus-implies-ge: forall* {N0} {N1} {N2} forall {P:plus N0 N1 N2} exists {G:ge N2 N1} true. - : plus-implies-ge plus/z (ge/= eq/). - : plus-implies-ge P (ge/> N2>N1) <- plus-implies-gt P eq/ N2>N1. %worlds () (plus-implies-ge N0+N1=N2 %{=>}% N2>=N1). %total { } (plus-implies-ge _ _). %theorem ge-zero-always : forall {N} exists {G:ge N z} true. - : ge-zero-always _ N>=0 <- plus-right-identity _ N+0=N <- plus-implies-ge N+0=N N>=0. %worlds () (ge-zero-always _ _). %total { } (ge-zero-always _ _). %theorem nonzero-times-implies-ge : forall* {N0} {N1} {N2} forall {P:times (s N0) N1 N2} exists {G:ge N2 N1} true. - : nonzero-times-implies-ge (times/s _ X+N1=N2) N2>=N1 <- plus-implies-ge 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 : forall* {N0} {N1} {N2} forall {P:times N0 (s N1) N2} exists {G:ge N2 N0} true. - : times-nonzero-implies-ge A*B=C C>=A <- times-commutative A*B=C B*A=C <- nonzero-times-implies-ge B*A=C C>=A. %worlds () (times-nonzero-implies-ge _ _). %total { } (times-nonzero-implies-ge _ _). %theorem non-trivial-times-implies-much-gt* : forall* {N1} {N2} {N3} forall {D:times (s (s N1)) (s (s N2)) N3} exists {G:gt N3 (s (s (s N1)))} true. - : non-trivial-times-implies-much-gt* (times/s (times/s N1*ssN2=P1 P1+ssN2=P2) P2+ssN2=N3) N3>sssN1 <- times-nonzero-implies-ge N1*ssN2=P1 P1>=N1 <- succ-preserves-ge P1>=N1 SP1>=sN1 <- plus-swap-succ-converse P1+ssN2=P2 SP1+sN2=P2 <- plus-commutative SP1+sN2=P2 SN2+sP1=P2 <- plus-implies-gt SN2+sP1=P2 eq/ P2>sP1 <- gt-transitive-ge P2>sP1 SP1>=sN1 P2>sN1 <- succ-preserves-gt P2>sN1 SP2>ssN1 <- gt-implies-ge-succ SP2>ssN1 SP2>=sssN1 <- plus-commutative P2+ssN2=N3 SSN2+P2=N3 <- plus-swap-succ SSN2+P2=N3 SN2+sP2=N3 <- plus-implies-gt SN2+sP2=N3 eq/ N3>sP2 <- gt-transitive-ge N3>sP2 SP2>=sssN1 N3>sssN1. %worlds () (non-trivial-times-implies-much-gt* _ _). %total { } (non-trivial-times-implies-much-gt* _ _). %theorem non-trivial-times-implies-much-gt : forall* {N1} {N2} {N3} forall {D:times (s (s N1)) (s (s N2)) N3} exists {G1:gt N3 (s (s (s N1)))} {G2:gt N3 (s (s (s N2)))} true. - : non-trivial-times-implies-much-gt T G1 G2 <- non-trivial-times-implies-much-gt* T G1 <- times-commutative T Tc <- non-trivial-times-implies-much-gt* Tc G2. %worlds () (non-trivial-times-implies-much-gt _ _ _). %total { } (non-trivial-times-implies-much-gt _ _ _). %theorem plus-left-preserves-ge* : forall* {X1} {X2} {X3} {X4} {X5} forall {G:ge X2 X4} {OP1:plus X1 X2 X3} {OP2:plus X1 X4 X5} exists {G2:ge X3 X5} true. - : plus-left-preserves-ge* (ge/= eq/) X1+X2=X3 X1+X2=X5 (ge/= X3=X5) <- plus-deterministic X1+X2=X3 X1+X2=X5 eq/ eq/ X3=X5. - : plus-left-preserves-ge* (ge/> X2>X4) X1+X2=X3 X1+X4=X5 (ge/> X3>X5) <- plus-left-preserves-gt* X2>X4 X1+X2=X3 X1+X4=X5 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 : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {OP1:plus X1 X2 X3} {OP2:plus Y1 Y2 Y3} {E1:eq X1 Y1} {G3:ge X3 Y3} exists {G2:ge X2 Y2} true. - : plus-left-cancels-ge X1+X2=X3 X1+Y2=X3 eq/ (ge/= eq/) (ge/= X2=Y2) <- plus-left-cancels X1+X2=X3 X1+Y2=X3 eq/ eq/ X2=Y2. - : plus-left-cancels-ge X1+X2=X3 X1+Y2=Y3 eq/ (ge/> X3>Y3) (ge/> X2>Y2) <- plus-left-cancels-gt X1+X2=X3 X1+Y2=Y3 eq/ X3>Y3 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 : forall* {X1} {X2} {X4} forall {G:ge X2 X4} exists {X3} {X5} {O1:plus X1 X2 X3} {O2:plus X1 X4 X5} {G2:ge X3 X5} true. - : plus-left-preserves-ge X2>=X4 X3 X5 X1+X2=A3 X1+X4=X5 X3>=X5 <- plus-total X1+X2=A3 <- plus-total X1+X4=X5 <- plus-left-preserves-ge* X2>=X4 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* : forall* {X1} {X2} {X3} {X4} {X5} forall {G1:ge X1 X2} {O1:plus X1 X3 X4} {O2:plus X2 X3 X5} exists {G2:ge X4 X5} true. - : plus-right-preserves-ge* X1>=X2 X1+X3=X4 X2+X3=X5 X4>=X5 <- plus-commutative X1+X3=X4 X3+X1=X4 <- plus-commutative X2+X3=X5 X3+X2=X5 <- plus-left-preserves-ge* X1>=X2 X3+X1=X4 X3+X2=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 : forall* {X1} {X2} {X3} forall {G1:ge X1 X2} exists {X4} {X5} {O1:plus X1 X3 X4} {O2:plus X2 X3 X5} {G2:ge X4 X5} true. - : plus-right-preserves-ge X1>=X2 X4 X5 X1+X3=X4 X2+X3=X5 X4>=X5 <- plus-total X1+X3=X4 <- plus-total X2+X3=X5 <- plus-right-preserves-ge* X1>=X2 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* : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {G1:ge X1 Y1} {G2:ge X2 Y2} {MX:plus X1 X2 X3} {MY:plus Y1 Y2 Y3} exists {G3:ge X3 Y3} true. - : plus-preserves-ge* X1>=Y1 X2>=Y2 X1+X2=X3 Y1+Y2=Y3 X3>=Y3 <- plus-total Y1+X2=X <- plus-right-preserves-ge* X1>=Y1 X1+X2=X3 Y1+X2=X X3>=X <- plus-left-preserves-ge* X2>=Y2 Y1+X2=X Y1+Y2=Y3 X>=Y3 <- ge-transitive X3>=X X>=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 : forall* {X1} {X2} {Y1} {Y2} forall {G1:ge X1 Y1} {G2:ge X2 Y2} exists {X3} {Y3} {MX:plus X1 X2 X3} {MY:plus Y1 Y2 Y3} {G3:ge X3 Y3} true. - : plus-preserves-ge X1>=Y1 X2>=Y2 X3 Y3 X1+X2=X3 Y1+Y2=Y3 X3>=Y3 <- plus-total X1+X2=X3 <- plus-total Y1+Y2=Y3 <- plus-preserves-ge* X1>=Y1 X2>=Y2 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 : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {OP1:plus X1 X2 X3} {OP2:plus Y1 Y2 Y3} {E2:eq X2 Y2} {G3:ge X3 Y3} exists {G1:ge X1 Y1} true. - : plus-right-cancels-ge X1+X2=X3 Y1+Y2=Y3 X2=Y2 X3>=Y3 X1>=Y1 <- plus-commutative X1+X2=X3 X2+X1=X3 <- plus-commutative Y1+Y2=Y3 Y2+Y1=Y3 <- plus-left-cancels-ge X2+X1=X3 Y2+Y1=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 _ _ _ _ _). % Times preserves ge only because multiplying with zero yields equality. %theorem times-left-preserves-ge* : forall* {X1} {X2} {X3} {X4} {X5} forall {G:ge X2 X4} {OP1:times X1 X2 X3} {OP2:times X1 X4 X5} exists {G2:ge X3 X5} true. - : times-left-preserves-ge* _ times/z times/z (ge/= eq/). - : times-left-preserves-ge* (ge/= eq/) X1*X2=X3 X1*X2=X5 (ge/= X3=X5) <- times-deterministic X1*X2=X3 X1*X2=X5 eq/ eq/ X3=X5. - : times-left-preserves-ge* (ge/> X2>X4) X1*X2=X3 X1*X4=X5 (ge/> X3>X5) <- times-left-preserves-gt X2>X4 X1*X2=X3 X1*X4=X5 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 : forall* {X1} {X2} {X4} forall {G:ge X2 X4} exists {X3} {X5} {O1:times X1 X2 X3} {O2:times X1 X4 X5} {G2:ge X3 X5} true. - : times-left-preserves-ge X2>=X4 X3 X5 X1*X2=A3 X1*X4=X5 X3>=X5 <- times-total X1*X2=A3 <- times-total X1*X4=X5 <- times-left-preserves-ge* X2>=X4 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* : forall* {X1} {X2} {X3} {X4} {X5} forall {G1:ge X1 X2} {O1:times X1 X3 X4} {O2:times X2 X3 X5} exists {G2:ge X4 X5} true. - : times-right-preserves-ge* X1>=X2 X1*X3=X4 X2*X3=X5 X4>=X5 <- times-commutative X1*X3=X4 X3*X1=X4 <- times-commutative X2*X3=X5 X3*X2=X5 <- times-left-preserves-ge* X1>=X2 X3*X1=X4 X3*X2=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 : forall* {X1} {X2} {X3} forall {G1:ge X1 X2} exists {X4} {X5} {O1:times X1 X3 X4} {O2:times X2 X3 X5} {G2:ge X4 X5} true. - : times-right-preserves-ge X1>=X2 X4 X5 X1*X3=X4 X2*X3=X5 X4>=X5 <- times-total X1*X3=X4 <- times-total X2*X3=X5 <- times-right-preserves-ge* X1>=X2 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 _ _ _ _ _ _). %%%% Definitions ne : nat -> nat -> type. ne/< : ne X Y <- gt Y X. ne/> : ne X Y <- gt X Y. eq? : nat -> nat -> bool -> type. eq?/yes : eq? X X true. eq?/no : eq? X Y false <- ne X Y. %%%% Theorems %%% Theorems about ne %theorem false-implies-ne : forall* {X1} {X2} forall {F:void} exists {G:ne X1 X2} true. %worlds () (false-implies-ne _ _). %total { } (false-implies-ne _ _). %theorem ne-respects-eq : forall* {X1} {X2} {Y1} {Y2} forall {D1:ne X1 X2} {E1:eq X1 Y1} {E2:eq X2 Y2} exists {D2:ne Y1 Y2} true. - : ne-respects-eq X1<>X2 eq/ eq/ X1<>X2. %worlds () (ne-respects-eq _ _ _ _). %total { } (ne-respects-eq _ _ _ _). %theorem ne-anti-reflexive : forall* {X} forall {R:ne X X} exists {F:void} true. - : ne-anti-reflexive (ne/< X X>X) F <- gt-anti-reflexive X>X F. %worlds () (ne-anti-reflexive X<>X %{=>}% _). %total {} (ne-anti-reflexive _ _). %theorem ne-symmetric : forall* {X} {Y} forall {R1:ne X Y} exists {R2:ne Y X} true. - : ne-symmetric (ne/< X X X>Y) (ne/< X>Y). %worlds () (ne-symmetric X<>Y %{=>}% Y<>X). %total {} (ne-symmetric _ _). %theorem eq-ne-implies-false : forall* {X} {Y} forall {D1:eq X Y} {D2:ne X Y} exists {F:void} true. - : eq-ne-implies-false eq/ X<>X F <- ne-anti-reflexive X<>X F. %worlds () (eq-ne-implies-false X=Y X<>Y %{=>}% _). %total {} (eq-ne-implies-false _ _ _). %theorem ge-ne-implies-gt : forall* {X} {Y} forall {D1:ge X Y} {D2:ne X Y} exists {D3:gt X Y} true. - : ge-ne-implies-gt (ge/> X>Y) _ X>Y. - : ge-ne-implies-gt (ge/= eq/) X<>X X>X <- ne-anti-reflexive X<>X F <- false-implies-gt F X>X. %worlds () (ge-ne-implies-gt X>=Y X<>Y %{=>}% X>Y). %total {} (ge-ne-implies-gt _ _ _). %theorem eq?-total* : forall {M} {N} exists {B} {T:eq? M N B} true. %theorem eq?-total*/L : forall* {M} {N} {C} forall {CMP:compare M N C} exists {B} {T:eq? M N B} true. - : eq?-total*/L compare/= true eq?/yes. - : eq?-total*/L (compare/< X X>Y) false (eq?/no (ne/> X>Y)). %worlds () (eq?-total*/L _ _ _). %total { } (eq?-total*/L _ _ _). - : eq?-total* M N B T <- compare-total CMP <- eq?-total*/L CMP B T. %worlds () (eq?-total* _ _ _ _). %total { } (eq?-total* _ _ _ _). %abbrev eq?-total = eq?-total* _ _ _. %theorem succ-preserves-ne : forall* {M} {N} forall {D:ne M N} exists {D':ne (s M) (s N)} true. - : succ-preserves-ne (ne/< N>M) (ne/< N+1>M+1) <- succ-preserves-gt N>M N+1>M+1. - : succ-preserves-ne (ne/> N>M) (ne/> N+1>M+1) <- succ-preserves-gt N>M N+1>M+1. %worlds () (succ-preserves-ne M<>N %{=>}% M+1<>N+1). %total {} (succ-preserves-ne _ _). %theorem succ-preserves-ne-converse : forall* {M} {N} forall {D':ne (s M) (s N)} exists {D:ne M N} true. - : succ-preserves-ne-converse (ne/< N+1>M+1) (ne/< N>M) <- succ-preserves-gt-converse N+1>M+1 N>M. - : succ-preserves-ne-converse (ne/> N+1>M+1) (ne/> N>M) <- succ-preserves-gt-converse N+1>M+1 N>M. %worlds () (succ-preserves-ne-converse M+1<>N+1 %{=>}% M<>N). %total {} (succ-preserves-ne-converse _ _). %theorem plus-left-preserves-ne* : forall* {X1} {X2} {X3} {X4} {X5} forall {G:ne X2 X4} {OP1:plus X1 X2 X3} {OP2:plus X1 X4 X5} exists {G2:ne X3 X5} true. - : plus-left-preserves-ne* (ne/< X4>X2) X1+X2=X3 X1+X4=X5 (ne/< X5>X3) <- plus-left-preserves-gt* X4>X2 X1+X4=X5 X1+X2=X3 X5>X3. - : plus-left-preserves-ne* (ne/> X2>X4) X1+X2=X3 X1+X4=X5 (ne/> X3>X5) <- plus-left-preserves-gt* X2>X4 X1+X2=X3 X1+X4=X5 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 : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {OP1:plus X1 X2 X3} {OP2:plus Y1 Y2 Y3} {E1:eq X1 Y1} {G3:ne X3 Y3} exists {G2:ne X2 Y2} true. - : plus-left-cancels-ne X1+X2=X3 X1+Y2=Y3 eq/ (ne/< Y3>X3) (ne/< Y2>X2) <- 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/> X3>Y3) (ne/> X2>Y2) <- plus-left-cancels-gt X1+X2=X3 X1+Y2=Y3 eq/ X3>Y3 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 : forall* {X1} {X2} {X4} forall {G:ne X2 X4} exists {X3} {X5} {O1:plus X1 X2 X3} {O2:plus X1 X4 X5} {G2:ne X3 X5} true. - : plus-left-preserves-ne X2<>X4 X3 X5 X1+X2=A3 X1+X4=X5 X3<>X5 <- plus-total X1+X2=A3 <- plus-total X1+X4=X5 <- plus-left-preserves-ne* X2<>X4 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* : forall* {X1} {X2} {X3} {X4} {X5} forall {G1:ne X1 X2} {O1:plus X1 X3 X4} {O2:plus X2 X3 X5} exists {G2:ne X4 X5} true. - : plus-right-preserves-ne* X1<>X2 X1+X3=X4 X2+X3=X5 X4<>X5 <- plus-commutative X1+X3=X4 X3+X1=X4 <- plus-commutative X2+X3=X5 X3+X2=X5 <- plus-left-preserves-ne* X1<>X2 X3+X1=X4 X3+X2=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 : forall* {X1} {X2} {X3} forall {G1:ne X1 X2} exists {X4} {X5} {O1:plus X1 X3 X4} {O2:plus X2 X3 X5} {G2:ne X4 X5} true. - : plus-right-preserves-ne X1<>X2 X4 X5 X1+X3=X4 X2+X3=X5 X4<>X5 <- plus-total X1+X3=X4 <- plus-total X2+X3=X5 <- plus-right-preserves-ne* X1<>X2 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 : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {OP1:plus X1 X2 X3} {OP2:plus Y1 Y2 Y3} {E2:eq X2 Y2} {G3:ne X3 Y3} exists {G1:ne X1 Y1} true. - : plus-right-cancels-ne X1+X2=X3 Y1+Y2=Y3 X2=Y2 X3<>Y3 X1<>Y1 <- plus-commutative X1+X2=X3 X2+X1=X3 <- plus-commutative Y1+Y2=Y3 Y2+Y1=Y3 <- plus-left-cancels-ne X2+X1=X3 Y2+Y1=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 _ _ _ _ _). %%%%% nat-less.elf %%%%% Inverse relations for natural numbers %%%%% This file is part of the nat.elf signature %%%% Definitions %abbrev lt = [X] [Y] gt Y X. %%%% Theorems about lt %theorem false-implies-lt : forall* {X1} {X2} forall {F:void} exists {G:lt X1 X2} true. %worlds () (false-implies-lt _ _). %total { } (false-implies-lt _ _). %theorem lt-respects-eq : forall* {X1} {X2} {Y1} {Y2} forall {D1:lt X1 X2} {E1:eq X1 Y1} {E2:eq X2 Y2} exists {D2:lt Y1 Y2} true. - : lt-respects-eq X1X1 X1>X2 R <- gt-anti-symmetric X1>X2 X2>X1 R. %worlds () (lt-anti-symmetric _ _ _). %total {} (lt-anti-symmetric _ _ _). %theorem lt-transitive : forall* {X1} {X2} {X3} forall {G1:lt X1 X2} {G2:lt X2 X3} exists {G3:lt X1 X3} true. - : lt-transitive X1X2 X1+X2=X3 X1+X4=X5 X5>X3 <- plus-left-preserves-gt* X4>X2 X1+X4=X5 X1+X2=X3 X5>X3. %worlds () (plus-left-preserves-lt* X2}% X3X3 Y2>X2 <- plus-left-cancels-gt X1+Y2=X3 X1+X2=X3 eq/ Y3>X3 Y2>X2. %worlds () (plus-left-cancels-lt X1+X2=X3 Y1+Y2=Y3 X1=Y1 X3}% X2}% X3 X5 X1+X2=A3 X1+X4=X5 X3}% X4}% X4 X5 X1+X3=X4 X2+X3=X5 X4}% X3}% X3 Y3 X1+X2=X3 Y1+Y2=Y3 X3}% X1=X1 X1>=X2 R <- ge-anti-symmetric X1>=X2 X2>=X1 R. %worlds () (le-anti-symmetric _ _ _). %total {} (le-anti-symmetric _ _ _). %theorem le-transitive : forall* {X1} {X2} {X3} forall {G1:le X1 X2} {G2:le X2 X3} exists {G3:le X1 X3} true. - : le-transitive X1<=X2 X2<=X3 X1<=X3 <- ge-transitive X2<=X3 X1<=X2 X1<=X3. %worlds () (le-transitive X1<=X2 X2<=X3 X1<=X3). %total {} (le-transitive _ _ _). %abbrev le-reflexive = ge-reflexive. %theorem le-transitive-lt: forall* {X1} {X2} {X3} forall {L1:le X1 X2} {L2:lt X2 X3} exists {L3:lt X1 X3} true. - : le-transitive-lt X2>=X1 X3>X2 X3>X1 <- gt-transitive-ge X3>X2 X2>=X1 X3>X1. %worlds () (le-transitive-lt X1<=X2 X2}% X1X1 X3>=X2 X3>X1 <- ge-transitive-gt X3>=X2 X2>X1 X3>X1. %worlds () (lt-transitive-le X1}% X1=X2 X1+X2=X3 X1+X4=X5 X5>=X3 <- plus-left-preserves-ge* X4>=X2 X1+X4=X5 X1+X2=X3 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 : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {OP1:plus X1 X2 X3} {OP2:plus Y1 Y2 Y3} {E1:eq X1 Y1} {R3:le X3 Y3} exists {R2:le X2 Y2} true. - : plus-left-cancels-le X1+X2=X3 X1+Y2=X3 eq/ Y3>=X3 Y2>=X2 <- plus-left-cancels-ge X1+Y2=X3 X1+X2=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 : forall* {X1} {X2} {X4} forall {G:le X2 X4} exists {X3} {X5} {O1:plus X1 X2 X3} {O2:plus X1 X4 X5} {G2:le X3 X5} true. - : plus-left-preserves-le X2<=X4 X3 X5 X1+X2=A3 X1+X4=X5 X3<=X5 <- plus-total X1+X2=A3 <- plus-total X1+X4=X5 <- plus-left-preserves-le* X2<=X4 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* : forall* {X1} {X2} {X3} {X4} {X5} forall {G1:le X1 X2} {O1:plus X1 X3 X4} {O2:plus X2 X3 X5} exists {G2:le X4 X5} true. - : plus-right-preserves-le* X1<=X2 X1+X3=X4 X2+X3=X5 X4<=X5 <- plus-commutative X1+X3=X4 X3+X1=X4 <- plus-commutative X2+X3=X5 X3+X2=X5 <- plus-left-preserves-le* X1<=X2 X3+X1=X4 X3+X2=X5 X4<=X5. %worlds () (plus-right-preserves-le* X1<=X2 X1+X3=X4 X2+X3=X5 %{=>}% X4<=X5). %total {} (plus-right-preserves-le* _ _ _ _). %theorem plus-right-preserves-le : forall* {X1} {X2} {X3} forall {G1:le X1 X2} exists {X4} {X5} {O1:plus X1 X3 X4} {O2:plus X2 X3 X5} {G2:le X4 X5} true. - : plus-right-preserves-le X1<=X2 X4 X5 X1+X3=X4 X2+X3=X5 X4<=X5 <- plus-total X1+X3=X4 <- plus-total X2+X3=X5 <- plus-right-preserves-le* X1<=X2 X1+X3=X4 X2+X3=X5 X4<=X5. %worlds () (plus-right-preserves-le X1<=X2 %{=>}% X4 X5 X1+X3=X4 X2+X3=X5 X4<=X5). %total {} (plus-right-preserves-le _ _ _ _ _ _). %theorem plus-preserves-le* : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {G1:le X1 Y1} {G2:le X2 Y2} {MX:plus X1 X2 X3} {MY:plus Y1 Y2 Y3} exists {G3:le X3 Y3} true. - : plus-preserves-le* X1<=Y1 X2<=Y2 X1+X2=X3 Y1+Y2=Y3 X3<=Y3 <- plus-total Y1+X2=X <- plus-right-preserves-le* X1<=Y1 X1+X2=X3 Y1+X2=X X3<=X <- plus-left-preserves-le* X2<=Y2 Y1+X2=X Y1+Y2=Y3 X<=Y3 <- le-transitive X3<=X X<=Y3 X3<=Y3. %worlds () (plus-preserves-le* X1<=Y1 X2<=Y2 X1+X2=X3 Y1+Y2=Y3 %{=>}% X3<=Y3). %total {} (plus-preserves-le* _ _ _ _ _). %theorem plus-preserves-le : forall* {X1} {X2} {Y1} {Y2} forall {G1:le X1 Y1} {G2:le X2 Y2} exists {X3} {Y3} {MX:plus X1 X2 X3} {MY:plus Y1 Y2 Y3} {G3:le X3 Y3} true. - : plus-preserves-le X1<=Y1 X2<=Y2 X3 Y3 X1+X2=X3 Y1+Y2=Y3 X3<=Y3 <- plus-total X1+X2=X3 <- plus-total Y1+Y2=Y3 <- plus-preserves-le* X1<=Y1 X2<=Y2 X1+X2=X3 Y1+Y2=Y3 X3<=Y3. %worlds () (plus-preserves-le X1<=Y1 X2<=Y2 %{=>}% X3 Y3 X1+X2=X3 Y1+Y2=Y3 X3<=Y3). %total {} (plus-preserves-le _ _ _ _ _ _ _). %theorem plus-right-cancels-le : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {OP1:plus X1 X2 X3} {OP2:plus Y1 Y2 Y3} {E2:eq X2 Y2} {G3:le X3 Y3} exists {G1:le X1 Y1} true. - : plus-right-cancels-le X1+X2=X3 Y1+Y2=Y3 X2=Y2 X3<=Y3 X1<=Y1 <- plus-commutative X1+X2=X3 X2+X1=X3 <- plus-commutative Y1+Y2=Y3 Y2+Y1=Y3 <- plus-left-cancels-le X2+X1=X3 Y2+Y1=Y3 X2=Y2 X3<=Y3 X1<=Y1. %worlds () (plus-right-cancels-le X1+X2=X3 Y1+Y2=Y3 X2=Y2 X3<=Y3 %{=>}% X1<=Y1). %total {} (plus-right-cancels-le _ _ _ _ _). %theorem times-left-preserves-le* : forall* {X1} {X2} {X3} {X4} {X5} forall {R1:le X2 X4} {OP1:times X1 X2 X3} {OP2:times X1 X4 X5} exists {R2:le X3 X5} true. - : times-left-preserves-le* X4>=X2 X1*X2=X3 X1*X4=X5 X5>=X3 <- times-left-preserves-ge* X4>=X2 X1*X4=X5 X1*X2=X3 X5>=X3. %worlds () (times-left-preserves-le* X2<=X4 X1*X2=X3 X1*X4=X5 %{=>}% X3<=X5). %total {} (times-left-preserves-le* _ _ _ _). %theorem times-left-preserves-le : forall* {X1} {X2} {X4} forall {G:le X2 X4} exists {X3} {X5} {O1:times X1 X2 X3} {O2:times X1 X4 X5} {G2:le X3 X5} true. - : times-left-preserves-le X2<=X4 X3 X5 X1*X2=A3 X1*X4=X5 X3<=X5 <- times-total X1*X2=A3 <- times-total X1*X4=X5 <- times-left-preserves-le* X2<=X4 X1*X2=A3 X1*X4=X5 X3<=X5. %worlds () (times-left-preserves-le X2<=X4 %{=>}% X3 X5 X1*X2=A3 X1*X4=X5 X3<=X5). %total {} (times-left-preserves-le _ _ _ _ _ _). %theorem times-right-preserves-le* : forall* {X1} {X2} {X3} {X4} {X5} forall {G1:le X1 X2} {O1:times X1 X3 X4} {O2:times X2 X3 X5} exists {G2:le X4 X5} true. - : times-right-preserves-le* X1<=X2 X1*X3=X4 X2*X3=X5 X4<=X5 <- times-commutative X1*X3=X4 X3*X1=X4 <- times-commutative X2*X3=X5 X3*X2=X5 <- times-left-preserves-le* X1<=X2 X3*X1=X4 X3*X2=X5 X4<=X5. %worlds () (times-right-preserves-le* X1<=X2 X1*X3=X4 X2*X3=X5 %{=>}% X4<=X5). %total {} (times-right-preserves-le* _ _ _ _). %theorem times-right-preserves-le : forall* {X1} {X2} {X3} forall {G1:le X1 X2} exists {X4} {X5} {O1:times X1 X3 X4} {O2:times X2 X3 X5} {G2:le X4 X5} true. - : times-right-preserves-le X1<=X2 X4 X5 X1*X3=X4 X2*X3=X5 X4<=X5 <- times-total X1*X3=X4 <- times-total X2*X3=X5 <- times-right-preserves-le* X1<=X2 X1*X3=X4 X2*X3=X5 X4<=X5. %worlds () (times-right-preserves-le X1<=X2 %{=>}% X4 X5 X1*X3=X4 X2*X3=X5 X4<=X5). %total {} (times-right-preserves-le _ _ _ _ _ _). %theorem times-preserves-le* : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {G1:le X1 Y1} {G2:le X2 Y2} {MX:times X1 X2 X3} {MY:times Y1 Y2 Y3} exists {G3:le X3 Y3} true. - : times-preserves-le* X1<=Y1 X2<=Y2 X1*X2=X3 Y1*Y2=Y3 X3<=Y3 <- times-total Y1*X2=X <- times-right-preserves-le* X1<=Y1 X1*X2=X3 Y1*X2=X X3<=X <- times-left-preserves-le* X2<=Y2 Y1*X2=X Y1*Y2=Y3 X<=Y3 <- le-transitive X3<=X X<=Y3 X3<=Y3. %worlds () (times-preserves-le* X1<=Y1 X2<=Y2 X1*X2=X3 Y1*Y2=Y3 %{=>}% X3<=Y3). %total {} (times-preserves-le* _ _ _ _ _). %theorem times-preserves-le : forall* {X1} {X2} {Y1} {Y2} forall {G1:le X1 Y1} {G2:le X2 Y2} exists {X3} {Y3} {MX:times X1 X2 X3} {MY:times Y1 Y2 Y3} {G3:le X3 Y3} true. - : times-preserves-le X1<=Y1 X2<=Y2 X3 Y3 X1*X2=X3 Y1*Y2=Y3 X3<=Y3 <- times-total X1*X2=X3 <- times-total Y1*Y2=Y3 <- times-preserves-le* X1<=Y1 X2<=Y2 X1*X2=X3 Y1*Y2=Y3 X3<=Y3. %worlds () (times-preserves-le X1<=Y1 X2<=Y2 %{=>}% X3 Y3 X1*X2=X3 Y1*Y2=Y3 X3<=Y3). %total {} (times-preserves-le _ _ _ _ _ _ _). %%%%% nat-inv-comp.elf %%%%% Theorems about minus and composed relations %%%%% This file is part of the nat.elf signature %%%% Theorems %%% Theorems about minus %theorem minus-left-inverts-ge* : forall* {X1} {X2} {X3} {X4} {X5} forall {G:ge X2 X4} {IOP1:minus X1 X2 X3} {IOP2:minus X1 X4 X5} exists {GP:ge X5 X3} true. - : minus-left-inverts-ge* X2>=X4 X3+X2=X1 X5+X4=X1 X5>=X3 <- plus-total X3+X4=X7 <- plus-left-preserves-ge* X2>=X4 X3+X2=X1 X3+X4=X7 X1>=X7 <- plus-right-cancels-ge X5+X4=X1 X3+X4=X7 eq/ X1>=X7 X5>=X3. %worlds () (minus-left-inverts-ge* X2>=X4 X1-X2=X3 X1-X4=X5 %{=>}% X5>=X3). %total {} (minus-left-inverts-ge* _ _ _ _). %theorem minus-right-preserves-ge* : forall* {X1} {X2} {X3} {X4} {X5} forall {G:ge X1 X2} {IOP1:minus X1 X3 X4} {IOP2:minus X2 X3 X5} exists {GP:ge X4 X5} true. - : minus-right-preserves-ge* X1>=X2 X4+X3=X1 X5+X3=X2 X4>=X5 <- plus-right-cancels-ge X4+X3=X1 X5+X3=X2 eq/ X1>=X2 X4>=X5. %worlds () (minus-right-preserves-ge* X1>=X2 X1-X3=X4 X2-X3=X5 %{=>}% X4>=X5). %total {} (minus-right-preserves-ge* _ _ _ _). %theorem minus-left-cancels-inverts-ge : forall* {X1} {X2} {X3} {X4} {X5} {X6} forall {IOP1:minus X1 X2 X3} {IOP2:minus X4 X5 X6} {E:eq X1 X4} {G:ge X3 X6} exists {GP:ge X5 X2} true. - : minus-left-cancels-inverts-ge X3+X2=X1 X6+X5=X4 X1=X4 X3>=X6 X5>=X2 <- plus-total X6+X2=X7 <- plus-right-preserves-ge* X3>=X6 X3+X2=X1 X6+X2=X7 X1>=X7 <- eq-symmetric X1=X4 X4=X1 <- plus-respects-eq X6+X5=X4 eq/ eq/ X4=X1 X6+X5=X1 <- plus-left-cancels-ge X6+X5=X1 X6+X2=X7 eq/ X1>=X7 X5>=X2. %worlds () (minus-left-cancels-inverts-ge X1-X2=X3 X4-X5=X6 X1=X4 X3>=X6 %{=>}% X5>=X2). %total {} (minus-left-cancels-inverts-ge _ _ _ _ _). %theorem minus-right-cancels-ge : forall* {X1} {X2} {X3} {X4} {X5} {X6} forall {IOP1:minus X1 X2 X3} {IOP2:minus X4 X5 X6} {E2:eq X2 X5} {G3:ge X3 X6} exists {G1:ge X1 X4} true. - : minus-right-cancels-ge X3+X2=X1 X6+X5=X4 X2=X5 X3>=X6 X1>=X4 <- plus-respects-eq X3+X2=X1 eq/ X2=X5 eq/ X3+X5=X1 <- plus-right-preserves-ge* X3>=X6 X3+X5=X1 X6+X5=X4 X1>=X4. %worlds () (minus-right-cancels-ge X1-X2=X3 X4-X5=X6 X2=X5 X3>=X6 %{=>}% X1>=X4). %total {} (minus-right-cancels-ge _ _ _ _ _). %theorem minus-left-preserves-ne* : forall* {X1} {X2} {X3} {X4} {X5} forall {G:ne X2 X4} {IOP1:minus X1 X2 X3} {IOP2:minus X1 X4 X5} exists {GP:ne X3 X5} true. - : minus-left-preserves-ne* X2<>X4 X3+X2=X1 X5+X4=X1 X3<>X5 <- plus-total X3+X4=X7 <- plus-left-preserves-ne* X2<>X4 X3+X2=X1 X3+X4=X7 X1<>X7 <- plus-right-cancels-ne X5+X4=X1 X3+X4=X7 eq/ X1<>X7 X5<>X3 <- ne-symmetric X5<>X3 X3<>X5. %worlds () (minus-left-preserves-ne* X2<>X4 X1-X2=X3 X1-X4=X5 %{=>}% X3<>X5). %total {} (minus-left-preserves-ne* _ _ _ _). %theorem minus-right-preserves-ne* : forall* {X1} {X2} {X3} {X4} {X5} forall {G:ne X1 X2} {IOP1:minus X1 X3 X4} {IOP2:minus X2 X3 X5} exists {GP:ne X4 X5} true. - : minus-right-preserves-ne* X1<>X2 X4+X3=X1 X5+X3=X2 X4<>X5 <- plus-right-cancels-ne X4+X3=X1 X5+X3=X2 eq/ X1<>X2 X4<>X5. %worlds () (minus-right-preserves-ne* X1<>X2 X1-X3=X4 X2-X3=X5 %{=>}% X4<>X5). %total {} (minus-right-preserves-ne* _ _ _ _). %theorem minus-left-cancels-ne : forall* {X1} {X2} {X3} {X4} {X5} {X6} forall {IOP1:minus X1 X2 X3} {IOP2:minus X4 X5 X6} {E:eq X1 X4} {G:ne X3 X6} exists {GP:ne X2 X5} true. - : minus-left-cancels-ne X3+X2=X1 X6+X5=X4 X1=X4 X3<>X6 X2<>X5 <- plus-total X6+X2=X7 <- plus-right-preserves-ne* X3<>X6 X3+X2=X1 X6+X2=X7 X1<>X7 <- eq-symmetric X1=X4 X4=X1 <- plus-respects-eq X6+X5=X4 eq/ eq/ X4=X1 X6+X5=X1 <- plus-left-cancels-ne X6+X5=X1 X6+X2=X7 eq/ X1<>X7 X5<>X2 <- ne-symmetric X5<>X2 X2<>X5. %worlds () (minus-left-cancels-ne X1-X2=X3 X4-X5=X6 X1=X4 X3<>X6 %{=>}% X2<>X5). %total {} (minus-left-cancels-ne _ _ _ _ _). %theorem minus-right-cancels-ne : forall* {X1} {X2} {X3} {X4} {X5} {X6} forall {IOP1:minus X1 X2 X3} {IOP2:minus X4 X5 X6} {E2:eq X2 X5} {G3:ne X3 X6} exists {G1:ne X1 X4} true. - : minus-right-cancels-ne X3+X2=X1 X6+X5=X4 X2=X5 X3<>X6 X1<>X4 <- plus-respects-eq X3+X2=X1 eq/ X2=X5 eq/ X3+X5=X1 <- plus-right-preserves-ne* X3<>X6 X3+X5=X1 X6+X5=X4 X1<>X4. %worlds () (minus-right-cancels-ne X1-X2=X3 X4-X5=X6 X2=X5 X3<>X6 %{=>}% X1<>X4). %total {} (minus-right-cancels-ne _ _ _ _ _). %%%%% nat-inv-less.elf %%%%% Theorems about minus and inverted relations %%%%% This file is part of the nat.elf signature %%%% Theorems %%% Theorems about minus %theorem minus-left-inverts-lt* : forall* {X1} {X2} {X3} {X4} {X5} forall {G:lt X2 X4} {IOP1:minus X1 X2 X3} {IOP2:minus X1 X4 X5} exists {GP:lt X5 X3} true. - : minus-left-inverts-lt* X2}% X5}% X4}% X5}% X1}% X5<=X3). %total {} (minus-left-inverts-le* _ _ _ _). %theorem minus-right-preserves-le* : forall* {X1} {X2} {X3} {X4} {X5} forall {G:le X1 X2} {IOP1:minus X1 X3 X4} {IOP2:minus X2 X3 X5} exists {GP:le X4 X5} true. - : minus-right-preserves-le* X1<=X2 X4+X3=X1 X5+X3=X2 X4<=X5 <- plus-right-cancels-le X4+X3=X1 X5+X3=X2 eq/ X1<=X2 X4<=X5. %worlds () (minus-right-preserves-le* X1<=X2 X1-X3=X4 X2-X3=X5 %{=>}% X4<=X5). %total {} (minus-right-preserves-le* _ _ _ _). %theorem minus-left-cancels-inverts-le : forall* {X1} {X2} {X3} {X4} {X5} {X6} forall {IOP1:minus X1 X2 X3} {IOP2:minus X4 X5 X6} {E:eq X1 X4} {G:le X3 X6} exists {GP:le X5 X2} true. - : minus-left-cancels-inverts-le X3+X2=X1 X6+X5=X4 X1=X4 X3<=X6 X5<=X2 <- plus-total X6+X2=X7 <- plus-right-preserves-le* X3<=X6 X3+X2=X1 X6+X2=X7 X1<=X7 <- eq-symmetric X1=X4 X4=X1 <- plus-respects-eq X6+X5=X4 eq/ eq/ X4=X1 X6+X5=X1 <- plus-left-cancels-le X6+X5=X1 X6+X2=X7 eq/ X1<=X7 X5<=X2. %worlds () (minus-left-cancels-inverts-le X1-X2=X3 X4-X5=X6 X1=X4 X3<=X6 %{=>}% X5<=X2). %total {} (minus-left-cancels-inverts-le _ _ _ _ _). %theorem minus-right-cancels-le : forall* {X1} {X2} {X3} {X4} {X5} {X6} forall {IOP1:minus X1 X2 X3} {IOP2:minus X4 X5 X6} {E2:eq X2 X5} {G3:le X3 X6} exists {G1:le X1 X4} true. - : minus-right-cancels-le X3+X2=X1 X6+X5=X4 X2=X5 X3<=X6 X1<=X4 <- plus-respects-eq X3+X2=X1 eq/ X2=X5 eq/ X3+X5=X1 <- plus-right-preserves-le* X3<=X6 X3+X5=X1 X6+X5=X4 X1<=X4. %worlds () (minus-right-cancels-le X1-X2=X3 X4-X5=X6 X2=X5 X3<=X6 %{=>}% X1<=X4). %total {} (minus-right-cancels-le _ _ _ _ _). %%%%% nat-divrem.elf %%%%% Integer quotient/remainder division %%%%% This file is part of the nat.elf signature %%%% Definitions %%% Division with remainder divrem : nat -> nat -> nat -> nat -> type. divrem/z : divrem M N z M <- gt N M. divrem/s : divrem M (s N-) (s Q) R <- plus D (s N-) M <- divrem D (s N-) Q R. %%%% Theorems %%% Theorems about divrem %theorem false-implies-divrem : forall* {M} {N} {Q} {R} forall {F:void} exists {D:divrem M N Q R} true. %worlds () (false-implies-divrem _ %{=>}% M/N=Q,R). %total {} (false-implies-divrem _ _). %theorem divrem-respects-eq : forall* {M} {N} {Q} {R} {M'} {N'} {Q'} {R'} forall {D:divrem M N Q R} {E1:eq M M'} {E2:eq N N'} {E3:eq Q Q'} {E4:eq R R'} exists {D':divrem M' N' Q' R'} true. - : divrem-respects-eq D eq/ eq/ eq/ eq/ D. %worlds () (divrem-respects-eq M/N=Q,R M=M' N=N' Q=Q' R=R' %{=>}% M'/N'=Q',R'). %total {} (divrem-respects-eq _ _ _ _ _ _). %theorem divrem-total** : forall {M} {N-1} {C} {CMP:compare M N-1 C} exists {Q} {R} {D:divrem M (s N-1) Q R} true. - : divrem-total** M N-1 equal CMP z M (divrem/z N>M) <- equal-implies-eq CMP M=N-1 <- succ-implies-gt eq/ N>N-1 <- eq-symmetric M=N-1 N-1=M <- gt-respects-eq N>N-1 eq/ N-1=M N>M. - : divrem-total** M N-1 less CMP z M (divrem/z N>M) <- less-implies-lt CMP N-1>M <- succ-implies-gt eq/ N>N-1 <- gt-transitive N>N-1 N-1>M N>M. - : divrem-total** M N-1 greater CMP (s Q) R (divrem/s D/N=Q,R D+N=M) <- greater-implies-gt CMP M>N-1 <- gt-implies-plus M>N-1 D SD+N-1=M <- plus-swap-succ SD+N-1=M D+N=M <- plus-commutative D+N=M N+D=M <- plus-implies-gt N+D=M eq/ M>D <- meta-gt M D M>D <- compare-total* D N-1 C' CMP' <- divrem-total** D N-1 C' CMP' Q R D/N=Q,R. %worlds () (divrem-total** M N-1 C MCN %{=>}% Q R M/N=Q,R). %total (M) (divrem-total** M _ _ _ _ _ _). %theorem divrem-total* : forall {M} {N-} exists {Q} {R} {D:divrem M (s N-) Q R} true. - : divrem-total* M N-1 Q R M/N=Q,R <- compare-total* M N-1 C CMP <- divrem-total** M N-1 C CMP Q R M/N=Q,R. %worlds () (divrem-total* M N-1 %{=>}% Q R M/N=Q,R). %total {} (divrem-total* _ _ _ _ _). %abbrev divrem-total = divrem-total* _ _ _ _. %theorem divrem-deterministic : forall* {M} {N} {Q} {R} {M'} {N'} {Q'} {R'} forall {D:divrem M N Q R} {D':divrem M' N' Q' R'} {E1:eq M M'} {E2:eq N N'} exists {E3:eq Q Q'} {E4:eq R R'} true. - : divrem-deterministic (divrem/z _) (divrem/z _) eq/ eq/ eq/ eq/. - : divrem-deterministic (divrem/s D/N=Q,R D+N=M) (divrem/s D'/N=Q',R' D'+N=M) eq/ eq/ SQ=SQ' R=R' <- plus-right-cancels D+N=M D'+N=M eq/ eq/ D=D' <- divrem-deterministic D/N=Q,R D'/N=Q',R' D=D' eq/ Q=Q' R=R' <- succ-deterministic Q=Q' SQ=SQ'. %% contradiction cases: - : divrem-deterministic (divrem/z N>M) (divrem/s _ D+N=M) eq/ eq/ Q=Q' R=R' <- plus-commutative D+N=M N+D=M <- plus-gt-contradiction N+D=M N>M F <- false-implies-eq F Q=Q' <- false-implies-eq F R=R'. - : divrem-deterministic (divrem/s _ D+N=M) (divrem/z N>M) eq/ eq/ Q=Q' R=R' <- plus-commutative D+N=M N+D=M <- plus-gt-contradiction N+D=M N>M F <- false-implies-eq F Q=Q' <- false-implies-eq F R=R'. %worlds () (divrem-deterministic M/N=Q,R M'/N'=Q'/R' M=M' N=N' %{=>}% Q=Q' R=R'). %total (D) (divrem-deterministic D _ _ _ _ _). %theorem divrem-implies-positive : forall* {M} {N} {Q} {R} forall {D:divrem M N Q R} exists {N-1} {E:eq N (s N-1)} true. - : divrem-implies-positive (divrem/z N>M) N-1 N=sN-1 <- gt-implies-positive N>M N-1 N=sN-1. - : divrem-implies-positive (divrem/s _ _) _ eq/. %worlds () (divrem-implies-positive M/N=Q,R %{=>}% N-1 N=sN-1). %total {} (divrem-implies-positive _ _ _). %theorem divrem-implies-gt : forall* {M} {N} {Q} {R} forall {D:divrem M N Q R} exists {G:gt N R} true. - : divrem-implies-gt (divrem/z N>M) N>M. - : divrem-implies-gt (divrem/s D/N=Q,R _) N>R <- divrem-implies-gt D/N=Q,R N>R. %worlds () (divrem-implies-gt M/N=Q,R %{=>}% N>R). %total D (divrem-implies-gt D _). %theorem divrem-contradiction : forall* {M} {N} {Q} {R} {X} forall {D:divrem M N Q R} {P:plus N X R} exists {F:void} true. - : divrem-contradiction D P F <- divrem-implies-gt D N>R <- plus-commutative P Pc <- plus-implies-ge Pc R>=N <- gt-transitive-ge N>R R>=N N>N <- gt-anti-reflexive N>N F. %worlds () (divrem-contradiction _ _ _). %total { } (divrem-contradiction _ _ _). %theorem divrem-can-be-inverted : forall* {M} {N} {Q} {R} forall {D:divrem M N Q R} exists {X} {T:times Q N X} {P:plus X R M} true. - : divrem-can-be-inverted (divrem/z _) z times/z plus/z. - : divrem-can-be-inverted (divrem/s D/N=Q,R D+N=M) X (times/s Q*N=Y Y+N=X) X+R=M <- divrem-can-be-inverted D/N=Q,R Y Q*N=Y Y+R=D <- plus-commutative Y+R=D R+Y=D <- plus-associative R+Y=D D+N=M X Y+N=X R+X=M <- plus-commutative R+X=M X+R=M. %worlds () (divrem-can-be-inverted M/N=Q,R %{=>}% X Q*N=X X+R=M). %total (D) (divrem-can-be-inverted D _ _ _). %theorem div-can-be-inverted : forall* {M} {N} {Q} forall {D:divrem M N Q z} exists {T:times Q N M} true. - : div-can-be-inverted (divrem/z _) times/z. - : div-can-be-inverted (divrem/s D/N=Q,z D+N=M) (times/s Q*N=D D+N=M) <- div-can-be-inverted D/N=Q,z Q*N=D. %worlds () (div-can-be-inverted _ _). %total (D) (div-can-be-inverted D _). %theorem divrem-can-be-constructed : forall* {M} {N} {Q} {R} {X} forall {T:times Q N X} {P:plus X R M} {G:gt N R} exists {D:divrem M N Q R} true. - : divrem-can-be-constructed (times/z) (plus/z) N>R (divrem/z N>R). - : divrem-can-be-constructed (times/s Q*N=Y Y+N=X) X+R=M N>R (divrem/s Z/N=Q,R Z+N=M) <- plus-commutative Y+N=X N+Y=X <- plus-associative N+Y=X X+R=M Z Y+R=Z N+Z=M <- plus-commutative N+Z=M Z+N=M <- divrem-can-be-constructed Q*N=Y Y+R=Z N>R Z/N=Q,R. - : divrem-can-be-constructed _ _ ZERO>R D <- gt-contradiction ZERO>R F <- false-implies-divrem F D. %worlds () (divrem-can-be-constructed Q*N=X X+R=M N>R %{=>}% M/N=Q,R). %total (T) (divrem-can-be-constructed T _ _ _). %theorem div-can-be-constructed : forall* {M} {N} {Q} forall {T:times Q (s N) M} exists {D:divrem M (s N) Q z} true. - : div-can-be-constructed (times/z) (divrem/z N+1>0) <- succ-implies-gt-zero _ N+1>0. - : div-can-be-constructed (times/s Q*sN=D D+sN=M) (divrem/s D/sN=Q,z D+sN=M) <- div-can-be-constructed Q*sN=D D/sN=Q,z. %worlds () (div-can-be-constructed _ _). %total (T) (div-can-be-constructed T _). %theorem remainder-implies-gt-quotient : forall* {M} {N} {Q} {R} forall {D:divrem M N Q (s R)} exists {G:gt M Q} true. - : remainder-implies-gt-quotient (divrem/z _) R+1>0 <- succ-implies-gt-zero _ R+1>0. - : remainder-implies-gt-quotient (divrem/s D/N=Q,sR D+N=M) M>sQ <- remainder-implies-gt-quotient D/N=Q,sR D>Q <- gt-implies-ge-succ D>Q D>=sQ <- plus-commutative D+N=M N+D=M <- plus-implies-gt N+D=M eq/ M>D <- gt-transitive-ge M>D D>=sQ M>sQ. %worlds () (remainder-implies-gt-quotient _ _). %total (D) (remainder-implies-gt-quotient D _). %theorem quotient-of-nonzero-is-smaller : forall* {M} {N} {Q} {R} {M-} forall {DR:divrem M (s (s N)) Q R} {EN:eq M (s M-)} exists {G:gt M Q} true. - : quotient-of-nonzero-is-smaller _ eq/ M>0 <- succ-implies-gt-zero _ M>0. - : quotient-of-nonzero-is-smaller M/N=Q,R eq/ M>Q <- divrem-can-be-inverted M/N=Q,R X Q*N=X X+R=M <- times-right-identity _ Q*1=Q <- succ-implies-gt-zero _ N->0 <- succ-preserves-gt N->0 N>1 <- times-left-preserves-gt N>1 Q*N=X Q*1=Q X>Q <- plus-commutative X+R=M R+X=M <- plus-implies-ge R+X=M M>=X <- ge-transitive-gt M>=X X>Q M>Q. %worlds () (quotient-of-nonzero-is-smaller _ _ _). %total { } (quotient-of-nonzero-is-smaller _ _ _). %theorem quotient-is-no-greater : forall* {M} {N} {Q} {R} forall {DR:divrem M N Q R} exists {ge:ge M Q} true. - : quotient-is-no-greater M/N=Q,R M>=Q <- divrem-can-be-inverted M/N=Q,R X Q*N=X X+R=M <- divrem-implies-positive M/N=Q,R NN N=NN+1 <- eq-symmetric N=NN+1 NN+1=N <- succ-implies-gt-zero NN NN+1>0 <- gt-respects-eq NN+1>0 NN+1=N eq/ N>0 <- gt-implies-ge-succ N>0 N>=1 <- times-right-identity _ Q*1=Q <- times-left-preserves-ge* N>=1 Q*N=X Q*1=Q X>=Q <- plus-commutative X+R=M R+X=M <- plus-implies-ge R+X=M M>=X <- ge-transitive M>=X X>=Q M>=Q. %worlds () (quotient-is-no-greater _ _). %total { } (quotient-is-no-greater _ _). %%%%% minmax.elf %%%%% Minimum and Maximum functor %%%%% John Boyland %{% Minimum and maximum defined given anti-reflexive gt total order. We assume compare three-way comparison. We assume that ge is defined from gt and eq. %}% %%%% Definitions min : nat -> nat -> nat -> type. min/= : min X X X. min/> : gt X1 X2 -> min X1 X2 X2. min/< : gt X2 X1 -> min X1 X2 X1. max : nat -> nat -> nat -> type. max/= : max X X X. max/> : gt X1 X2 -> max X1 X2 X1. max/< : gt X2 X1 -> max X1 X2 X2. %%%% Theorems %%% Theorems about min %theorem false-implies-min : forall* {X1} {X2} {X3} forall {F:void} exists {M:min X1 X2 X3} true. %worlds () (false-implies-min _ _). %total { } (false-implies-min _ _). %theorem min-respects-eq : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {MX:min X1 X2 X3} {E1:eq X1 Y1} {E2:eq X2 Y2} {E3:eq X3 Y3} exists {MY:min Y1 Y2 Y3} true. - : min-respects-eq M eq/ eq/ eq/ M. %worlds () (min-respects-eq _ _ _ _ _). %total { } (min-respects-eq _ _ _ _ _). %theorem min-total** : forall* {X1} {X2} {C} forall {D:compare X1 X2 C} exists {X3} {M:min X1 X2 X3} true. - : min-total** compare/= _ min/=. - : min-total** (compare/> X1>X2) _ (min/> X1>X2). - : min-total** (compare/< X2>X1) _ (min/< X2>X1). %worlds () (min-total** _ _ _). %total { } (min-total** _ _ _). %theorem min-total* : forall {X1} {X2} exists {X3} {M:min X1 X2 X3} true. - : min-total* X1 X2 X3 M <- compare-total D <- min-total** D X3 M. %worlds () (min-total* _ _ _ _). %total { } (min-total* _ _ _ _). %abbrev min-total = min-total* _ _ _. %theorem min-deterministic : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {MX:min X1 X2 X3} {MY:min Y1 Y2 Y3} {E1:eq X1 Y1} {E2:eq X2 Y2} exists {E3:eq X3 Y3} true. - : min-deterministic (min/=) (min/=) eq/ eq/ eq/. - : min-deterministic (min/=) (min/> X>X) eq/ eq/ eq/. - : min-deterministic (min/=) (min/< X>X) eq/ eq/ eq/. - : min-deterministic (min/> X>X) (min/=) eq/ eq/ eq/. - : min-deterministic (min/> X>Y) (min/> X>YP) eq/ eq/ eq/. - : min-deterministic (min/> X>Y) (min/< Y>X) eq/ eq/ E <- gt-anti-symmetric X>Y Y>X F <- false-implies-eq F E. - : min-deterministic (min/< X>X) (min/=) eq/ eq/ eq/. - : min-deterministic (min/< X>Y) (min/> Y>X) eq/ eq/ E <- gt-anti-symmetric X>Y Y>X F <- false-implies-eq F E. - : min-deterministic (min/< X>Y) (min/< X>YP) eq/ eq/ eq/. %worlds () (min-deterministic _ _ _ _ _). %total { } (min-deterministic _ _ _ _ _). %theorem min-commutative : forall* {X1} {X2} {X3} forall {M:min X1 X2 X3} exists {Mc:min X2 X1 X3} true. - : min-commutative min/= min/=. - : min-commutative (min/> X>Y) (min/< X>Y). - : min-commutative (min/< X>Y) (min/> X>Y). %worlds () (min-commutative _ _). %total { } (min-commutative _ _). %theorem ge-implies-min : forall* {X1} {X2} forall {G:ge X1 X2} exists {M:min X1 X2 X2} true. - : ge-implies-min (ge/> X1>X2) (min/> X1>X2). - : ge-implies-min (ge/= eq/) (min/=). %worlds () (ge-implies-min _ _). %total { } (ge-implies-min _ _). %theorem le-implies-min : forall* {X1} {X2} forall {G:le X1 X2} exists {M:min X1 X2 X1} true. - : le-implies-min X2>=X1 M <- ge-implies-min X2>=X1 Mc <- min-commutative Mc M. %worlds () (le-implies-min _ _). %total { } (le-implies-min _ _). %theorem min-implies-ge : forall* {X1} {X2} {X3} forall {M:min X1 X2 X3} exists {G1:ge X1 X3} {G2:ge X2 X3} true. - : min-implies-ge min/= (ge/= eq/) (ge/= eq/). - : min-implies-ge (min/> X1>X2) (ge/> X1>X2) (ge/= eq/). - : min-implies-ge (min/< X2>X1) (ge/= eq/) (ge/> X2>X1). %worlds () (min-implies-ge _ _ _). %total { } (min-implies-ge _ _ _). %theorem min-left-preserves-ge* : forall* {X1} {X2} {X3} {X4} {X5} forall {G:ge X2 X4} {M12:min X1 X2 X3} {M14:min X1 X4 X5} exists {G:ge X3 X5} true. - : min-left-preserves-ge* _ min/= M G <- min-implies-ge M G _. - : min-left-preserves-ge* X2>=X4 (min/> X1>X2) X1&X4=X5 X2>=X5 <- min-implies-ge X1&X4=X5 _ X4>=X5 <- ge-transitive X2>=X4 X4>=X5 X2>=X5. - : min-left-preserves-ge* _ (min/< _) X1&X4=X5 X1>=X5 <- min-implies-ge X1&X4=X5 X1>=X5 _. %worlds () (min-left-preserves-ge* _ _ _ _). %total { } (min-left-preserves-ge* _ _ _ _). %theorem min-left-preserves-le* : forall* {X1} {X2} {X3} {X4} {X5} forall {G:le X2 X4} {M12:min X1 X2 X3} {M14:min X1 X4 X5} exists {G:le X3 X5} true. - : min-left-preserves-le* G1 M12 M14 G2 <- min-left-preserves-ge* G1 M14 M12 G2. %worlds () (min-left-preserves-le* _ _ _ _). %total { } (min-left-preserves-le* _ _ _ _). %theorem min-left-preserves-ge : forall* {X1} {X2} {X4} forall {G:ge X2 X4} exists {X3} {X5} {O1:min X1 X2 X3} {O2:min X1 X4 X5} {G2:ge X3 X5} true. - : min-left-preserves-ge X2>=X4 X3 X5 X1&X2=A3 X1&X4=X5 X3>=X5 <- min-total X1&X2=A3 <- min-total X1&X4=X5 <- min-left-preserves-ge* X2>=X4 X1&X2=A3 X1&X4=X5 X3>=X5. %worlds () (min-left-preserves-ge X2>=X4 %{=>}% X3 X5 X1&X2=A3 X1&X4=X5 X3>=X5). %total {} (min-left-preserves-ge _ _ _ _ _ _). %theorem min-right-preserves-ge* : forall* {X1} {X2} {X3} {X4} {X5} forall {G1:ge X1 X2} {O1:min X1 X3 X4} {O2:min X2 X3 X5} exists {G2:ge X4 X5} true. - : min-right-preserves-ge* X1>=X2 X1&X3=X4 X2&X3=X5 X4>=X5 <- min-commutative X1&X3=X4 X3&X1=X4 <- min-commutative X2&X3=X5 X3&X2=X5 <- min-left-preserves-ge* X1>=X2 X3&X1=X4 X3&X2=X5 X4>=X5. %worlds () (min-right-preserves-ge* X1>=X2 X1&X3=X4 X2&X3=X5 %{=>}% X4>=X5). %total {} (min-right-preserves-ge* _ _ _ _). %theorem min-right-preserves-ge : forall* {X1} {X2} {X3} forall {G1:ge X1 X2} exists {X4} {X5} {O1:min X1 X3 X4} {O2:min X2 X3 X5} {G2:ge X4 X5} true. - : min-right-preserves-ge X1>=X2 X4 X5 X1&X3=X4 X2&X3=X5 X4>=X5 <- min-total X1&X3=X4 <- min-total X2&X3=X5 <- min-right-preserves-ge* X1>=X2 X1&X3=X4 X2&X3=X5 X4>=X5. %worlds () (min-right-preserves-ge X1>=X2 %{=>}% X4 X5 X1&X3=X4 X2&X3=X5 X4>=X5). %total {} (min-right-preserves-ge _ _ _ _ _ _). %theorem min-preserves-ge* : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {G1:ge X1 Y1} {G2:ge X2 Y2} {MX:min X1 X2 X3} {MY:min Y1 Y2 Y3} exists {G3:ge X3 Y3} true. - : min-preserves-ge* X1>=Y1 X2>=Y2 X1&X2=X3 Y1&Y2=Y3 X3>=Y3 <- min-total Y1&X2=X <- min-right-preserves-ge* X1>=Y1 X1&X2=X3 Y1&X2=X X3>=X <- min-left-preserves-ge* X2>=Y2 Y1&X2=X Y1&Y2=Y3 X>=Y3 <- ge-transitive X3>=X X>=Y3 X3>=Y3. %worlds () (min-preserves-ge* X1>=Y1 X2>=Y2 X1&X2=X3 Y1&Y2=Y3 %{=>}% X3>=Y3). %total {} (min-preserves-ge* _ _ _ _ _). %theorem min-preserves-ge : forall* {X1} {X2} {Y1} {Y2} forall {G1:ge X1 Y1} {G2:ge X2 Y2} exists {X3} {Y3} {MX:min X1 X2 X3} {MY:min Y1 Y2 Y3} {G3:ge X3 Y3} true. - : min-preserves-ge X1>=Y1 X2>=Y2 X3 Y3 X1&X2=X3 Y1&Y2=Y3 X3>=Y3 <- min-total X1&X2=X3 <- min-total Y1&Y2=Y3 <- min-preserves-ge* X1>=Y1 X2>=Y2 X1&X2=X3 Y1&Y2=Y3 X3>=Y3. %worlds () (min-preserves-ge X1>=Y1 X2>=Y2 %{=>}% X3 Y3 X1&X2=X3 Y1&Y2=Y3 X3>=Y3). %total {} (min-preserves-ge _ _ _ _ _ _ _). %theorem min-left-preserves-le : forall* {X1} {X2} {X4} forall {G:le X2 X4} exists {X3} {X5} {O1:min X1 X2 X3} {O2:min X1 X4 X5} {G2:le X3 X5} true. - : min-left-preserves-le X2<=X4 X3 X5 X1&X2=A3 X1&X4=X5 X3<=X5 <- min-total X1&X2=A3 <- min-total X1&X4=X5 <- min-left-preserves-le* X2<=X4 X1&X2=A3 X1&X4=X5 X3<=X5. %worlds () (min-left-preserves-le X2<=X4 %{=>}% X3 X5 X1&X2=A3 X1&X4=X5 X3<=X5). %total {} (min-left-preserves-le _ _ _ _ _ _). %theorem min-right-preserves-le* : forall* {X1} {X2} {X3} {X4} {X5} forall {G1:le X1 X2} {O1:min X1 X3 X4} {O2:min X2 X3 X5} exists {G2:le X4 X5} true. - : min-right-preserves-le* X1<=X2 X1&X3=X4 X2&X3=X5 X4<=X5 <- min-commutative X1&X3=X4 X3&X1=X4 <- min-commutative X2&X3=X5 X3&X2=X5 <- min-left-preserves-le* X1<=X2 X3&X1=X4 X3&X2=X5 X4<=X5. %worlds () (min-right-preserves-le* X1<=X2 X1&X3=X4 X2&X3=X5 %{=>}% X4<=X5). %total {} (min-right-preserves-le* _ _ _ _). %theorem min-right-preserves-le : forall* {X1} {X2} {X3} forall {G1:le X1 X2} exists {X4} {X5} {O1:min X1 X3 X4} {O2:min X2 X3 X5} {G2:le X4 X5} true. - : min-right-preserves-le X1<=X2 X4 X5 X1&X3=X4 X2&X3=X5 X4<=X5 <- min-total X1&X3=X4 <- min-total X2&X3=X5 <- min-right-preserves-le* X1<=X2 X1&X3=X4 X2&X3=X5 X4<=X5. %worlds () (min-right-preserves-le X1<=X2 %{=>}% X4 X5 X1&X3=X4 X2&X3=X5 X4<=X5). %total {} (min-right-preserves-le _ _ _ _ _ _). %theorem min-preserves-le* : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {G1:le X1 Y1} {G2:le X2 Y2} {MX:min X1 X2 X3} {MY:min Y1 Y2 Y3} exists {G3:le X3 Y3} true. - : min-preserves-le* X1<=Y1 X2<=Y2 X1&X2=X3 Y1&Y2=Y3 X3<=Y3 <- min-total Y1&X2=X <- min-right-preserves-le* X1<=Y1 X1&X2=X3 Y1&X2=X X3<=X <- min-left-preserves-le* X2<=Y2 Y1&X2=X Y1&Y2=Y3 X<=Y3 <- le-transitive X3<=X X<=Y3 X3<=Y3. %worlds () (min-preserves-le* X1<=Y1 X2<=Y2 X1&X2=X3 Y1&Y2=Y3 %{=>}% X3<=Y3). %total {} (min-preserves-le* _ _ _ _ _). %theorem min-preserves-le : forall* {X1} {X2} {Y1} {Y2} forall {G1:le X1 Y1} {G2:le X2 Y2} exists {X3} {Y3} {MX:min X1 X2 X3} {MY:min Y1 Y2 Y3} {G3:le X3 Y3} true. - : min-preserves-le X1<=Y1 X2<=Y2 X3 Y3 X1&X2=X3 Y1&Y2=Y3 X3<=Y3 <- min-total X1&X2=X3 <- min-total Y1&Y2=Y3 <- min-preserves-le* X1<=Y1 X2<=Y2 X1&X2=X3 Y1&Y2=Y3 X3<=Y3. %worlds () (min-preserves-le X1<=Y1 X2<=Y2 %{=>}% X3 Y3 X1&X2=X3 Y1&Y2=Y3 X3<=Y3). %total {} (min-preserves-le _ _ _ _ _ _ _). %theorem min-is-glb : forall* {X1} {X2} {X3} {X4} forall {M:min X1 X2 X3} {G1:ge X1 X4} {G2:ge X2 X4} exists {G3:ge X3 X4} true. - : min-is-glb min/= G _ G. - : min-is-glb (min/> X1>X2) _ G G. - : min-is-glb (min/< X2>X1) G _ G. %worlds () (min-is-glb _ _ _ _). %total { } (min-is-glb _ _ _ _). %theorem min-associative : forall* {X1} {X2} {X3} {X4} {X7} forall {M12:min X1 X2 X3} {M34:min X3 X4 X7} exists {X6} {M24:min X2 X4 X6} {M16:min X1 X6 X7} true. - : min-associative min/= min/= _ min/= min/=. - : min-associative min/= (min/> X3>X4) _ (min/> X3>X4) (min/> X3>X4). - : min-associative min/= (min/< X4>X3) _ (min/< X4>X3) (min/=). - : min-associative (min/> X1>X2) min/= _ (min/=) (min/> X1>X2). - : min-associative (min/> X1>X2) (min/> X2>X4) _ (min/> X2>X4) (min/> X1>X4) <- gt-transitive X1>X2 X2>X4 X1>X4. - : min-associative (min/> X1>X2) (min/< X4>X2) _ (min/< X4>X2) (min/> X1>X2). - : min-associative (min/< X2>X1) min/= _ (min/> X2>X1) min/=. - : min-associative (min/< X2>X1) (min/> X1>X4) _ (min/> X2>X4) (min/> X1>X4) <- gt-transitive X2>X1 X1>X4 X2>X4. - : min-associative (min/< X2>X1) (min/< X4>X1) _ M24 M16 <- min-total M24 <- min-is-glb M24 (ge/> X2>X1) (ge/> X4>X1) (X6>=X1: ge X6 X1) <- ge-implies-min X6>=X1 M16c <- min-commutative M16c M16. %worlds () (min-associative _ _ _ _ _). %total { } (min-associative _ _ _ _ _). %theorem min-associative* : forall* {X1} {X2} {X12} {X3} {X23} {X123} forall {OP12:min X1 X2 X12} {OP12-3:min X12 X3 X123} {OP23:min X2 X3 X23} exists {OP1-23:min X1 X23 X123} true. - : min-associative* X1&X2=X3 X3&X4=X7 X2&X4=X6 X1&X6=X7 <- min-associative X1&X2=X3 X3&X4=X7 Y6 X2&X4=Y6 X1&Y6=X7 <- min-deterministic X2&X4=Y6 X2&X4=X6 eq/ eq/ Y6=X6 <- min-respects-eq X1&Y6=X7 eq/ Y6=X6 eq/ X1&X6=X7. %worlds () (min-associative* _ _ _ _). %total {} (min-associative* _ _ _ _). %theorem min-associative-converse : forall* {X1} {X2} {X4} {X6} {X7} forall {OP24:min X2 X4 X6} {OP16:min X1 X6 X7} exists {X3} {OP12:min X1 X2 X3} {OP34:min X3 X4 X7} true. - : min-associative-converse X2&X4=X6 X1&X6=X7 _ X1&X2=X3 X3&X4=X7 <- min-commutative X2&X4=X6 X4&X2=X6 <- min-commutative X1&X6=X7 X6&X1=X7 <- min-associative X4&X2=X6 X6&X1=X7 _ X2&X1=X3 X4&X3=X7 <- min-commutative X2&X1=X3 X1&X2=X3 <- min-commutative X4&X3=X7 X3&X4=X7. %worlds () (min-associative-converse X2&X4=X6 X1&X6=X7 X3 X1&X2=X3 X3&X4=X7). %total {} (min-associative-converse _ _ _ _ _). %theorem min-associative-converse* : forall* {X1} {X2} {X3} {X4} {X6} {X7} forall {OP24:min X2 X4 X6} {OP16:min X1 X6 X7} {OP12:min X1 X2 X3} exists {OP34:min X3 X4 X7} true. - : min-associative-converse* X2&X4=X6 X1&X6=X7 X1&X2=X3 X3&X4=X7 <- min-associative-converse X2&X4=X6 X1&X6=X7 X3P X1&X2=X3P X3P&X4=X7 <- min-deterministic X1&X2=X3P X1&X2=X3 eq/ eq/ X3P=X3 <- min-respects-eq X3P&X4=X7 X3P=X3 eq/ eq/ X3&X4=X7. %worlds () (min-associative-converse* X2&X4=X6 X1&X6=X7 X1&X2=X3 %{=>}% X3&X4=X7). %total {} (min-associative-converse* _ _ _ _). %theorem min-assoc-commutative* : forall* {X1} {X2} {X3} {X4} {X5} {X7} forall {OP1:min X1 X2 X3} {OP2:min X3 X4 X7} {OP3:min X1 X4 X5} exists {OP4:min X5 X2 X7} true. - : min-assoc-commutative* X1&X2=X3 X3&X4=X7 X1&X4=X5 X5&X2=X7 <- min-associative X1&X2=X3 X3&X4=X7 X6 X2&X4=X6 X1&X6=X7 <- min-commutative X2&X4=X6 X4&X2=X6 <- min-associative-converse* X4&X2=X6 X1&X6=X7 X1&X4=X5 X5&X2=X7. %worlds () (min-assoc-commutative* X1&X2=X3 X3&X4=X7 X1&X4=X5 %{=>}% X5&X2=X7). %total {} (min-assoc-commutative* _ _ _ _). %theorem min-assoc-commutative : forall* {X1} {X2} {X3} {X4} {X7} forall {OP1:min X1 X2 X3} {OP2:min X3 X4 X7} exists {X5} {OP3:min X1 X4 X5} {OP4:min X5 X2 X7} true. - : min-assoc-commutative X1&X2=X3 X3&X4=X7 X5 X1&X4=X5 X5&X2=X7 <- min-associative X1&X2=X3 X3&X4=X7 X6 X2&X4=X6 X1&X6=X7 <- min-commutative X2&X4=X6 X4&X2=X6 <- min-associative-converse X4&X2=X6 X1&X6=X7 X5 X1&X4=X5 X5&X2=X7. %worlds () (min-assoc-commutative X1&X2=X3 X3&X4=X7 %{=>}% X5 X1&X4=X5 X5&X2=X7). %total {} (min-assoc-commutative _ _ _ _ _). %theorem min-double-associative* : forall* {A} {B} {C} {D} {A+B} {C+D} {A+C} {B+D} {X} forall {AB:min A B A+B} {CD:min C D C+D} {ABCD:min A+B C+D X} {AC:min A C A+C} {BD:min B D B+D} exists {ACBD:min A+C B+D X} true. - : min-double-associative* X1&X2=X3 X4&X8=XC X3&XC=XF X1&X4=X5 X2&X8=XA X5&XA=XF <- min-associative X1&X2=X3 X3&XC=XF XE X2&XC=XE X1&XE=XF <- min-commutative X4&X8=XC X8&X4=XC <- min-associative-converse* X8&X4=XC X2&XC=XE X2&X8=XA XA&X4=XE <- min-commutative XA&X4=XE X4&XA=XE <- min-associative-converse* X4&XA=XE X1&XE=XF X1&X4=X5 X5&XA=XF. %worlds () (min-double-associative* X1&X2=X3 X4&X8=XC X3&XC=XF X1&X4=X5 X2&X8=XA %{=>}% X5&XA=XF). %total {} (min-double-associative* _ _ _ _ _ _). %theorem min-double-associative : forall* {A} {B} {C} {D} {A+B} {C+D} {X} forall {AB:min A B A+B} {CD:min C D C+D} {ABCD:min A+B C+D X} exists {A+C} {B+D} {AC:min A C A+C} {BD:min B D B+D} {ACBD:min A+C B+D X} true. - : min-double-associative X1&X2=X3 X4&X8=XC X3&XC=XF X5 XA X1&X4=X5 X2&X8=XA X5&XA=XF <- min-associative X1&X2=X3 X3&XC=XF XE X2&XC=XE X1&XE=XF <- min-commutative X4&X8=XC X8&X4=XC <- min-associative-converse X8&X4=XC X2&XC=XE XA X2&X8=XA XA&X4=XE <- min-commutative XA&X4=XE X4&XA=XE <- min-associative-converse X4&XA=XE X1&XE=XF X5 X1&X4=X5 X5&XA=XF. %worlds () (min-double-associative _ _ _ _ _ _ _ _). %total { } (min-double-associative _ _ _ _ _ _ _ _). %%% Theorems about max %theorem false-implies-max : forall* {X1} {X2} {X3} forall {F:void} exists {M:max X1 X2 X3} true. %worlds () (false-implies-max _ _). %total { } (false-implies-max _ _). %theorem max-respects-eq : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {MX:max X1 X2 X3} {E1:eq X1 Y1} {E2:eq X2 Y2} {E3:eq X3 Y3} exists {MY:max Y1 Y2 Y3} true. - : max-respects-eq M eq/ eq/ eq/ M. %worlds () (max-respects-eq _ _ _ _ _). %total { } (max-respects-eq _ _ _ _ _). %theorem max-total** : forall* {X1} {X2} {C} forall {D:compare X1 X2 C} exists {X3} {M:max X1 X2 X3} true. - : max-total** compare/= _ max/=. - : max-total** (compare/> X1>X2) _ (max/> X1>X2). - : max-total** (compare/< X2>X1) _ (max/< X2>X1). %worlds () (max-total** _ _ _). %total { } (max-total** _ _ _). %theorem max-total* : forall {X1} {X2} exists {X3} {M:max X1 X2 X3} true. - : max-total* X1 X2 X3 M <- compare-total D <- max-total** D X3 M. %worlds () (max-total* _ _ _ _). %total { } (max-total* _ _ _ _). %abbrev max-total = max-total* _ _ _. %theorem max-deterministic : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {MX:max X1 X2 X3} {MY:max Y1 Y2 Y3} {E1:eq X1 Y1} {E2:eq X2 Y2} exists {E3:eq X3 Y3} true. - : max-deterministic (max/=) (max/=) eq/ eq/ eq/. - : max-deterministic (max/=) (max/> X>X) eq/ eq/ eq/. - : max-deterministic (max/=) (max/< X>X) eq/ eq/ eq/. - : max-deterministic (max/> X>X) (max/=) eq/ eq/ eq/. - : max-deterministic (max/> X>Y) (max/> X>YP) eq/ eq/ eq/. - : max-deterministic (max/> X>Y) (max/< Y>X) eq/ eq/ E <- gt-anti-symmetric X>Y Y>X F <- false-implies-eq F E. - : max-deterministic (max/< X>X) (max/=) eq/ eq/ eq/. - : max-deterministic (max/< X>Y) (max/> Y>X) eq/ eq/ E <- gt-anti-symmetric X>Y Y>X F <- false-implies-eq F E. - : max-deterministic (max/< X>Y) (max/< X>YP) eq/ eq/ eq/. %worlds () (max-deterministic _ _ _ _ _). %total { } (max-deterministic _ _ _ _ _). %theorem max-commutative : forall* {X1} {X2} {X3} forall {M:max X1 X2 X3} exists {Mc:max X2 X1 X3} true. - : max-commutative max/= max/=. - : max-commutative (max/> X>Y) (max/< X>Y). - : max-commutative (max/< X>Y) (max/> X>Y). %worlds () (max-commutative _ _). %total { } (max-commutative _ _). %theorem ge-implies-max : forall* {X1} {X2} forall {G:ge X1 X2} exists {M:max X1 X2 X1} true. - : ge-implies-max (ge/> X1>X2) (max/> X1>X2). - : ge-implies-max (ge/= eq/) (max/=). %worlds () (ge-implies-max _ _). %total { } (ge-implies-max _ _). %theorem le-implies-max : forall* {X1} {X2} forall {G:le X1 X2} exists {M:max X1 X2 X2} true. - : le-implies-max X2>=X1 M <- ge-implies-max X2>=X1 Mc <- max-commutative Mc M. %worlds () (le-implies-max _ _). %total { } (le-implies-max _ _). %theorem max-implies-ge : forall* {X1} {X2} {X3} forall {M:max X1 X2 X3} exists {G1:ge X3 X1} {G2:ge X3 X2} true. - : max-implies-ge max/= (ge/= eq/) (ge/= eq/). - : max-implies-ge (max/> X1>X2) (ge/= eq/) (ge/> X1>X2). - : max-implies-ge (max/< X2>X1) (ge/> X2>X1) (ge/= eq/). %worlds () (max-implies-ge _ _ _). %total { } (max-implies-ge _ _ _). %theorem max-is-lub : forall* {X0} {X1} {X2} {X3} forall {M:max X1 X2 X3} {G1:ge X0 X1} {G2:ge X0 X2} exists {G3:ge X0 X3} true. - : max-is-lub max/= G _ G. - : max-is-lub (max/> X1>X2) G _ G. - : max-is-lub (max/< X2>X1) _ G G. %worlds () (max-is-lub _ _ _ _). %total { } (max-is-lub _ _ _ _). %theorem max-left-preserves-ge* : forall* {X1} {X2} {X3} {X4} {X5} forall {G:ge X2 X4} {M12:max X1 X2 X3} {M14:max X1 X4 X5} exists {G:ge X3 X5} true. - : max-left-preserves-ge* X>=X4 max/= X|X4=X5 X>=X5 <- ge-reflexive _ X>=X <- max-is-lub X|X4=X5 X>=X X>=X4 X>=X5. - : max-left-preserves-ge* X2>=X4 (max/> X1>X2) X1|X4=X5 X1>=X5 <- ge-transitive (ge/> X1>X2) X2>=X4 X1>=X4 <- ge-reflexive _ X1>=X1 <- max-is-lub X1|X4=X5 X1>=X1 X1>=X4 X1>=X5. - : max-left-preserves-ge* X2>=X4 (max/< X2>X1) X1|X4=X5 X2>=X5 <- max-is-lub X1|X4=X5 (ge/> X2>X1) X2>=X4 X2>=X5. %worlds () (max-left-preserves-ge* _ _ _ _). %total { } (max-left-preserves-ge* _ _ _ _). %theorem max-left-preserves-le* : forall* {X1} {X2} {X3} {X4} {X5} forall {G:le X2 X4} {M12:max X1 X2 X3} {M14:max X1 X4 X5} exists {G:le X3 X5} true. - : max-left-preserves-le* G1 M12 M14 G2 <- max-left-preserves-ge* G1 M14 M12 G2. %worlds () (max-left-preserves-le* _ _ _ _). %total { } (max-left-preserves-le* _ _ _ _). %theorem max-left-preserves-ge : forall* {X1} {X2} {X4} forall {G:ge X2 X4} exists {X3} {X5} {O1:max X1 X2 X3} {O2:max X1 X4 X5} {G2:ge X3 X5} true. - : max-left-preserves-ge X2>=X4 X3 X5 X1&X2=A3 X1&X4=X5 X3>=X5 <- max-total X1&X2=A3 <- max-total X1&X4=X5 <- max-left-preserves-ge* X2>=X4 X1&X2=A3 X1&X4=X5 X3>=X5. %worlds () (max-left-preserves-ge X2>=X4 %{=>}% X3 X5 X1&X2=A3 X1&X4=X5 X3>=X5). %total {} (max-left-preserves-ge _ _ _ _ _ _). %theorem max-right-preserves-ge* : forall* {X1} {X2} {X3} {X4} {X5} forall {G1:ge X1 X2} {O1:max X1 X3 X4} {O2:max X2 X3 X5} exists {G2:ge X4 X5} true. - : max-right-preserves-ge* X1>=X2 X1&X3=X4 X2&X3=X5 X4>=X5 <- max-commutative X1&X3=X4 X3&X1=X4 <- max-commutative X2&X3=X5 X3&X2=X5 <- max-left-preserves-ge* X1>=X2 X3&X1=X4 X3&X2=X5 X4>=X5. %worlds () (max-right-preserves-ge* X1>=X2 X1&X3=X4 X2&X3=X5 %{=>}% X4>=X5). %total {} (max-right-preserves-ge* _ _ _ _). %theorem max-right-preserves-ge : forall* {X1} {X2} {X3} forall {G1:ge X1 X2} exists {X4} {X5} {O1:max X1 X3 X4} {O2:max X2 X3 X5} {G2:ge X4 X5} true. - : max-right-preserves-ge X1>=X2 X4 X5 X1&X3=X4 X2&X3=X5 X4>=X5 <- max-total X1&X3=X4 <- max-total X2&X3=X5 <- max-right-preserves-ge* X1>=X2 X1&X3=X4 X2&X3=X5 X4>=X5. %worlds () (max-right-preserves-ge X1>=X2 %{=>}% X4 X5 X1&X3=X4 X2&X3=X5 X4>=X5). %total {} (max-right-preserves-ge _ _ _ _ _ _). %theorem max-preserves-ge* : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {G1:ge X1 Y1} {G2:ge X2 Y2} {MX:max X1 X2 X3} {MY:max Y1 Y2 Y3} exists {G3:ge X3 Y3} true. - : max-preserves-ge* X1>=Y1 X2>=Y2 X1&X2=X3 Y1&Y2=Y3 X3>=Y3 <- max-total Y1&X2=X <- max-right-preserves-ge* X1>=Y1 X1&X2=X3 Y1&X2=X X3>=X <- max-left-preserves-ge* X2>=Y2 Y1&X2=X Y1&Y2=Y3 X>=Y3 <- ge-transitive X3>=X X>=Y3 X3>=Y3. %worlds () (max-preserves-ge* X1>=Y1 X2>=Y2 X1&X2=X3 Y1&Y2=Y3 %{=>}% X3>=Y3). %total {} (max-preserves-ge* _ _ _ _ _). %theorem max-preserves-ge : forall* {X1} {X2} {Y1} {Y2} forall {G1:ge X1 Y1} {G2:ge X2 Y2} exists {X3} {Y3} {MX:max X1 X2 X3} {MY:max Y1 Y2 Y3} {G3:ge X3 Y3} true. - : max-preserves-ge X1>=Y1 X2>=Y2 X3 Y3 X1&X2=X3 Y1&Y2=Y3 X3>=Y3 <- max-total X1&X2=X3 <- max-total Y1&Y2=Y3 <- max-preserves-ge* X1>=Y1 X2>=Y2 X1&X2=X3 Y1&Y2=Y3 X3>=Y3. %worlds () (max-preserves-ge X1>=Y1 X2>=Y2 %{=>}% X3 Y3 X1&X2=X3 Y1&Y2=Y3 X3>=Y3). %total {} (max-preserves-ge _ _ _ _ _ _ _). %theorem max-left-preserves-le : forall* {X1} {X2} {X4} forall {G:le X2 X4} exists {X3} {X5} {O1:max X1 X2 X3} {O2:max X1 X4 X5} {G2:le X3 X5} true. - : max-left-preserves-le X2<=X4 X3 X5 X1&X2=A3 X1&X4=X5 X3<=X5 <- max-total X1&X2=A3 <- max-total X1&X4=X5 <- max-left-preserves-le* X2<=X4 X1&X2=A3 X1&X4=X5 X3<=X5. %worlds () (max-left-preserves-le X2<=X4 %{=>}% X3 X5 X1&X2=A3 X1&X4=X5 X3<=X5). %total {} (max-left-preserves-le _ _ _ _ _ _). %theorem max-right-preserves-le* : forall* {X1} {X2} {X3} {X4} {X5} forall {G1:le X1 X2} {O1:max X1 X3 X4} {O2:max X2 X3 X5} exists {G2:le X4 X5} true. - : max-right-preserves-le* X1<=X2 X1&X3=X4 X2&X3=X5 X4<=X5 <- max-commutative X1&X3=X4 X3&X1=X4 <- max-commutative X2&X3=X5 X3&X2=X5 <- max-left-preserves-le* X1<=X2 X3&X1=X4 X3&X2=X5 X4<=X5. %worlds () (max-right-preserves-le* X1<=X2 X1&X3=X4 X2&X3=X5 %{=>}% X4<=X5). %total {} (max-right-preserves-le* _ _ _ _). %theorem max-right-preserves-le : forall* {X1} {X2} {X3} forall {G1:le X1 X2} exists {X4} {X5} {O1:max X1 X3 X4} {O2:max X2 X3 X5} {G2:le X4 X5} true. - : max-right-preserves-le X1<=X2 X4 X5 X1&X3=X4 X2&X3=X5 X4<=X5 <- max-total X1&X3=X4 <- max-total X2&X3=X5 <- max-right-preserves-le* X1<=X2 X1&X3=X4 X2&X3=X5 X4<=X5. %worlds () (max-right-preserves-le X1<=X2 %{=>}% X4 X5 X1&X3=X4 X2&X3=X5 X4<=X5). %total {} (max-right-preserves-le _ _ _ _ _ _). %theorem max-preserves-le* : forall* {X1} {X2} {X3} {Y1} {Y2} {Y3} forall {G1:le X1 Y1} {G2:le X2 Y2} {MX:max X1 X2 X3} {MY:max Y1 Y2 Y3} exists {G3:le X3 Y3} true. - : max-preserves-le* X1<=Y1 X2<=Y2 X1&X2=X3 Y1&Y2=Y3 X3<=Y3 <- max-total Y1&X2=X <- max-right-preserves-le* X1<=Y1 X1&X2=X3 Y1&X2=X X3<=X <- max-left-preserves-le* X2<=Y2 Y1&X2=X Y1&Y2=Y3 X<=Y3 <- le-transitive X3<=X X<=Y3 X3<=Y3. %worlds () (max-preserves-le* X1<=Y1 X2<=Y2 X1&X2=X3 Y1&Y2=Y3 %{=>}% X3<=Y3). %total {} (max-preserves-le* _ _ _ _ _). %theorem max-preserves-le : forall* {X1} {X2} {Y1} {Y2} forall {G1:le X1 Y1} {G2:le X2 Y2} exists {X3} {Y3} {MX:max X1 X2 X3} {MY:max Y1 Y2 Y3} {G3:le X3 Y3} true. - : max-preserves-le X1<=Y1 X2<=Y2 X3 Y3 X1&X2=X3 Y1&Y2=Y3 X3<=Y3 <- max-total X1&X2=X3 <- max-total Y1&Y2=Y3 <- max-preserves-le* X1<=Y1 X2<=Y2 X1&X2=X3 Y1&Y2=Y3 X3<=Y3. %worlds () (max-preserves-le X1<=Y1 X2<=Y2 %{=>}% X3 Y3 X1&X2=X3 Y1&Y2=Y3 X3<=Y3). %total {} (max-preserves-le _ _ _ _ _ _ _). %theorem max-associative : forall* {X1} {X2} {X3} {X4} {X7} forall {M12:max X1 X2 X3} {M34:max X3 X4 X7} exists {X6} {M24:max X2 X4 X6} {M16:max X1 X6 X7} true. - : max-associative max/= max/= _ max/= max/=. - : max-associative max/= (max/> X3>X4) _ (max/> X3>X4) max/=. - : max-associative max/= (max/< X4>X3) _ (max/< X4>X3) (max/< X4>X3). - : max-associative (max/> X1>X2) max/= _ (max/< X1>X2) max/=. - : max-associative (max/> X1>X2) (max/> X1>X4) _ M24 M16 <- max-total M24 <- max-is-lub M24 (ge/> X1>X2) (ge/> X1>X4) X1>=X6 <- ge-implies-max X1>=X6 M16. - : max-associative (max/> X1>X2) (max/< X4>X1) _ (max/< X4>X2) (max/< X4>X1) <- gt-transitive X4>X1 X1>X2 X4>X2. - : max-associative (max/< X2>X1) max/= _ max/= (max/< X2>X1). - : max-associative (max/< X2>X1) (max/> X2>X4) _ (max/> X2>X4) (max/< X2>X1). - : max-associative (max/< X2>X1) (max/< X4>X2) _ (max/< X4>X2) (max/< X4>X1) <- gt-transitive X4>X2 X2>X1 X4>X1. %worlds () (max-associative _ _ _ _ _). %total { } (max-associative _ _ _ _ _). %theorem max-associative* : forall* {X1} {X2} {X12} {X3} {X23} {X123} forall {OP12:max X1 X2 X12} {OP12-3:max X12 X3 X123} {OP23:max X2 X3 X23} exists {OP1-23:max X1 X23 X123} true. - : max-associative* X1|X2=X3 X3|X4=X7 X2|X4=X6 X1|X6=X7 <- max-associative X1|X2=X3 X3|X4=X7 Y6 X2|X4=Y6 X1|Y6=X7 <- max-deterministic X2|X4=Y6 X2|X4=X6 eq/ eq/ Y6=X6 <- max-respects-eq X1|Y6=X7 eq/ Y6=X6 eq/ X1|X6=X7. %worlds () (max-associative* _ _ _ _). %total {} (max-associative* _ _ _ _). %theorem max-associative-converse : forall* {X1} {X2} {X4} {X6} {X7} forall {OP24:max X2 X4 X6} {OP16:max X1 X6 X7} exists {X3} {OP12:max X1 X2 X3} {OP34:max X3 X4 X7} true. - : max-associative-converse X2|X4=X6 X1|X6=X7 _ X1|X2=X3 X3|X4=X7 <- max-commutative X2|X4=X6 X4|X2=X6 <- max-commutative X1|X6=X7 X6|X1=X7 <- max-associative X4|X2=X6 X6|X1=X7 _ X2|X1=X3 X4|X3=X7 <- max-commutative X2|X1=X3 X1|X2=X3 <- max-commutative X4|X3=X7 X3|X4=X7. %worlds () (max-associative-converse X2|X4=X6 X1|X6=X7 X3 X1|X2=X3 X3|X4=X7). %total {} (max-associative-converse _ _ _ _ _). %theorem max-associative-converse* : forall* {X1} {X2} {X3} {X4} {X6} {X7} forall {OP24:max X2 X4 X6} {OP16:max X1 X6 X7} {OP12:max X1 X2 X3} exists {OP34:max X3 X4 X7} true. - : max-associative-converse* X2|X4=X6 X1|X6=X7 X1|X2=X3 X3|X4=X7 <- max-associative-converse X2|X4=X6 X1|X6=X7 X3P X1|X2=X3P X3P|X4=X7 <- max-deterministic X1|X2=X3P X1|X2=X3 eq/ eq/ X3P=X3 <- max-respects-eq X3P|X4=X7 X3P=X3 eq/ eq/ X3|X4=X7. %worlds () (max-associative-converse* X2|X4=X6 X1|X6=X7 X1|X2=X3 %{=>}% X3|X4=X7). %total {} (max-associative-converse* _ _ _ _). %theorem max-assoc-commutative* : forall* {X1} {X2} {X3} {X4} {X5} {X7} forall {OP1:max X1 X2 X3} {OP2:max X3 X4 X7} {OP3:max X1 X4 X5} exists {OP4:max X5 X2 X7} true. - : max-assoc-commutative* X1|X2=X3 X3|X4=X7 X1|X4=X5 X5|X2=X7 <- max-associative X1|X2=X3 X3|X4=X7 X6 X2|X4=X6 X1|X6=X7 <- max-commutative X2|X4=X6 X4|X2=X6 <- max-associative-converse* X4|X2=X6 X1|X6=X7 X1|X4=X5 X5|X2=X7. %worlds () (max-assoc-commutative* X1|X2=X3 X3|X4=X7 X1|X4=X5 %{=>}% X5|X2=X7). %total {} (max-assoc-commutative* _ _ _ _). %theorem max-assoc-commutative : forall* {X1} {X2} {X3} {X4} {X7} forall {OP1:max X1 X2 X3} {OP2:max X3 X4 X7} exists {X5} {OP3:max X1 X4 X5} {OP4:max X5 X2 X7} true. - : max-assoc-commutative X1|X2=X3 X3|X4=X7 X5 X1|X4=X5 X5|X2=X7 <- max-associative X1|X2=X3 X3|X4=X7 X6 X2|X4=X6 X1|X6=X7 <- max-commutative X2|X4=X6 X4|X2=X6 <- max-associative-converse X4|X2=X6 X1|X6=X7 X5 X1|X4=X5 X5|X2=X7. %worlds () (max-assoc-commutative X1|X2=X3 X3|X4=X7 %{=>}% X5 X1|X4=X5 X5|X2=X7). %total {} (max-assoc-commutative _ _ _ _ _). %theorem max-double-associative* : forall* {A} {B} {C} {D} {A+B} {C+D} {A+C} {B+D} {X} forall {AB:max A B A+B} {CD:max C D C+D} {ABCD:max A+B C+D X} {AC:max A C A+C} {BD:max B D B+D} exists {ACBD:max A+C B+D X} true. - : max-double-associative* X1|X2=X3 X4|X8=XC X3|XC=XF X1|X4=X5 X2|X8=XA X5|XA=XF <- max-associative X1|X2=X3 X3|XC=XF XE X2|XC=XE X1|XE=XF <- max-commutative X4|X8=XC X8|X4=XC <- max-associative-converse* X8|X4=XC X2|XC=XE X2|X8=XA XA|X4=XE <- max-commutative XA|X4=XE X4|XA=XE <- max-associative-converse* X4|XA=XE X1|XE=XF X1|X4=X5 X5|XA=XF. %worlds () (max-double-associative* X1|X2=X3 X4|X8=XC X3|XC=XF X1|X4=X5 X2|X8=XA %{=>}% X5|XA=XF). %total {} (max-double-associative* _ _ _ _ _ _). %theorem max-double-associative : forall* {A} {B} {C} {D} {A+B} {C+D} {X} forall {AB:max A B A+B} {CD:max C D C+D} {ABCD:max A+B C+D X} exists {A+C} {B+D} {AC:max A C A+C} {BD:max B D B+D} {ACBD:max A+C B+D X} true. - : max-double-associative X1|X2=X3 X4|X8=XC X3|XC=XF X5 XA X1|X4=X5 X2|X8=XA X5|XA=XF <- max-associative X1|X2=X3 X3|XC=XF XE X2|XC=XE X1|XE=XF <- max-commutative X4|X8=XC X8|X4=XC <- max-associative-converse X8|X4=XC X2|XC=XE XA X2|X8=XA XA|X4=XE <- max-commutative XA|X4=XE X4|XA=XE <- max-associative-converse X4|XA=XE X1|XE=XF X5 X1|X4=X5 X5|XA=XF. %worlds () (max-double-associative _ _ _ _ _ _ _ _). %total { } (max-double-associative _ _ _ _ _ _ _ _). %%% Distributivity theorems %theorem min-right-distributes-over-max : forall* {X1} {X2} {X3} {X4} {X7} forall {A12:max X1 X2 X3} {M34:min X3 X4 X7} exists {X5} {X6} {M14:min X1 X4 X5} {M24:min X2 X4 X6} {A56:max X5 X6 X7} true. - : min-right-distributes-over-max max/= M _ _ M M max/=. - : min-right-distributes-over-max (max/> X1>X2) X1&X4=X7 _ _ X1&X4=X7 X2&X4=X6 X7|X6=X7 <- min-total X2&X4=X6 <- min-right-preserves-ge* (ge/> X1>X2) X1&X4=X7 X2&X4=X6 X7>=X6 <- ge-implies-max X7>=X6 X7|X6=X7. - : min-right-distributes-over-max (max/< X2>X1) X2&X4=X7 _ _ X1&X4=X5 X2&X4=X7 X5|X7=X7 <- min-total X1&X4=X5 <- min-right-preserves-ge* (ge/> X2>X1) X2&X4=X7 X1&X4=X5 X7>=X5 <- ge-implies-max X7>=X5 X7|X5=X7 <- max-commutative X7|X5=X7 X5|X7=X7. %worlds () (min-right-distributes-over-max _ _ _ _ _ _ _). %total { } (min-right-distributes-over-max _ _ _ _ _ _ _). %theorem max-right-distributes-over-min : forall* {X1} {X2} {X3} {X4} {X7} forall {A12:min X1 X2 X3} {M34:max X3 X4 X7} exists {X5} {X6} {M14:max X1 X4 X5} {M24:max X2 X4 X6} {A56:min X5 X6 X7} true. - : max-right-distributes-over-min min/= M _ _ M M min/=. - : max-right-distributes-over-min (min/> X1>X2) X2|X4=X7 _ _ X1|X4=X5 X2|X4=X7 X5&X7=X7 <- max-total X1|X4=X5 <- max-right-preserves-ge* (ge/> X1>X2) X1|X4=X5 X2|X4=X7 X5>=X7 <- ge-implies-min X5>=X7 X5&X7=X7. - : max-right-distributes-over-min (min/< X2>X1) X1|X4=X7 _ _ X1|X4=X7 X2|X4=X6 X7&X6=X7 <- max-total X2|X4=X6 <- max-right-preserves-ge* (ge/> X2>X1) X2|X4=X6 X1|X4=X7 X6>=X7 <- le-implies-min X6>=X7 X7&X6=X7. %worlds () (max-right-distributes-over-min _ _ _ _ _ _ _). %total { } (max-right-distributes-over-min _ _ _ _ _ _ _). %theorem min-right-distributes-over-max* : forall* {X1} {X2} {X3} {X4} {X5} {X6} {X7} forall {A12:max X1 X2 X3} {M34:min X3 X4 X7} {M14:min X1 X4 X5} {M24:min X2 X4 X6} exists {A56:max X5 X6 X7} true. - : min-right-distributes-over-max* X1|X2=X3 X3&X4=X7 X1&X4=X5 X2&X4=X6 X5|X6=X7 <- min-right-distributes-over-max X1|X2=X3 X3&X4=X7 Y5 Y6 X1&X4=Y5 X2&X4=Y6 Y5|Y6=X7 <- min-deterministic X1&X4=Y5 X1&X4=X5 eq/ eq/ Y5=X5 <- min-deterministic X2&X4=Y6 X2&X4=X6 eq/ eq/ Y6=X6 <- max-respects-eq Y5|Y6=X7 Y5=X5 Y6=X6 eq/ X5|X6=X7. %worlds () (min-right-distributes-over-max* X1|X2=X3 X3&X4=X7 X1&X4=X5 X2&X4=X6 %{=>}% X5|X6=X7). %total {} (min-right-distributes-over-max* _ _ _ _ _). %theorem min-left-distributes-over-max* : forall* {X1} {X2} {X3} {X4} {X5} {X6} {X7} forall {A12:max X2 X4 X6} {M34:min X1 X6 X7} {M14:min X1 X2 X3} {M24:min X1 X4 X5} exists {A56:max X3 X5 X7} true. - : min-left-distributes-over-max* X2|X4=X6 X1&X6=X7 X1&X2=X3 X1&X4=X5 X3|X5=X7 <- min-commutative X1&X6=X7 X6&X1=X7 <- min-commutative X1&X2=X3 X2&X1=X3 <- min-commutative X1&X4=X5 X4&X1=X5 <- min-right-distributes-over-max* X2|X4=X6 X6&X1=X7 X2&X1=X3 X4&X1=X5 X3|X5=X7. %worlds () (min-left-distributes-over-max* X2|X4=X6 X1&X6=X7 X1&X2=X3 X1&X4=X5 %{=>}% X3|X5=X7). %total {} (min-left-distributes-over-max* _ _ _ _ _). %theorem min-left-distributes-over-max : forall* {X1} {X2} {X4} {X6} {X7} forall {A12:max X2 X4 X6} {M34:min X1 X6 X7} exists {X3} {X5} {M14:min X1 X2 X3} {M24:min X1 X4 X5} {A56:max X3 X5 X7} true. - : min-left-distributes-over-max X2|X4=X6 X1&X6=X7 X3 X5 X1&X2=X3 X1&X4=X5 X3|X5=X7 <- min-total X1&X2=X3 <- min-total X1&X4=X5 <- min-left-distributes-over-max* X2|X4=X6 X1&X6=X7 X1&X2=X3 X1&X4=X5 X3|X5=X7. %worlds () (min-left-distributes-over-max X2|X4=X6 X1&X6=X7 %{=>}% X3 X5 X1&X2=X3 X1&X4=X5 X3|X5=X7). %total {} (min-left-distributes-over-max _ _ _ _ _ _ _). %theorem min-right-factors-over-max : forall* {X1} {X2} {X4} {X5} {X6} {X7} forall {M14:min X1 X4 X5} {M24:min X2 X4 X6} {A56:max X5 X6 X7} exists {X3} {A12:max X1 X2 X3} {M34:min X3 X4 X7} true. - : min-right-factors-over-max X1&X4=X5 X2&X4=X6 X5|X6=X7 X3 X1|X2=X3 X3&X4=X7 <- max-total X1|X2=X3 <- min-total X3&X4=Y7 <- min-right-distributes-over-max* X1|X2=X3 X3&X4=Y7 X1&X4=X5 X2&X4=X6 X5|X6=Y7 <- max-deterministic X5|X6=Y7 X5|X6=X7 eq/ eq/ Y7=X7 <- min-respects-eq X3&X4=Y7 eq/ eq/ Y7=X7 X3&X4=X7. %worlds () (min-right-factors-over-max X1&X4=X5 X2&X4=X6 X5|X6=X7 %{=>}% X3 X1|X2=X3 X3&X4=X7 ). %total {} (min-right-factors-over-max _ _ _ _ _ _). %theorem min-right-factors-over-max* : forall* {X1} {X2} {X3} {X4} {X5} {X6} {X7} forall {M14:min X1 X4 X5} {M24:min X2 X4 X6} {A56:max X5 X6 X7} {A12:max X1 X2 X3} exists {M34:min X3 X4 X7} true. - : min-right-factors-over-max* X1&X4=X5 X2&X4=X6 X5|X6=X7 X1|X2=X3 X3&X4=X7 <- min-total X3&X4=Y7 <- min-right-distributes-over-max* X1|X2=X3 X3&X4=Y7 X1&X4=X5 X2&X4=X6 X5|X6=Y7 <- max-deterministic X5|X6=Y7 X5|X6=X7 eq/ eq/ Y7=X7 <- min-respects-eq X3&X4=Y7 eq/ eq/ Y7=X7 X3&X4=X7. %worlds () (min-right-factors-over-max* X1&X4=X5 X2&X4=X6 X5|X6=X7 X1|X2=X3 %{=>}% X3&X4=X7 ). %total {} (min-right-factors-over-max* _ _ _ _ _). %theorem min-left-factors-over-max : forall* {X1} {X2} {X3} {X4} {X5} {X7} forall {M12:min X1 X2 X3} {M14:min X1 X4 X5} {A35:max X3 X5 X7} exists {X6} {A24:max X2 X4 X6} {M16:min X1 X6 X7} true. - : min-left-factors-over-max X1&X2=X3 X1&X4=X5 X3|X5=X7 X6 X2|X4=X6 X1&X6=X7 <- min-commutative X1&X2=X3 X2&X1=X3 <- min-commutative X1&X4=X5 X4&X1=X5 <- min-right-factors-over-max X2&X1=X3 X4&X1=X5 X3|X5=X7 X6 X2|X4=X6 X6&X1=X7 <- min-commutative X6&X1=X7 X1&X6=X7. %worlds () (min-left-factors-over-max X1&X2=X3 X1&X4=X5 X3|X5=X7 %{=>}% X6 X2|X4=X6 X1&X6=X7). %total {} (min-left-factors-over-max _ _ _ _ _ _). %theorem min-left-factors-over-max* : forall* {X1} {X2} {X3} {X4} {X5} {X6} {X7} forall {M12:min X1 X2 X3} {M14:min X1 X4 X5} {A35:max X3 X5 X7} {A24:max X2 X4 X6} exists {M16:min X1 X6 X7} true. - : min-left-factors-over-max* X1&X2=X3 X1&X4=X5 X3|X5=X7 X2|X4=X6 X1&X6=X7 <- min-total X1&X6=Y7 <- min-left-distributes-over-max* X2|X4=X6 X1&X6=Y7 X1&X2=X3 X1&X4=X5 X3|X5=Y7 <- max-deterministic X3|X5=Y7 X3|X5=X7 eq/ eq/ Y7=X7 <- min-respects-eq X1&X6=Y7 eq/ eq/ Y7=X7 X1&X6=X7. %worlds () (min-left-factors-over-max* X1&X2=X3 X1&X4=X5 X3|X5=X7 X2|X4=X6 %{=>}% X1&X6=X7). %total {} (min-left-factors-over-max* _ _ _ _ _). %theorem max-right-distributes-over-min* : forall* {X1} {X2} {X3} {X4} {X5} {X6} {X7} forall {A12:min X1 X2 X3} {M34:max X3 X4 X7} {M14:max X1 X4 X5} {M24:max X2 X4 X6} exists {A56:min X5 X6 X7} true. - : max-right-distributes-over-min* X1&X2=X3 X3|X4=X7 X1|X4=X5 X2|X4=X6 X5&X6=X7 <- max-right-distributes-over-min X1&X2=X3 X3|X4=X7 Y5 Y6 X1|X4=Y5 X2|X4=Y6 Y5&Y6=X7 <- max-deterministic X1|X4=Y5 X1|X4=X5 eq/ eq/ Y5=X5 <- max-deterministic X2|X4=Y6 X2|X4=X6 eq/ eq/ Y6=X6 <- min-respects-eq Y5&Y6=X7 Y5=X5 Y6=X6 eq/ X5&X6=X7. %worlds () (max-right-distributes-over-min* X1&X2=X3 X3|X4=X7 X1|X4=X5 X2|X4=X6 %{=>}% X5&X6=X7). %total {} (max-right-distributes-over-min* _ _ _ _ _). %theorem max-left-distributes-over-min* : forall* {X1} {X2} {X3} {X4} {X5} {X6} {X7} forall {A12:min X2 X4 X6} {M34:max X1 X6 X7} {M14:max X1 X2 X3} {M24:max X1 X4 X5} exists {A56:min X3 X5 X7} true. - : max-left-distributes-over-min* X2&X4=X6 X1|X6=X7 X1|X2=X3 X1|X4=X5 X3&X5=X7 <- max-commutative X1|X6=X7 X6|X1=X7 <- max-commutative X1|X2=X3 X2|X1=X3 <- max-commutative X1|X4=X5 X4|X1=X5 <- max-right-distributes-over-min* X2&X4=X6 X6|X1=X7 X2|X1=X3 X4|X1=X5 X3&X5=X7. %worlds () (max-left-distributes-over-min* X2&X4=X6 X1|X6=X7 X1|X2=X3 X1|X4=X5 %{=>}% X3&X5=X7). %total {} (max-left-distributes-over-min* _ _ _ _ _). %theorem max-left-distributes-over-min : forall* {X1} {X2} {X4} {X6} {X7} forall {A12:min X2 X4 X6} {M34:max X1 X6 X7} exists {X3} {X5} {M14:max X1 X2 X3} {M24:max X1 X4 X5} {A56:min X3 X5 X7} true. - : max-left-distributes-over-min X2&X4=X6 X1|X6=X7 X3 X5 X1|X2=X3 X1|X4=X5 X3&X5=X7 <- max-total X1|X2=X3 <- max-total X1|X4=X5 <- max-left-distributes-over-min* X2&X4=X6 X1|X6=X7 X1|X2=X3 X1|X4=X5 X3&X5=X7. %worlds () (max-left-distributes-over-min X2&X4=X6 X1|X6=X7 %{=>}% X3 X5 X1|X2=X3 X1|X4=X5 X3&X5=X7). %total {} (max-left-distributes-over-min _ _ _ _ _ _ _). %theorem max-right-factors-over-min : forall* {X1} {X2} {X4} {X5} {X6} {X7} forall {M14:max X1 X4 X5} {M24:max X2 X4 X6} {A56:min X5 X6 X7} exists {X3} {A12:min X1 X2 X3} {M34:max X3 X4 X7} true. - : max-right-factors-over-min X1|X4=X5 X2|X4=X6 X5&X6=X7 X3 X1&X2=X3 X3|X4=X7 <- min-total X1&X2=X3 <- max-total X3|X4=Y7 <- max-right-distributes-over-min* X1&X2=X3 X3|X4=Y7 X1|X4=X5 X2|X4=X6 X5&X6=Y7 <- min-deterministic X5&X6=Y7 X5&X6=X7 eq/ eq/ Y7=X7 <- max-respects-eq X3|X4=Y7 eq/ eq/ Y7=X7 X3|X4=X7. %worlds () (max-right-factors-over-min X1|X4=X5 X2|X4=X6 X5&X6=X7 %{=>}% X3 X1&X2=X3 X3|X4=X7 ). %total {} (max-right-factors-over-min _ _ _ _ _ _). %theorem max-right-factors-over-min* : forall* {X1} {X2} {X3} {X4} {X5} {X6} {X7} forall {M14:max X1 X4 X5} {M24:max X2 X4 X6} {A56:min X5 X6 X7} {A12:min X1 X2 X3} exists {M34:max X3 X4 X7} true. - : max-right-factors-over-min* X1|X4=X5 X2|X4=X6 X5&X6=X7 X1&X2=X3 X3|X4=X7 <- max-total X3|X4=Y7 <- max-right-distributes-over-min* X1&X2=X3 X3|X4=Y7 X1|X4=X5 X2|X4=X6 X5&X6=Y7 <- min-deterministic X5&X6=Y7 X5&X6=X7 eq/ eq/ Y7=X7 <- max-respects-eq X3|X4=Y7 eq/ eq/ Y7=X7 X3|X4=X7. %worlds () (max-right-factors-over-min* X1|X4=X5 X2|X4=X6 X5&X6=X7 X1&X2=X3 %{=>}% X3|X4=X7 ). %total {} (max-right-factors-over-min* _ _ _ _ _). %theorem max-left-factors-over-min : forall* {X1} {X2} {X3} {X4} {X5} {X7} forall {M12:max X1 X2 X3} {M14:max X1 X4 X5} {A35:min X3 X5 X7} exists {X6} {A24:min X2 X4 X6} {M16:max X1 X6 X7} true. - : max-left-factors-over-min X1|X2=X3 X1|X4=X5 X3&X5=X7 X6 X2&X4=X6 X1|X6=X7 <- max-commutative X1|X2=X3 X2|X1=X3 <- max-commutative X1|X4=X5 X4|X1=X5 <- max-right-factors-over-min X2|X1=X3 X4|X1=X5 X3&X5=X7 X6 X2&X4=X6 X6|X1=X7 <- max-commutative X6|X1=X7 X1|X6=X7. %worlds () (max-left-factors-over-min X1|X2=X3 X1|X4=X5 X3&X5=X7 %{=>}% X6 X2&X4=X6 X1|X6=X7). %total {} (max-left-factors-over-min _ _ _ _ _ _). %theorem max-left-factors-over-min* : forall* {X1} {X2} {X3} {X4} {X5} {X6} {X7} forall {M12:max X1 X2 X3} {M14:max X1 X4 X5} {A35:min X3 X5 X7} {A24:min X2 X4 X6} exists {M16:max X1 X6 X7} true. - : max-left-factors-over-min* X1|X2=X3 X1|X4=X5 X3&X5=X7 X2&X4=X6 X1|X6=X7 <- max-total X1|X6=Y7 <- max-left-distributes-over-min* X2&X4=X6 X1|X6=Y7 X1|X2=X3 X1|X4=X5 X3&X5=Y7 <- min-deterministic X3&X5=Y7 X3&X5=X7 eq/ eq/ Y7=X7 <- max-respects-eq X1|X6=Y7 eq/ eq/ Y7=X7 X1|X6=X7. %worlds () (max-left-factors-over-min* X1|X2=X3 X1|X4=X5 X3&X5=X7 X2&X4=X6 %{=>}% X1|X6=X7). %total {} (max-left-factors-over-min* _ _ _ _ _). %abbrev nat`nat = nat. %abbrev nat`z = z. %abbrev nat`s = s. %abbrev nat`plus = plus. %abbrev nat`plus/z = plus/z. %abbrev nat`plus/s = plus/s. %abbrev nat`times = times. %abbrev nat`times/z = times/z. %abbrev nat`times/s = times/s. %abbrev nat`eq = eq. %abbrev nat`eq/ = eq/. %abbrev nat`gt = gt. %abbrev nat`gt/1 = gt/1. %abbrev nat`gt/> = gt/>. %abbrev nat`compare = compare. %abbrev nat`compare/= = compare/=. %abbrev nat`compare/< = compare/<. %abbrev nat`compare/> = compare/>. %abbrev nat`meta-eq = meta-eq. %abbrev nat`false-implies-eq = false-implies-eq. %abbrev nat`eq-symmetric = eq-symmetric. %abbrev nat`eq-transitive = eq-transitive. %abbrev nat`succ-deterministic = succ-deterministic. %abbrev nat`succ-cancels = succ-cancels. %abbrev nat`succ-contradiction = succ-contradiction. %abbrev nat`eq-contradiction = eq-contradiction. %abbrev nat`meta-gt = meta-gt. %abbrev nat`false-implies-gt = false-implies-gt. %abbrev nat`gt-respects-eq = gt-respects-eq. %abbrev nat`succ-implies-gt = succ-implies-gt. %abbrev nat`succ-implies-gt-zero = succ-implies-gt-zero. %abbrev nat`succ-preserves-gt = succ-preserves-gt. %abbrev nat`succ-preserves-gt-converse = succ-preserves-gt-converse. %abbrev nat`gt-implies-positive = gt-implies-positive. %abbrev nat`gt-anti-reflexive* = gt-anti-reflexive*. %abbrev nat`gt-anti-reflexive = gt-anti-reflexive. %abbrev nat`gt-transitive = gt-transitive. %abbrev nat`gt-anti-symmetric = gt-anti-symmetric. %abbrev nat`gt-implies-plus = gt-implies-plus. %abbrev nat`gt-contradiction = gt-contradiction. %abbrev nat`false-implies-compare = false-implies-compare. %abbrev nat`succ-preserves-compare = succ-preserves-compare. %abbrev nat`compare-total* = compare-total*. %abbrev nat`compare-total = compare-total. %abbrev nat`greater-implies-gt = greater-implies-gt. %abbrev nat`less-is-reverse-greater = less-is-reverse-greater. %abbrev nat`less-implies-lt = less-implies-lt. %abbrev nat`equal-implies-eq = equal-implies-eq. %abbrev nat`false-implies-plus = false-implies-plus. %abbrev nat`plus-respects-eq = plus-respects-eq. %abbrev nat`plus-total* = plus-total*. %abbrev nat`plus-total = plus-total. %abbrev nat`plus-deterministic = plus-deterministic. %abbrev nat`plus-left-identity = plus-left-identity. %abbrev nat`plus-left-increase = plus-left-increase. %abbrev nat`plus-right-identity = plus-right-identity. %abbrev nat`plus-right-increase = plus-right-increase. %abbrev nat`plus-left-decrease = plus-left-decrease. %abbrev nat`plus-right-decrease = plus-right-decrease. %abbrev nat`plus-swap-succ = plus-swap-succ. %abbrev nat`plus-swap-succ-converse = plus-swap-succ-converse. %abbrev nat`plus-left-preserves-positive = plus-left-preserves-positive. %abbrev nat`plus-right-preserves-positive = plus-right-preserves-positive. %abbrev nat`plus-is-zero-implies-zero = plus-is-zero-implies-zero. %abbrev nat`plus-commutative = plus-commutative. %abbrev nat`plus-associative = plus-associative. %abbrev nat`plus-associative* = plus-associative*. %abbrev nat`plus-associative-converse = plus-associative-converse. %abbrev nat`plus-associative-converse* = plus-associative-converse*. %abbrev nat`plus-assoc-commutative* = plus-assoc-commutative*. %abbrev nat`plus-assoc-commutative = plus-assoc-commutative. %abbrev nat`plus-double-associative* = plus-double-associative*. %abbrev nat`plus-double-associative = plus-double-associative. %abbrev nat`plus-left-cancels = plus-left-cancels. %abbrev nat`plus-right-cancels* = plus-right-cancels*. %abbrev nat`plus-right-cancels = plus-right-cancels. %abbrev nat`plus-left-preserves-gt* = plus-left-preserves-gt*. %abbrev nat`plus-left-cancels-gt = plus-left-cancels-gt. %abbrev nat`plus-left-preserves-gt = plus-left-preserves-gt. %abbrev nat`plus-right-preserves-gt* = plus-right-preserves-gt*. %abbrev nat`plus-right-preserves-gt = plus-right-preserves-gt. %abbrev nat`plus-preserves-gt* = plus-preserves-gt*. %abbrev nat`plus-preserves-gt = plus-preserves-gt. %abbrev nat`plus-right-cancels-gt = plus-right-cancels-gt. %abbrev nat`plus-implies-gt = plus-implies-gt. %abbrev nat`plus-gt-contradiction = plus-gt-contradiction. %abbrev nat`false-implies-times = false-implies-times. %abbrev nat`times-respects-eq = times-respects-eq. %abbrev nat`times-total* = times-total*. %abbrev nat`times-total = times-total. %abbrev nat`times-deterministic = times-deterministic. %abbrev nat`times-left-identity = times-left-identity. %abbrev nat`times-right-identity = times-right-identity. %abbrev nat`times-right-zero = times-right-zero. %abbrev nat`times-preserves-positive = times-preserves-positive. %abbrev nat`times-preserves-positive* = times-preserves-positive*. %abbrev nat`times-positive-implies-positive = times-positive-implies-positive. %abbrev nat`times-left-increase = times-left-increase. %abbrev nat`times-right-increase = times-right-increase. %abbrev nat`times-left-decrease = times-left-decrease. %abbrev nat`times-right-decrease = times-right-decrease. %abbrev nat`times-commutative = times-commutative. %abbrev nat`times-right-distributes-over-plus = times-right-distributes-over-plus. %abbrev nat`times-right-distributes-over-plus* = times-right-distributes-over-plus*. %abbrev nat`times-left-distributes-over-plus* = times-left-distributes-over-plus*. %abbrev nat`times-left-distributes-over-plus = times-left-distributes-over-plus. %abbrev nat`times-right-factors-over-plus = times-right-factors-over-plus. %abbrev nat`times-right-factors-over-plus* = times-right-factors-over-plus*. %abbrev nat`times-left-factors-over-plus = times-left-factors-over-plus. %abbrev nat`times-left-factors-over-plus* = times-left-factors-over-plus*. %abbrev nat`times-associative = times-associative. %abbrev nat`times-associative* = times-associative*. %abbrev nat`times-associative-converse = times-associative-converse. %abbrev nat`times-associative-converse* = times-associative-converse*. %abbrev nat`times-assoc-commutative* = times-assoc-commutative*. %abbrev nat`times-assoc-commutative = times-assoc-commutative. %abbrev nat`times-double-associative* = times-double-associative*. %abbrev nat`times-double-associative = times-double-associative. %abbrev nat`times-right-cancels = times-right-cancels. %abbrev nat`times-right-cancels* = times-right-cancels*. %abbrev nat`times-right-cancels** = times-right-cancels**. %abbrev nat`times-left-cancels = times-left-cancels. %abbrev nat`times-left-cancels* = times-left-cancels*. %abbrev nat`times-left-preserves-gt = times-left-preserves-gt. %abbrev nat`times-left-preserves-gt* = times-left-preserves-gt*. %abbrev nat`times-right-preserves-gt = times-right-preserves-gt. %abbrev nat`times-right-preserves-gt* = times-right-preserves-gt*. %abbrev nat`times-preserves-gt = times-preserves-gt. %abbrev nat`times-right-cancels-gt = times-right-cancels-gt. %abbrev nat`times-left-cancels-gt = times-left-cancels-gt. %abbrev nat`minus = minus. %abbrev nat`false-implies-minus = false-implies-minus. %abbrev nat`minus-respects-eq = minus-respects-eq. %abbrev nat`minus-deterministic = minus-deterministic. %abbrev nat`plus-associates-with-minus* = plus-associates-with-minus*. %abbrev nat`plus-associates-with-minus-converse* = plus-associates-with-minus-converse*. %abbrev nat`plus-associates-with-minus-converse = plus-associates-with-minus-converse. %abbrev nat`minus-associates-from-plus* = minus-associates-from-plus*. %abbrev nat`minus-associates-from-plus-converse* = minus-associates-from-plus-converse*. %abbrev nat`minus-associates-to-plus* = minus-associates-to-plus*. %abbrev nat`minus-associates-to-plus = minus-associates-to-plus. %abbrev nat`minus-associates-to-plus-converse* = minus-associates-to-plus-converse*. %abbrev nat`minus-associates-to-plus-converse = minus-associates-to-plus-converse. %abbrev nat`minus-is-zero-implies-eq = minus-is-zero-implies-eq. %abbrev nat`minus-implies-gt = minus-implies-gt. %abbrev nat`minus-left-cancels = minus-left-cancels. %abbrev nat`minus-right-cancels = minus-right-cancels. %abbrev nat`minus-left-inverts-gt* = minus-left-inverts-gt*. %abbrev nat`minus-right-preserves-gt* = minus-right-preserves-gt*. %abbrev nat`minus-left-cancels-inverts-gt = minus-left-cancels-inverts-gt. %abbrev nat`minus-right-cancels-gt = minus-right-cancels-gt. %abbrev nat`times-right-distributes-over-minus = times-right-distributes-over-minus. %abbrev nat`times-right-distributes-over-minus* = times-right-distributes-over-minus*. %abbrev nat`times-left-distributes-over-minus* = times-left-distributes-over-minus*. %abbrev nat`times-left-distributes-over-minus = times-left-distributes-over-minus. %abbrev nat`times-right-factors-over-minus* = times-right-factors-over-minus*. %abbrev nat`times-left-factors-over-minus* = times-left-factors-over-minus*. %abbrev nat`times-right-factors-over-minus = times-right-factors-over-minus. %abbrev nat`times-left-factors-over-minus = times-left-factors-over-minus. %abbrev nat`ge = ge. %abbrev nat`ge/= = ge/=. %abbrev nat`ge/> = ge/>. %abbrev nat`false-implies-ge = false-implies-ge. %abbrev nat`ge-respects-eq = ge-respects-eq. %abbrev nat`ge-reflexive = ge-reflexive. %abbrev nat`ge-transitive = ge-transitive. %abbrev nat`ge-anti-symmetric = ge-anti-symmetric. %abbrev nat`ge-transitive-gt = ge-transitive-gt. %abbrev nat`gt-transitive-ge = gt-transitive-ge. %abbrev nat`meta-ge = meta-ge. %abbrev nat`succ-preserves-ge = succ-preserves-ge. %abbrev nat`succ-preserves-ge-converse = succ-preserves-ge-converse. %abbrev nat`ge-succ-implies-gt = ge-succ-implies-gt. %abbrev nat`ge-implies-succ-gt = ge-implies-succ-gt. %abbrev nat`succ-gt-implies-ge = succ-gt-implies-ge. %abbrev nat`gt-implies-ge-succ = gt-implies-ge-succ. %abbrev nat`ge-implies-plus = ge-implies-plus. %abbrev nat`plus-implies-ge = plus-implies-ge. %abbrev nat`ge-zero-always = ge-zero-always. %abbrev nat`nonzero-times-implies-ge = nonzero-times-implies-ge. %abbrev nat`times-nonzero-implies-ge = times-nonzero-implies-ge. %abbrev nat`non-trivial-times-implies-much-gt* = non-trivial-times-implies-much-gt*. %abbrev nat`non-trivial-times-implies-much-gt = non-trivial-times-implies-much-gt. %abbrev nat`plus-left-preserves-ge* = plus-left-preserves-ge*. %abbrev nat`plus-left-cancels-ge = plus-left-cancels-ge. %abbrev nat`plus-left-preserves-ge = plus-left-preserves-ge. %abbrev nat`plus-right-preserves-ge* = plus-right-preserves-ge*. %abbrev nat`plus-right-preserves-ge = plus-right-preserves-ge. %abbrev nat`plus-preserves-ge* = plus-preserves-ge*. %abbrev nat`plus-preserves-ge = plus-preserves-ge. %abbrev nat`plus-right-cancels-ge = plus-right-cancels-ge. %abbrev nat`times-left-preserves-ge* = times-left-preserves-ge*. %abbrev nat`times-left-preserves-ge = times-left-preserves-ge. %abbrev nat`times-right-preserves-ge* = times-right-preserves-ge*. %abbrev nat`times-right-preserves-ge = times-right-preserves-ge. %abbrev nat`ne = ne. %abbrev nat`ne/< = ne/<. %abbrev nat`ne/> = ne/>. %abbrev nat`eq? = eq?. %abbrev nat`eq?/yes = eq?/yes. %abbrev nat`eq?/no = eq?/no. %abbrev nat`false-implies-ne = false-implies-ne. %abbrev nat`ne-respects-eq = ne-respects-eq. %abbrev nat`ne-anti-reflexive = ne-anti-reflexive. %abbrev nat`ne-symmetric = ne-symmetric. %abbrev nat`eq-ne-implies-false = eq-ne-implies-false. %abbrev nat`ge-ne-implies-gt = ge-ne-implies-gt. %abbrev nat`eq?-total* = eq?-total*. %abbrev nat`eq?-total*/L = eq?-total*/L. %abbrev nat`eq?-total = eq?-total. %abbrev nat`succ-preserves-ne = succ-preserves-ne. %abbrev nat`succ-preserves-ne-converse = succ-preserves-ne-converse. %abbrev nat`plus-left-preserves-ne* = plus-left-preserves-ne*. %abbrev nat`plus-left-cancels-ne = plus-left-cancels-ne. %abbrev nat`plus-left-preserves-ne = plus-left-preserves-ne. %abbrev nat`plus-right-preserves-ne* = plus-right-preserves-ne*. %abbrev nat`plus-right-preserves-ne = plus-right-preserves-ne. %abbrev nat`plus-right-cancels-ne = plus-right-cancels-ne. %abbrev nat`lt = lt. %abbrev nat`false-implies-lt = false-implies-lt. %abbrev nat`lt-respects-eq = lt-respects-eq. %abbrev nat`lt-anti-symmetric = lt-anti-symmetric. %abbrev nat`lt-transitive = lt-transitive. %abbrev nat`lt-anti-reflexive = lt-anti-reflexive. %abbrev nat`plus-left-preserves-lt* = plus-left-preserves-lt*. %abbrev nat`plus-left-cancels-lt = plus-left-cancels-lt. %abbrev nat`plus-left-preserves-lt = plus-left-preserves-lt. %abbrev nat`plus-right-preserves-lt* = plus-right-preserves-lt*. %abbrev nat`plus-right-preserves-lt = plus-right-preserves-lt. %abbrev nat`plus-preserves-lt* = plus-preserves-lt*. %abbrev nat`plus-preserves-lt = plus-preserves-lt. %abbrev nat`plus-right-cancels-lt = plus-right-cancels-lt. %abbrev nat`le = le. %abbrev nat`false-implies-le = false-implies-le. %abbrev nat`le-respects-eq = le-respects-eq. %abbrev nat`le-anti-symmetric = le-anti-symmetric. %abbrev nat`le-transitive = le-transitive. %abbrev nat`le-reflexive = le-reflexive. %abbrev nat`le-transitive-lt = le-transitive-lt. %abbrev nat`lt-transitive-le = lt-transitive-le. %abbrev nat`plus-left-preserves-le* = plus-left-preserves-le*. %abbrev nat`plus-left-cancels-le = plus-left-cancels-le. %abbrev nat`plus-left-preserves-le = plus-left-preserves-le. %abbrev nat`plus-right-preserves-le* = plus-right-preserves-le*. %abbrev nat`plus-right-preserves-le = plus-right-preserves-le. %abbrev nat`plus-preserves-le* = plus-preserves-le*. %abbrev nat`plus-preserves-le = plus-preserves-le. %abbrev nat`plus-right-cancels-le = plus-right-cancels-le. %abbrev nat`times-left-preserves-le* = times-left-preserves-le*. %abbrev nat`times-left-preserves-le = times-left-preserves-le. %abbrev nat`times-right-preserves-le* = times-right-preserves-le*. %abbrev nat`times-right-preserves-le = times-right-preserves-le. %abbrev nat`times-preserves-le* = times-preserves-le*. %abbrev nat`times-preserves-le = times-preserves-le. %abbrev nat`minus-left-inverts-ge* = minus-left-inverts-ge*. %abbrev nat`minus-right-preserves-ge* = minus-right-preserves-ge*. %abbrev nat`minus-left-cancels-inverts-ge = minus-left-cancels-inverts-ge. %abbrev nat`minus-right-cancels-ge = minus-right-cancels-ge. %abbrev nat`minus-left-preserves-ne* = minus-left-preserves-ne*. %abbrev nat`minus-right-preserves-ne* = minus-right-preserves-ne*. %abbrev nat`minus-left-cancels-ne = minus-left-cancels-ne. %abbrev nat`minus-right-cancels-ne = minus-right-cancels-ne. %abbrev nat`minus-left-inverts-lt* = minus-left-inverts-lt*. %abbrev nat`minus-right-preserves-lt* = minus-right-preserves-lt*. %abbrev nat`minus-left-cancels-inverts-lt = minus-left-cancels-inverts-lt. %abbrev nat`minus-right-cancels-lt = minus-right-cancels-lt. %abbrev nat`minus-left-inverts-le* = minus-left-inverts-le*. %abbrev nat`minus-right-preserves-le* = minus-right-preserves-le*. %abbrev nat`minus-left-cancels-inverts-le = minus-left-cancels-inverts-le. %abbrev nat`minus-right-cancels-le = minus-right-cancels-le. %abbrev nat`divrem = divrem. %abbrev nat`divrem/z = divrem/z. %abbrev nat`divrem/s = divrem/s. %abbrev nat`false-implies-divrem = false-implies-divrem. %abbrev nat`divrem-respects-eq = divrem-respects-eq. %abbrev nat`divrem-total** = divrem-total**. %abbrev nat`divrem-total* = divrem-total*. %abbrev nat`divrem-total = divrem-total. %abbrev nat`divrem-deterministic = divrem-deterministic. %abbrev nat`divrem-implies-positive = divrem-implies-positive. %abbrev nat`divrem-implies-gt = divrem-implies-gt. %abbrev nat`divrem-contradiction = divrem-contradiction. %abbrev nat`divrem-can-be-inverted = divrem-can-be-inverted. %abbrev nat`div-can-be-inverted = div-can-be-inverted. %abbrev nat`divrem-can-be-constructed = divrem-can-be-constructed. %abbrev nat`div-can-be-constructed = div-can-be-constructed. %abbrev nat`remainder-implies-gt-quotient = remainder-implies-gt-quotient. %abbrev nat`quotient-of-nonzero-is-smaller = quotient-of-nonzero-is-smaller. %abbrev nat`quotient-is-no-greater = quotient-is-no-greater. %abbrev nat`min = min. %abbrev nat`min/= = min/=. %abbrev nat`min/> = min/>. %abbrev nat`min/< = min/<. %abbrev nat`max = max. %abbrev nat`max/= = max/=. %abbrev nat`max/> = max/>. %abbrev nat`max/< = max/<. %abbrev nat`false-implies-min = false-implies-min. %abbrev nat`min-respects-eq = min-respects-eq. %abbrev nat`min-total** = min-total**. %abbrev nat`min-total* = min-total*. %abbrev nat`min-total = min-total. %abbrev nat`min-deterministic = min-deterministic. %abbrev nat`min-commutative = min-commutative. %abbrev nat`ge-implies-min = ge-implies-min. %abbrev nat`le-implies-min = le-implies-min. %abbrev nat`min-implies-ge = min-implies-ge. %abbrev nat`min-left-preserves-ge* = min-left-preserves-ge*. %abbrev nat`min-left-preserves-le* = min-left-preserves-le*. %abbrev nat`min-left-preserves-ge = min-left-preserves-ge. %abbrev nat`min-right-preserves-ge* = min-right-preserves-ge*. %abbrev nat`min-right-preserves-ge = min-right-preserves-ge. %abbrev nat`min-preserves-ge* = min-preserves-ge*. %abbrev nat`min-preserves-ge = min-preserves-ge. %abbrev nat`min-left-preserves-le = min-left-preserves-le. %abbrev nat`min-right-preserves-le* = min-right-preserves-le*. %abbrev nat`min-right-preserves-le = min-right-preserves-le. %abbrev nat`min-preserves-le* = min-preserves-le*. %abbrev nat`min-preserves-le = min-preserves-le. %abbrev nat`min-is-glb = min-is-glb. %abbrev nat`min-associative = min-associative. %abbrev nat`min-associative* = min-associative*. %abbrev nat`min-associative-converse = min-associative-converse. %abbrev nat`min-associative-converse* = min-associative-converse*. %abbrev nat`min-assoc-commutative* = min-assoc-commutative*. %abbrev nat`min-assoc-commutative = min-assoc-commutative. %abbrev nat`min-double-associative* = min-double-associative*. %abbrev nat`min-double-associative = min-double-associative. %abbrev nat`false-implies-max = false-implies-max. %abbrev nat`max-respects-eq = max-respects-eq. %abbrev nat`max-total** = max-total**. %abbrev nat`max-total* = max-total*. %abbrev nat`max-total = max-total. %abbrev nat`max-deterministic = max-deterministic. %abbrev nat`max-commutative = max-commutative. %abbrev nat`ge-implies-max = ge-implies-max. %abbrev nat`le-implies-max = le-implies-max. %abbrev nat`max-implies-ge = max-implies-ge. %abbrev nat`max-is-lub = max-is-lub. %abbrev nat`max-left-preserves-ge* = max-left-preserves-ge*. %abbrev nat`max-left-preserves-le* = max-left-preserves-le*. %abbrev nat`max-left-preserves-ge = max-left-preserves-ge. %abbrev nat`max-right-preserves-ge* = max-right-preserves-ge*. %abbrev nat`max-right-preserves-ge = max-right-preserves-ge. %abbrev nat`max-preserves-ge* = max-preserves-ge*. %abbrev nat`max-preserves-ge = max-preserves-ge. %abbrev nat`max-left-preserves-le = max-left-preserves-le. %abbrev nat`max-right-preserves-le* = max-right-preserves-le*. %abbrev nat`max-right-preserves-le = max-right-preserves-le. %abbrev nat`max-preserves-le* = max-preserves-le*. %abbrev nat`max-preserves-le = max-preserves-le. %abbrev nat`max-associative = max-associative. %abbrev nat`max-associative* = max-associative*. %abbrev nat`max-associative-converse = max-associative-converse. %abbrev nat`max-associative-converse* = max-associative-converse*. %abbrev nat`max-assoc-commutative* = max-assoc-commutative*. %abbrev nat`max-assoc-commutative = max-assoc-commutative. %abbrev nat`max-double-associative* = max-double-associative*. %abbrev nat`max-double-associative = max-double-associative. %abbrev nat`min-right-distributes-over-max = min-right-distributes-over-max. %abbrev nat`max-right-distributes-over-min = max-right-distributes-over-min. %abbrev nat`min-right-distributes-over-max* = min-right-distributes-over-max*. %abbrev nat`min-left-distributes-over-max* = min-left-distributes-over-max*. %abbrev nat`min-left-distributes-over-max = min-left-distributes-over-max. %abbrev nat`min-right-factors-over-max = min-right-factors-over-max. %abbrev nat`min-right-factors-over-max* = min-right-factors-over-max*. %abbrev nat`min-left-factors-over-max = min-left-factors-over-max. %abbrev nat`min-left-factors-over-max* = min-left-factors-over-max*. %abbrev nat`max-right-distributes-over-min* = max-right-distributes-over-min*. %abbrev nat`max-left-distributes-over-min* = max-left-distributes-over-min*. %abbrev nat`max-left-distributes-over-min = max-left-distributes-over-min. %abbrev nat`max-right-factors-over-min = max-right-factors-over-min. %abbrev nat`max-right-factors-over-min* = max-right-factors-over-min*. %abbrev nat`max-left-factors-over-min = max-left-factors-over-min. %abbrev nat`max-left-factors-over-min* = max-left-factors-over-min*.