## redirect add_multiply.gh param (PROP prop.ghi () "") param (PREDICATE_EQ predicate_eq.ghi (PROP) "") param (ADD_MULTIPLY_MIN add_multiply_min.ghi (PROP PREDICATE_EQ) "") tvar (wff ph ps ch th ta) tvar (nat A B C D) var (nat v w x y z) 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)) ## Additive Identity ## auto-right('Simplify', '0') stmt (addidr () () (= (+ (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)))) ## Multiplicative Identity ## auto-right('Simplify', '1') stmt (mulidr() () (= (* (1) A) A)) ## Inequality over Addition ## ## (-. (= [ A ] [ [ B )) ## (-. (= (+ C [ A ] ) (+ [ C [ B))) ##
stmt (addneq2i () ((-. (= A B))) (-. (= (+ C A) (+ C B)))) ## Multiply by 0 ## This rederives one of the Peano axioms. stmt (mul0 () () (= (* A (0)) (0))) ## Multiply by 0 ## auto-right('Simplify','0') stmt (mul0r () () (= (* (0) A) (0))) ## 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))))) ## 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))) # 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)) ## Add a number to both sides of an equation ## ## (-> (= A B) (= (+ A C) (+ B C))) ##