(def-script set-equality-script 0 ( (label-node top) (apply-macete-with-minor-premises tr%subseteq-antisymmetry) direct-inference (jump-to-node top) (for-nodes (unsupported-descendents) (block insistent-direct-inference (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly)) ))

(def-script set-containment-script 0 ( insistent-direct-inference (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly ))

(def-theorem equality-of-conditional-term"forall(x,y:ind_1,p:prop, if(p,x,?ind_1)=y iff (p and x=y))"(proof ( (raise-conditional (0)) )) (theory pure-generic-theory-1) (usages transportable-macete))

(def-theorem equality-of-conditional-term-backwards"forall(x,y:ind_1,p:prop, y=if(p,x,?ind_1) iff (p and x=y))"(proof ( (force-substitution"y=if(p,x,?ind_1)""if(p,x,?ind_1)=y"(0)) (move-to-sibling 1) direct-and-antecedent-inference-strategy (raise-conditional (0)) )) (theory pure-generic-theory-1) (usages transportable-macete))

(def-theorem indic-free-characterization-of-dom"forall(f:[ind_1,ind_2], a:sets[ind_1], dom{f}=a iff forall(x:ind_1, x in a iff #(f(x))))"(theory pure-generic-theory-2) (usages transportable-macete) (proof ( (apply-macete-with-minor-premises rev%domain-membership-iff-defined) (apply-macete-with-minor-premises tr%subseteq-antisymmetry) direct-and-antecedent-inference-strategy simplify simplify simplify-insistently simplify-insistently )))

(def-theorem indic-free-characterization-of-ran"forall(f:[ind_1,ind_2], a:sets[ind_2], ran{f}=a iff forall(y:ind_2, y in a iff forsome(x:ind_1, f(x)=y)))"(theory pure-generic-theory-2) (usages transportable-macete) (proof ( (apply-macete-with-minor-premises tr%subseteq-antisymmetry) direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(f:[ind_1,ind_2],a:sets[ind_2],a subseteq ran{f});"("y")) (incorporate-antecedent"with(y:ind_2,f:[ind_1,ind_2],y in ran{f});") (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (instantiate-existential ("x_$1")) (instantiate-universal-antecedent"with(a:sets[ind_2],f:[ind_1,ind_2],ran{f} subseteq a);"("y")) (contrapose"with(p:prop,not(p));") (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly (instantiate-existential ("x")) set-containment-script direct-and-antecedent-inference-strategy (backchain"with(p:prop,forall(y:ind_2,p));") (instantiate-existential ("x")) set-containment-script direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop,forall(y:ind_2,p iff p));"("x_$1")) (instantiate-existential ("x")) )))

(def-theorem diff-conditionally-one-to-one"forall(a,b,c:sets[ind_1], c subseteq a and c subseteq b implies a diff c = b diff c iff a = b)"(theory pure-generic-theory-1) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"a = (a diff c) union c") (move-to-sibling 1) (apply-macete-with-minor-premises tr%diff-union-equal-whole) (backchain"with(c,f,a:sets[ind_1],a=f union c);") (backchain"with(b,c,a:sets[ind_1],a diff c=b diff c);") (apply-macete-with-minor-premises tr%diff-union-equal-whole) simplify )))

(def-theorem diff-conditionally-onto"forall(a,b:sets[ind_1], a disj b implies (a union b) diff b = a)"(theory pure-generic-theory-1) (proof ( direct-and-antecedent-inference-strategy set-equality-script direct-and-antecedent-inference-strategy direct-and-antecedent-inference-strategy (backchain"with(b,a:sets[ind_1],a disj b);") (weaken (0)) )))

(def-theorem f_card_differenceRemark: This entry is multiply defined. See: [1] [2]"forall(s,t:sets[ind_1], x:ind_1, f_indic_q{s} and t subseteq s implies f_card{s diff t}=f_card{s}-f_card{t})"(theory generic-theory-1) (proof ( direct-and-antecedent-inference-strategy (force-substitution"s""(s diff t) union t"(1)) (move-to-sibling 1) insistent-direct-inference (apply-macete-with-minor-premises tr%subseteq-antisymmetry) direct-and-antecedent-inference-strategy simplify-insistently simplify-insistently direct-and-antecedent-inference-strategy simplify (apply-macete-with-minor-premises f-card-disjoint-union) (move-to-sibling 1) (apply-macete-with-minor-premises subset-of-finite-indic-is-finite) auto-instantiate-existential simplify-with-minor-premises (apply-macete-with-minor-premises subset-of-finite-indic-is-finite) (instantiate-existential ("s")) simplify-insistently simplify-insistently )))

