```
(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))
)))
```

```
"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)")
) )
(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)")
) )
simplify
)
))
(theory abelian-groups))
```

```
"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"))
(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 push-inv)
(assume-theorem group-commutativity)
(backchain "forall(x,y:gg,x+y=y+x);")
))
(theory abelian-groups)
(usages transportable-macete))
```

```
"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
(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)
)))
```

```
(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
)))
```