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