(def-constant monotone 
    "lambda(f:[uu,uu], forall(x,y:uu, x prec y implies f(x) prec f(y)))"
    (theory partial-order))


(def-theorem knaster-fixed-point-theorem 
    "forall(f:[uu,uu], 
                      forsome(bot,top:uu, forall(x:uu, bot prec x and x prec top))
                        and
                      monotone(f)
                        implies
                      forsome(z:uu, f(z)=z))"
    (theory complete-partial-order)
    (usages transportable-macete)
    (proof
      (
        (unfold-single-defined-constant (0) monotone)
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "total_q{f,[uu,uu]} and #(prec%sup(indic{x:uu,  x prec f(x)}))")
        (move-to-sibling 1)
        (block (script-comment "node added by `cut-with-single-formula' at (1)")
	      direct-and-antecedent-inference-strategy
	      (block (script-comment "node added by `direct-and-antecedent-inference-strategy' at (0)")
		    insistent-direct-inference
		    (instantiate-universal-antecedent "with(p:prop,forall(x,y:uu,p));"
						        ("x_0" "x_0"))
		    (contrapose "with(p:prop,not(p));")
		    (apply-macete-with-minor-premises prec-reflexivity))
	      (block (script-comment "node added by `direct-and-antecedent-inference-strategy' at (1)")
		    (apply-macete-with-minor-premises prec%sup-defined)
		    direct-and-antecedent-inference-strategy
		    (block (script-comment "node added by `direct-and-antecedent-inference-strategy' at (0)")
			  (instantiate-existential ("bot"))
			  (apply-macete-with-minor-premises indicator-facts-macete)
			  beta-reduce-repeatedly
			  (backchain "with(p:prop,forall(x:uu,p and p));"))
		    (block (script-comment "node added by `direct-and-antecedent-inference-strategy' at (1 0)")
			  (instantiate-existential ("top"))
			  (unfold-single-defined-constant (0) prec%majorizes)
			  (apply-macete-with-minor-premises indicator-facts-macete)
			  beta-reduce-repeatedly
			  direct-and-antecedent-inference-strategy)))
        (block (script-comment "node added by `cut-with-single-formula' at (0)")
	      (instantiate-existential ("prec%sup(indic{x:uu, x prec f(x)})"))
	      (script-comment "we show x_0 prec f(x_0) and f(x_0) prec x_0 separately.")
	      (apply-macete-with-minor-premises prec-anti-symmetry)
	      (cut-with-single-formula "prec%sup(indic{x:uu,  x prec f(x)})
      prec f(prec%sup(indic{x:uu,  x prec f(x)}))")
	      direct-inference
	      (move-to-ancestor 2)
	      (move-to-descendent (1))
	      (block (script-comment "node added by `cut-with-single-formula' at (1)")
		    (apply-macete-with-minor-premises lub-property-of-prec%sup)
		    direct-inference
		    (unfold-single-defined-constant (0) prec%majorizes)
		    (apply-macete-with-minor-premises indicator-facts-macete)
		    beta-reduce-repeatedly
		    direct-and-antecedent-inference-strategy
		    (apply-macete-with-minor-premises prec-transitivity)
		    auto-instantiate-existential
		    (backchain "with(p:prop,forall(x,y:uu,p));")
		    (apply-macete-with-minor-premises minorizes-property-of-prec%sup)
		    direct-inference
		    (instantiate-existential ("x_$0"))
		    (block (script-comment "node added by `instantiate-existential' at (0 0)")
			  (apply-macete-with-minor-premises indicator-facts-macete)
			  beta-reduce-repeatedly)
		    (apply-macete-with-minor-premises prec-reflexivity))
	      (block (script-comment "node added by `direct-inference' at (0)")
		    (cut-with-single-formula "f(prec%sup(indic{x:uu,  x prec f(x)})) in indic{x:uu,  x prec f(x)}")
		    (cut-with-single-formula "prec%sup(indic{x:uu,  x prec f(x)}) prec f(prec%sup(indic{x:uu,  x prec f(x)}))")
		    (move-to-ancestor 2)
		    (move-to-descendent (1))
		    (block (script-comment "node added by `cut-with-single-formula' at (1)")
			  (apply-macete-with-minor-premises indicator-facts-macete)
			  beta-reduce-repeatedly
			  (backchain "with(p:prop,forall(x,y:uu,p));"))
		    (block (script-comment "node added by `cut-with-single-formula' at (0 (1 . 0))")
			  (apply-macete-with-minor-premises minorizes-property-of-prec%sup)
			  direct-and-antecedent-inference-strategy
			  auto-instantiate-existential
			  (apply-macete-with-minor-premises prec-reflexivity))))
        )))

