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