(def-theory-ensemble-multiple metric-spaces 3)

(def-theory-ensemble-instances metric-spaces
  (permutations (0 1) (1 2) (0 2))
  (target-multiple 3))

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

(def-theorem general-composition-of-continuous-functions 
    "forall(f:[pp_0,pp_1],g:[pp_1,pp_2],x:pp_0,continuous%at%point(f,x) and continuous%at%point(g,f(x)) implies continuous%at%point(g oo f,x))"
    (theory metric-spaces-3-tuples)
    (proof
      (
        unfold-defined-constants
        beta-reduce-with-minor-premises
        direct-and-antecedent-inference-strategy
        (auto-instantiate-universal-antecedent "with(p:prop,forall(eps:rr,  0<eps implies p))")
        (instantiate-universal-antecedent "with(p:prop,forall(eps:rr,  0<eps implies p))" ("delta_$0"))
        (instantiate-existential ("delta"))
        (backchain "forall(y_$0:pp_1,dist_1(f(x),y_$0)<=delta_$0
          implies 
        dist_2(g(f(x)),g(y_$0))<=eps_$0)")
        (backchain "forall(y:pp_0,
        dist_0(x,y)<=delta implies dist_1(f(x),f(y))<=delta_$0)")
        (cut-with-single-formula "dist_1(f(x),f(y_$0))<=delta_$0")
        (instantiate-universal-antecedent "with(p:prop, forall(eps:rr, 0<eps implies p))" ("1"))
        (simplify-antecedent "not(0<1);")
        (cut-with-single-formula "dist_1(f(x),f(x))<=1")
        (backchain "forall(y:pp_0,dist_0(x,y)<=delta implies dist_1(f(x),f(y))<=1)")
        (apply-macete-with-minor-premises tr%zero-self-distance)
        simplify
        )
      (usages transportable-macete)))