(def-theorem uniform-continuity-is-closed-under-uniform-limits 
    "forall(s:[zz,ms%bfun],x:pp_0,
          forsome(m:zz,
              forall(n:zz,
                  m<=n
                    implies 
                    uniformly%continuous(s(n))))
            and 
          #(lim(s))
            implies 
          uniformly%continuous(lim(s)))"
    (usages transportable-macete)
    (theory pointed-ms-2-tuples)
    (proof
      (
        
        (force-substitution "uniformly%continuous(s(n))" "total_q{s(n),[pp_0,pp_1]} and uniformly%continuous(s(n))" (0))
        (unfold-single-defined-constant (0 1) uniformly%continuous)
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "lim(s)=lim(s)")
        (incorporate-antecedent "with(s:[zz,ms%bfun],lim(s)=lim(s));")
        (apply-macete-with-minor-premises tr%characterization-of-limit)
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent "with(p:prop, forall(eps:rr,0<eps implies p))" ("eps/3"))
        (simplify-antecedent "with(p:prop, not(p))")
        (instantiate-universal-antecedent "with(eps:rr,s:[zz,ms%bfun],n_$0:zz,
    forall(p_$0:zz,
        n_$0<=p_$0 implies dist(lim(s),s(p_$0))<=eps/3));" ("max(n_$0,m)"))
        (contrapose "with(p:prop, not(p))")
        (apply-macete-with-minor-premises maximum-1st-arg)
        (instantiate-universal-antecedent "with(m:zz, p:prop,  forall(n:zz,  m<=n implies p))" ("max(n_$0,m)"))
        (contrapose "with(p:prop, not(p))")
        (apply-macete-with-minor-premises maximum-2nd-arg)
        (instantiate-universal-antecedent "with(p:prop, forall(eps:rr,  0<eps implies p))" ("eps/3"))
        (simplify-antecedent "with(p:prop, not(p))")
        (instantiate-existential ("delta_$0"))
        (instantiate-universal-antecedent "with(p:prop, forall(x,y:pp_0, p))" ("x" "y"))
        (contrapose "with(x:pp_0,m,n_$0:zz,s:[zz,ms%bfun],
    not(#(s(max(n_$0,m))(x))));")
        (contrapose "with(y:pp_0,m,n_$0:zz,s:[zz,ms%bfun],
    not(#(s(max(n_$0,m))(y))));")
        (cut-with-single-formula "dist_1(lim(s)(x),lim(s)(y))<=dist_1(lim(s)(x),s(max(n_$0,m))(x))
+dist_1(s(max(n_$0,m))(x),s(max(n_$0,m))(y))+dist_1(lim(s)(y),s(max(n_$0,m))(y)) and forall(x:
pp_0, dist_1(lim(s)(x),s(max(n_$0,m))(x))<=dist(lim(s),s(max(n_$0,m))))")
        (antecedent-inference "with(p,q:prop, p and q)")
        (instantiate-universal-antecedent-multiply 
          "with(r:rr,forall(x:pp_0,r<=r));"
          (("x") ("y")))
        simplify
        direct-and-antecedent-inference-strategy
        (weaken (0 2 4 6))
        (cut-with-single-formula "total_q{dist_1,[pp_1,pp_1,rr]} and forall(x,y,z,u:pp_1, dist_1(x,u)
<=dist_1(x,y)+dist_1(y,z)+dist_1(u,z))")
        (backchain "with(q,p:prop,q and p)")
        (weaken (0 1 2))
        direct-and-antecedent-inference-strategy
        insistent-direct-inference
        (cut-with-single-formula "0<=dist_1(x_0,x_1)")
        (apply-macete-with-minor-premises tr%positivity-of-distance)
        (apply-macete-with-minor-premises tr%triangle-inequality-alternate-form)
        (instantiate-existential ("y"))
        simplify
        (apply-macete-with-minor-premises tr%triangle-inequality-alternate-form)
        (instantiate-existential ("z"))
        simplify
        (apply-macete-locally tr%symmetry-of-distance (0) " dist_1(z,u) ")
        simplify
        (apply-macete-with-minor-premises tr%bounded-bfun%dist)
        direct-and-antecedent-inference-strategy
        insistent-direct-inference
        (apply-macete-with-minor-premises tr%bfun-values-defined-lemma)
        )
      ))

(def-theorem ()
    "lambda(s:ms%bfun, uniformly%continuous(s))(lambda(x:pp_0,a_0))"
    (proof
      (
        (unfold-single-defined-constant (0) uniformly%continuous)
        beta-reduce-with-minor-premises
        beta-reduce-repeatedly
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises tr%zero-self-distance)
        simplify
        (instantiate-existential ("1"))
        simplify
        (apply-macete-with-minor-premises ms%bfun-defining-axiom_pointed-ms-2-tuples)
        insistent-direct-inference-strategy
        simplify
        (apply-macete-with-minor-premises tr%prec%sup-defined)
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises tr%non-empty-range)
        (instantiate-existential ("x_$0"))
        simplify-insistently
        (apply-macete-with-minor-premises tr%zero-self-distance)
        (instantiate-existential ("0"))
        (unfold-single-defined-constant (0) majorizes)
        simplify-insistently
        (apply-macete-with-minor-premises tr%zero-self-distance)
        simplify
        )
      )
    (theory pointed-ms-2-tuples))

