(def-theory abelian-groups (component-theories groups) (axioms (group-commutativity"forall(x,y:gg, x mul y = y mul x)")))

(def-recursive-constant multiple"lambda(phi:[zz,gg,gg], lambda(k:zz, m:gg,if(0<k,m mul phi(k-1,m),k=0, e, inv(phi(-k,m)))))"(definition-name multiple) (theory abelian-groups))

(def-overloading + (h-o-real-arithmetic +) (abelian-groups mul))

(def-overloading - (h-o-real-arithmetic -) (abelian-groups inv))

(def-theorem multiple-totality"total_q{multiple,[zz,gg,gg]}"(theory abelian-groups) (usages d-r-convergence transportable-macete) (proof ( insistent-direct-inference (case-split ("0<=x_0")) (induction integer-inductor ("x_0")) (unfold-single-defined-constant (0) multiple) simplify (cut-with-single-formula"forall(n:zz,0<=n implies #(multiple(n,x_1)))") (backchain"with(x_1:gg,forall(n:zz,0<=n implies #(multiple(n,x_1))));") simplify (weaken (0)) )))

(def-theorem multiple-additivity-lemma"forall(m,n:zz, g:gg, 0<=m and 0<=n implies multiple(m+n,g)=multiple(m,g)+multiple(n,g))"reverse lemma (proof ( (induction trivial-integer-inductor ()) beta-reduce-repeatedly (unfold-single-defined-constant (1) multiple) simplify (unfold-single-defined-constant (0) multiple) simplify )) (theory abelian-groups))

(def-theorem multiple-difference-lemma"forall(m,n:zz, g:gg, 0<=m and 0<=n implies multiple(m-n,g)=multiple(m,g)+-multiple(n,g))"lemma (proof ( direct-and-antecedent-inference-strategy (case-split ("n<=m")) (block (script-comment"`case-split' at (1)") (cut-with-single-formula" multiple(m,g)=multiple(m-n,g)+multiple(n,g)") (block (script-comment"`cut-with-single-formula' at (0)") (backchain"with(g:gg,g=g);") (apply-macete-with-minor-premises group-cancellation-laws) (apply-macete-with-minor-premises right-mul-inv) ) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises rev%multiple-additivity-lemma) simplify ) ) (block (script-comment"`case-split' at (2)") (force-substitution"m-n""-(n-m)"(0)) (block (script-comment"`force-substitution' at (0)") (unfold-single-defined-constant (0) multiple) simplify (cut-with-single-formula"multiple(n,g)=multiple(n+[-1]*m,g)+multiple(m,g)") (block (script-comment"`cut-with-single-formula' at (0)") (backchain"with(g:gg,g=g);") (apply-macete-with-minor-premises push-inv) (apply-macete-with-minor-premises group-cancellation-laws) (apply-macete-with-minor-premises right-mul-inv) ) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises rev%multiple-additivity-lemma) simplify ) ) simplify ) )) (theory abelian-groups))

(def-theorem multiple-is-additive"forall(m,n:zz, g:gg, multiple(m+n,g)=multiple(m,g)+multiple(n,g))"(proof ( direct-inference (case-split ("0<=n""0<=m")) (apply-macete-with-minor-premises rev%multiple-additivity-lemma) (force-substitution"m+n""n-(-m)"(0)) (apply-macete-with-minor-premises multiple-difference-lemma) (unfold-single-defined-constant (2) multiple) simplify (assume-theorem group-commutativity) (backchain"forall(x,y:gg,x+y=y+x);") simplify (force-substitution"m+n""m-(-n)"(0)) (apply-macete-with-minor-premises multiple-difference-lemma) (apply-macete-with-minor-premises group-cancellation-laws) (unfold-single-defined-constant (1) multiple) simplify simplify (unfold-single-defined-constant (0 1 2) multiple) simplify (apply-macete-with-minor-premises multiple-additivity-lemma) (apply-macete-with-minor-premises push-inv) (assume-theorem group-commutativity) (backchain"forall(x,y:gg,x+y=y+x);") )) (theory abelian-groups) (usages transportable-macete))

(def-theorem multiple-is-additive-in-group"forall(m:zz, g,h:gg, multiple(m,g+h)=multiple(m,g)+multiple(m,h))"(theory abelian-groups) (usages transportable-macete) (proof ( direct-inference (case-split ("0<=m")) (induction trivial-integer-inductor ("m")) beta-reduce-repeatedly unfold-defined-constants simplify (apply-macete-with-minor-premises group-cancellation-laws) (assume-theorem group-commutativity) (backchain"forall(x,y:gg,x+y=y+x);") unfold-defined-constants simplify (cut-with-single-formula"forall(m:zz,0<=m implies multiple(m,g+h)=multiple(m,g)+multiple(m,h))") (backchain"with(h,g:gg, forall(m:zz, 0<=m implies multiple(m,g+h)=multiple(m,g)+multiple(m,h)));") (apply-macete-with-minor-premises push-inv) (assume-theorem group-commutativity) (backchain"forall(x,y:gg,x+y=y+x);") direct-and-antecedent-inference-strategy simplify )))

