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