(def-theorem removing-an-element-from-a-finite-set"forall(s:sets[ind_1], x:ind_1, f_indic_q{s} and x in s implies f_card{s}=f_card{s diff singleton{x}}+1)"(usages transportable-macete) (theory generic-theory-1) (proof ( direct-and-antecedent-inference-strategy (force-substitution"s""(s diff singleton{x}) union singleton{x} "(0)) (move-to-sibling 1) (apply-macete-with-minor-premises tr%diff-union-equal-whole) simplify-insistently (apply-macete-with-minor-premises f-card-disjoint-union) (apply-macete-with-minor-premises singleton-has-f-card-one-rewrite) (cut-with-single-formula"#(f_card{s diff singleton{x}})") simplify (apply-macete-with-minor-premises subset-of-finite-indic-is-finite) (instantiate-existential ("s")) simplify-insistently (apply-macete-with-minor-premises iota-free-definition-of-f-indic-q) (apply-macete-with-minor-premises singleton-has-f-card-one-rewrite) (instantiate-existential ("1")) (apply-macete-with-minor-premises tr%diff-with-indic-is-disj-from-indic) )))

(def-constant maximal"lambda(x:uu,s:sets[uu], x in s and forall(y:uu, y in s and x prec y implies x=y))"(theory partial-order))

(def-theorem finite-sets-have-maximal-elements"forall(s:sets[uu], f_indic_q{s} and nonempty_indic_q{s} implies forsome(x:uu, maximal(x,s)))"(theory partial-order) (usages transportable-macete) (proof ( (apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q) direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(m:zz, 1<=m and n=m)") (move-to-sibling 1) (instantiate-existential ("n")) (backchain-backwards"with(n:nn,n=n);") (force-substitution"1""f_card{singleton{x}}"(0)) (apply-macete-with-minor-premises tr%f-card-leq-iff-finite-and-embeds) (apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q) direct-and-antecedent-inference-strategy (move-to-sibling 1) (apply-macete-with-minor-premises tr%subset-embeds-in-superset) simplify-insistently (instantiate-existential ("n")) (apply-macete-with-minor-premises tr%singleton-has-f-card-one-rewrite) (antecedent-inference"with(p:prop,forsome(m:zz,p));") (incorporate-antecedent"with(n:nn,n=n);") (backchain"with(p:prop,p and p);") (antecedent-inference"with(p:prop,p and p);") (weaken (0)) (weaken (1)) (cut-with-single-formula"forall(s:sets[uu], f_card{s}=m implies forsome(x_$4:uu,maximal(x_$4,s)))") (backchain"with(p:prop,forall(s:sets[uu],p));") (induction trivial-integer-inductor ("m")) beta-reduce-repeatedly (apply-macete-with-minor-premises tr%singleton-has-f-card-one) direct-and-antecedent-inference-strategy (instantiate-existential ("y")) (unfold-single-defined-constant (0) maximal) (backchain"with(p:prop,p);") (backchain"with(p:prop,p);") (apply-macete-with-minor-premises tr%singleton-equality-conversion) simplify (cut-with-single-formula"forsome(x:uu, x in s)") (antecedent-inference"with(s:sets[uu],nonempty_indic_q{s});") (instantiate-universal-antecedent"with(p:prop,forall(s:sets[uu],p));"("s diff singleton{x}")) (contrapose"with(p:prop,not(p));") (cut-with-single-formula"f_card{s}=f_card{s diff singleton{x}}+1") (move-to-sibling 1) (apply-macete-with-minor-premises tr%removing-an-element-from-a-finite-set) simplify (case-split ("x_$9 prec x")) (instantiate-existential ("x")) (unfold-single-defined-constant (0) maximal) direct-and-antecedent-inference-strategy (contrapose"with(f:sets[uu],x_$9:uu,maximal(x_$9,f));") (unfold-single-defined-constant (0) maximal) (contrapose"with(p:prop,not(p));") (antecedent-inference"with(p:prop,p and p);") (contrapose"with(p:prop,forall(y_$0:uu,p));") (instantiate-existential ("y")) simplify-insistently (apply-macete-with-minor-premises prec-transitivity) auto-instantiate-existential (contrapose"with(p:prop,not(p));") (apply-macete-with-minor-premises prec-anti-symmetry) simplify (instantiate-existential ("x_$9")) (incorporate-antecedent"with(f:sets[uu],x_$9:uu,maximal(x_$9,f));") (unfold-single-defined-constant-globally maximal) direct-and-antecedent-inference-strategy (incorporate-antecedent"with(x_$9:uu,f,s:sets[uu],x_$9 in s diff f);") simplify-insistently simplify (backchain"with(p:prop,forall(y_$0:uu,p));") (cut-with-single-formula"not(x=y)") (move-to-ancestor 1) simplify-insistently (simplify-antecedent"with(y,x_$9:uu,x_$9 prec y);") (apply-macete-with-minor-premises tr%rev%positive-f-card-iff-nonempty) simplify )))

(def-transported-symbols (maximal) (translation order-reverse) (renamer third-renamer))

(def-theorem finite-sets-have-minimal-elements"forall(s:sets[uu], f_indic_q{s} and nonempty_indic_q{s} implies forsome(x:uu, minimal(x,s)))"(theory partial-order) (usages transportable-macete) (proof ( (apply-macete-with-minor-premises tr%finite-sets-have-maximal-elements) )))

(def-theory linear-order (component-theories partial-order) (axioms (totality-of-order"forall(a,b:uu, a prec b or b prec a)")))

(def-constant maximum"lambda(x:uu, s:sets[uu], x in s and forall(y:uu, y in s implies y prec x))"(theory partial-order))

(def-theorem maximal-is-maximum"forall(a:uu, s:sets[uu], maximal(a,s) implies maximum(a,s))"(usages transportable-macete) (theory linear-order) (proof ( unfold-defined-constants direct-and-antecedent-inference-strategy (cut-with-single-formula"y prec a or a prec a") (move-to-ancestor 1) (cut-with-single-formula"y prec a or a prec y") (move-to-sibling 1) (apply-macete-with-minor-premises totality-of-order) (antecedent-inference"with(p:prop,p or p);") (instantiate-universal-antecedent"with(p:prop,forall(y:uu,p));"("y")) simplify )))

(def-transported-symbols (maximum) (translation order-reverse) (renamer fourth-renamer))

(def-translation linear-order-reverse (source linear-order) (target linear-order) (core-translation order-reverse) (theory-interpretation-check using-simplification))

(def-theorem minimal-is-minimum"forall(a:uu, s:sets[uu], minimal(a,s) implies minimum(a,s))"(theory linear-order) (proof ( (apply-macete-with-minor-premises tr%maximal-is-maximum) )))

(def-theorem finite-sets-have-maximum-elements"forall(s:sets[uu], f_indic_q{s} and nonempty_indic_q{s} implies forsome(x:uu, maximum(x,s)))"(theory linear-order) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises maximal-is-maximum) (apply-macete-with-minor-premises finite-sets-have-maximal-elements) direct-and-antecedent-inference-strategy (instantiate-existential ("x")) )))

(def-theorem finite-sets-have-minimum-elements"forall(s:sets[uu], f_indic_q{s} and nonempty_indic_q{s} implies forsome(x:uu, minimum(x,s)))"(theory linear-order) (usages transportable-macete) (proof ( (apply-macete-with-minor-premises tr%finite-sets-have-maximum-elements) )))