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