```(def-language groups
Remark: This entry is multiply defined. See:  [1] [2]
(embedded-languages monoid-language)
(constants (inv (uu uu ))))
```

```
(def-theory groups
Remark: This entry is multiply defined. See:  [1] [2]
(component-theories monoid-theory)
(language groups)
(axioms
(right-inverse-property "forall(x:uu,x**inv(x)=e)" rewrite)))
```

```
(def-theorem inv-is-total
Remark: This entry is multiply defined. See:  [1] [2]
"total_q(inv,[uu,uu])"
(usages d-r-convergence)
(theory groups)
(proof
(
insistent-direct-inference
(cut-with-single-formula "x_0**inv(x_0)=e")
(apply-macete-with-minor-premises right-inverse-property)
)
))
```

```(def-language normed-groups
(embedded-language groups)
(constants
(norm "[uu,rr]")))
```

```
(def-theory normed-groups
(language normed-groups)
(component-theories groups)
(axioms
(norm-totality
"total_q{norm,[uu, rr]}" d-r-convergence transportable-macete)
(positivity-of-norm
"forall(x:uu, 0<=norm(x))" transportable-macete)
(norm-zero
"forall(x:uu, norm(x)=0 iff x = e)" transportable-macete)
(norm-triangle-inequality
"forall(x,y:uu, norm(x**y) <= norm(x) + norm(y))" transportable-macete)))
```

```(def-theory-ensemble-instances
metric-spaces
(target-theories normed-groups normed-groups)
(multiples 1 2)
(theory-interpretation-check using-simplification)
(sorts (pp uu uu))
(constants (dist "lambda(x,y:uu, norm(x**inv(y)))" "lambda(x,y:uu, norm(x**inv(y)))")))
```