(def-language pointed-target-space
    (embedded-languages metric-spaces-2-tuples)
    (constants (a_0 pp_1)))

(def-theory pointed-ms-2-tuples 
    (language  pointed-target-space)
    (component-theories  metric-spaces-2-tuples))

(def-translation mappings-pointed-metric-spaces-2-tuples 
    force-under-quick-load
    (source mappings-into-a-pointed-metric-space)
    (target pointed-ms-2-tuples)
    (sort-pairs (ind_1 pp_0) (pp pp_1))
    (constant-pairs (a_0 a_0) (dist dist_1))
    (fixed-theories h-o-real-arithmetic)
    (theory-interpretation-check using-simplification))

(def-transported-symbols (bfun%dist bfun)
    (translation  mappings-pointed-metric-spaces-2-tuples)
    (renamer mappings-to-pointed-target-space-renamer))

(def-theorem ()
    "forall(x,y,z:bfun, bfun%dist(x,z)<=bfun%dist(x,y)+bfun%dist(y,z))"
    lemma
    (home-theory mappings-into-a-pointed-metric-space)
    (translation mappings-pointed-metric-spaces-2-tuples)
    (proof existing-theorem)
    (theory  pointed-ms-2-tuples))

(def-theorem non-negativity-of-distance 
    "forall(x,y:bfun, 0<=bfun%dist(x,y))"
    (home-theory mappings-into-a-pointed-metric-space)
    (translation mappings-pointed-metric-spaces-2-tuples)
    (proof existing-theorem)
    (usages transportable-macete)
    (theory  pointed-ms-2-tuples))

(def-theorem ()
    "forall(x,y:bfun, bfun%dist(x,y)=bfun%dist(y,x))"
    lemma
    (home-theory mappings-into-a-pointed-metric-space)
    (translation mappings-pointed-metric-spaces-2-tuples)
    (proof existing-theorem)
    (theory  pointed-ms-2-tuples))

(def-theorem ()
    "forall(x,y:bfun, x=y iff bfun%dist(x,y)=0)"
    lemma
    (home-theory mappings-into-a-pointed-metric-space)
    (translation mappings-pointed-metric-spaces-2-tuples)
    (proof existing-theorem)
    (theory  pointed-ms-2-tuples))

(def-theory-ensemble-instances
    metric-spaces
    force-under-quick-load
    (permutations (0))
    (sorts (pp ms%bfun))
    (constants (dist ms%bfun%dist))
    (target-theories pointed-ms-2-tuples)
    (special-renamings
      (ball ms%bfun%ball)
      (open%ball ms%bfun%open%ball)
      (complete ms%bfun%complete)
      (lipschitz%bound%on ms%bfun%lipschitz%bound%on)
      (lipschitz%bound ms%bfun%lipschitz%bound)))

(def-theory-ensemble-overloadings metric-spaces (1 2))

(def-overloading dist
    (pointed-ms-2-tuples ms%bfun%dist)
    (metric-spaces dist))