(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))