(def-theorem multiple-commutes-with-negation"forall(m:zz,g:gg, multiple([-1]*m,g)=-multiple(m,g))"(theory abelian-groups) (proof ( direct-and-antecedent-inference-strategy (case-split ("0<=m")) (unfold-single-defined-constant (0) multiple) simplify (case-split ("0=m")) simplify (unfold-single-defined-constant (0) multiple) simplify simplify (unfold-single-defined-constant (1) multiple) simplify )))

(def-theorem multiple-commutes-with-negation-corollary"forall(g:gg, multiple([-1],g)=-g)"(theory abelian-groups) (proof ( (force-substitution"[-1]""[-1]*1"(0)) (apply-macete-with-minor-premises multiple-commutes-with-negation) (unfold-single-defined-constant (0) multiple) simplify (unfold-single-defined-constant (0) multiple) simplify simplify )))

(def-theorem multiple-commutes-with-negation-in-group"forall(m:zz,g:gg, multiple(m,-g)=-multiple(m,g))"(theory abelian-groups) (proof ( direct-inference (case-split ("0<=m")) (induction trivial-integer-inductor ("m")) beta-reduce-repeatedly (unfold-single-defined-constant (0 1) multiple) simplify (assume-theorem group-commutativity) (backchain"forall(x,y:gg,x+y=y+x);") (unfold-single-defined-constant (0 1) multiple) simplify (cut-with-single-formula"forall(m:zz, 0<=m implies multiple(m,-g)=-multiple(m,g))") (backchain"with(g:gg, forall(m:zz,0<=m implies multiple(m,-g)=-multiple(m,g)));") direct-inference simplify )))

(def-theorem multiple-is-homogenuous"forall(m,n:zz, g:gg, multiple(m*n,g)=multiple(m,multiple(n,g)))"(theory abelian-groups) (proof ( direct-inference (case-split ("0<=m")) (induction trivial-integer-inductor ()) beta-reduce-repeatedly (unfold-single-defined-constant (0 1) multiple) simplify (apply-macete-with-minor-premises multiple-is-additive) (force-substitution"m*n""([-1]*m)*([-1]*n)"(0)) (cut-with-single-formula"forall(m,n,k:zz,g:gg,0<=m implies multiple(m*n,g)=multiple(m,multiple(n,g)))") (backchain"forall(m,n,k:zz,g:gg, 0<=m implies multiple(m*n,g)=multiple(m,multiple(n,g)));") direct-inference simplify (apply-macete-with-minor-premises multiple-commutes-with-negation) (apply-macete-with-minor-premises multiple-commutes-with-negation) (apply-macete-with-minor-premises multiple-commutes-with-negation-in-group) (apply-macete-with-minor-premises inv-of-inv) (weaken (0)) direct-and-antecedent-inference-strategy simplify )) (usages transportable-macete))

(def-theorem multiple-of-group-identity"forall(m:zz, multiple(m,e)=e)"(theory abelian-groups) (proof ( direct-inference (cut-with-single-formula"multiple(m,e)=multiple(m,e)+multiple(m,e)") (incorporate-antecedent"with(m:zz,multiple(m,e)=multiple(m,e)+multiple(m,e));") (apply-macete-with-minor-premises group-cancellation-laws) simplify (cut-with-single-formula"multiple(m,e)+multiple(m,e)=multiple(m,e+e)") (backchain"with(m:zz,multiple(m,e)+multiple(m,e)=multiple(m,e+e));") (apply-macete-with-minor-premises right-mul-id) (apply-macete-with-minor-premises multiple-is-additive-in-group) )))

(def-theorem 0-multiple-is-group-identity"forall(g:gg, multiple(0,g)=e)"(theory abelian-groups) (proof ( (unfold-single-defined-constant (0) multiple) simplify )))

(def-theorem 1-multiple-is-element"forall(g:gg, multiple(1,g)=g)"(theory abelian-groups) (proof ( (unfold-single-defined-constant (0) multiple) simplify (unfold-single-defined-constant (0) multiple) simplify )))

(def-theorem multiple-totality-with-range"forall(g:gg,n:zz, #(multiple(n,g),gg))"(theory abelian-groups) (proof ( direct-inference )))