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