(def-theorem induction-in-cpos"forall(s:sets[uu],a:uu, a in s and forall(t:sets[uu], a in t and t subseteq s and #(prec%sup(t)) implies prec%sup(t) in s) and forall(y,z:uu, y in s and a prec y and y prec z and not(z=y) implies forsome(y_0:uu, y_0 in s and y_0 prec z and y prec y_0 and not(y=y_0))) implies forall(x:uu,a prec x implies x in s))"(theory complete-partial-order) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (script-comment"after breaking up the logical structure of the expression, we have to show that a fixed x belongs to s provided the assumptions on s hold and a prec s.") (instantiate-universal-antecedent"with(p:prop,forall(t:sets[uu],p));"("indic{w:uu, w in s and a prec w and w prec x}")) (block (script-comment"contraposition to show antecedent of instantiated assumption holds.") (contrapose"with(p:prop,not(p));") simplify-insistently (apply-macete-with-minor-premises prec-reflexivity) ) (block (script-comment"contraposition for a similar reason.") (contrapose"with(x_$0:uu,f:[uu,prop],x_$0 in pred_to_indic(f));") simplify-insistently) (block (contrapose"with(p:prop,not(p));") (apply-macete-with-minor-premises prec%sup-defined) direct-and-antecedent-inference-strategy (instantiate-existential ("a")) (unfold-single-defined-constant (0) prec%majorizes) simplify-insistently (instantiate-existential ("x"))) (block (instantiate-universal-antecedent"with(p:prop,forall(y,z:uu,p));"("prec%sup(indic{w:uu, w in s and a prec w and w prec x})""x")) (contrapose"with(p:prop,not(p));") (apply-macete-with-minor-premises minorizes-property-of-prec%sup) simplify-insistently (instantiate-existential ("a")) (apply-macete-with-minor-premises prec-reflexivity) (contrapose"with(p:prop,not(p));") (apply-macete-with-minor-premises lub-property-of-prec%sup) direct-and-antecedent-inference-strategy (unfold-single-defined-constant-globally prec%majorizes) simplify-insistently simplify (contrapose"with(p:prop,not(p));") (apply-macete-with-minor-premises prec-anti-symmetry) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises minorizes-property-of-prec%sup) direct-and-antecedent-inference-strategy (instantiate-existential ("y_$0")) simplify-insistently (apply-macete-with-minor-premises prec-transitivity) (instantiate-existential ("prec%sup(indic{w:uu, w in s and a prec w and w prec x})")) (apply-macete-with-minor-premises minorizes-property-of-prec%sup) direct-and-antecedent-inference-strategy simplify-insistently (instantiate-existential ("a")) (apply-macete-with-minor-premises prec-reflexivity) (apply-macete-with-minor-premises prec-reflexivity) ) )))

(def-theorem induction-principle-for-cpos"forall(p:[uu,prop],a,b:uu, a prec b implies forall(x:uu,a prec x and x prec b implies p(x)) iff (p(a) and (forall(t:sets[uu], a in t and t subseteq indic{x:uu, a prec x and x prec b and p(x)} implies p(prec%sup(t))) and forall(y,z:uu, p(y) and a prec y and y prec z and not(z=y) and z prec b implies forsome(y_0:uu, p(y_0) and y_0 prec z and y prec y_0 and not(y=y_0))))))"(theory complete-partial-order) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (backchain"with(p:prop,forall(x:uu,p));") direct-inference (apply-macete-with-minor-premises prec-reflexivity) (cut-with-single-formula"#(prec%sup(t))") (move-to-sibling 1) (apply-macete-with-minor-premises prec%sup-defined) direct-and-antecedent-inference-strategy (instantiate-existential ("a")) (instantiate-existential ("b")) (unfold-single-defined-constant (0) prec%majorizes) direct-and-antecedent-inference-strategy (incorporate-antecedent"with(f,t:sets[uu],t subseteq f);") simplify-insistently (backchain"forall(x:uu, with(p:prop,p and p) implies with(p:[uu,prop],p(x)));") direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises minorizes-property-of-prec%sup) direct-inference (instantiate-existential ("a")) (apply-macete-with-minor-premises lub-property-of-prec%sup) direct-and-antecedent-inference-strategy (unfold-single-defined-constant (0) prec%majorizes) direct-and-antecedent-inference-strategy (incorporate-antecedent"with(f,t:sets[uu],t subseteq f);") simplify-insistently (instantiate-existential ("z")) (backchain"with(p:prop,forall(x:uu,p));") direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises prec-transitivity) (instantiate-existential ("y")) (apply-macete-with-minor-premises prec-reflexivity) simplify (script-comment"this ends the proof in one direction.") (cut-with-single-formula"x in indic{x:uu, a prec x and (x prec b implies p(x))}") (incorporate-antecedent"with(x:uu,f:sets[uu],x in f);") simplify-insistently (apply-macete-with-minor-premises induction-in-cpos) simplify-insistently (instantiate-existential ("a")) (apply-macete-with-minor-premises prec-reflexivity) (apply-macete-with-minor-premises minorizes-property-of-prec%sup) direct-inference (instantiate-existential ("a")) (backchain"with(p:prop,forall(t:sets[uu],p));") direct-and-antecedent-inference-strategy simplify-insistently direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises prec-transitivity) (instantiate-existential ("prec%sup(t_$1)")) (apply-macete-with-minor-premises minorizes-property-of-prec%sup) direct-and-antecedent-inference-strategy (instantiate-existential ("x_$0")) (apply-macete-with-minor-premises prec-reflexivity) (backchain"with(p:prop,p and p and p);") direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop,forall(y,z:uu,p));"("y_$3""z_$1")) (instantiate-existential ("z_$1")) (apply-macete-with-minor-premises prec-transitivity) (instantiate-existential ("y_$3")) (antecedent-inference-strategy (3)) (contrapose"with(b,y_$3:uu,not(y_$3 prec b));") (apply-macete-with-minor-premises prec-transitivity) (instantiate-existential ("z_$1")) (apply-macete-with-minor-premises prec-reflexivity) simplify (instantiate-existential ("z_$1")) (apply-macete-with-minor-premises prec-transitivity) (instantiate-existential ("y_$3")) (apply-macete-with-minor-premises prec-reflexivity) simplify (instantiate-existential ("y_0")) (apply-macete-with-minor-premises prec-transitivity) (instantiate-existential ("y_$3")) )) )