```
(def-constant subgroup
"lambda(a:sets[gg],
nonempty_indic_q{a} and
forall(g,h:gg, ((g in a) and (h in a)) implies ((g mul h) in a)) and
forall(g:gg, (g in a) implies (inv(g) in a)))"
(theory groups))
```

```
(def-constant gg%subgroup
"sort_to_indic(gg)"
(theory groups))
```

```
(def-constant e%subgroup
"singleton{e}"
(theory groups))
```

```
(def-theorem gg-is-a-subgroup
"subgroup(gg%subgroup)"
(theory groups)
(usages transportable-macete)
(proof
(
unfold-defined-constants
simplify
(instantiate-existential ("e"))
simplify
)))
```

```
(def-theorem singleton-e-is-a-subgroup
"subgroup(e%subgroup)"
(theory groups)
(usages transportable-macete)
(proof
(
unfold-defined-constants
simplify-insistently
direct-and-antecedent-inference-strategy
simplify
simplify
)))
```

```
(def-theorem subgroups-are-subsets-of-gg%subgroup
"forall(a:sets[gg], subgroup(a) implies a subseteq gg%subgroup)"
(theory groups)
(usages transportable-macete)
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
insistent-direct-inference
simplify
)))
```

```
(def-theorem subgroups-are-nonempty
"forall(a:sets[gg], subgroup(a) implies nonempty_indic_q{a})"
(theory groups)
(usages transportable-macete)
(proof
(
(unfold-single-defined-constant-globally subgroup)
simplify
)))
```

```
(def-theorem subgroups-closed-under-mul
"forall(a:sets[gg], subgroup(a)
implies
forall(g,h:gg, (g in a) and (h in a) implies (g mul h) in a))"
(theory groups)
(usages transportable-macete)
(proof
(
(unfold-single-defined-constant-globally subgroup)
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop, forall(g,h:gg,p))" ("g" "h"))
)))
```

```
(def-theorem subgroups-closed-under-inv
"forall(a:sets[gg], subgroup(a)
implies
forall(g,h:gg, (g in a) implies inv(g) in a))"
(theory groups)
(usages transportable-macete)
(proof
(
(unfold-single-defined-constant-globally subgroup)
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop, forall(g:gg,p))" ("g"))
)))

```

```
(def-theorem subgroups-contain-e
"forall(a:sets[gg], subgroup(a) implies (e in a))"
(theory groups)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem subgroups-are-nonempty ("a"))
(force-substitution "e" "x mul inv(x)" (0))
(apply-macete-with-minor-premises subgroups-closed-under-mul)
simplify
(apply-macete-with-minor-premises subgroups-closed-under-inv)
simplify
simplify
simplify
)))
```

```
(def-compound-macete subgroup-membership
(series
(repeat
subgroups-closed-under-mul
subgroups-closed-under-inv
subgroups-contain-e)
simplify))
```

```
(def-theorem subgroups-are-groups
"forall(a:sets[gg], subgroup(a) implies group{a,mul,e,inv})"
(theory groups)
(usages transportable-macete)
(proof
(
insistent-direct-inference-strategy
(apply-macete-with-minor-premises subgroup-membership)
(apply-macete-with-minor-premises subgroup-membership)
(apply-macete-with-minor-premises subgroup-membership)
simplify
simplify
simplify
simplify
simplify
)))
```

```
(def-theorem groups->subgroup-obl-1
"forall(a:sets[gg],
nonempty_indic_q{a}
and
forall(g,h:gg,g in a and h in a implies (g mul h) in a)
and
forall(g:gg,g in a implies inv(g) in a)
implies
e in a)"
lemma
(theory groups)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent
"with(a:sets[gg], forall(g,h:gg,g in a and h in a implies (g mul h) in a));"
("x" "inv(x)"))
(instantiate-universal-antecedent
"with(a:sets[gg],forall(g:gg,g in a implies inv(g) in a));"
("x"))
(incorporate-antecedent "with(x:gg,a:sets[gg],(x mul inv(x)) in a);")
simplify
)))
```

```
(def-theorem groups->subgroup-obl-2
"forall(a:sets[gg],
nonempty_indic_q{a}
and
forall(g,h:gg,g in a and h in a implies (g mul h) in a)
and
forall(g:gg,g in a implies inv(g) in a)
implies
forall(x:gg,x in a implies if(e in a, x, ?gg)=x))"
lemma
(theory groups)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem groups->subgroup-obl-1 ("a"))
(contrapose "with(a:sets[gg],empty_indic_q{a});")
auto-instantiate-existential
simplify
)))
```

```
(def-translation groups->subgroup
(source groups)
(target groups)
(assumptions
"with(a:sets[gg], nonempty_indic_q{a})"
"with(a:sets[gg], forall(g,h:gg, (g in a) and (h in a) implies (g mul h) in a))"
"with(a:sets[gg], forall(g:gg, (g in a) implies (inv(g) in a)))")
(fixed-theories h-o-real-arithmetic)
(sort-pairs
(gg (indic "with(a:sets[gg], a)")))
(constant-pairs
(mul "with(a:sets[gg], lambda(x,y:gg, if((x in a) and (y in a), x mul y, ?gg)))")
(inv "with(a:sets[gg], lambda(x:gg, if(x in a, inv(x), ?gg)))"))