(def-translation ind_1->pp 
    force-under-quick-load
    (source generic-theory-1)
    (target metric-spaces)
    (fixed-theories h-o-real-arithmetic)
    (sort-pairs (ind_1 "pp")))

(def-transported-symbols iterate
    (renamer iterate-renamer)
    (translation ind_1->pp))

(def-overloading iterate
    (generic-theory-1 iterate) (metric-spaces ms%iterate))

(def-theorem ()
    iterate-totality
    (theory metric-spaces)
    (translation ind_1->pp)
    (usages d-r-convergence)
    (proof existing-theorem))
(ensemble-dont-translate-constant metric-spaces "ms%iterate")

(def-theorem iterated-distance-bound 
    "forall(f:[pp,pp],x:pp,p:zz,r:rr, 
          lipschitz%bound(f,r) and  0<=p 
            implies 
          dist(iterate(f,x)(p),iterate(f,x)(p+1))<=r^p*dist(x,f(x)))"
    (theory metric-spaces)
    
    (proof
      (
        (unfold-single-defined-constant (0) lipschitz%bound)
        (unfold-single-defined-constant (0) lipschitz%bound%on)
        direct-and-antecedent-inference-strategy
        (induction integer-inductor ("p"))
        (unfold-single-defined-constant (1) ms%iterate)
        simplify
        (instantiate-universal-antecedent "with(r:rr,f:[pp,pp],
    forall(x_$0,y_$0:pp,
        x_$0 in sort_to_indic{pp} and y_$0 in sort_to_indic{pp}
          implies 
        dist(f(x_$0),f(y_$0))<=r*dist(x_$0,y_$0)));" ("iterate(f,x)(t)" "iterate(f,x)(1+t)"))
        (simplify-antecedent "with(p:prop, not(p))")
        (simplify-antecedent "with(p:prop, not(p))")
        (apply-macete-with-minor-premises transitivity-of-<=)
        auto-instantiate-existential
        (apply-macete-with-minor-premises transitivity-of-<=)
        direct-inference
        (instantiate-existential ("dist(x,f(x))*r^t*r"))
        simplify
        simplify
        )))

(def-theorem iterate-sequence-converges 
    "complete implies forall(f:[pp,pp],x:pp ,r:rr,
          lipschitz%bound(f,r) and r<1 
            implies 
          #(lim(iterate(f,x))))"
    (theory metric-spaces)
    (proof
      (
        (apply-macete-with-minor-premises convergence-test-for-complete-spaces)
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("lambda(j:zz,r^j*dist(x,f(x)))" "0"))
        (apply-macete-with-minor-premises geometric-series-is-summable%nonnegative)
        (cut-with-single-formula "total_q{f,[pp,pp]} and 0<r")
        simplify
        (apply-macete-with-minor-premises tr%lipschitz-bound-is-total)
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("r"))
        (incorporate-antecedent "with(r:rr,f:[pp,pp],lipschitz%bound(f,r));")
        (unfold-single-defined-constant (0) lipschitz%bound)
        (unfold-single-defined-constant (0) lipschitz%bound%on)
        simplify
        beta-reduce-repeatedly
        (apply-macete-with-minor-premises iterated-distance-bound)
        simplify
        ))
    )

(def-theorem contractive-mapping-fixed-point-theorem 
    "forall(f:[pp,pp],r:rr, 
          complete and lipschitz%bound(f,r) and r<1 
            implies 
          forsome(x:pp,f(x)=x))"
    (theory metric-spaces)
    (usages transportable-macete)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("lim(iterate(f,x))"))
        (apply-macete-with-minor-premises tr%rev%lim-preservation)
        (apply-macete-with-minor-premises tr%iterate-translate)
        (force-substitution 
          "lambda(n:zz,if(n=[-1], ?pp, iterate(f,x)(n+1)))" 
          "lambda(m:zz, lambda(n:zz,if(n=0, ?pp, iterate(f,x)(n)))(1*m+1))" (0))
        (apply-macete-with-minor-premises limit-translation-invariance)
        (apply-macete-with-minor-premises limit-depends-on-tail)
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("1"))
        simplify
        (apply-macete-with-minor-premises tr%iterate-definedness)
        simplify
        (apply-macete-with-minor-premises tr%lipschitz-bound-is-total)
        (instantiate-existential ("r"))
        (weaken (0))
        (apply-macete-with-minor-premises iterate-sequence-converges)
        (instantiate-existential ("r"))
        (force-substitution "lim(lambda(n:zz,if(n=0, ?pp, iterate(f,x)(n))))" "lim(iterate(f,x))" (0))
        simplify
        (apply-macete-with-minor-premises tr%lipschitz-bound-is-continuous)
        (instantiate-existential ("r"))
        )
      ))

