```(def-language group-action-language
(embedded-language groups-language)
(base-types uu)
(constants
(act "[uu,gg,uu]")))
```

```
(def-theory group-actions
(language group-action-language)
(component-theories groups)
(axioms
(act-id
"forall(alpha:uu,g:gg, act(alpha,e) = alpha)"
rewrite transportable-macete)
(act-associativity
"forall(alpha:uu,g,h:gg, act(alpha,g mul h) = act(act(alpha,g),h))"
transportable-macete)))
```

```
(def-constant orbit
"lambda(alpha:uu, indic{beta:uu, forsome(g:gg, beta = act(alpha,g))})"
(theory group-actions))
```

```
(def-constant stabilizer
"lambda(alpha:uu, indic{g:gg, act(alpha,g)=alpha})"
(theory group-actions))
```

```
(def-theorem act-is-total
"total_q(act,[uu,gg,uu])"
(theory group-actions)
(usages d-r-convergence transportable-macete)
(proof
(
insistent-direct-inference
(instantiate-theorem act-associativity ("x_0" "x_1" "e"))
)))
```

```
(def-theorem orbit-is-total
"total_q(orbit,[uu,sets[uu]])"
(theory group-actions)
(usages d-r-convergence transportable-macete)
(proof
(
(unfold-single-defined-constant-globally orbit)
simplify-insistently
)))
```

```
(def-theorem stabilizer-is-total
"total_q(stabilizer,[uu,sets[gg]])"
(theory group-actions)
(usages d-r-convergence transportable-macete)
(proof
(
(unfold-single-defined-constant-globally stabilizer)
simplify-insistently
)))
```

```
(def-theorem reverse-act-associativity
"forall(alpha:uu,g,h:gg, act(act(alpha,g),h) = act(alpha,g mul h))"
(theory group-actions)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises act-associativity)
simplify
)))
```

```
(def-theorem action-by-stabilizer-member
"forall(alpha:uu,g:gg, g in stabilizer(alpha) implies act(alpha,g)=alpha)"
(theory group-actions)
(usages transportable-macete)
(proof
(
(unfold-single-defined-constant-globally stabilizer)
simplify
)))
```

```
(def-theorem left-act-inv
"forall(alpha:uu,g:gg, act(act(alpha,inv(g)),g) = alpha)"
(theory group-actions)
(usages rewrite transportable-macete)
(proof
(
(apply-macete-with-minor-premises reverse-act-associativity)
simplify
)))
```

```
(def-theorem right-act-inv
"forall(alpha:uu,g:gg, act(act(alpha,g),inv(g)) = alpha)"
(theory group-actions)
(usages rewrite transportable-macete)
(proof
(
(apply-macete-with-minor-premises reverse-act-associativity)
simplify
)))
```

```
(def-compound-macete simplify-actions
(series
(repeat reverse-act-associativity)
simplify))
```

```
(def-translation act->left-mul
(source group-actions)
(target groups)
(fixed-theories h-o-real-arithmetic)
(sort-pairs
(uu "gg"))
(constant-pairs
(mul "lambda(x,y:gg, y mul x)")
(act "lambda(x,y:gg, y mul x)"))
(theory-interpretation-check using-simplification))
```

```
(def-translation act->right-mul
(source group-actions)
(target groups)
(fixed-theories h-o-real-arithmetic)
(sort-pairs
(uu "gg"))
(constant-pairs
(act "mul"))
(theory-interpretation-check using-simplification))
```

```
(def-translation act->conjugate
(source group-actions)
(target groups)
(fixed-theories h-o-real-arithmetic)
(sort-pairs
(uu "gg"))
(constant-pairs
(act "lambda(g,h:gg, (inv(h) mul g) mul h)"))
(theory-interpretation-check using-simplification))
```

```
(def-theorem action-macete
"forall(alpha,beta:uu,g:gg, alpha=beta iff act(alpha,g) = act(beta,g))"
reverse
(theory group-actions)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-theorem act-associativity ("alpha" "g" "inv(g)"))
(contrapose "with(g,h:gg,alpha,beta:uu, act(alpha,g)=act(beta,h))")
(force-substitution "act(alpha,g)" "act(beta,g)" (0))
simplify
)))
```

```
(def-theorem stabilizers-are-subgroups
"forall(alpha:uu, subgroup(stabilizer(alpha)))"
(theory group-actions)
(usages transportable-macete)
(proof
(
unfold-defined-constants
simplify-insistently
direct-and-antecedent-inference-strategy
(instantiate-existential ("e"))
simplify
(apply-macete-with-minor-premises act-associativity)
simplify
(apply-macete-with-minor-premises action-macete)
(instantiate-existential ("g_\$0"))
simplify
)))
```