(def-constant ff%dist"lambda(f,g:ff, fn%dist(f,g))"(theory graded-monoid))

(def-theorem ff%dist-is-bounded"forall(f,g:ff, ff%dist(f,g)<=1)"(theory graded-monoid) (proof ( direct-and-antecedent-inference-strategy (unfold-single-defined-constant-globally ff%dist) (cut-with-single-formula"forsome(f_1,g_1:total%fns, f=f_1 and g=g_1)") (block (script-comment"`cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,p);") (backchain"with(p:prop,p);") (backchain"with(p:prop,p);") (weaken (0)) (apply-macete-with-minor-premises tr%fn%dist-is-bounded)) (instantiate-existential ("f""g")) )))

(def-theorem stop-is-in-ff"#(stop_ff,ff)"(theory graded-monoid) lemma (proof ( (apply-macete-with-minor-premises ff-defining-axiom_directed-monoid-theory) (apply-macete-with-minor-premises stop-is-a-failure) )))

(def-theorem positivity-of-ff%dist"forall(x,y:ff,0<=ff%dist(x,y))"lemma (theory graded-monoid) (proof ( (unfold-single-defined-constant-globally ff%dist) (apply-macete-with-minor-premises graded-monoid-fn%dist-non-negative) )))

(def-theorem ()"forall(x,y:ff,x=y iff ff%dist(x,y)=0)"(theory graded-monoid) lemma (proof ( (unfold-single-defined-constant-globally ff%dist) (apply-macete-with-minor-premises graded-monoid-fn%dist-reflexive) )))

(def-theorem ()"forall(x,y:ff,ff%dist(x,y)=ff%dist(y,x))"(theory graded-monoid) lemma (proof ( (unfold-single-defined-constant-globally ff%dist) (apply-macete-locally graded-monoid-fn%dist-symmetric (0)"fn%dist(x,y)") simplify direct-and-antecedent-inference-strategy (cut-with-single-formula"0<=fn%dist(y,x)") (apply-macete-with-minor-premises graded-monoid-fn%dist-non-negative) )))

(def-theorem ()"forall(x,y,z:ff,ff%dist(x,z)<=ff%dist(x,y)+ff%dist(y,z))"(theory graded-monoid) lemma (proof ( (unfold-single-defined-constant-globally ff%dist) (apply-macete-with-minor-premises graded-monoid-fn%dist-triangle-inequality) )))

(def-translation pointed-metric-space-to-graded-monoid force-under-quick-load (source pointed-metric-spaces) (target graded-monoid) (fixed-theories h-o-real-arithmetic) (sort-pairs (pp ff)) (constant-pairs (a_0 stop_ff) (dist ff%dist)) (theory-interpretation-check using-simplification))

(def-transported-symbols (complete cauchy lim) (translation pointed-metric-space-to-graded-monoid) (renamer pms-to-gm) )

(def-theorem ff-completeness"ff%complete"(theory graded-monoid) (proof ( (cut-with-single-formula"sub%complete") (move-to-sibling 1) (apply-macete-with-minor-premises completeness-of-ff) (block (script-comment"`cut-with-single-formula' at (0)") (incorporate-antecedent"sub%complete;") unfold-defined-constants unfold-defined-constants (unfold-single-defined-constant-globally ff%dist)) )))

(def-theory parametrized-graded-monoid (component-theories graded-monoid generic-theory-1))

(def-theorem ()"forsome(h:[ind_1,ff],total_q{h,[ind_1,ff]})"(theory parametrized-graded-monoid) (proof ( (instantiate-existential ("with(f:ff, lambda(x:ind_1,f))")) simplify-insistently )))