(def-language language-for-ms-closed-ball
    (embedded-languages metric-spaces-language)
    (constants 
      (a pp)
      (r rr)))
            

(def-theory ms-closed-ball 
    (component-theories metric-spaces)
    (language language-for-ms-closed-ball)
    (axioms
      (positivity-of-r "0<=r")))

(def-theorem ()
    "nonempty_indic_q{ball(a,r)}"
    (proof
      (
        (instantiate-existential ("a"))
        (apply-macete-with-minor-premises ball-membership-condition)
        simplify
        ))
    (theory ms-closed-ball))

(def-atomic-sort bb 
    "lambda(x:pp, x in ball(a,r))"
    (theory ms-closed-ball))

(def-theorem bb-sort-characterization 
    "forall(x:bb, dist(a,x)<=r)"
    (proof
      (
        direct-inference
        (instantiate-theorem bb-defining-axiom_ms-closed-ball ("x"))
        (contrapose "with(x:bb,x in ball(a,r));")
        (apply-macete-with-minor-premises ball-membership-condition)
        (contrapose "with(x:bb,not(#(x,bb)));")
        ))
    (usages rewrite)
    (theory ms-closed-ball))

(def-translation ms-subspace-to-ms-closed-ball 
    force-under-quick-load
    (source ms-subspace)
    (target ms-closed-ball)
    (sort-pairs (aa bb))
    (fixed-theories h-o-real-arithmetic)
    (theory-interpretation-check using-simplification))

(def-transported-symbols
    (sub%ball
      sub%open%ball
      sub%lipschitz%bound
      sub%lipschitz%bound%on
      sub%complete
      sub%cauchy
      sub%lim)
    (translation  ms-subspace-to-ms-closed-ball))

(def-theorem () 
    "forall(x,y,z:bb,dist(x,z)<=dist(y,z)+dist(x,y))" 
    lemma
    (theory ms-closed-ball)
    (proof
      (
        (apply-macete-with-minor-premises commutative-law-for-addition)
        (apply-macete-with-minor-premises triangle-inequality-for-distance)
        )))

(def-translation ms-to-ms-closed-ball 
    force-under-quick-load
    (source metric-spaces)
    (target ms-closed-ball)
    (sort-pairs (pp bb))
    (constant-pairs (dist "lambda(x,y:bb, dist(x,y))"))
    (fixed-theories h-o-real-arithmetic)
    (theory-interpretation-check using-simplification))

(def-theorem invariance-of-ball 
    "forall(f:[pp,pp],c:rr,x:pp,
          lipschitz%bound%on(f,c,ball(a,r))
            and 
          dist(a,f(a))<r*(1-c)
            and 
          x in ball(a,r)
            implies 
          f(x) in ball(a,r))"
    (theory ms-closed-ball)
    (proof
      (
        (unfold-single-defined-constant (0) lipschitz%bound%on)
        beta-reduce-with-minor-premises
        (apply-macete-with-minor-premises ball-membership-condition)
        direct-and-antecedent-inference-strategy
        (instantiate-universal-antecedent "with(p:prop,  forall(x,y:pp, p))" ("a" "x"))
        (simplify-antecedent "with(p:prop, not(p))")
        (cut-with-single-formula "dist(a,x)*c<=r*c")
        (apply-macete-with-minor-premises triangle-inequality-alternate-form)
        (instantiate-existential ("f(a)"))
        simplify
        simplify
        (unfold-single-defined-constant (0) ball)
        )
      ))  

