## redirect integers.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) "") param (PEANO_THMS /peano/peano_stmts.ghi (PROP PEANO_MIN PEANO NAIVE_SET) "") 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 (wff (=z A B)) term (wff (<=z A B)) term (wff (z A B)) term (wff (>=z A B)) term (wff (zpos A)) term (nat (+z A B)) term (nat (*z A B)) term (nat (-n A)) term (nat (- A B)) term (nat (int A)) term (nat (zn A)) term (nat (0z)) term (nat (1z)) term (nat (2z)) term (nat (3z)) term (nat (4z)) term (nat (5z)) term (nat (6z)) term (nat (7z)) term (nat (8z)) term (nat (9z)) term (nat (10z)) ## Convert Natural to Integer Equality ## Use this sparingly. stmt (eqzeqi () ((= A B)) (=z A B)) ## Convert Natural to Integer Equality ## Use this sparingly. stmt (eqzeqd () ((-> ph (= A B))) (-> ph (=z A B))) ## Reflexive Property ## Integer equality is reflexive. stmt (zeqid () () (=z A A)) ## Symmetric Property ## Integer equality is symmetric. ## right('Commute', '=') stmt (zeqcom() () (<-> (=z A B) (=z B A))) ## Symmetric Property stmt (zeqcomi() ((=z A B)) (=z B A)) ## Transitive Property ## right('Simplify', '=') stmt (zeqtr() () (-> (/\ (=z A B) (=z B C)) (=z A C))) ## Transitive Property stmt (zeqtrd () ((-> ph (=z A B)) (-> ph (=z B C))) (-> ph (=z A C))) stmt (zeqzeq1() () (-> (=z A B) (<-> (=z A C) (=z B C)))) ## Equivalence over Equality stmt (zeqzeq2 () () (-> (=z A B) (<-> (=z C A) (=z C B)))) ## Equivalence over Equality ## ## (=z A ] ] [ B ] ) ## (<-> (=z A ] C) ] [ (=z B ] C)) ##
stmt (zeqzeq1i () ((=z A B)) (<-> (=z A C) (=z B C))) ## Equivalence over Equality ## ## (-> ph (= A ] ] [ B ] )) ## (-> ph (<-> (= A ] C) ] [ (= B ] C))) ##
stmt (zeqzeq1d () ((-> ph (=z A B))) (-> ph (<-> (=z A C) (=z B C)))) ## Equivalence over Equality ## ## (=z [ A ] [ [ B) ## (<-> (=z C [ A) ] [ (=z C [ B)) ##
stmt (zeqzeq2i () ((=z A B)) (<-> (=z C A) (=z C B))) ## Equivalence over Equality ## ## (-> ph (= [ A ] [ [ B)) ## (-> ph (<-> (= C [ A) ] [ (= C [ B))) ##
stmt (zeqzeq2d () ((-> ph (=z A B))) (-> ph (<-> (=z C A) (=z C B)))) ## Equivalence over Equality stmt (zeqzeq12i () ((=z A B) (=z C D)) (<-> (=z A C) (=z B D))) ## Transitive Property stmt (zeqzeq12d () ((-> ph (=z A B)) (-> ph (=z C D))) (-> ph (<-> (=z A C) (=z B D)))) ## ## (<-> (=z A B) (=z (+z A C) (+z B C))) ##
stmt (zaddcan1() () (<-> (=z A B) (=z (+z A C) (+z B C)))) ## ## (<-> (=z A B) (=z (+z C A) (+z C B))) ##
stmt (zaddcan2() () (<-> (=z A B) (=z (+z C A) (+z C B)))) stmt (zaddzeq1() () (-> (=z A B) (=z (+z A C) (+z B C)))) stmt (zaddzeq2() () (-> (=z A B) (=z (+z C A) (+z C B)))) stmt (zaddzeq1i () ( (=z A B)) (=z (+z A C) (+z B C))) stmt (zaddzeq1d () ( (-> ph (=z A B))) (-> ph (=z (+z A C) (+z B C)))) stmt (zaddzeq2i () ( (=z A B)) (=z (+z C A) (+z C B))) stmt (zaddzeq2d () ( (-> ph (=z A B))) (-> ph (=z (+z C A) (+z C B)))) stmt (zaddzeq12() () (-> (/\ (=z A B) (=z C D)) (=z (+z A C) (+z B D)))) ## Equality over Addition ## ## (=z A ] ] ] [ B ] ] ) ## (=z [ [ C ] [ [ [ D) ## (=z (+z A ] [ C ] ) (+z [ B ] [ D)) ##