(def-theorem ()"forall(h:[ind_1,ff], total_q{h,[ind_1,ff]} iff (total_q{h,[ind_1,ff]} and #(sup(lambda(a:rr, if(forsome(u:ind_1, a=ff%dist(stop_ff,h(u))), an%individual, ?unit%sort))))))"(theory parametrized-graded-monoid) lemma (proof ( direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises tr%prec%sup-defined) direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0)") simplify-insistently (instantiate-existential ("with(u:ind_1, ff%dist(stop_ff,h(u)))")) (block (script-comment"`instantiate-existential' at (0)") (instantiate-existential ("u")) (cut-with-single-formula"0<=ff%dist(stop_ff,h(u))") (apply-macete-with-minor-premises positivity-of-ff%dist) (apply-macete-with-minor-premises stop-is-in-ff)) (cut-with-single-formula"0<=ff%dist(stop_ff,h(u))")) (block (script-comment"`direct-and-antecedent-inference-strategy' at (1 0)") (instantiate-existential ("1")) (unfold-single-defined-constant-globally majorizes) simplify-insistently direct-and-antecedent-inference-strategy (backchain"with(r,x_$0:rr,x_$0=r);") (apply-macete-with-minor-premises ff%dist-is-bounded)) )))

(def-translation mappings-into-a-pointed-metric-space-to-parametrized-graded-monoid force-under-quick-load (source mappings-into-a-pointed-metric-space) (target parametrized-graded-monoid) (fixed-theories h-o-real-arithmetic) (sort-pairs (bfun (pred"lambda(x:[ind_1, ff], total_q{x,[ind_1 -> ff]})"))) (core-translation pointed-metric-space-to-graded-monoid) (theory-interpretation-check using-simplification))

(def-transported-symbols (bfun%dist) (translation mappings-into-a-pointed-metric-space-to-parametrized-graded-monoid) (renamer mpms-to-pgm) )

(def-theorem ()"forall(x,y,z:bfun, bfun%dist(x,z)<=bfun%dist(x,y)+bfun%dist(y,z))"lemma (theory parametrized-graded-monoid) (translation mappings-into-a-pointed-metric-space-to-parametrized-graded-monoid) (proof existing-theorem))

(def-theorem ()"forall(x,y:bfun, 0<=bfun%dist(x,y))"lemma (theory parametrized-graded-monoid) (translation mappings-into-a-pointed-metric-space-to-parametrized-graded-monoid) (proof existing-theorem))

(def-theorem ()"forall(x,y:bfun, bfun%dist(x,y)=bfun%dist(y,x))"lemma (theory parametrized-graded-monoid) (translation mappings-into-a-pointed-metric-space-to-parametrized-graded-monoid) (proof existing-theorem))

(def-theorem ()"forall(x,y:bfun, x=y iff bfun%dist(x,y)=0)"lemma (theory parametrized-graded-monoid) (translation mappings-into-a-pointed-metric-space-to-parametrized-graded-monoid) (proof existing-theorem))

(def-theorem ()"forall(f,g:[ind_1,ff], #(ff%dist_p(f,g)) implies total_q{f,[ind_1,ff]} and total_q{g,[ind_1,ff]})"lemma (theory parametrized-graded-monoid) (proof ( (unfold-single-defined-constant-globally ff%dist_p) simplify )))

(def-theory-ensemble-instances metric-spaces force-under-quick-load (permutations (0) (0 1)) (sorts (pp (pred"lambda(x:[ind_1, ff], total_q{x,[ind_1 -> ff]})") (pred"lambda(x:[ind_1, ff], total_q{x,[ind_1 -> ff]})"))) (constants (dist ff%dist_p ff%dist_p)) (target-theories parametrized-graded-monoid parametrized-graded-monoid) (special-renamings (complete ff%complete_p) (contraction ff%contraction_p) (mu ff%mu_p)))

(def-theorem parametrized-completeness"ff%complete_p"(theory parametrized-graded-monoid) (proof ( (assume-transported-theorem bfun-completeness mappings-into-a-pointed-metric-space-to-parametrized-graded-monoid) (backchain"with(p:prop,p);") (apply-macete-with-minor-premises ff-completeness) )))

(def-theorem parametrized-definedness-of-mu-for-contractions-lemma definedness-of-mu-for-contractions lemma (theory parametrized-graded-monoid) (translation metric-spaces-to-parametrized-graded-monoid) (proof existing-theorem))

(def-theorem parametrized-condition-for-contractions-on-function-spaces-lemma condition-for-contractions-on-function-spaces lemma (theory parametrized-graded-monoid) (translation mappings-into-a-pointed-metric-space-to-parametrized-graded-monoid) (proof existing-theorem))

(def-atomic-sort ff_p"lambda(x:[ind_1, ff], total_q{x,[ind_1 -> ff]})"(theory parametrized-graded-monoid))

(def-theorem parametrized-definedness-of-mu-for-contractions"forall(f:[ff_p->ff_p], ff%contraction_p(f) and total_q{f,[ff_p->ff_p]} implies #(ff%mu_p(f)))"(theory parametrized-graded-monoid) (proof ( (unfold-single-defined-constant-globally ff%contraction_p) simplify-insistently direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises parametrized-definedness-of-mu-for-contractions-lemma) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises parametrized-completeness) (block (script-comment"`direct-and-antecedent-inference-strategy' at (2)") (unfold-single-defined-constant-globally ff%contraction_p) simplify-insistently auto-instantiate-existential) (backchain"with(f:[ff_p,ff_p],total_q{f,[ff_p,ff_p]});") )))