(def-atomic-sort unif%continuous%bfun 
    "lambda(s:ms%bfun, uniformly%continuous(s))"
    (theory pointed-ms-2-tuples)
    (witness "lambda(x:pp_0,a_0)"))

(def-theorem ()
    "forall(x,y,z:unif%continuous%bfun, dist(x,z)<=dist(y,z)+dist(x,y))"
    (theory pointed-ms-2-tuples)
    (proof
      (
        (apply-macete-with-minor-premises commutative-law-for-addition)
        (apply-macete-with-minor-premises tr%triangle-inequality-for-distance)
        )))

(def-theory-ensemble-instances
    metric-spaces 
    force-under-quick-load
    (target-theories pointed-ms-2-tuples)
    (multiples 1)
    (theory-interpretation-check using-simplification)
    (sorts (pp unif%continuous%bfun))
    (constants (dist "lambda(f,g: unif%continuous%bfun, ms%bfun%dist(f,g))"))
    (special-renamings 
      (ball ucbfun%ball)
      (open%ball ucbfun%open%ball)
      (lipschitz%bound ucbfun%lipschitz%bound)
      (lipschitz%bound%on ucbfun%lipschitz%bound%on)
      (complete ucbfun%complete)
      (cauchy ucbfun%cauchy)
      (lim ucbfun%lim)))

(def-translation subspaces-to-uc-function-subspace 
    force-under-quick-load
    (source ms-subspace)
    (target pointed-ms-2-tuples)
    (fixed-theories h-o-real-arithmetic)
    (sort-pairs (aa unif%continuous%bfun) (pp ms%bfun))
    (constant-pairs (dist ms%bfun%dist))
    (theory-interpretation-check using-simplification))

(def-theorem uniformly%continuous%bfun%complete 
    "complete_1 implies ucbfun%complete"
    
    (proof
      (
        (apply-macete-with-minor-premises tr%rev%completeness-extends)
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises tr%limit-definedness-extends)
        (apply-macete-with-minor-premises unif%continuous%bfun-defining-axiom_pointed-ms-2-tuples)
        beta-reduce-repeatedly
        (apply-macete-with-minor-premises tr%rev%limit-definedness-extends)
        (apply-macete-with-minor-premises uniform-continuity-is-closed-under-uniform-limits)
        direct-and-antecedent-inference-strategy
        (incorporate-antecedent "with(t:unif%continuous%bfun,#(t))")
        (apply-macete-with-minor-premises tr%existence-of-limit)
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent "with(p:prop, forall(eps:rr, 0<eps implies p))" ("1"))
        (simplify-antecedent "with(p:prop,not(p))")
        (instantiate-existential ("n_$0"))
        insistent-direct-inference-strategy
        (cut-with-single-formula "forsome(f:ms%bfun,f=s(n))")
        (antecedent-inference "with(p:prop, forsome(f:ms%bfun,p))")
        (backchain-backwards "with(f,g: ms%bfun, f=g)")
        (apply-macete-with-minor-premises unif%continuous%bfun-in-quasi-sort_pointed-ms-2-tuples)
        (instantiate-existential ("s(n)"))
        (instantiate-universal-antecedent "with(p:prop, forall(n:zz,p))" ("n"))
        (instantiate-universal-antecedent "with(p:prop, forall(n:zz,p))" ("n"))
        (apply-macete-with-minor-premises tr%limit-definedness-extends)
        (apply-macete-with-minor-premises tr%bfun-completeness)
        ))
    (usages transportable-macete)
    (theory pointed-ms-2-tuples))