```(def-language group-language
(base-types gg)
(constants
(e "gg")
(mul "[gg,gg,gg]")
(inv "[gg,gg]")))
```

```
(def-theory groups
Remark: This entry is multiply defined. See:  [1] [2]
(language group-language)
(component-theories h-o-real-arithmetic)
(axioms
(left-mul-id
"forall(x:gg, e mul x = x)"
rewrite)
(right-mul-id
"forall(x:gg, x mul e = x)"
rewrite)
(left-mul-inv
"forall(x:gg, inv(x) mul x = e)"
rewrite)
(right-mul-inv
"forall(x:gg, x mul inv(x) = e)"
rewrite)
(mul-associativity
"forall(x,y,z:gg, (x mul y) mul z = x mul (y mul z))"
rewrite)))
```

```
(def-quasi-constructor group
"lambda(gg%:sets[gg], mul%:[gg,gg,gg], e%:gg, inv%:[gg,gg],
forall(x,y:gg, x in gg% and y in gg% implies mul%(x,y) in gg%) and
e% in gg% and
forall(x:gg, x in gg% implies inv%(x) in gg%) and
forall(x:gg, x in gg% implies mul%(e%,x)=x) and
forall(x:gg, x in gg% implies mul%(x,e%)=x) and
forall(x:gg, x in gg% implies mul%(inv%(x),x)=e%) and
forall(x:gg, x in gg% implies mul%(x,inv%(x))=e%) and
forall(x,y,z:gg, ((x in gg%) and (y in gg%) and (z in gg%)) implies
mul%(mul%(x,y),z) = mul%(x,mul%(y,z))))"
(language groups))
```

```
(def-theorem mul-is-total
"total_q{mul,[gg,gg,gg]}"
(theory groups)
(usages d-r-convergence transportable-macete)
(proof
(
insistent-direct-inference
(instantiate-theorem mul-associativity ("x_0" "x_1" "x_1"))
)))
```

```
(def-theorem inv-is-total
Remark: This entry is multiply defined. See:  [1] [2]
"total_q{inv,[gg,gg]}"
(theory groups)
(usages d-r-convergence transportable-macete)
(proof
(
insistent-direct-inference
(instantiate-theorem left-mul-inv ("x_0"))
)))
```

```
(def-theorem reverse-mul-associativity
"forall(x,y,z:gg, x mul (y mul z) = (x mul y) mul z)"
(theory groups)
(usages transportable-macete)
(proof (simplify)))
```

```
(def-theorem left-inv-cancellation
"forall(x,y:gg, inv(x) mul (x mul y) = y)"
(theory groups)
(usages rewrite transportable-macete)
(proof
(
(apply-macete-with-minor-premises reverse-mul-associativity)
(apply-macete-with-minor-premises left-mul-inv)
simplify
)))
```

```
(def-theorem right-inv-cancellation
"forall(x,y:gg, x mul (inv(x) mul y) = y)"
(theory groups)
(usages rewrite transportable-macete)
(proof  ;; obtained by editing the previous proof script
(
(apply-macete-with-minor-premises reverse-mul-associativity)
(apply-macete-with-minor-premises right-mul-inv)
simplify
)))
```

```(def-script inv-cancellation-script 1
(
(apply-macete-with-minor-premises reverse-mul-associativity)
(apply-macete-with-minor-premises \$1)
simplify
))
```

```
(def-theorem inv-of-e
"inv(e)=e"
(theory groups)
(usages rewrite transportable-macete)
(proof
(
(instantiate-theorem left-mul-id ("inv(e)"))
(force-substitution "inv(e)" "e mul inv(e)" (0))
simplify
)))
```

```
(def-theorem inv-of-inv
"forall(x:gg, inv(inv(x))=x)"
(theory groups)
(usages rewrite transportable-macete)
(proof
(
(instantiate-theorem mul-associativity ("inv(inv(x))" "inv(x)" "x"))
(contrapose "with(p:prop,p)")
(force-substitution "inv(inv(x)) mul inv(x)" "e" (0))
(force-substitution "inv(x) mul x" "e" (0))
simplify
simplify
simplify
)))
```

```
(def-theorem push-inv
"forall(g,h:gg, inv(g mul h) = inv(h) mul inv(g))"
(theory groups)
(usages rewrite transportable-macete)
(proof
(
(instantiate-theorem mul-associativity
("inv(g mul h)" "g mul h" "inv(h) mul inv(g)"))
(contrapose "with(p:prop,p)")
(force-substitution "inv(g mul h) mul (g mul h)" "e" (0))
(force-substitution "(g mul h) mul (inv(h) mul inv(g))" "e" (0))
simplify
simplify
simplify
)))
```

```
(def-translation mul-reverse
(source groups)
(target groups)
(fixed-theories h-o-real-arithmetic)
(constant-pairs
(mul "lambda(x,y:gg, y mul x)"))
(theory-interpretation-check using-simplification))
```

```
(def-theorem left-cancellation-law
"forall(x,y,z:gg, x mul y = x mul z iff y=z)"
(theory groups)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem mul-associativity ("inv(x)" "x" "y"))
(contrapose "with(y,x:gg,(inv(x) mul x) mul y=inv(x) mul (x mul y))")
(force-substitution "x mul y" "x mul z" (0))
(apply-macete-with-minor-premises mul-associativity)
(apply-macete-with-minor-premises left-inv-cancellation)
)))
```

```
(def-theorem left-trivial-cancellation-law-left
"forall(x,y:gg, x = x mul y iff e=y)"
(theory groups)
(usages transportable-macete)
(proof
(
(instantiate-theorem left-cancellation-law ("x" "e" "y"))
simplify
simplify
(contrapose "with(y,x:gg,not(x mul e=x mul y))")
simplify
)))
```

```
(def-theorem left-trivial-cancellation-law-right
"forall(x,y:gg, x mul y = x iff y=e)"
(theory groups)
(usages transportable-macete)
(proof
(
(instantiate-theorem left-trivial-cancellation-law-left ("x" "y"))
simplify
simplify
)))
```

```
(def-theorem right-cancellation-law
left-cancellation-law
(theory groups)
(usages transportable-macete)
(translation mul-reverse)
(proof existing-theorem))
```

```
(def-theorem right-trivial-cancellation-law-left
left-trivial-cancellation-law-left
(theory groups)
(usages transportable-macete)
(translation mul-reverse)
(proof existing-theorem))
```

```
(def-theorem right-trivial-cancellation-law-right
left-trivial-cancellation-law-right
(theory groups)
(usages transportable-macete)
(translation mul-reverse)
(proof existing-theorem))
```

```
(def-compound-macete group-cancellation-laws
(series
(repeat mul-associativity)
(repeat left-cancellation-law)
left-trivial-cancellation-law-left
left-trivial-cancellation-law-right
(repeat reverse-mul-associativity)
(repeat right-cancellation-law)
right-trivial-cancellation-law-left
right-trivial-cancellation-law-right))
```