(def-theorem subsets-of-finite-cardinality"forall(s:sets[ind_1], l:zz, l<=f_card{s} and 0<=l implies forsome(t:sets[ind_1], t subseteq s and f_card{t}=l))"(theory generic-theory-1) (proof ( (induction trivial-integer-inductor ("l")) (block (script-comment"`induction' at (0 0 0 0 0 0 0 0)") simplify direct-and-antecedent-inference-strategy (instantiate-existential ("empty_indic{ind_1}")) (block (script-comment"`instantiate-existential' at (0 0)") simplify-insistently) (apply-macete-with-minor-premises empty-indic-has-f-card-zero-rewrite)) (block (script-comment"`induction' at (0 0 0 0 0 0 0 1 0 0 0 0 0)") (antecedent-inference"with(p:prop,p implies p);") (simplify-antecedent"with(p:prop,not(p));") (block (script-comment"`antecedent-inference' at (1)") (antecedent-inference"with(p:prop,forsome(t:sets[ind_1],p));") (cut-with-single-formula"forsome(x:ind_1, x in s diff t)") (block (script-comment"`cut-with-single-formula' at (0)") (antecedent-inference"with(f:sets[ind_1],nonempty_indic_q{f});") (instantiate-existential ("t union singleton{x}")) (block (script-comment"`instantiate-existential' at (0 0)") simplify-insistently direct-and-antecedent-inference-strategy (backchain"with(p:prop,p and p);") (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 1)") simplify (incorporate-antecedent"with(x:ind_1,f:sets[ind_1],x in f);") simplify-insistently)) (block (script-comment"`instantiate-existential' at (0 1)") (apply-macete-with-minor-premises f-card-disjoint-union) (block (script-comment"`apply-macete-with-minor-premises' at (0)") (apply-macete-with-minor-premises singleton-has-f-card-one-rewrite) simplify) (block (script-comment"`apply-macete-with-minor-premises' at (1)") (cut-with-single-formula"f_card{singleton{x}}=1") (apply-macete-with-minor-premises singleton-has-f-card-one-rewrite)) (block (script-comment"`apply-macete-with-minor-premises' at (2)") (incorporate-antecedent"with(x:ind_1,f:sets[ind_1],x in f);") simplify-insistently direct-and-antecedent-inference-strategy simplify (contrapose"with(p:prop,not(p));") simplify))) (block (script-comment"`cut-with-single-formula' at (1)") (contrapose"with(s:sets[ind_1],t_$0:zz,1+t_$0<=f_card{s});") (cut-with-single-formula"s=t") simplify (block (script-comment"`cut-with-single-formula' at (1)") (incorporate-antecedent"with(f:sets[ind_1],empty_indic_q{f});") simplify-insistently direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises tr%subseteq-antisymmetry) direct-and-antecedent-inference-strategy simplify)))) )))

(def-theorem cardinality-reduction"forall(s:sets[ind_1], n:zz, 1<=n implies (f_card{s}=n iff forsome(x:ind_1, x in s and f_card{s diff singleton{x}}=n-1)))"(theory generic-theory-1) (proof ( direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0)") (apply-macete-with-minor-premises f_card_difference) (block (script-comment"`apply-macete-with-minor-premises' at (0)") (apply-macete-with-minor-premises singleton-has-f-card-one-rewrite) simplify (apply-macete-with-minor-premises rev%positive-f-card-iff-nonempty) simplify) simplify-insistently) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 1 0 0)") (cut-with-single-formula"f_indic_q{s}") (block (script-comment"`cut-with-single-formula' at (0)") (incorporate-antecedent"with(r:rr,n:nn,n=r);") (apply-macete-with-minor-premises f_card_difference) (block (script-comment"`apply-macete-with-minor-premises' at (0)") (apply-macete-with-minor-premises singleton-has-f-card-one-rewrite) simplify) simplify-insistently) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises iota-free-definition-of-f-indic-q) (force-substitution"s""(s diff singleton{x}) union singleton{x}"(0)) (block (script-comment"`force-substitution' at (0)") (apply-macete-with-minor-premises f-card-disjoint-union) (block (script-comment"`apply-macete-with-minor-premises' at (0)") (apply-macete-with-minor-premises singleton-has-f-card-one-rewrite) simplify) (block (script-comment"`apply-macete-with-minor-premises' at (1)") (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"))) simplify-insistently) (block (script-comment"`force-substitution' at (1)") (apply-macete-with-minor-premises tr%diff-union-equal-whole) simplify-insistently))) )))

(def-compound-macete compute-card (repeat cardinality-reduction simplify empty-indic-has-f-card-zero))

(def-theorem cardinality-3"forall(s:sets[ind_1],f_card{s}=3 iff forsome(x,y,z:ind_1, not(x=y) and not(x=z) and not(y=z) and s = singleton{x} union singleton{y} union singleton{z}))"(theory generic-theory-1) (proof ( (apply-macete-with-minor-premises compute-card) direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0 0 0 0 0 0)") (instantiate-existential ("x""x_$17""x_$16")) simplify (block (script-comment"`instantiate-existential' at (0 3)") (incorporate-antecedent"with(f:sets[ind_1],f=f);") (apply-macete-with-minor-premises tr%subseteq-antisymmetry) simplify-insistently direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop,forall(x_$2:ind_1,p));"("x_$2")) simplify simplify simplify)) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 0 0)") (incorporate-antecedent"with(f,s:sets[ind_1],s=f);") (apply-macete-with-minor-premises tr%subseteq-antisymmetry) simplify-insistently direct-and-antecedent-inference-strategy (instantiate-existential ("x")) simplify (block (script-comment"`instantiate-existential' at (0 1)") (instantiate-existential ("y")) simplify simplify (block (script-comment"`instantiate-existential' at (0 2)") (instantiate-existential ("z")) simplify simplify simplify simplify))) )))