(def-constant power"lambda(s:sets[ind_1], indic{a:sets[ind_1], a subseteq s})"(theory generic-theory-1))

(def-constant filter"lambda(x:ind_1, indic{a:sets[ind_1], x in a})"(theory generic-theory-1))

(def-theorem power-decomposition"forall(s:sets[ind_1], x:ind_1, n:nn, x in s implies power(s)=power(s diff singleton{x}) union power(s) inters filter(x))"(theory generic-theory-1) (proof ( direct-and-antecedent-inference-strategy unfold-defined-constants set-equality-script direct-and-antecedent-inference-strategy (contrapose"with(p:prop,not(p));") simplify-insistently (contrapose"with(p:prop,not(p));") simplify direct-and-antecedent-inference-strategy set-containment-script direct-and-antecedent-inference-strategy (incorporate-antecedent"with(f,x:sets[ind_1],x subseteq f);") simplify-insistently )))

(def-theorem power-disjointness"forall(s:sets[ind_1], x:ind_1, n:nn, power(s diff singleton{x}) disj power(s) inters filter(x))"(theory generic-theory-1) (proof ( direct-and-antecedent-inference-strategy unfold-defined-constants simplify-insistently )))

(def-theorem power-reduction"forall(s:sets[ind_1], x:ind_1, x in s implies power(s) inters filter(x) equinumerous power(s diff singleton{x}))"(theory generic-theory-1) (proof ( direct-and-antecedent-inference-strategy (instantiate-existential ("lambda(t:sets[ind_1], if(t in power(s) inters filter(x), t diff singleton{x}, ?sets[ind_1]))")) insistent-direct-inference-strategy (apply-macete-with-minor-premises tr%indic-free-characterization-of-dom) beta-reduce-repeatedly direct-and-antecedent-inference-strategy simplify (weaken (0)) unfold-defined-constants (apply-macete-with-minor-premises tr%indic-free-characterization-of-ran) beta-reduce-repeatedly (apply-macete-with-minor-premises tr%equality-of-conditional-term) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (instantiate-existential ("y_$0 union singleton{x}")) set-containment-script direct-and-antecedent-inference-strategy (incorporate-antecedent"with(f,y_$0:sets[ind_1],y_$0 subseteq f);") simplify-insistently simplify simplify-insistently (apply-macete-with-minor-premises diff-conditionally-onto) (incorporate-antecedent"with(f,y_$0:sets[ind_1],y_$0 subseteq f);") simplify-insistently (incorporate-antecedent"with(y_$0,f:sets[ind_1],f=y_$0);") (move-to-ancestor 1) (backchain-backwards"with(y_$0,f:sets[ind_1],f=y_$0);") set-containment-script direct-and-antecedent-inference-strategy simplify (weaken (1)) (incorporate-antecedent"with(p:prop,p and p and p);") beta-reduce-repeatedly (apply-macete-with-minor-premises tr%equality-of-conditional-term) (apply-macete-with-minor-premises tr%equality-of-conditional-term-backwards) (apply-macete-with-minor-premises diff-conditionally-one-to-one) direct-and-antecedent-inference-strategy (incorporate-antecedent"with(x_$0:sets[ind_1],x:ind_1,s:sets[ind_1], x_$0 in power(s) inters filter(x));") unfold-defined-constants simplify-insistently (incorporate-antecedent"with(x_$3:sets[ind_1],x:ind_1,s:sets[ind_1], x_$3 in power(s) inters filter(x));") unfold-defined-constants simplify-insistently )))

(def-constant combinations"lambda(s:sets[ind_1], n:nn, indic{a:sets[ind_1], a subseteq s and f_card{a}=n})"(theory generic-theory-1))