(def-transported-symbols monotone
    (translation relativize-to-interval)
    (renamer  cpo-to-interval)
    )


(def-theorem relativized-knaster-fixed-point-theorem 
    "forall(f:[uu,uu], 
	        ii%monotone(f)
                        implies
	        forsome(z:ii, f(z)=z))"
    (home-theory interval-in-cpo)
    (theory complete-partial-order)
    (proof
      (
        direct-and-antecedent-inference-strategy
        (instantiate-transported-theorem knaster-fixed-point-theorem
				          relativize-to-interval
				          ("lambda(z:ii,f(z))"))
        (contrapose "with(p:prop,forall(bot,top:ii,p));")
        (label-node l_0)
        (instantiate-existential ("bot" "top"))
        (jump-to-node l_0)
        (for-nodes 
          (unsupported-descendents)
          (if (matches? "with(a:uu,#(a,ii))")
	  (block
	    (apply-macete-with-minor-premises ii-defining-axiom_interval-in-cpo)
	    (apply-macete-with-minor-premises non-triviality)
	    (apply-macete-with-minor-premises prec-reflexivity))
              (block
	(cut-with-single-formula "#(x,ii)")
	(incorporate-antecedent "with(x:ii,#(x,ii));")
	(apply-macete-with-minor-premises ii-defining-axiom_interval-in-cpo)
	direct-and-antecedent-inference-strategy)))
        (contrapose "with(p:prop,not(p));")
        (incorporate-antecedent "with(f:[uu,uu],ii%monotone(f));")
        (weaken (0))
        unfold-defined-constants
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula "#(f,[ii,ii])")
        (beta-reduce-antecedent "with(p:prop,f:[uu,uu], lambda(f:[ii,ii],p) (f));")
        beta-reduce-with-minor-premises
        beta-reduce-repeatedly
        (cut-with-single-formula "forsome(g:[ii,ii],f=g)")
        (move-to-sibling 1)
        (weaken (0))
        (instantiate-existential ("f"))
        (antecedent-inference "with(p:prop,forsome(g:[ii,ii],p));")
        (backchain "with(g:[ii,ii],f:[uu,uu],f=g);")
        (instantiate-existential ("z"))
        (beta-reduce-antecedent "with(z:ii,f:[uu,uu],lambda(z:ii,f(z))(z)=z);")
        (incorporate-antecedent "with(p:prop,p);")
        (unfold-single-defined-constant-globally ii%monotone)
        direct-and-antecedent-inference-strategy)))


(def-theorem knaster-fixed-point-theorem-corollary 
    "forall(top,bot:uu,f:[uu,uu],
          bot prec top
            and 
          bot prec f(bot)
            and 
          f(top) prec top
            and 
          forall(x,y:uu,
              bot prec x
                and 
              x prec top
                and 
              bot prec y
                and 
              y prec top
                and 
              x prec y
                implies 
              f(x) prec f(y))
            implies 
          forsome(z:uu,(bot prec z and z prec top) and f(z)=z))"
    (theory complete-partial-order)
    (usages transportable-macete)
    (proof
      (
        
        direct-and-antecedent-inference-strategy
        (cut-with-single-formula
          "forall(x:uu, bot prec x and x prec top implies bot prec f(x) and f(x) prec top)")
        (let-script
          prove-cut 1
          (
            (apply-macete-with-minor-premises prec-transitivity)
            direct-inference
            (instantiate-existential ((% "f(~a)" $1)))
            (backchain "with(p:prop,forall(x,y:uu,p));")
            simplify
            (apply-macete-with-minor-premises prec-reflexivity)
            (instantiate-universal-antecedent "with(p:prop,forall(x,y:uu,p));" ("x" "x")))
          )
        (move-to-sibling 1)
        direct-and-antecedent-inference-strategy
        ($prove-cut "bot")
        ($prove-cut "top")
        (cut-with-single-formula
          "forsome(z:uu,(bot prec z and z prec top) and
              lambda(z:uu,if(bot prec z and z prec top,f(z),?uu))(z)=z)")
        (instantiate-existential ("z"))
        (contrapose "with(z,u:uu,p:prop,(p and p) and u=z);")
        simplify
        (label-node l_0)
        (apply-macete-with-minor-premises relativized-knaster-fixed-point-theorem)
        direct-and-antecedent-inference-strategy
        (jump-to-node l_0)
        (for-nodes
          (unsupported-descendents)
          simplify)
        
        
        )))