# Building up theorems of peano arithmetic. ## redirect peano_thms.gh param (PROP /peano/prop.ghi () "") param (PEANO_MIN /peano/peano_min.ghi (PROP) "") param (PEANO /peano/peano_ax.ghi (PROP PEANO_MIN) "") param (NAIVE_SET /peano/naive_set.ghi (PROP PEANO_MIN PEANO) "") tvar (wff ph ps ch th ta) tvar (nat A B C D A' B' C' D' A0 A1 A2 A3 i j k) var (nat v w x y z v' w' x' y' z') tvar (set S T U V S0 S1 S2 S3 S4 S5 S6 S7 S8 S9) tvar (wff zi si) term (nat (mod A B)) term (nat (div A B)) term (wff (| A B)) term (wff (>= A B)) term (wff (> A B)) term (nat (exp A B)) term (nat (! A)) term (nat (.- A B)) term (wff (prime A)) term (set ({...} A B)) term (set (lambda y A)) term (nat (apply S A)) term (nat (sum A B S)) term (nat (product A B S)) term (nat (head A)) term (nat (tail A)) term (nat (<,> A B)) term (nat (fibonacci A)) term (nat (tri A)) term (nat (ifn ph A B)) term (wff (=mod A B C)) term (nat (2)) term (nat (3)) term (nat (4)) term (nat (5)) term (nat (6)) term (nat (7)) term (nat (8)) term (nat (9)) term (nat (10)) # == Pure predicate calculus == stmt (a4i () ((A. x ph)) ph) stmt (mpg () ((-> (A. x ph) ps) ph) ps ) stmt (19.3 ((ph x)) () (<-> (A. x ph) ph) ) # aka 19.7 stmt (alnex () () (<-> (A. x (-. ph)) (-. (E. x ph))) ) stmt (19.8a () () (-> ph (E. x ph)) ) stmt (19.8ai () (ph) (E. x ph)) stmt (19.2 () () (-> (A. x ph) (E. x ph)) ) stmt (19.9 ((ph x)) () (<-> (E. x ph) ph) ) stmt (19.9d ((ps x)) ((-> ph (E. x ps))) (-> ph ps)) stmt (19.15 () () (-> (A. x (<-> ph ps)) (<-> (A. x ph) (A. x ps)))) stmt (19.15i () ((A. x (<-> ph ps))) (<-> (A. x ph) (A. x ps)) ) stmt (19.15d () ((-> ph (A. x (<-> ps ch)))) (-> ph (<-> (A. x ps) (A. x ch))) ) ## Equivalence over Quantification ## ## (<-> [ ph ] [ ps ] ) ## (<-> (A. x [ ph ] ) (A. x [ ps ] )) ##
stmt (albii () ((<-> ph ps)) (<-> (A. x ph) (A. x ps)) ) ## Equivalence over Quantification ## ## (A. x [ ph ] ) ## (<-> [ ph ] [ ps ] ) ## (A. x [ [ [ ps ] ) ##
stmt (albiii () ((A. x ph) (<-> ph ps)) (A. x ps) ) ## Equivalence over Quantification ## ## (<-> [ ph ] [ ps ] ) ## (<-> (E. x [ ph ] ) (E. x [ ps ] )) ##
stmt (exbii () ((<-> ph ps)) (<-> (E. x ph) (E. x ps)) ) ## Equivalence over Quantification ## ## (E. x [ ph ] ) ## (<-> [ ph ] [ ps ] ) ## (E. x [ [ [ ps ] ) ##
stmt (exbiii () ((E. x ph) (<-> ph ps)) (E. x ps) ) # aka 19.6 ## Definition of ∃ ## right('Equivalence', '∃') stmt (alex () () (<-> (A. x ph) (-. (E. x (-. ph)))) ) stmt (19.20i () ((-> ph ps)) (-> (A. x ph) (A. x ps)) ) stmt (19.21 ((ph x)) () (<-> (A. x (-> ph ps)) (-> ph (A. x ps))) ) stmt (19.21ai ((ph x)) ((-> ph ps)) (-> ph (A. x ps)) ) stmt (19.5 () () (<-> (A. x (A. y ph)) (A. y (A. x ph))) ) stmt (19.22 () () (-> (A. x (-> ph ps)) (-> (E. x ph) (E. x ps))) ) stmt (19.22i () ((-> ph ps)) (-> (E. x ph) (E. x ps)) ) stmt (19.22d ((ph x)) ((-> ph (-> ps ch))) (-> ph (-> (E. x ps) (E. x ch))) ) stmt (19.18 () () (-> (A. x (<-> ph ps)) (<-> (E. x ph) (E. x ps))) ) stmt (exbid ((ph x)) ((-> ph (<-> ps ch))) (-> ph (<-> (E. x ps) (E. x ch))) ) ## Additive Identity ## auto-right('Simplify', '0') stmt (pa_ax3r () () (= (+ (0) A) A)) ## Definition of 2 stmt (df-2 () () (= (2) (+ (1) (1)))) ## Definition of 3 stmt (df-3 () () (= (3) (+ (2) (1)))) ## Definition of 4 stmt (df-4 () () (= (4) (+ (3) (1)))) ## Definition of 5 stmt (df-5 () () (= (5) (+ (4) (1)))) ## Definition of 6 stmt (df-6 () () (= (6) (+ (5) (1)))) ## Definition of 7 stmt (df-7 () () (= (7) (+ (6) (1)))) ## Definition of 8 stmt (df-8 () () (= (8) (+ (7) (1)))) ## Definition of 9 stmt (df-9 () () (= (9) (+ (8) (1)))) ## Definition of 10 stmt (df-10 () () (= (10) (+ (9) (1)))) ## Reflexive Property stmt (eqid () () (= A A)) ## Multiplicative Identity ## right('Simplify', '1') ## ## (= (* A (1)) A) ##
## auto-right('Simplify') stmt (mulid () () (= (* A (1)) A)) ## Multiplicative Identity ## auto-right('Simplify', '1') stmt (mulidr() () (= (* (1) A) A)) ## No Natural Numbers Below Zero stmt (0le () () (<= (0) A)) ## No Natural Numbers Below Zero stmt (ge0 () () (>= A (0))) ## Inequality Conversion ## left('Simplify', '<') stmt (axlttri2 () () (<-> (< A B) (/\ (-. (= A B)) (<= A B)))) ## Inequality Conversion ## left('Simplify', '>') stmt (axgrtri () () (<-> (> A B) (/\ (-. (= A B)) (>= A B)))) ## Inequality over Addition ## ## (-. (= [ A ] [ [ B )) ## (-. (= (+ C [ A ] ) (+ [ C [ B))) ##
stmt (addneq2i () ((-. (= A B))) (-. (= (+ C A) (+ C B)))) ## Addition is Monotonic ## Addition is strictly monotonic in the first addend ## left('Cancel', '+') stmt (leadd1 () () (<-> (<= A B) (<= (+ A C) (+ B C)))) ## Addition is Monotonic ## Addition is strictly monotonic in the second addend ## left('Cancel', '+') ## ## (<-> (<= A B) (<= (+ C A) (+ C B))) ##
stmt (leadd2 () () (<-> (<= A B) (<= (+ C A) (+ C B)))) ## Addition Over Inequality ## ## (<= A ] [ B ] ) ## (<= (+ A ] C) (+ [ B ] C)) ##
stmt (leadd1i () ((<= A B)) (<= (+ A C) (+ B C))) ## Addition Over Inequality ## ## (<= [ A ] [ B ) ## (<= (+ C [ A ] ) (+ C [ B )) ##
stmt (leadd2i () ((<= A B)) (<= (+ C A) (+ C B))) ## Inequality Over Addition ## ## (< A ] [ B ] ) ## (< (+ A ] C) (+ [ B ] C)) ##
stmt (ltadd1i () ((< A B)) (< (+ A C) (+ B C))) ## Inequality Over Addition ## ## (< [ A ] [ B ) ## (< (+ C [ A ] ) (+ C [ B )) ##
stmt (ltadd2i () ((< A B)) (< (+ C A) (+ C B))) ## Addition is Monotonic ## left('Cancel', '+') stmt (ltadd1 () () (<-> (< A B) (< (+ A C) (+ B C)))) ## Addition is Monotonic ## left('Cancel', '+') stmt (ltadd2 () () (<-> (< A B) (< (+ C A) (+ C B)))) ## Inequality relation for two equal sums stmt (ltadd12 () () (-> (= (+ A B) (+ C D)) (<-> (< A C) (< D B)))) ## Transitive Property ## right('Simplify', '≤ ≤') stmt (letr () () (-> (/\ (<= A B) (<= B C)) (<= A C))) ## Combine Inequalities stmt (letradd () () (-> (/\ (<= A B) (<= C D)) (<= (+ A C) (+ B D)))) ## Combine Inequalities stmt (lttradd () () (-> (/\ (< A B) (< C D)) (< (+ A C) (+ B D)))) ## Combine Inequalities stmt (lelttradd () () (-> (/\ (<= A B) (< C D)) (< (+ A C) (+ B D)))) ## Addition Over Inequality ## ## (> A ] [ B ] ) ## (> (+ A ] C) (+ [ B ] C)) ##
stmt (gtadd1i () ((> A B)) (> (+ A C) (+ B C))) ## Addition Over Inequality ## ## (> A ] [ B ] ) ## (> (+ A ] C) (+ [ B ] C)) ##
stmt (gtadd2i () ((> A B)) (> (+ C A) (+ C B))) ## Addition Over Inequality ## ## (>= A ] [ B ] ) ## (>= (+ A ] C) (+ [ B ] C)) ##
stmt (geadd1i () ((>= A B)) (>= (+ A C) (+ B C))) ## Addition Over Inequality ## ## (>= [ A ] [ B ) ## (>= (+ C [ A ] ) (+ C [ B )) ##
stmt (geadd2i () ((>= A B)) (>= (+ C A) (+ C B))) ## Multiply by 0 ## auto-right('Simplify','0') stmt (pa_ax5r () () (= (* (0) A) (0))) # Successor is equivalent to adding one ## Successor Adds One ## right('Equivalence', '+1') stmt (a1suc () () (= (S A) (+ A (1)))) # Reverse the hypothesis and conclusion of con4bii. ## Equivalence over Negation ## ## (<-> [ ph ] [ ps ] ) ## (<-> (-. [ ph ] ) (-. [ ps ] )) ##
stmt (con4biir () ((<-> ph ps)) (<-> (-. ph) (-. ps)) ) # Reorder sylbi a bit. ## Syllogism ## ## (-> ps ] ] ] ch) ## (<-> ps ] [ ph ] ) ## (-> [ [ ph ] ch) ##
stmt (sylbi2() ((-> ps ch) (<-> ps ph)) (-> ph ch) ) # Commute the conclusion of bitr3i. ## Transitive Property ## ## (<-> ps [ [ [ ph ] ) ## (<-> ps [ ch ] ] ] ) ## [ (<-> ch ] [ ph ] ) ##
stmt (bitr3icom() ((<-> ps ph) (<-> ps ch)) (<-> ch ph) ) ## Equivalence over Disjunction ## ## (\/ ph ] ] ] ps) ## (<-> ph ] [ ch ] ) ## (\/ [ [ ch ] ps) ##
stmt (orbi1ii () ((\/ ph ps) (<-> ph ch)) (\/ ch ps) ) ## Equivalence over Disjunction ## ## (\/ ph [ ps ] ] ] ) ## (<-> [ ps ] [ ch ] ) ## (\/ ph [ [ [ ch ] ) ##
stmt (orbi2ii () ((\/ ph ps) (<-> ps ch)) (\/ ph ch) ) ## Equivalence over Conjunction ## ## (/\ ph ] ] ] ps) ## (<-> ph ] [ ch ] ) ## (\/ [ [ ch ] ps) ##
stmt (anbi1ii () ((/\ ph ps) (<-> ph ch)) (/\ ch ps) ) ## Equivalence over Conjunction ## ## (/\ ph [ ps ] ] ] ) ## (<-> [ ps ] [ ch ] ) ## (/\ ph [ [ [ ch ] ) ##
stmt (anbi2ii () ((/\ ph ps) (<-> ps ch)) (/\ ph ch) ) ## Associative Property stmt (orassi () ((\/ (\/ ph ps) ch)) (\/ ph (\/ ps ch)) ) ## Associative Property stmt (orassli () ((\/ ph (\/ ps ch))) (\/ (\/ ph ps) ch) ) ## Associative Property stmt (anassi () ((/\ (/\ ph ps) ch)) (/\ ph (/\ ps ch)) ) ## Associative Property stmt (anassli () ((/\ ph (/\ ps ch))) (/\ (/\ ph ps) ch) ) ## Associative Property stmt (biassi () ((<-> (<-> ph ps) ch)) (<-> ph (<-> ps ch)) ) ## Associative Property stmt (biassli () ((<-> ph (<-> ps ch))) (<-> (<-> ph ps) ch) ) ## Associative Property ## right('Associate', 'R') left('Associate', 'L') stmt (addass () () (= (+ (+ A B) C) (+ A (+ B C))) ) ## Associative Property ## right('Associate', 'R') left('Associate', 'L') stmt (mulass () () (= (* (* A B) C) (* A (* B C))) ) ## Commute Conjunction ## ## (/\ ph ps) ## (/\ ps ph) ##
stmt (ancomi () ((/\ ph ps)) (/\ ps ph) ) ## Commute Disjunction ## ## (\/ ph ps) ## (\/ ps ph) ##
stmt (orcomi () ((\/ ph ps)) (\/ ps ph) ) term (wff (T)) term (wff (F)) ## T is true stmt (tru () () (T)) ## F is false stmt (notfal () () (-. (F))) ## Remove Implies ## ## [ ph ] ## (<-> (-> [ ph ] ps) ps) ##
stmt (impRemove1 () (ph) (<-> (-> ph ps) ps)) ## Remove Implies ## ## [ ph ] ## (<-> (-> ps [ ph ] ) (T)) ##
stmt (impRemove2 () (ph) (<-> (-> ps ph) (T))) ## Remove Implies ## ## [ (-. [ ph ] ) ## (<-> (-> [ [ ph ] ps) (T)) ##
stmt (impNotRemove1 () ((-. ph)) (<-> (-> ph ps) (T))) ## Remove Equivalence ## ## [ (-. [ ph ] ) ## (<-> (-> ps [ [ ph ] ) (-. ps)) ##
stmt (impNotRemove2 () ((-. ph)) (<-> (-> ps ph) (-. ps))) ## Remove Equivalence ## ## [ ph ] ## (<-> (<-> [ ph ] ps) ps) ##
stmt (biRemove1 () (ph) (<-> (<-> ph ps) ps)) ## Remove Equivalence ## ## [ ph ] ## (<-> (<-> ps [ ph ] ) ps) ##
stmt (biRemove2 () (ph) (<-> (<-> ps ph) ps)) ## Remove Equivalence ## ## [ (-. [ ph ] ) ## (<-> (<-> ps [ [ ph ] ) (-. ps)) ##
stmt (biNotRemove2 () ((-. ph)) (<-> (<-> ps ph) (-. ps))) ## Remove Equivalence ## ## [ (-. [ ph ] ) ## (<-> (<-> [ [ ph ] ps) ps) ##
stmt (biNotRemove1 () ((-. ph)) (<-> (<-> ph ps) (-. ps))) ## Remove AND ## ## [ ph ] ## (<-> (/\ [ ph ] ps) ps) ##
stmt (anRemove1 () (ph) (<-> (/\ ph ps) ps)) ## Remove AND ## ## [ ph ] ## (<-> (/\ ps [ ph ] ) ps) ##
stmt (anRemove2 () (ph) (<-> (/\ ps ph) ps)) ## Remove AND ## ## [ (-. [ ph ] ) ## (<-> (/\ [ [ ph ] ps) (F)) ##
stmt (anNotRemove1 () ((-. ph)) (<-> (/\ ph ps) (F))) ## Remove AND ## ## [ (-. [ ph ] ) ## (<-> (/\ ps [ [ ph ] ) (F)) ##
stmt (anNotRemove2 () ((-. ph)) (<-> (/\ ps ph) (F))) ## Remove OR ## ## [ ph ] ## (<-> (\/ [ ph ] ps) (T)) ##
stmt (orRemove1 () (ph) (<-> (\/ ph ps) (T))) ## Remove OR ## ## [ ph ] ## (<-> (\/ ps [ ph ] ) (T)) ##
stmt (orRemove2 () (ph) (<-> (\/ ps ph) (T))) ## Remove OR ## ## [ (-. [ ph ] ) ## (<-> (\/ [ [ ph ] ps) ps) ##
stmt (orNotRemove1 () ((-. ph)) (<-> (\/ ph ps) ps)) ## Remove OR ## ## [ (-. [ ph ] ) ## (<-> (\/ ps [ [ ph ] ) ps) ##
stmt (orNotRemove2 () ((-. ph)) (<-> (\/ ps ph) ps)) # ax-mp with the order of the first and second hypotheses reversed. ## Modus Ponens ## ## (-> ph ] [ ps) ## ph ] ] ## [ [ ps ##
stmt (ax-mpRemove () ((-> ph ps) ph ) ps) # mto with the order of the first and second hypotheses reversed. ## Modus Tollens ## ## (-> [ ph ] [ [ ps) ## [ [ [ (-. [ ps) ## (-. [ ph ] ) ] ] ##
stmt (mtoRemove () ((-> ph ps) (-. ps)) (-. ph)) # mpbi with the order of the first and second hypotheses reversed. ## Modus Ponens ## ## (<-> ph ] [ ps ] ) ## ph ] ] ] ## [ [ ps ] ##
stmt (mpbiRemove () ((<-> ph ps) ph ) ps) # mpbir with the order of the first and second hypotheses reversed. ## Modus Ponens ## ## (<-> ph ] [ ps ] ) ## [ [ ps ] ## ph ] ] ] ##
stmt (mpbirRemove () ((<-> ph ps) ps ) ph) # mtbi with the order of the first and second hypotheses reversed. ## Modus Tollens ## ## (<-> [ ph ] [ [ ps) ## [ [ [ (-. [ ps) ## (-. [ ph ] ) ] ] ##
stmt (mtbiRemove () ((<-> ph ps) (-. ph)) (-. ps)) # mtbir with the order of the first and second hypotheses reversed. ## Modus Tollens ## ## (<-> [ ph ] [ [ ps) ## [ [ (-. [ ps) ## (-. [ ph) ] ] ] ##
stmt (mtbirRemove () ((<-> ph ps) (-. ps)) (-. ph)) ## Symmetric Property ## right('Commute', '=') stmt (eqcom () () (<-> (= A B) (= B A))) ## Symmetric Property ## ## (= A B) ## (= B A) ##
stmt (eqcomi () ((= A B)) (= B A)) ## Converse of ≤ ## right('Commute', '≤') left('Commute', '≥') stmt (lecon () () (<-> (<= A B) (>= B A))) ## Converse of ≤ stmt (leconi () ((<= A B)) (>= B A)) ## Converse of ≤ ## right('Commute', '≤') left('Commute', '≥') stmt (leconold () () (<-> (<= A B) (-. (< B A)))) ## Converse of < ## right('Commute', '<') left('Commute', '>') stmt (ltcon () () (<-> (< A B) (> B A))) ## Converse of < stmt (ltconi () ((< A B)) (> B A)) ## Def. Greater Than or Equal to ## right('Define', '≤') left('Simplify', '≥') stmt (df-ge () () (<-> (>= A B) (-. (< A B)))) ## Def. Greater Than ## right('Define', '<') left('Simplify', '>') stmt (df-gt () () (<-> (> A B) (-. (<= A B)))) ## Commutative Property ## right('Commute', '+') stmt (addcom () () (= (+ A B) (+ B A))) ## Commutative Property ## ## (= (* A B) (* B A)) ##
## right('Commute', '*') stmt (mulcom () () (= (* A B) (* B A))) # Distribution of addition through multiplication ## Distributive Property ## right('Distribute', 'R') left('Distribute', '-R') stmt (distr () () (= (* A (+ B C)) (+ (* A B) (* A C)))) ## Distributive Property ## right('Distribute', 'L') left('Distribute', '-L') stmt (distl () () (= (* (+ A B) C) (+ (* A C) (* B C)))) ## Distributive Property ## ## (= (* (+ A B) (+ C D)) (+ (+ (* A C) (* B C)) (+ (* A D) (* B D)))) ##
## Distribution of addition through multiplication, both arguments ## right('Distribute', 'RL') left('Distribute', 'RL') stmt (distrl () () (= (* (+ A B) (+ C D)) (+ (+ (* A C) (* B C)) (+ (* A D) (* B D))))) ## Equivalence over Equality stmt(eqeq1 () () (-> (= A B) (<-> (= A C) (= B C)))) ## Equivalence over Equality stmt(eqeq2 () () (-> (= A B) (<-> (= C A) (= C B)))) ## Equivalence over Equality ## ## (= A ] ] [ B ] ) ## (<-> (= A ] C) ] [ (= B ] C)) ##
stmt (eqeq1i () ((= A B)) (<-> (= A C) (= B C))) ## Equivalence over Equality ## ## (= [ A ] [ [ B) ## (<-> (= C [ A) ] [ (= C [ B)) ##
stmt (eqeq2i () ((= A B)) (<-> (= C A) (= C B))) ## Equivalence over Equality ## ## (-> ph (= A ] ] [ B ] )) ## (-> ph (<-> (= A ] C) ] [ (= B ] C))) ##
stmt(eqeq1d () ((-> ph (= A B))) (-> ph (<-> (= A C) (= B C)))) ## Equivalence over Equality ## ## (-> ph (= [ A ] [ [ B)) ## (-> ph (<-> (= C [ A) ] [ (= C [ B))) ##
stmt(eqeq2d () ((-> ph (= A B))) (-> ph (<-> (= C A) (= C B)))) stmt (eqeq12 () () (-> (/\ (= A B) (= C D)) (<-> (= A C) (= B D)))) stmt (eqeq12d () ((-> ph (= A B)) (-> ph (= C D))) (-> ph (<-> (= A C) (= B D)))) ## Equivalence over Inequality ## ## (= A ] ] [ B ] ) ## (<-> (< A ] C ] ) (< [ B ] C)) ##
stmt (lteq1i () ((= A B)) (<-> (< A C) (< B C))) ## Equivalence over Inequality ## ## (= [ A ] [ [ B ] ) ## (<-> (< C [ A ] ) (< [ C [ B ] )) ##
stmt (lteq2i () ((= A B)) (<-> (< C A) (< C B))) stmt (lteq1d () ( (-> ph (= A C))) (-> ph (<-> (< A B) (< C B)))) stmt (lteq2d () ( (-> ph (= B C))) (-> ph (<-> (< A B) (< A C)))) stmt (lteq12d () ((-> ph (= A B)) (-> ph (= C D))) (-> ph (<-> (< A C) (< B D)))) ## Equality over Succession ## ## (= A ] [ B) ## (= (S A) ] [ (S B) ##
stmt (pa_ax2i () ((= A B)) (= (S A) (S B))) ## Equality over Addition ## ## (= A ] [ B ] ) ## (= (+ A ] C) (+ [ B ] C)) ##
stmt (addeq1i () ((= A B)) (= (+ A C) (+ B C))) ## Equality over Addition ## ## (= [ A ] [ B ) ## (= (+ C [ A ] ) (+ C [ B)) ##
stmt (addeq2i () ((= A B)) (= (+ C A) (+ C B))) ## Equality over Multiplication ## ## (= A ] [ B ] ) ## (= (* A ] C) (* [ B ] C)) ##
stmt (muleq1i () ((= A B)) (= (* A C) (* B C))) ## Equality over Multiplication ## ## (= [ A ] [ B ) ## (= (* C [ A ] ) (* C [ B)) ##
stmt (muleq2i () ((= A B)) (= (* C A) (* C B))) ## Transitive Property ## ## (= A [ B ] ] ) ## [ (= B ] [ C) ## (= A [ [ [ C) ##
stmt (eqtr () ((= A B) (= B C)) (= A C)) ## Transitive Property ## ## (-> ph (= A [ B ] ] )) ## (-> ph [ (= B ] [ C)) ## (-> ph (= A [ [ [ C)) ##
stmt (eqtrd () ((-> ph (= A B)) (-> ph (= B C))) (-> ph (= A C))) ## Transitive Property ## ## (= A [ [ [ B) ## (= A [ C ] ] ) ## [ (= C ] [ B ) ##
stmt (eqtr5 () ((= A B) (= A C)) (= C B)) ## Equivalence over Inequality ## ## (<= A ] ] ] [ C) ## (= A ] [ B ] ] ) ## (<= [ [ B ] [ C) ##
stmt (leeq1ii () ((<= A C) (= A B)) (<= B C)) ## Equivalence over Inequality ## ## (<= C [ A ] ] ) ## (= [ A ] [ B) ## (<= C [ [ [ B) ##
stmt (leeq2ii () ((<= C A) (= A B)) (<= C B)) ## Equivalence over Inequality ## ## (< A ] ] ] [ C) ## (= A ] [ B ] ] ) ## (< [ [ B ] [ C) ##
stmt (lteq1ii () ((< A C) (= A B)) (< B C)) ## Equivalence over Inequality ## ## (< C [ A ] ] ) ## (= [ A ] [ B) ## (< C [ [ [ B) ##
stmt (lteq2ii () ((< C A) (= A B)) (< C B)) ## Convert between inequalities stmt (axlttri2i () ((-. (= A B)) (<= A B)) (< A B)) ## Multiplication is Monotonic ## ## (< B ] ] ] [ C ] ] ) ## (< [ [ (0) ] [ [ [ A ) ## (< (* B ] [ A ] ) (* [ C ] [ A )) ##
stmt (ltmul2i () ((< B C) (< (0) A)) (< (* B A) (* C A))) stmt (ltmul () () (-> (/\ (< A B) (< C D)) (< (* A C) (* B D)))) stmt (gtmul () () (-> (/\ (> A B) (> C D)) (> (* A C) (* B D)))) stmt (ltmul4 () () (-> (/\ (< A B) (< C D)) (< (+ (* B C) (* A D)) (+ (* B D) (* A C))))) stmt (gtmul4 () () (-> (/\ (> B A) (> D C)) (> (+ (* B D) (* A C)) (+ (* B C) (* A D))))) stmt (lthalfminus () () (-> (< A B) (< (0) (.- B A)))) stmt (gthalfminus () () (-> (> B A) (> (.- B A) (0)))) ## A number is less, equal, or greater stmt (inequalities () () (\/ (< A B) (\/ (= A B) (> A B)))) stmt (emptySnIn1 () ((-. (e. A S))) (=_ (i^i ({} A) S) ({/}))) stmt (emptySnIn2 () ((-. (e. A S))) (=_ (i^i S ({} A)) ({/}))) ## Multiplication is Monotonic ## ## (> B ] ] ] [ C ] ] ) ## (> [ [ A ] [ [ [ (0) ) ## (> (+ B ] [ A ] ) (+ [ C ] [ A )) ##
stmt (gtmul2i () ((> B C) (> A (0))) (> (* B A) (* C A))) ## Modulo Value stmt (modvali () ((< C B) (= (+ (* B D) C) A)) (= (mod A B) C)) ## Combine Set Inclusions stmt (dfpssi () ((C_ S T) (-. (=_ S T))) (C. S T)) ## Sets are not equal stmt (notSeq () ((e. A S) (-. (e. A T))) (-. (=_ S T))) ## Sets are not equal stmt (notSeq2 () ((-. (e. A S)) (e. A T)) (-. (=_ S T))) ## Not a Subset stmt (notSs () ((e. A S) (-. (e. A T))) (-. (C_ S T))) ## Subset of a Union stmt (ssUnion () () (C_ S (u. S T))) ## Inequality Conversion stmt (axgrtrii () ((-. (= A B)) (>= A B)) (> A B)) stmt (divval () ((> B (0)) (= (+ (* B C) (mod A B)) A)) (= (div A B) C)) stmt (proveDivides () ((= (* A B) C)) (| A C)) stmt (notDivides () () (-> (/\ (< (* A C) B) (< B (* A (+ C (1))))) (-. (| A B)))) ## ## (e. A [ S ] ) ## (e. A (u. [ S ] U)) ##
stmt (unionAttach1 () ((e. A S)) (e. A (u. S U))) ## ## (e. A ] [ S) ## (e. A ] (u. U [ S)) ##
stmt (unionAttach2 () ((e. A S)) (e. A (u. U S))) stmt (notInSingleton () ((-. (= A B))) (-. (e. A ({} B)))) stmt (notInSingletonUnion () ((-. (= A B)) (-. (e. A S))) (-. (e. A (u. ({} B) S)))) stmt (notInSingletonUnion2 () ((-. (e. A S)) (-. (= A B)) ) (-. (e. A (u. S ({} B))))) stmt (pa_ax1plus () () (-. (= (0) (+ A (1))))) stmt (expplus1 () () (= (exp A (+ B (1))) (* A (exp A B)))) stmt (exp0 () () (= (exp A (0)) (1))) ## Exponent Right Identity stmt (expid () () (= (exp A (1)) A)) ## Union is Idempotent stmt (unidm() () (=_ (u. S S) S)) ## Union Identity stmt (unid() () (=_ (u. S ({/})) S)) ## Union Identity stmt (unidr() () (=_ (u. ({/}) S) S)) ## Intersection is Idempotent stmt (inidm() () (=_ (i^i S S) S)) ## Reflexive Property stmt (seqid () () (=_ S S)) stmt (snid () () (e. A ({} A))) ## Empty Set Contains Nothing stmt (noel () () (-. (e. A ({/})))) ## Transitive law ## right('Simplify', '<') stmt (lelttr () () (-> (/\ (<= A B) (< B C)) (< A C))) ## Transitive Inequality ## ## (< [ B ] [ [ C ] ) ## (-> (< A [ B ] ) (< [ A [ C ] )) ##
stmt (ltTrlt () ((< B C)) (-> (< A B) (< A C))) ## Transitive Inequality ## ## (< [ B ] [ [ C ] ) ## (-> (<= A [ B ] ) (< [ A [ C ] )) ##
stmt (ltTrle () ((< B C)) (-> (<= A B) (< A C))) ## Transitive Inequality ## ## (< [ B ] [ [ C ] ) ## (-> (= A [ B ] ) (< [ A [ C ] )) ##
stmt (ltTreq () ((< B C)) (-> (= A B) (< A C))) ## Transitive Inequality ## ## (<= [ B ] [ [ C ] ) ## (-> (= A [ B ] ) (<= [ A [ C ] )) ##
stmt (leTreq () ((<= B C)) (-> (= A B) (<= A C))) ## Transitive Inequality ## ## (<= [ B ] [ [ C ] ) ## (-> (= A [ B ] ) (<= [ A [ C ] )) ##
stmt (leTrlt () ((<= B C)) (-> (< A B) (< A C))) ## Transitive Inequality ## ## (<= [ B ] [ [ C ] ) ## (-> (<= A [ B ] ) (<= [ A [ C ] )) ##
stmt (leTrle () ((<= B C)) (-> (<= A B) (<= A C))) ## Transitive Inequality ## ## (-. (> [ B ] [ [ C ] )) ## (-> (> A [ B ] ) (> [ A [ C ] )) ##
stmt (gtTrgt () ((> B C)) (-> (> A B) (> A C))) ## Transitive Inequality ## ## (>= [ B ] [ [ C ] ) ## (-> (> A [ B ] ) (> [ A [ C ] )) ##
stmt (geTrgt () ((>= B C)) (-> (> A B) (> A C))) ## Transitive Inequality ## ## (>= [ B ] [ [ C ] ) ## (-> (= A [ B ] ) (>= [ A [ C ] )) ##
stmt (geTreq () ((>= B C)) (-> (= A B) (>= A C))) ## Transitive Inequality ## ## (> [ B ] [ [ C ] ) ## (-> (= A [ B ] ) (> [ A [ C ] )) ##
stmt (gtTreq () ((> B C)) (-> (= A B) (> A C))) ## Transitive Inequality ## ## (> [ B ] [ [ C ] ) ## (-> (>= A [ B ] )) (> [ A [ C ] )) ##
stmt (gtTrge () ((> B C)) (-> (>= C A) (> B A))) ## Transitive Inequality ## ## (>= [ B ] [ [ C ] ) ## (-> (>= A [ B ] ) (>= [ A [ C ] )) ##
stmt (geTrge () ((>= B C)) (-> (>= A B) (>= A C))) # This is identical to eqtr. So ideally we would use eqtr instead. ## Substitution ## ## (= A [ B ] ] ] ) ## (= [ B ] [ C ] ) ## (= A [ [ [ C ] ) ##
stmt (EqReplaceEq1 () ((= A B) (= B C)) (= A C)) ## Equivalence over Inequality ## ## (= A ] ] [ B ] ) ## (<-> (>= A ] C ] ) (>= [ B ] C)) ##
stmt (geeq1i () ( (= A C)) (<-> (>= A B) (>= C B))) ## Equivalence over Inequality ## ## (= [ A ] [ [ B ] ) ## (<-> (>= C [ A ] ) (>= [ C [ B ] )) ##
stmt (geeq2i () ((= A B)) (<-> (>= C A) (>= C B))) ## Equivalence over Inequality ## ## (= A ] ] [ B ] ) ## (<-> (> A ] C ] ) (> [ B ] C)) ##
stmt (gteq1i () ((= A C)) (<-> (> A B) (> C B))) ## Equivalence over Inequality ## ## (= [ A ] [ [ B ] ) ## (<-> (> C [ A ] ) (> [ C [ B ] )) ##
stmt (gteq2i () ((= B C)) (<-> (> A B) (> A C))) # Equality inference for the divides relation. ## Equivalence over Divides ## ## (= A ] ] [ B ] ) ## (<-> (| A ] C ] ) (< [ B ] C)) ##
stmt (divideseq1i () ((= A B)) (<-> (| A C) (| B C))) ## Equivalence over Divides ## ## (= [ A ] [ [ B ] ) ## (<-> (| C [ A ] ) (| [ C [ B ] )) ##
stmt (divideseq2i () ((= A B)) (<-> (| C A) (| C B))) ## Equality over Exponentiation stmt (expeq1i () ((= A B)) (= (exp A C) (exp B C))) ## Equality over Exponentiation stmt (expeq2i () ((= A B)) (= (exp C A) (exp C B))) stmt (expeq1d () ((-> ph (= A B))) (-> ph (= (exp A C) (exp B C)))) stmt (expeq2d () ((-> ph (= A B))) (-> ph (= (exp C A) (exp C B)))) ## Operator Conversion ## right('Infer', '≠') stmt (ltneq () () (-> (< A B) (-. (= A B)))) ## Inequality Conversion ## right('Infer', '≤') stmt (ltle () () (-> (< A B) (<= A B))) ## Inequality Conversion ## right('Infer', '≠') stmt (gtneq () () (-> (> A B) (-. (= A B)))) ## Inequality Conversion ## right('Infer', '≥') stmt (gtge () () (-> (> A B) (>= A B))) ## Equality Conversion ## right('Infer', '≤') stmt (eqle() () (-> (= A B) (<= A B))) ## Equality Conversion ## right('Infer', '≥') stmt (eqge() () (-> (= A B) (>= A B))) ## Equality Conversion ## right('Infer', '¬<') stmt (eqnlt () () (-> (= A B) (-. (< A B)))) ## Inequality Conversion ## right('Infer', '¬<') stmt (gtnlt () () (-> (> A B) (-. (< A B)))) ## Inequality Conversion ## right('Infer', '¬≤') stmt (gtnle () () (-> (> A B) (-. (<= A B)))) ## Inequality Conversion ## right('Infer', '¬>') stmt (ltngt () () (-> (< A B) (-. (> A B)))) ## Inequality Conversion ## right('Infer', '¬≥') stmt (ltnge () () (-> (< A B) (-. (>= A B)))) ## Inequality Conversion ## right('Infer', '¬>') stmt (eqngt () () (-> (= A B) (-. (> A B)))) ## Proper Subset Implies Inequality ## right('Infer', '≠') stmt (pssNeq () () (-> (C. S T) (-. (=_ S T)))) ## Proper Subset Implies Subset ## right('Infer', '⊆') stmt (pssSs () () (-> (C. S T) (C_ S T))) ## Not Subset Implies Not Proper Subset ## right('Infer', '⊄') stmt (nssNpss () () (-> (-. (C_ S T)) (-. (C. S T)))) ## Equality Implies Not Proper Subset ## right('Infer', '⊄') stmt (seqNpss () () (-> (=_ S T) (-. (C. S T)))) ## Distributive Property ## right('Distribute', 'R') left('Distribute', '-R') stmt (undi () () (=_ (u. S (i^i T U)) (i^i (u. S T) (u. S U)))) ## Distributive Property ## right('Distribute', 'L') left('Distribute', '-L') stmt (undir () () (=_ (u. (i^i T U) S) (i^i (u. T S) (u. U S)))) ## Distributive Property ## right('Distribute', 'R') left('Distribute', '-R') stmt (indi () () (=_ (i^i S (u. T U)) (u. (i^i S T) (i^i S U)))) ## Distributive Property ## right('Distribute', 'L') left('Distribute', '-L') stmt (indir () () (=_ (i^i (u. T U) S) (u. (i^i T S) (i^i U S)))) stmt (seqseq1i () ((=_ S T)) (<-> (=_ S U) (=_ T U))) stmt (seqseq2i () ((=_ S T)) (<-> (=_ U S) (=_ U T))) ## Equivalence over Subset ## ## (=_ S ] ] [ T ] ) ## (=_ (C_ S ] U) ] [ (C_ T ] U)) ##
stmt (sseq1i () ((=_ S T)) (<-> (C_ S U) (C_ T U))) stmt (sseq2i () ((=_ S T)) (<-> (C_ U S) (C_ U T))) ## Equivalence over Union ## ## (=_ S ] ] [ T ] ) ## (=_ (u. S ] U) ] [ (u. T ] U)) ##
stmt (unseq1i () ((=_ S T)) (=_ (u. S U) (u. T U))) ## Equivalence over Union ## ## (=_ [ S ] [ [ T) ## (=_ (u. U [ S) ] [ (u. U [ T)) ##
stmt (unseq2i () ((=_ S T)) (=_ (u. U S) (u. U T))) ## Equivalence over Intersection ## ## (=_ S ] ] [ T ] ) ## (=_ (i^i S ] U) ] [ (i^i T ] U)) ##
stmt (inseq1i () ((=_ S T)) (=_ (i^i S U) (i^i T U))) ## Equivalence over Intersection ## ## (=_ [ S ] [ [ T) ## (=_ (i^i U [ S) ] [ (i^i U [ T)) ##
stmt (inseq2i () ((=_ S T)) (=_ (i^i U S) (i^i U T))) ## Commutative Property ## right('Commute', '=') stmt (seqcom () () (<-> (=_ S T) (=_ T S))) ## Commutative Property of Set Equality ## ## (=_ S T) ## (=_ T S) ##
stmt (seqcomi () ((=_ S T)) (=_ T S)) ## Commutative Property ## right('Commute', '∪') stmt (uncom () () (=_ (u. S T) (u. T S))) ## Commutative Property ## right('Commute', '∩') stmt (incom () () (=_ (i^i S T) (i^i T S))) stmt (notPrime () ((| B A) (/\ (< (1) B) (< B A))) (-. (prime A))) stmt (notDividesSeti ((B x) (A x)) ((-. (| A B))) (e. A ({|} x (-. (| x B))))) stmt (unSubset () ((C_ S U) (C_ T U)) (C_ (u. S T) U)) stmt (provePrime ((A y)) ((C_ ({...} (2) A) ({|} y (-. (| y (+ A (1)))))) (> A (0))) (prime (+ A (1)))) stmt (provePrime2 ((A y)) ((C_ ({...} (2) (.- A (1))) ({|} y (-. (| y A)))) (< (1) A)) (prime A)) stmt (intervalSn () () (=_ ({...} A A) ({} A))) stmt (intervalAttach () ((<= A B)) (=_ (u. ({...} A B) ({} (+ B (1)))) ({...} A (+ B (1)))) ) ## Subset and Element Of Equivalence <title> ## <suggest> left('Simplify', '∈') right('Infer', '⊆') </suggest> stmt (elSubset () () (<-> (e. A S) (C_ ({} A) S))) stmt (primeeq () () (-> (= A B) (<-> (prime A) (prime B)))) stmt (intervaleq1 () () (-> (= A C) (=_ ({...} A B) ({...} C B)))) stmt (intervaleq2 () () (-> (= B C) (=_ ({...} A B) ({...} A C)))) ## <title> Equality over Interval ## ## (= A ] ] [ B ] ) ## (<-> ({...} A ] C ] ) ({...} [ B ] C)) ##
stmt (intervaleq2i () ((= B C)) (=_ ({...} A B) ({...} A C))) ## Equivalence over Interval ## ## (= A ] ] [ B ] ) ## (=_ ({...} A ] C ] ) ({...} [ B ] C)) ##
stmt (intervaleq1i () ((= A C)) (=_ ({...} A B) ({...} C B))) ## Equivalence over Prime ## ## (= [ A ] [ B ] ) ## (<-> (prime [ A ] ) (prime [ B ] )) ##
stmt (primeeqi () ((= A B)) (<-> (prime A) (prime B))) stmt (sneqi () ((= A B)) (=_ ({} A) ({} B))) ## Associative Property ## right('Associate', 'R') left('Associate', 'L') stmt (unass () () (=_ (u. (u. S T) U) (u. S (u. T U)))) ## Associative Property ## right('Associate', 'R') left('Associate', 'L') stmt (inass () () (=_ (i^i (i^i S T) U) (i^i S (i^i T U)))) ## Equivalence over Element Of ## ## (= A ] ] [ B ] ) ## (<-> (e. A ] S) ] [ (e. B ] S)) ##
stmt (eleq1i () ((= A B)) (<-> (e. A S) (e. B S))) ## Equivalence over Element Of ## ## (=_ [ S ] [ [ T ) ## (<-> (e. A [ S) ] [ (e. A [ T )) ##
stmt (elseq2i () ((=_ S T)) (<-> (e. A S) (e. A T))) ## Factorial of 0 stmt (factorial0 () () (= (! (0)) (1))) ## Factorial of 1 stmt (factorial1 () () (= (! (1)) (1))) ## Recursive Definition of Factorial stmt (factorialrecurse () () (= (! (+ A (1))) (* (! A) (+ A (1))))) ## Equivalence for ! ## stmt (factorialeq () () (-> (= A B) (= (! A) (! B)))) ## Equivalence for ! ## stmt (factorialeqi () ((= A B)) (= (! A) (! B))) ## Equivalence for ! ## stmt (factorialeqd () ((-> ph (= A B))) (-> ph (= (! A) (! B)))) ## Addition & Subtraction Equivalence stmt (addhalfminusi () ((= C (+ A B))) (= (.- C A) B)) ## Half-minus Never Goes Negative </suggest> stmt (halfminus-negi () ((<= A B)) (= (.- A B) (0))) ## <title> Commute Half Minus ## ## (= (.- (.- A B) C) (.- (.- A C) B)) ##
stmt (halfminuscom () () (= (.- (.- A B) C) (.- (.- A C) B))) ## Minus is the inverse of addition stmt (halfminus () () (-> (<= B A) (= (+ (.- A B) B) A))) ## Half minus cancellation ## right('Simplify', '-') ## ## (= (.- (+ A B) B) A) ##
stmt (halfminuscan () () (= (.- (+ A B) B) A)) ## Distributive Property ## right('Distribute', 'R') left('Distribute', '-R') stmt (halfminusdist () () (= (* A (.- B C)) (.- (* A B) (* A C)))) ## Distributive Property ## right('Distribute', 'L') left('Distribute', '-L') stmt (halfminusdist2 () () (= (* (.- B C) A) (.- (* B A) (* C A)))) ## Apply the identity function stmt (applyfunid ((A x)) () (= (apply (lambda x x) A) A)) ## Apply a constant function stmt (applylambdaconst ((A x) (B x)) () (= (apply (lambda x A) B) A)) ## Apply the function stmt (applylambda ((D x) (A x) (C x) (B y)) ((-> (= x y) (= B D)) (-> (= x A) (= B C))) (= (apply (lambda x B) A) C)) ## Multiply a sequence of One Number stmt (product1 () () (= (product A A S) (apply S A))) ## Detach the last number in a product stmt (productdetachi () ((< A B)) (= (product A B S) (* (product A (.- B (1)) S) (apply S B)))) ## Sum a sequence of One Number stmt (sum1 () () (= (sum A A S) (apply S A))) ## Detach the Last Number in a sum stmt (sumdetachi () ((< A B)) (= (sum A B S) (+ (sum A (.- B (1)) S) (apply S B)))) ## Add a number to both sides of an equation ## ## (-> (= A B) (= (+ A C) (+ B C))) ##
stmt (addeq1 () () (-> (= A B) (= (+ A C) (+ B C)))) ## Add a number to both sides of an equation stmt (addeq2 () () (-> (= A B) (= (+ C A) (+ C B)))) ## Equality over Addition stmt (addeq1d () ((-> ph (= A B))) (-> ph (= (+ A C) (+ B C)))) ## Equality over Addition stmt (addeq2d () ((-> ph (= A B))) (-> ph (= (+ C A) (+ C B)))) ## Equality over Addition stmt (addeq12i () ((= A B) (= C D)) (= (+ A C) (+ B D))) ## Equality over Addition stmt (addeq12d () ((-> ph (= A B)) (-> ph (= C D))) (-> ph (= (+ A C) (+ B D)))) ## Equivalence for div ## stmt (diveq1 () () (-> (= A C) (= (div A B) (div C B)))) stmt (diveq2 () () (-> (= B C) (= (div A B) (div A C)))) stmt (diveq1d () ( (-> ph (= A C))) (-> ph (= (div A B) (div C B)))) stmt (expeq1 () () (-> (= A B) (= (exp A C) (exp B C)))) stmt (expeq2 () () (-> (= A B) (= (exp C A) (exp C B)))) stmt (halfminuseq1 () () (-> (= A C) (= (.- A B) (.- C B)))) ## Equivalence for - stmt (halfminuseq2 () () (-> (= B C) (= (.- A B) (.- A C)))) stmt (halfminuseq1d () ( (-> ph (= A B))) (-> ph (= (.- A C) (.- B C)))) stmt (halfminuseq2d () ( (-> ph (= B C))) (-> ph (= (.- A B) (.- A C)))) stmt (halfminuseq12 () () (-> (/\ (= A B) (= C D)) (= (.- A C) (.- B D)))) stmt (modeq1 () () (-> (= A B) (= (mod A C) (mod B C)))) stmt (modeq2 () () (-> (= A B) (= (mod C A) (mod C B)))) stmt (modeq1d () ( (-> ph (= A B))) (-> ph (= (mod A C) (mod B C)))) stmt (modeq2d () ( (-> ph (= A B))) (-> ph (= (mod C A) (mod C B)))) ## Equality over Multiplication ## ## (-> (= A B) (= (* A C) (* B C))) ##
stmt (muleq1 () () (-> (= A B) (= (* A C) (* B C)))) ## Equality over Multiplication ## ## (-> (= A B) (= (* C A) (* C B))) ##
stmt (muleq2 () () (-> (= A B) (= (* C A) (* C B)))) ## Equality over Multiplication stmt (muleq1d () ((-> ph (= A B))) (-> ph (= (* A C) (* B C)))) stmt (muleq2d () ((-> ph (= A B))) (-> ph (= (* C A) (* C B)))) stmt (muleq12d () ((-> ph (= A B)) (-> ph (= C D))) (-> ph (= (* A C) (* B D)))) ## Equality over Multiplication stmt (muleq12i () ((= A B) (= C D)) (= (* A C) (* B D))) ## Divide both sides of an equation ## ## (= [ A ] [ C ) ## (= (div [ A B) ] (div [ C B)) ##
stmt (diveq1i () ( (= A C)) (= (div A B) (div C B))) stmt (halfminuseq1i () ( (= A B)) (= (.- A C) (.- B C))) stmt (halfminuseq2i () ( (= B C)) (= (.- A B) (.- A C))) stmt (modeq1i () ( (= A B)) (= (mod A C) (mod B C))) stmt (modeq2i () ( (= A B)) (= (mod C A) (mod C B))) ## Equivalence for sum ## stmt (sumeq1 () () (-> (= A C) (= (sum A B S) (sum C B S)))) stmt (sumeq1i () ( (= A C)) (= (sum A B S) (sum C B S))) stmt (sumeq1d () ( (-> ph (= A C))) (-> ph (= (sum A B S) (sum C B S)))) ## Equivalence for sum ## stmt (sumeq2 () () (-> (= B C) (= (sum A B S) (sum A C S)))) stmt (sumeq2i () ( (= B C)) (= (sum A B S) (sum A C S))) stmt (sumeq2d () ( (-> ph (= B C))) (-> ph (= (sum A B S) (sum A C S)))) ## Equivalence for sum ## stmt (sumseq3 () () (-> (=_ S T) (= (sum A B S) (sum A B T)))) stmt (sumseq3i () ( (=_ S T)) (= (sum A B S) (sum A B T))) stmt (sumseq3d () ( (-> ph (=_ S T))) (-> ph (= (sum A B S) (sum A B T)))) ## Equivalence for product ## stmt (producteq1 () () (-> (= A C) (= (product A B S) (product C B S)))) stmt (producteq1i () ((= A C)) (= (product A B S) (product C B S))) stmt (producteq1d () ( (-> ph (= A C))) (-> ph (= (product A B S) (product C B S)))) ## Equivalence for product ## stmt (producteq2 () () (-> (= B C) (= (product A B S) (product A C S)))) stmt (producteq2i () ( (= B C)) (= (product A B S) (product A C S))) stmt (producteq2d () ( (-> ph (= B C))) (-> ph (= (product A B S) (product A C S)))) ## Equivalence for product ## stmt (productseq3 () () (-> (=_ S T) (= (product A B S) (product A B T)))) stmt (productseq3i () ( (=_ S T)) (= (product A B S) (product A B T))) stmt (productseq3d () ( (-> ph (=_ S T))) (-> ph (= (product A B S) (product A B T)))) # Statements needed for integers. ## Apply Head Operator ## right('Simplify', 'Hd') stmt (headop () () (= (head (<,> A B)) A)) ## Apply Tail Operator ## right('Simplify', 'Tl') stmt (tailop () () (= (tail (<,> A B)) B)) ## Equality theorem for head stmt (headeq () () (-> (= A B) (= (head A) (head B)))) ## Equality theorem for tail stmt (taileq () () (-> (= A B) (= (tail A) (tail B)))) ## Equality theorem for head stmt (headeqi () ((= A B)) (= (head A) (head B))) ## Equality theorem for tail stmt (taileqi () ((= A B)) (= (tail A) (tail B))) stmt (headeqd () ((-> ph (= A B))) (-> ph (= (head A) (head B)))) stmt (taileqd () ((-> ph (= A B))) (-> ph (= (tail A) (tail B)))) ## Ordered Pair Equality stmt (opeq1 () () (-> (= A B) (= (<,> A C) (<,> B C)))) ## Ordered Pair Equality stmt (opeq2 () () (-> (= A B) (= (<,> C A) (<,> C B)))) stmt (opeq1i () ((= A B)) (= (<,> A C) (<,> B C))) stmt (opeq1d () ((-> ph (= A B))) (-> ph (= (<,> A C) (<,> B C)))) stmt (opeq2i () ((= A B)) (= (<,> C A) (<,> C B))) stmt (opeq2d () ((-> ph (= A B))) (-> ph (= (<,> C A) (<,> C B)))) ## Ordered Pair Equality stmt (opeq12 () () (-> (/\ (= A B) (= C D)) (= (<,> A C) (<,> B D)))) ## Ordered Pair Equality stmt (opeq12d () ((-> ph (= A B)) (-> ph (= C D))) (-> ph (= (<,> A C) (<,> B D)))) ## Cancellation of addition stmt (addcan2 () () (<-> (= (+ A B) (+ A C)) (= B C))) ## Cancellation of addition stmt (addcan () () (<-> (= (+ B A) (+ C A)) (= B C))) ## Rearrange Addition Terms ## ## (= (+ (+ A B) (+ C D)) (+ (+ A C) (+ B D))) ##
stmt (add4 () () (= (+ (+ A B) (+ C D)) (+ (+ A C) (+ B D)))) ## Rearrange the second and fourth terms ## ## (= (+ (+ A B) (+ C D)) (+ (+ A D) (+ C B))) ##
stmt (add24 () () (= (+ (+ A B) (+ C D)) (+ (+ A D) (+ C B)))) ## Rearrange Addition Terms stmt (add432 () () (= (+ (+ A B) (+ C D)) (+ (+ A D) (+ B C)))) ## Inequality Equivalence stmt (leeq1 () () (-> (= A B) (<-> (<= A C) (<= B C)))) ## Inequality Equivalence stmt (leeq2 () () (-> (= A B) (<-> (<= C A) (<= C B)))) ## Equivalence over Inequality ## Equality inference for less than or equal relation ## ## (= A ] ] [ B ] ) ## (<-> (<= A ] C ] ) (<= [ B ] C)) ##
stmt (leeq1i () ((= A B)) (<-> (<= A C) (<= B C))) ## Equivalence over Inequality ## Equality inference for less than or equal relation ## ## (= [ A ] [ [ B ] ) ## (<-> (<= C [ A ] ) (<= [ C [ B ] )) ##
stmt (leeq2i () ((= A B)) (<-> (<= C A) (<= C B))) ## Inequality Equivalence ## Equality deduction for less than or equal relation stmt (leeq1d () ((-> ph (= A B))) (-> ph (<-> (<= A C) (<= B C)))) ## Inequality Equivalence ## Equality deduction for less than or equal relation ## ## (-> ph (= [ A ] [ [ B ] )) ## (-> ph (<-> (<= C [ A ] ) (<= [ C [ B ] ))) ##
stmt (leeq2d () ((-> ph (= A B))) (-> ph (<-> (<= C A) (<= C B)))) ## Inequality relation for two equal sums stmt (leadd12 () () (-> (= (+ A B) (+ C D)) (<-> (<= A C) (<= D B)))) ## A number minus zero is itself stmt (halfminuszero () () (= (.- A (0)) A)) ## Cancel Multiplication stmt (mulcant () () (-> (< (0) C) (<-> (= (* A C) (* B C)) (= A B)))) ## Cancel Multiplication stmt (mulcant2 () () (-> (< (0) C) (<-> (= (* C A) (* C B)) (= A B)))) stmt (ltDiff ((A x) (B x)) () (<-> (< A B) (E. x (/\ (= (+ A x) B) (-. (= x (0))))))) ## All nonzero natural numbers are positive ## right('Equivalence', '<') stmt (0inequalities2 () () (<-> (-. (= A (0))) (> A (0)))) stmt (neqlt () () (-> (-. (= A B)) (\/ (< A B) (> A B)))) stmt (lemul1 () () (-> (<= A B) (<= (* A C) (* B C)))) ## Multiply Both Sides ## Multiplication is monotonic in its second argument stmt (lemul2 () () (-> (<= A B) (<= (* C A) (* C B)))) stmt (lemul12 () () (-> (/\ (<= A B) (<= C D)) (<= (* A C) (* B D)))) stmt(addge01t () () (<= A (+ A B))) stmt (addge02t () () (<= A (+ B A))) stmt (halfminus-neg () () (-> (<= A B) (= (.- A B) (0)))) ## Commute Half Minus ## ## (-> (<= B A) (= (+ (.- A B) C) (.- (+ A C) B))) ##
stmt (halfminusaddcom () () (-> (<= B A) (= (+ (.- A B) C) (.- (+ A C) B)))) ## There is a number equal to any expression stmt (tyex ((A x)) () (E. x (= x A))) ## Subset and Element Of Equivalence <title> stmt (elSubseti () ((e. A S)) (C_ ({} A) S)) ## <title> Recursive Definition of Fibonacci Numbers stmt (df-fibRecurse () () (= (fibonacci (+ A (2))) (+ (fibonacci A) (fibonacci (+ A (1)))))) ## Equivalence for fibonacci ## stmt (fibonaccieq () () (-> (= A B) (= (fibonacci A) (fibonacci B)))) stmt (fibonaccieqi () ((= A B)) (= (fibonacci A) (fibonacci B))) stmt (fibonaccieqd () ((-> ph (= A B))) (-> ph (= (fibonacci A) (fibonacci B)))) stmt (fibonacci0 () () (= (fibonacci (0)) (0))) stmt (fibonacci1 () () (= (fibonacci (1)) (1))) ## Equivalence for triangular number ## stmt (trieq () () (-> (= A B) (= (tri A) (tri B)))) stmt (trieqi () ((= A B)) (= (tri A) (tri B))) stmt (trieqd () ((-> ph (= A B))) (-> ph (= (tri A) (tri B)))) stmt (trianglePlus1r () () (= (tri (+ A (1))) (+ (+ (tri A) A) (1)))) stmt (triangle0 () () (= (tri (0)) (0))) ## Expand Ordered Pair stmt (opexpand () () (= A (<,> (head A) (tail A)))) ## Alpha conversion for set abstraction stmt (abeq ((ph y) (ps x)) ((-> (= x y) (<-> ph ps))) (=_ ({|} x ph) ({|} y ps))) ## Make an implicit substitution explicit stmt (sbcie ((A x) (ps x)) ((-> (= x A) (<-> ph ps))) (<-> ([/] A x ph) ps)) ## First branch of ternary expression stmt (ifn1 () () (-> ph (= (ifn ph A B) A))) ## Second branch of ternary expression stmt (ifn2 () () (-> (-. ph) (= (ifn ph A B) B))) ## Equivalence of predicate in ifn stmt (ifnbi1 () () (-> (<-> ph ps) (= (ifn ph A B) (ifn ps A B)))) stmt (ifnbi1i () ( (<-> ph ps)) (= (ifn ph A B) (ifn ps A B))) stmt (ifnbi1d () ( (-> ch (<-> ph ps))) (-> ch (= (ifn ph A B) (ifn ps A B)))) ## Equality of first term for ifn stmt (ifneq2 () () (-> (= A B) (= (ifn ph A C) (ifn ph B C)))) stmt (ifneq2i () ( (= A B)) (= (ifn ph A C) (ifn ph B C))) stmt (ifneq2d () ( (-> ps (= A B))) (-> ps (= (ifn ph A C) (ifn ph B C)))) ## Equality of second term for ifn stmt (ifneq3 () () (-> (= A B) (= (ifn ph C A) (ifn ph C B)))) stmt (ifneq3i () ( (= A B)) (= (ifn ph C A) (ifn ph C B))) stmt (ifneq3d () ( (-> ps (= A B))) (-> ps (= (ifn ph C A) (ifn ph C B)))) ## Modulo Congruence Definition ## ## Two numbers A and B are congruent modulo C if there values ## mod C are equal. ## stmt (df-modcon () () (<-> (=mod A B C) (= (mod A C) (mod B C)))) ## Additive Identity stmt (addid () () (= (+ A (0)) A)) ## Additive Identity stmt (addidr () () (= (+ (0) A) A))