(def-constant mu"lambda(f:[pp->pp], iota(x:pp, f(x)=x))"(theory metric-spaces))

(def-constant contraction"lambda(f: [pp -> pp], forsome(r:rr, 0<r and r<1 and forall(x,y:pp, x in dom{f} and y in dom{f} implies dist(f(x),f(y))<=r*dist(x,y))))"(theory metric-spaces))

(def-theorem iota-free-characterization-of-mu"forall(f:[pp->pp], r:rr, x:pp, contraction(f) implies (mu(f)=x iff f(x)=x))"(theory metric-spaces) (proof ( unfold-defined-constants direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0 0)") (contrapose"with(x,p:pp,p=x);") (apply-macete-with-minor-premises eliminate-iota-macete) (contrapose"with(p:prop,not(p));")) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 0 0)") (apply-macete-with-minor-premises eliminate-iota-macete) direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop,forall(x,y:pp,p));"("b""x")) (simplify-antecedent"with(p:prop,not(p));") (simplify-antecedent"with(p:prop,not(p));") (block (script-comment"`instantiate-universal-antecedent' at (0 0 1)") (contrapose"with(r:rr,r<=r);") (backchain"with(b:pp,f:[pp,pp],f(b)=b);") (backchain"with(x:pp,f:[pp,pp],f(x)=x);") (contrapose"with(p:prop,not(p));") (apply-macete-with-minor-premises point-separation-for-distance) (simplify-antecedent"with(r:rr,r<=r);"))))))

(def-theorem definedness-of-mu-for-contractions"forall(f:[pp->pp], complete and contraction(f) and total_q{f,[pp->pp]} implies #(mu(f)))"(theory metric-spaces) (usages transportable-macete) (proof ( (unfold-single-defined-constant (0) contraction) direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(x:pp, mu(f)=x)") (antecedent-inference"with(p:prop,forsome(x:pp,p));") (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises iota-free-characterization-of-mu) (block (script-comment"`apply-macete-with-minor-premises' at (0)") (apply-macete-with-minor-premises contractive-mapping-fixed-point-theorem) (instantiate-existential ("r")) (unfold-single-defined-constant (0) lipschitz%bound) (unfold-single-defined-constant (0) lipschitz%bound%on) direct-and-antecedent-inference-strategy simplify) (block (script-comment"`apply-macete-with-minor-premises' at (1)") (unfold-single-defined-constant-globally contraction) auto-instantiate-existential)) )))

(def-theory-ensemble-instances metric-spaces force-under-quick-load (permutations (0)) (sorts (pp bfun)) (constants (dist bfun%dist)) (target-theories mappings-into-a-pointed-metric-space) (special-renamings (ball bfun%ball) (complete bfun%complete) (lipschitz%bound%on bfun%lipschitz%bound%on) (lipschitz%bound bfun%lipschitz%bound)))

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

(def-theorem definedness-of-mu-for-contractions-on-functions"forall(f:[bfun->bfun], complete and contraction(f) and total_q{f,[bfun->bfun]} implies #(mu(f)))"(theory mappings-into-a-pointed-metric-space) (proof ( (apply-macete-with-minor-premises tr%definedness-of-mu-for-contractions) (apply-macete-with-minor-premises bfun-completeness) )))

(def-theorem condition-for-contractions-on-function-spaces"forall(f:[bfun->bfun], forsome(k:rr,0<k and k<1 and forall(phi,psi:bfun, x:ind_1, forsome(y:ind_1, dist(f(phi)(x),f(psi)(x))<=k*dist(phi(y),psi(y))))) implies contraction(f))"(theory mappings-into-a-pointed-metric-space) (proof ( direct-and-antecedent-inference-strategy (unfold-single-defined-constant-globally contraction_0) (instantiate-existential ("k")) (unfold-single-defined-constant-globally bfun%dist) beta-reduce-with-minor-premises (move-to-sibling 1) (instantiate-universal-antecedent"with(p:prop,forall(phi,psi:bfun,x:ind_1,p));"("y""y""with(x:ind_1,x)")) (move-to-sibling 2) (instantiate-universal-antecedent"with(p:prop,forall(phi,psi:bfun,x:ind_1,p));"("x""x""with(x:ind_1,x)")) (block (script-comment"`beta-reduce-with-minor-premises' at (0)") (apply-macete-with-minor-premises tr%lub-property-of-prec%sup) direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0)") (apply-macete-with-minor-premises tr%prec%majorizes%characterization) (block (script-comment"`apply-macete-with-minor-premises' at (0)") beta-reduce-with-minor-premises direct-and-antecedent-inference-strategy (cut-with-single-formula"k^(-1)*dist(f(x)(n_$0),f(y)(n_$0)) <=sup(ran{lambda(x_$0:ind_1,dist(x(x_$0),y(x_$0)))})") (block (script-comment"`cut-with-single-formula' at (0)") (incorporate-antecedent"with(r:rr,r<=r);") (apply-macete-with-minor-premises fractional-expression-manipulation) simplify) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises tr%minorizes-property-of-prec%sup) (instantiate-universal-antecedent"with(p:prop,forall(phi,psi:bfun,x:ind_1,p));"("x""y""n_$0")) direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0)") (instantiate-existential ("dist(x(y_$0),y(y_$0))")) (block (script-comment"`instantiate-existential' at (0 0)") simplify-insistently (instantiate-existential ("y_$0"))) (block (script-comment"`instantiate-existential' at (0 1)") (incorporate-antecedent"with(r:rr,r<=r);") (apply-macete-with-minor-premises fractional-expression-manipulation) simplify)) (block (script-comment"`direct-and-antecedent-inference-strategy' at (1 0 0)") (cut-with-single-formula"#(bfun%dist(x,y))") (weaken (7 6 5 4 3 2 1)) (incorporate-antecedent"with(p:prop,p);") (unfold-single-defined-constant-globally bfun%dist)))) (block (script-comment"`apply-macete-with-minor-premises' at (1)") (cut-with-single-formula"#(bfun%dist(x,y))") (weaken (3 2 1 4)))) (block (script-comment"`direct-and-antecedent-inference-strategy' at (1)") (cut-with-single-formula"#(bfun%dist(f(x),f(y)))") (block (script-comment"`cut-with-single-formula' at (0)") (weaken (5 4 3 1)) (incorporate-antecedent"with(r:rr,#(r));") (unfold-single-defined-constant-globally bfun%dist) beta-reduce-with-minor-premises (block (script-comment"`beta-reduce-with-minor-premises' at (1)") (simplify-antecedent"with(p:prop,p);")) (simplify-antecedent"with(p:prop,p);")) (block (script-comment"`cut-with-single-formula' at (1)") (cut-with-single-formula"with(x,y:bfun,n:ind_1,dist(f(x)(n),f(y)(n))<=bfun%dist(f(x),f(y)))") (apply-macete-with-minor-premises bounded-bfun%dist)))) )))