(def-theorem combination-decomposition"forall(s:sets[ind_1], x:ind_1, n:nn, x in s implies combinations(s,n)=combinations(s diff singleton{x},n) union combinations(s,n) inters filter(x))"(theory generic-theory-1) (proof ( direct-and-antecedent-inference-strategy unfold-defined-constants set-equality-script direct-and-antecedent-inference-strategy (contrapose"with(p:prop,not(p));") simplify-insistently (contrapose"with(p:prop,not(p));") simplify direct-and-antecedent-inference-strategy set-containment-script direct-and-antecedent-inference-strategy (incorporate-antecedent"with(f,x:sets[ind_1],x subseteq f);") simplify-insistently )))

(def-theorem combination-disjointness"forall(s:sets[ind_1], x:ind_1, n:nn, combinations(s diff singleton{x},n) disj combinations(s,n) inters filter(x))"(theory generic-theory-1) (proof ( direct-and-antecedent-inference-strategy unfold-defined-constants simplify-insistently )))

(def-theorem combination-reduction"forall(s:sets[ind_1], x:ind_1, n:nn, x in s and 1<=n implies combinations(s,n) inters filter(x) equinumerous combinations(s diff singleton{x},n-1))"(theory generic-theory-1) (proof ( direct-and-antecedent-inference-strategy (instantiate-existential ("lambda(t:sets[ind_1], if(t in combinations(s,n) inters filter(x), t diff singleton{x}, ?sets[ind_1]))")) insistent-direct-inference-strategy (apply-macete-with-minor-premises tr%indic-free-characterization-of-dom) beta-reduce-repeatedly direct-and-antecedent-inference-strategy simplify (weaken (0)) unfold-defined-constants (apply-macete-with-minor-premises tr%indic-free-characterization-of-ran) beta-reduce-repeatedly (apply-macete-with-minor-premises tr%equality-of-conditional-term) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (instantiate-existential ("y_$0 union singleton{x}")) set-containment-script direct-and-antecedent-inference-strategy (incorporate-antecedent"with(f,y_$0:sets[ind_1],y_$0 subseteq f);") simplify-insistently simplify (apply-macete-with-minor-premises f-card-disjoint-union) (apply-macete-with-minor-premises singleton-has-f-card-one-lemma-2) (move-to-ancestor 1) (apply-macete-with-minor-premises singleton-has-f-card-one-rewrite) simplify (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")) (incorporate-antecedent"with(f,s,y_$0:sets[ind_1],y_$0 subseteq s diff f);") simplify-insistently simplify-insistently (apply-macete-with-minor-premises diff-conditionally-onto) (incorporate-antecedent"with(f,y_$0:sets[ind_1],y_$0 subseteq f);") simplify-insistently (incorporate-antecedent"with(y_$0,f:sets[ind_1],f=y_$0);") (move-to-ancestor 1) (backchain-backwards"with(y_$0,f:sets[ind_1],f=y_$0);") set-containment-script direct-and-antecedent-inference-strategy simplify (backchain-backwards"with(y_$0,f:sets[ind_1],f=y_$0);") (apply-macete-with-minor-premises f_card_difference) (move-to-sibling 1) simplify-insistently (apply-macete-with-minor-premises singleton-has-f-card-one-rewrite) simplify (weaken (1)) (incorporate-antecedent"with(p:prop,p and p and p);") beta-reduce-repeatedly (apply-macete-with-minor-premises tr%equality-of-conditional-term) (apply-macete-with-minor-premises tr%equality-of-conditional-term-backwards) (apply-macete-with-minor-premises diff-conditionally-one-to-one) direct-and-antecedent-inference-strategy (incorporate-antecedent"with(x_$0:sets[ind_1],x:ind_1,n:nn,s:sets[ind_1], x_$0 in combinations(s,n) inters filter(x));") unfold-defined-constants simplify-insistently (incorporate-antecedent"with(x_$3:sets[ind_1],x:ind_1,n:nn,s:sets[ind_1], x_$3 in combinations(s,n) inters filter(x));") unfold-defined-constants simplify-insistently )))

(def-theorem power-card"forall(s:sets[ind_1],f_indic_q{s} implies f_card{power(s)}=2^f_card{s})"(theory generic-theory-1) (usages transportable-macete) (proof ( (block (script-comment"this is the basic set induction script.") (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, 0<=m and n=m)") (move-to-sibling 1) (instantiate-existential ("n")) (apply-macete-with-minor-premises nn-in-quasi-sort_h-o-real-arithmetic) (backchain"with(n:nn,n=n);") (antecedent-inference"with(p:prop,forsome(m:zz,p));") (backchain"with(p:prop,p and p);") (incorporate-antecedent"with(n:nn,n=n);") (backchain"with(p:prop,p);") (antecedent-inference"with(p:prop,p);") (weaken (0)) (cut-with-single-formula"forall(s:sets[ind_1], f_card{s}=m implies f_card{power(s)}=2^m)") (backchain"with(p:prop,forall(s:sets[ind_1],p));") (induction trivial-integer-inductor ("m")) ) beta-reduce-repeatedly simplify (apply-macete-with-minor-premises empty-indic-has-f-card-zero) (apply-macete-with-minor-premises tr%singleton-has-f-card-one) direct-and-antecedent-inference-strategy (backchain"with(p:prop,p);") (instantiate-existential ("empty_indic{ind_1}")) (weaken (0)) (unfold-single-defined-constant (0) power) set-equality-script direct-and-antecedent-inference-strategy set-equality-script (apply-macete-with-minor-premises indicator-facts-macete) (incorporate-antecedent"with(p:prop,p);") simplify-insistently (apply-macete-with-minor-premises tr%subseteq-antisymmetry) direct-and-antecedent-inference-strategy (unfold-single-defined-constant (0) power) (cut-with-single-formula"forsome(x:ind_1, x in s)") (move-to-sibling 1) (apply-macete-with-minor-premises rev%positive-f-card-iff-nonempty) simplify (antecedent-inference"with(s:sets[ind_1],nonempty_indic_q{s});") (instantiate-universal-antecedent"with(p:prop,forall(s:sets[ind_1],p));"("s diff singleton{x}")) (contrapose"with(p:prop,not(p));") (apply-macete-with-minor-premises f_card_difference) (apply-macete-with-minor-premises singleton-has-f-card-one-rewrite) simplify simplify-insistently (force-substitution"power(s)""power(s diff singleton{x}) union power(s) inters filter(x)"(0)) (apply-macete-with-minor-premises power-decomposition) (apply-macete-with-minor-premises tr%f-card-disjoint-union) (cut-with-single-formula"f_card{power(s) inters filter(x)}=f_card{power(s diff singleton{x})}") (move-to-sibling 1) (apply-macete-with-minor-premises tr%f-card-equal-iff-finite-and-equinumerous) (apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q) direct-and-antecedent-inference-strategy auto-instantiate-existential (apply-macete-with-minor-premises power-reduction) (apply-macete-with-minor-premises power-reduction) (unfold-single-defined-constant (0) power) (unfold-single-defined-constant (0) power) (backchain"with(f:sets[sets[ind_1]],f_card{f}=f_card{f});") (case-split ("t=0")) simplify (apply-macete-with-minor-premises exp-out) simplify (apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q) (cut-with-single-formula"f_card{power(s) inters filter(x)}=f_card{power(s diff singleton{x})}") (backchain"with(f:sets[sets[ind_1]],f_card{f}=f_card{f});") auto-instantiate-existential (apply-macete-with-minor-premises power-disjointness) (apply-macete-with-minor-premises power-decomposition) )))

(def-theorem subset-equal-if-equal-cardinality"forall(s,a:sets[ind_1], a subseteq s and f_card{a}=f_card{s} implies a=s)"(theory generic-theory-1) (proof ( (apply-macete-with-minor-premises tr%subseteq-antisymmetry) direct-and-antecedent-inference-strategy (cut-with-single-formula"s subseteq a iff f_card{s diff a}=0") (move-to-sibling 1) (apply-macete-with-minor-premises empty-indic-has-f-card-zero) (apply-macete-with-minor-premises tr%subseteq-antisymmetry) direct-and-antecedent-inference-strategy set-containment-script direct-and-antecedent-inference-strategy (contrapose"with(p:prop,not(p));") simplify simplify-insistently set-containment-script direct-and-antecedent-inference-strategy (incorporate-antecedent"s diff a subseteq empty_indic{ind_1};") simplify-insistently (backchain"with(p:prop,p iff p);") (apply-macete-with-minor-premises f_card_difference) simplify )))

(def-theorem comb-reduction-schema"forall(p:[zz,zz,prop], forall(k,m:zz, 1<=k and k<=m and p(m,k-1) and p(m,k) implies p(1+m,k)) and forall(k:zz,0<=k implies p(k,0)) and forall(j:zz,0<=j implies p(j,j)) implies forall(m,k:zz,k<=m and 0<=k implies p(m,k)))"(theory h-o-real-arithmetic) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forall(m:zz,0<=m implies forall(k,j:zz,0<=k and k<=j and j<=m implies p(j,k)))") (backchain"with(p:prop,forall(m:zz,0<=m implies forall(k,j:zz,p)));") (instantiate-existential ("m")) simplify simplify (weaken (4 3)) (induction trivial-integer-inductor ("m")) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (cut-with-single-formula"k=0 and j=0") simplify simplify (case-split ("k=0")) simplify (case-split ("j<=t")) (backchain"forall(k,j:zz, with(p:prop,p and p and p) implies with(p:[zz,zz,prop],p(j,k)));") direct-and-antecedent-inference-strategy (case-split ("k=j")) (backchain"with(j,k:zz,k=j);") simplify (force-substitution"j""1+(j-1)"(0)) (backchain"with(r:rr, forall(k,m:zz, with(p:prop,p and p and p and p) implies with(p:[zz,zz,prop],p(r,k))));") direct-and-antecedent-inference-strategy (backchain"forall(k,j:zz, with(p:prop,p and p and p) implies with(p:[zz,zz,prop],p(j,k)));") simplify (backchain"forall(k,j:zz, with(p:prop,p and p and p) implies with(p:[zz,zz,prop],p(j,k)));") simplify simplify (backchain"forall(k,j:zz, with(p:prop,p and p and p) implies with(p:[zz,zz,prop],p(j,k)));") simplify simplify )))

(def-theorem combinations-card"forall(s:sets[ind_1],k:zz, f_indic_q{s} and 0<=k and k<=f_card{s} implies f_card{combinations(s,k)}=comb(f_card{s},k))"(theory generic-theory-1) (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, 0<=m and n=m)") (move-to-sibling 1) (instantiate-existential ("n")) (apply-macete-with-minor-premises nn-in-quasi-sort_h-o-real-arithmetic) (backchain"with(n:nn,n=n);") (antecedent-inference"with(p:prop,forsome(m:zz,p));") (backchain"with(p:prop,p and 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)) direct-and-antecedent-inference-strategy (contrapose"with(s:sets[ind_1],k:zz,k<=f_card{s});") (backchain"with(m:zz,n:nn,n=m);") (contrapose"with(p:prop,not(p));") (incorporate-antecedent"with(m:zz,n:nn,n=m);") (cut-with-single-formula"forall(s:sets[ind_1], f_card{s}=m implies f_card{combinations(s,k)}=comb(m,k))") direct-inference (backchain"with(p:prop,forall(s:sets[ind_1],p));") (force-substitution"forall(s:sets[ind_1], f_card{s}=m implies f_card{combinations(s,k)}=comb(m,k))""lambda(m,k:zz,forall(s:sets[ind_1], f_card{s}=m implies f_card{combinations(s,k)}=comb(m,k)))(m,k)"(0)) (move-to-sibling 1) beta-reduce-repeatedly (apply-macete-with-minor-premises comb-reduction-schema) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (weaken (7 6 5)) (cut-with-single-formula"forsome(x:ind_1, x in s_$0)") (move-to-sibling 1) (apply-macete-with-minor-premises rev%positive-f-card-iff-nonempty) simplify (antecedent-inference"with(s_$0:sets[ind_1],nonempty_indic_q{s_$0});") (instantiate-universal-antecedent"with(k_$0:zz,r:rr,m_$0:zz, forall(s_$0:sets[ind_1], f_card{s_$0}=m_$0 implies f_card{combinations(s_$0,r)}=comb(m_$0,k_$0-1)));"("s_$0 diff singleton{x}")) (contrapose"with(p:prop,not(p));") (apply-macete-with-minor-premises f_card_difference) (move-to-sibling 1) set-containment-script simplify (apply-macete-with-minor-premises singleton-has-f-card-one-rewrite) simplify (force-substitution"combinations(s_$0,k_$0)""combinations(s_$0 diff singleton{x},k_$0) union combinations(s_$0,k_$0) inters filter(x)"(0)) (move-to-sibling 1) (apply-macete-with-minor-premises combination-decomposition) (apply-macete-with-minor-premises tr%f-card-disjoint-union) (cut-with-single-formula"f_card{combinations(s_$0 diff singleton{x},k_$0-1)}= f_card{combinations(s_$0,k_$0) inters filter(x)}") (move-to-sibling 1) (apply-macete-with-minor-premises tr%finite-and-equinumerous-implies-f-card-equal) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises tr%equinumerous-is-symmetric) (move-to-sibling 1) (unfold-single-defined-constant (0) combinations) (apply-macete-with-minor-premises combination-reduction) direct-and-antecedent-inference-strategy (unfold-single-defined-constant (0) combinations) (backchain-backwards"with(f:sets[sets[ind_1]],f_card{f}=f_card{f});") (backchain"with(r:rr,m_$0:zz,f:sets[sets[ind_1]], f_card{f}=comb(m_$0,r));") (backchain"with(p:prop,forall(s:sets[ind_1],p));") (apply-macete-with-minor-premises f_card_difference) (apply-macete-with-minor-premises singleton-has-f-card-one-rewrite) (apply-macete-with-minor-premises comb-ident) simplify set-containment-script simplify (apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q) (cut-with-single-formula"f_card{combinations(s_$0 diff singleton{x},k_$0-1)}= f_card{combinations(s_$0,k_$0) inters filter(x)}") (backchain-backwards"with(f:sets[sets[ind_1]],f_card{f}=f_card{f});") (backchain"with(r:rr,m_$0:zz,f:sets[sets[ind_1]], f_card{f}=comb(m_$0,r));") (instantiate-existential ("comb(m_$0,k_$0-1)")) (apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q) (instantiate-existential ("f_card{combinations(s_$0 diff singleton{x},k_$0)}")) (unfold-single-defined-constant (0) combinations) (apply-macete-with-minor-premises combination-disjointness) (apply-macete-with-minor-premises comb-0-value-lemma) (apply-macete-with-minor-premises tr%singleton-has-f-card-one) (instantiate-existential ("empty_indic{ind_1}")) (unfold-single-defined-constant (0) combinations) set-equality-script (apply-macete-with-minor-premises empty-indic-has-f-card-zero) direct-and-antecedent-inference-strategy direct-and-antecedent-inference-strategy (backchain"with(f,x_$4:sets[ind_1],x_$4=f);") (weaken (0)) simplify-insistently (apply-macete-with-minor-premises empty-indic-has-f-card-zero) (unfold-single-defined-constant (0) combinations) (apply-macete-with-minor-premises comb-m-value-lemma) (apply-macete-with-minor-premises tr%singleton-has-f-card-one) (instantiate-existential ("s")) (unfold-single-defined-constant (0) combinations) set-equality-script (apply-macete-with-minor-premises subset-equal-if-equal-cardinality) direct-and-antecedent-inference-strategy simplify (unfold-single-defined-constant (0) combinations) )))