## 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))) ##
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)))) ## 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))) ## Cancellation of addition stmt (addcan2 () () (<-> (= (+ A B) (+ A C)) (= 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 ## ## (= (+ (+ A B) C) (+ (+ A C) B)) ##
stmt (add23 () () (= (+ (+ A B) C) (+ (+ A C) B))) ## Rearrange Addition Terms stmt (add432 () () (= (+ (+ A B) (+ C D)) (+ (+ A D) (+ B C)))) ## Cancel Addition ## ## (= (+ A ] C ) ] (+ [ B C)) ## (= A ] ] [ B) ##
stmt (addcani () ((= (+ A C) (+ B C))) (= A B)) ## Cancel Addition ## ## (= (+ C [ A ) ] (+ C [ B )) ## (= [ A ] [ B) ##
stmt (addcan2i () ((= (+ C A) (+ C B))) (= A B)) ## Reorder Multiplication Terms stmt (mul4() () (= (* (* A B) (* C D)) (* (* A C) (* B D)))) ## Reorder Multiplication Terms stmt (mul42() () (= (* (* A B) (* C D)) (* (* A D) (* C B)))) ## Commutative Property stmt (mulcom12 () () (= (* A (* B C)) (* B (* A C)))) stmt (dist_ax6 () () (= (* A (+ B (1))) (+ (* A B) A))) stmt (dist_ax6r () () (= (* (+ A (1)) B) (+ (* A B) B))) ## Adding twice mean Multiply by 2 ## right('Simplify', '2') stmt (add2mul () () (= (+ A A) (* (2) A)))