(def-theorem lipschitz%bound%on-extends 
    "forall(f:[pp,pp],c:rr, 
          lipschitz%bound%on(f,c,ball(a,r)) and dist(a,f(a))<r*(1-c) 
            implies
          sub%lipschitz%bound(restrict{f,ball(a,r)},c))"
    (theory ms-closed-ball)
    (proof
      (
        (unfold-single-defined-constant (0) sub%lipschitz%bound)
        (unfold-single-defined-constant (0) lipschitz%bound%on)
        (unfold-single-defined-constant (0) sub%lipschitz%bound%on)
        beta-reduce-with-minor-premises
        (apply-macete-with-minor-premises ball-membership-condition)
        direct-and-antecedent-inference-strategy
        simplify-insistently
        (apply-macete-with-minor-premises ball-membership-condition)
        simplify
        (instantiate-universal-antecedent "with(p:prop, forall(x,y:pp,p))" ("x_$2" "y_$1"))
        (simplify-antecedent "with(x_$1:bb,not(dist(a,x_$1)<=r));")
        (simplify-antecedent "with(y_$1:bb,not(dist(a,y_$1)<=r));")
        simplify
        (unfold-single-defined-constant (0) ball)
        sort-definedness
        simplify-insistently
        (apply-macete-with-minor-premises bb-defining-axiom_ms-closed-ball)
        (apply-macete-with-minor-premises invariance-of-ball)
        direct-and-antecedent-inference-strategy
        (instantiate-existential ("c"))
        (unfold-single-defined-constant (0) lipschitz%bound%on)
        )))

(def-theorem restricted-fixed-point-theorem 
    "forall(f:[pp,pp],c:rr, 
          complete and lipschitz%bound%on(f,c,ball(a,r)) and c<1 and dist(a,f(a))<r*(1-c) 
            implies
          forsome(x:bb, f(x)=x))"
    (proof
      (
        
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "forsome(x:bb,restrict{f,ball(a,r)}(x)=x)")
        (block 
          (script-comment "node added by `cut-with-single-formula' at (0)")
          (instantiate-existential ("with(x:bb,x)"))
          (incorporate-antecedent "with(x:bb,p:pp,p=x);")
          simplify-insistently
          (apply-macete-with-minor-premises ball-membership-condition)
          simplify)
        (block 
          (script-comment "node added by `cut-with-single-formula' at (1)")
          (cut-with-single-formula "forsome(h:[bb,bb],restrict{f,ball(a,r)}=h)")
          (block 
            (script-comment "node added by `cut-with-single-formula' at (0)")
            (antecedent-inference "with(p:prop,forsome(h:[bb,bb],p));")
            (backchain "with(h:[bb,bb],f:[pp,pp],f=h);")
            (apply-macete-with-minor-premises tr%contractive-mapping-fixed-point-theorem)
            (instantiate-existential ("c"))
            (block 
              (script-comment "node added by `instantiate-existential' at (0 0)")
              (apply-macete-with-minor-premises tr%rev%completeness-extends)
              direct-and-antecedent-inference-strategy
              (apply-macete-with-minor-premises bb-defining-axiom_ms-closed-ball)
              (apply-macete-with-minor-premises closed-balls-are-closed)
              direct-inference
              simplify-insistently
              direct-and-antecedent-inference-strategy
              (backchain "with(b:bb,x_$0:pp,x_$0=b);")
              (apply-macete-with-minor-premises ball-membership-condition)
              simplify)
            (block 
              (script-comment "node added by `instantiate-existential' at (0 1)")
              (backchain-backwards "with(h:[bb,bb],f:[pp,pp],f=h);")
              (apply-macete-with-minor-premises lipschitz%bound%on-extends)
              direct-and-antecedent-inference-strategy))
          (block 
            (script-comment "node added by `cut-with-single-formula' at (1)")
            (instantiate-existential ("restrict{f,ball(a,r)}"))
            sort-definedness
            (apply-macete-with-minor-premises bb-defining-axiom_ms-closed-ball)
            direct-and-antecedent-inference-strategy
            (block 
              (script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 0 0)")
              (incorporate-antecedent "with(p:pp,#(p));")
              simplify-insistently)
            (block 
              (script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 0 1)")
              (force-substitution "restrict{f,ball(a,r)}(xx_0)"
			      "f(xx_0)"
			      (0))
              (block 
	(script-comment "node added by `force-substitution' at (0)")
	(apply-macete-with-minor-premises invariance-of-ball)
	(instantiate-existential ("c")))
              simplify)))
        )
      )
    (home-theory ms-closed-ball)
    (theory metric-spaces)
    (usages transportable-macete))