```
(def-translation ind_1->pp
(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
(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 triangle-inequality-for-distance)
)))
```

```
(def-translation ms-to-ms-closed-ball
(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))
```