```
(def-theorem f-card-zero-partition-lemma
"forall(p:sets[sets[ind_1]],s:sets[ind_1],
(partition_q{p,s} and f_card{p}=0) implies f_card{s}=0)"
(theory generic-theory-1)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises tr%empty-indic-has-f-card-zero)
direct-and-antecedent-inference-strategy
(weaken (1))
(contrapose "with(p:prop, forall(x:ind_1,p))")
(backchain "with(p,q:sets[sets[ind_1]],p=q)")
(weaken (1))
simplify
(contrapose "with(p:prop, p)")
extensionality
beta-reduce-repeatedly
)))
```

```
(def-theorem f-card-disjoint-union-lemma-1
"forall(n_\$0:nn,f_\$0,f:[ind_1,nn],
dom{lambda(a_\$1:ind_1,
if(a_\$1 in dom{f},
f(a_\$1),
a_\$1 in dom{f_\$0},
n_\$0+f_\$0(a_\$1),
?nn))}
=dom{f} union dom{f_\$0})"
lemma
(theory generic-theory-1)
(proof
(
direct-inference
extensionality
direct-inference
beta-reduce-repeatedly
(apply-macete-with-minor-premises tr%domain-membership-iff-defined)
(raise-conditional (0))
simplify
(raise-conditional (0))
simplify
)))

```

```
(def-theorem f-card-disjoint-union-lemma-2
"forall(n,n_\$0:nn,f_\$0,f:[ind_1,nn],
ran{f}=omega(n_\$0) and ran{f_\$0}=omega(n) and dom{f} disj dom{f_\$0}
implies
indic{y_\$1:nn,
forsome(x_\$5:ind_1,
y_\$1=lambda(a_\$1:ind_1,
if(a_\$1 in dom{f},
f(a_\$1),
a_\$1 in dom{f_\$0},
n_\$0+f_\$0(a_\$1),
?nn))(x_\$5))}
=omega(n_\$0+n))"
lemma
(theory generic-theory-1)
(proof
(
(apply-macete-with-minor-premises tr%domain-membership-iff-defined)
simplify
(raise-conditional (0))
simplify
direct-and-antecedent-inference-strategy
extensionality
simplify
direct-and-antecedent-inference-strategy
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy' at (0 0 0 0)")
(apply-macete-with-minor-premises finite-cardinal-application)
(backchain "with(n,x_0:nn,x_0=n);")
(cut-with-single-formula "f(x_\$5)<n_\$0")
simplify
(block
(script-comment "node added by `cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises rev%finite-cardinal-members-are-<)
(backchain-backwards "with(n_\$0:nn,f:[ind_1,nn],ran{f}=omega(n_\$0));")
beta-reduce-insistently
simplify
auto-instantiate-existential))
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy' at (0 0 0 1 0)")
(apply-macete-with-minor-premises finite-cardinal-application)
(backchain "with(r:rr,x_0:nn,x_0=r);")
(weaken (0))
simplify
(apply-macete-with-minor-premises rev%finite-cardinal-members-are-<)
(backchain-backwards "with(n:nn,f_\$0:[ind_1,nn],ran{f_\$0}=omega(n));")
simplify-insistently
(instantiate-existential ("x_\$5")))
(block
(script-comment
"node added by `direct-and-antecedent-inference-strategy' at (0 1)")
(case-split ("x_0<n_\$0"))
(block
(script-comment "node added by `case-split' at (1)")
(contrapose "with(n_\$0:nn,f:[ind_1,nn],ran{f}=omega(n_\$0));")
extensionality
(instantiate-existential ("x_0"))
(apply-macete-with-minor-premises finite-cardinal-application)
simplify
direct-inference
(contrapose "with(p:prop,not(p));")
(instantiate-existential ("x")))
(block
(script-comment "node added by `case-split' at (2)")
(contrapose "with(n:nn,f_\$0:[ind_1,nn],ran{f_\$0}=omega(n));")
extensionality
(instantiate-existential ("x_0-n_\$0"))
(apply-macete-with-minor-premises finite-cardinal-application)
simplify
direct-inference
(contrapose "with(p:prop,not(forsome(x_\$5:ind_1,p)));")
(instantiate-existential ("x"))
(contrapose "with(n:nn,#(n));")
(apply-macete-with-minor-premises tr%rev%domain-membership-iff-defined)
(backchain "with(f:sets[ind_1],f disj f);")
(apply-macete-with-minor-premises tr%domain-membership-iff-defined)))
)))
```

```
(def-theorem f-card-disjoint-union-lemma-3
"forall(n,n_\$0:nn,f_\$0,f:[ind_1,nn],
injective_on_q{f,dom{f}} and
injective_on_q{f_\$0,dom{f_\$0}} and
ran{f}=omega(n_\$0) and
ran{f_\$0}=omega(n) and
dom{f} disj dom{f_\$0}
implies
injective_on_q{lambda(a:ind_1,
if(a in dom{f},
f(a),
a in dom{f_\$0},
n_\$0+f_\$0(a),
?nn)),
dom{f} union dom{f_\$0}})"
lemma
(theory generic-theory-1)
(proof; 107 nodes
(
direct-and-antecedent-inference-strategy
insistent-direct-inference
beta-reduce-repeatedly
(force-substitution
"x_\$0 in dom{f} union dom{f_\$0}"
"(x_\$0 in dom{f}) or (x_\$0 in dom{f_\$0})" (0))
(force-substitution
"x_\$1 in dom{f} union dom{f_\$0}"
"(x_\$1 in dom{f}) or (x_\$1 in dom{f_\$0})" (0))
direct-and-antecedent-inference-strategy
(cut-with-single-formula "f(x_\$0)=f(x_\$1)")
(backchain "with(f:[ind_1,nn],injective_on_q{f,dom{f}})")
direct-inference
(weaken (3 4 5 6 7))
(incorporate-antecedent "with(m,n:nn, m=n)")
simplify
(instantiate-universal-antecedent
"with(a,b:sets[ind_1], a disj b)" ("x_\$0"))
(cut-with-single-formula "n_\$0+f_\$0(x_\$0)=f(x_\$1)")
(cut-with-single-formula "f(x_\$1)<n_\$0")
(weaken (2 3 4 5 6 7 8 9))
(contrapose "with(n_\$0:nn,x_\$1:ind_1,f:[ind_1,nn],f(x_\$1)<n_\$0)")
(backchain-backwards "with(m,n:nn, m=n)")
simplify
(apply-macete-with-minor-premises rev%finite-cardinal-members-are-<)
(backchain-backwards "with(n_\$0:nn,f:[ind_1,nn],ran{f}=omega(n_\$0))")
(apply-macete-with-minor-premises tr%range-domain-membership)
(weaken (4 5 6 7))
(contrapose "with(m,n:nn, m=n)")
(case-split-on-conditionals (2))
(apply-macete-with-minor-premises tr%rev%domain-membership-iff-defined)
(raise-conditional (0))
(contrapose "with(p:prop, not(p))")
(antecedent-inference "with(p,q,r:prop, if_form(p,q,r))")
(instantiate-universal-antecedent
"with(a,b:sets[ind_1], a disj b)" ("x_\$1"))
(cut-with-single-formula "n_\$0+f_\$0(x_\$1)=f(x_\$0)")
(cut-with-single-formula "f(x_\$0)<n_\$0")
(weaken (2 3 4 5 6 7 8 9))
(contrapose "with(n_\$0:nn,x_\$0:ind_1,f:[ind_1,nn],f(x_\$0)<n_\$0)")
(backchain-backwards "with(m,n:nn, m=n)")
simplify
(apply-macete-with-minor-premises rev%finite-cardinal-members-are-<)
(backchain-backwards "with(n_\$0:nn,f:[ind_1,nn],ran{f}=omega(n_\$0))")
(apply-macete-with-minor-premises tr%range-domain-membership)
(weaken (4 5 6 7))
(contrapose "with(m,n:nn, m=n)")
(case-split-on-conditionals (2))
(instantiate-universal-antecedent-multiply
"with(f:sets[ind_1],f disj f);"
(("x_\$0") ("x_\$1")))
(cut-with-single-formula "n_\$0+f_\$0(x_\$0)=n_\$0+f_\$0(x_\$1)")
(backchain "with(f_\$0:[ind_1,nn],injective_on_q{f_\$0,dom{f_\$0}})")
direct-inference
(weaken (1 2 3 4 5 6 7 8 9))
(contrapose "with(p:prop, p)")
simplify
(weaken (1 2 3 4))
(incorporate-antecedent "with(m,n:nn, m=n)")
(case-split-on-conditionals (0))
(apply-macete-with-minor-premises tr%rev%domain-membership-iff-defined)
(raise-conditional (0))
direct-and-antecedent-inference-strategy
(weaken (1 2 3 4))
(weaken (0 1 2 3 4 5))
simplify-insistently
(weaken (0 1 2 3 4))
simplify-insistently
)))
```

```
(def-theorem f-card-disjoint-union
"forall(u,v:sets[ind_1],
u disj v and f_indic_q{u} and f_indic_q{v} implies
f_card{u union v} = f_card{u} + f_card{v})"
(theory generic-theory-1)
(usages transportable-macete)
(proof; 68 nodes
(
(apply-macete-with-minor-premises iota-free-definition-of-f-indic-q)
direct-and-antecedent-inference-strategy
(backchain "with(n_\$0:nn,u:sets[ind_1],f_card{u}=n_\$0)")
(backchain "with(n:nn,v:sets[ind_1],f_card{v}=n)")
(apply-macete-with-minor-premises iota-free-definition-of-f-card)
(cut-with-single-formula "u equinumerous omega(n_\$0)")
(cut-with-single-formula "v equinumerous omega(n)")
(weaken (2 3))
(antecedent-inference-strategy (0 1))
(instantiate-existential
("lambda(a:ind_1,if(a in u, f(a), if(a in v, n_\$0+f_\$0(a), ?nn)))"))
(backchain-backwards "with(u:sets[ind_1],f:[ind_1,nn],dom{f}=u)")
(backchain-backwards "with(u:sets[ind_1],f:[ind_1,nn],dom{f}=u)")
(backchain-backwards "with(v:sets[ind_1],f_\$0:[ind_1,nn],dom{f_\$0}=v)")
(backchain-backwards "with(v:sets[ind_1],f_\$0:[ind_1,nn],dom{f_\$0}=v)")
(weaken (0 1 2 3 4 5 6))
(apply-macete-with-minor-premises f-card-disjoint-union-lemma-1)
(cut-with-single-formula "dom{f} disj dom{f_\$0}")
(backchain-backwards "with(u:sets[ind_1],f:[ind_1,nn],dom{f}=u)")
(backchain-backwards "with(v:sets[ind_1],f_\$0:[ind_1,nn],dom{f_\$0}=v)")
(weaken (1 3 4 5 6 8))
(apply-macete-with-minor-premises f-card-disjoint-union-lemma-2)
simplify
(backchain "with(v:sets[ind_1],f_\$0:[ind_1,nn],dom{f_\$0}=v)")
(backchain "with(u:sets[ind_1],f:[ind_1,nn],dom{f}=u)")
(incorporate-antecedent "with(v,u:sets[ind_1],u disj v)")
(backchain-backwards "with(u:sets[ind_1],f:[ind_1,nn],dom{f}=u)")
(backchain-backwards "with(u:sets[ind_1],f:[ind_1,nn],dom{f}=u)")
(backchain-backwards "with(u:sets[ind_1],f:[ind_1,nn],dom{f}=u)")
(backchain-backwards "with(v:sets[ind_1],f_\$0:[ind_1,nn],dom{f_\$0}=v)")
(backchain-backwards "with(v:sets[ind_1],f_\$0:[ind_1,nn],dom{f_\$0}=v)")
(backchain-backwards "with(v:sets[ind_1],f_\$0:[ind_1,nn],dom{f_\$0}=v)")
(apply-macete-with-minor-premises f-card-disjoint-union-lemma-3)
direct-inference
(instantiate-existential ("n"))
simplify
simplify
(weaken (0 1 2 3 4 5 6))
sort-definedness
direct-inference
simplify
(case-split-on-conditionals (0))
(incorporate-antecedent "with(n:nn,v:sets[ind_1],f_card{v}=n)")
(apply-macete-with-minor-premises iota-free-definition-of-f-card)
(incorporate-antecedent "with(n_\$0:nn,u:sets[ind_1],f_card{u}=n_\$0)")
(apply-macete-with-minor-premises iota-free-definition-of-f-card)
)))
```

```
(def-theorem finiteness-of-a-partition-lemma
"forall(p:sets[sets[ind_1]],s:sets[ind_1],
partition_q{p,s} and
f_indic_q{s} and
forall(u:sets[ind_1], u in p implies nonempty_indic_q{u})
implies
f_indic_q{p})"
lemma
(theory generic-theory-1)
(proof
(
direct-inference
direct-inference
(antecedent-inference "with(p:prop,p);")
(cut-with-single-formula "f_card{p}<=f_card{s}")
(apply-macete-with-minor-premises tr%f-card-leq-iff-finite-and-embeds)
direct-inference
(cut-with-single-formula
"forsome(g:[sets[ind_1],ind_1],
forall(z:sets[ind_1], z in p implies g(z) in z))"
)
(move-to-sibling 1)
choice-principle
(antecedent-inference "with(p:prop,forsome(g:[sets[ind_1],ind_1],p));")
(instantiate-existential ("restrict{g,p}"))
(block
(script-comment "`instantiate-existential' at (0 0)") extensionality
simplify-insistently direct-and-antecedent-inference-strategy simplify
(contrapose "with(p:prop,not(p));")
(auto-instantiate-universal-antecedent
"with(g:[sets[ind_1],ind_1],p:sets[sets[ind_1]],
forall(z:sets[ind_1],z in p implies g(z) in z));"
) )
(block
(script-comment "`instantiate-existential' at (0 1)") simplify-insistently
direct-and-antecedent-inference-strategy
(backchain "with(s:sets[ind_1],p:sets[sets[ind_1]],partition_q{p,s});")
auto-instantiate-existential simplify
)
simplify-insistently
insistent-direct-and-antecedent-inference-strategy
(antecedent-inference "with(s:sets[ind_1],p:sets[sets[ind_1]],partition_q{p,s});")
(instantiate-universal-antecedent "with(p:prop,forall(u,v:sets[ind_1],p));" ("x_\$0" "x_\$6"))
(instantiate-universal-antecedent "with(x_\$6,x_\$0:sets[ind_1],x_\$0 disj x_\$6);" ("g(x_\$0)"))
(auto-instantiate-universal-antecedent
"with(g:[sets[ind_1],ind_1],p:sets[sets[ind_1]],
forall(z:sets[ind_1],z in p implies g(z) in z));"
)
(auto-instantiate-universal-antecedent
"with(g:[sets[ind_1],ind_1],p:sets[sets[ind_1]],
forall(z:sets[ind_1],z in p implies g(z) in z));"
)
(contrapose "with(p:prop,not(p));")
(backchain "with(i:ind_1,i=i);")
(move-to-ancestor 5)
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1)")
(contrapose "with(p:prop,not(p));") (backchain "with(i:ind_1,i=i);")
(contrapose
"with(i:ind_1,p:sets[sets[ind_1]],
forall(z:sets[ind_1],z in p implies i in z));"
)
auto-instantiate-existential
)
)))

```

```
(def-theorem finiteness-of-a-partition
"forall(p:sets[sets[ind_1]],s:sets[ind_1],
partition_q{p,s} and f_indic_q{s} implies f_indic_q{p})"
(theory generic-theory-1)
(usages transportable-macete)
(proof; 101 nodes
(
direct-inference-strategy
(case-split ("forall(u:sets[ind_1], u in p implies nonempty_indic_q{u})"))
(antecedent-inference "with(p,q:prop, p and q)")
(antecedent-inference
"with(s:sets[ind_1],p:sets[sets[ind_1]],partition_q{p,s})")
(apply-macete-with-minor-premises finiteness-of-a-partition-lemma)
(instantiate-existential ("s"))
(cut-with-single-formula "empty_indic{ind_1} in p")
(cut-with-single-formula
"forsome(q:sets[sets[ind_1]],q = p diff singleton{empty_indic{ind_1}})")
(antecedent-inference "with(p:prop, forsome(q:sets[sets[ind_1]],p))")
(cut-with-single-formula "f_indic_q{q}")
(force-substitution "p" "q union singleton{empty_indic{ind_1}}" (0))
(apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q)
(apply-macete-with-minor-premises tr%f-card-disjoint-union)
(instantiate-existential ("f_card{q}+1"))
simplify
(apply-macete-with-minor-premises tr%singleton-has-f-card-one)
(instantiate-existential ("empty_indic{ind_1}"))
(apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q)
(instantiate-existential ("1"))
(backchain "with(p,q:sets[sets[ind_1]],p=q)")
(apply-macete-with-minor-premises tr%diff-with-indic-is-disj-from-indic)
(backchain "with(p,q:sets[sets[ind_1]],p=q)")
(cut-with-single-formula " singleton{empty_indic{ind_1}} subseteq p")
(apply-macete-with-minor-premises tr%diff-union-equal-whole)
insistent-direct-inference
(apply-macete-with-minor-premises tr%in-singleton-iff-equals-single-member)
simplify
(cut-with-single-formula "partition_q{q,s}")
(apply-macete-with-minor-premises finiteness-of-a-partition-lemma)
(antecedent-inference
"with(s:sets[ind_1],q:sets[sets[ind_1]],partition_q{q,s})")
(instantiate-existential ("s"))
(force-substitution "nonempty_indic_q{u}" "not(empty_indic_q{u})" (0))
(instantiate-transported-theorem equals-empty-indic-iff-empty () ("u"))
(contrapose "with(u:sets[ind_1],q:sets[sets[ind_1]],u in q)")
(backchain "with(u:sets[ind_1],u=empty_indic{ind_1})")
(backchain "with(p,q:sets[sets[ind_1]],p=q)")
(weaken (0 1 2 3 4 5 6 7 8))
simplify-insistently
(backchain "with(p,q:sets[sets[ind_1]],p=q)")
(force-substitution "s" "s diff empty_indic{ind_1}" (0))
(apply-macete-with-minor-premises tr%decremented-partition-lemma)
(antecedent-inference "with(p,q:prop, p and q)")
(antecedent-inference
"with(s:sets[ind_1],p:sets[sets[ind_1]],partition_q{p,s})")
direct-and-antecedent-inference-strategy
insistent-direct-inference
extensionality
direct-inference
(weaken (0 1 2 3 4 5))
simplify-insistently
(case-split-on-conditionals (0))
(instantiate-existential ("p diff singleton{empty_indic{ind_1}}"))
(weaken (1))
(contrapose "with(p:prop, not(p))")
direct-and-antecedent-inference-strategy
(force-substitution "nonempty_indic_q{u}" "not(empty_indic_q{u})" (0))
(instantiate-transported-theorem equals-empty-indic-iff-empty () ("u"))
(contrapose "with(p:prop, not(p))")
simplify
)))
```

```
(def-theorem finite-uniform-partition-lemma
"forall(n:zz, 0<=n implies
forall(p:sets[sets[ind_1]],s:sets[ind_1],m:nn,
(partition_q{p,s} and
f_card{p}=n and
forall(u:sets[ind_1], (u in p) implies f_card{u} = m))
implies f_card{s} = m * n))"
lemma
(theory generic-theory-1)
(proof
(
(apply-macete-with-minor-premises integer-induction)
beta-reduce-repeatedly
direct-inference
direct-inference
direct-inference
(force-substitution "m*0" "0" (0))
(apply-macete-with-minor-premises f-card-zero-partition-lemma)
simplify
(weaken (0))
direct-inference
direct-inference
direct-inference
direct-inference
direct-inference
(antecedent-inference "with(p,q,r:prop, p and q and r)")
(cut-with-single-formula "nonempty_indic_q{p}")
(antecedent-inference "with(p:sets[sets[ind_1]],nonempty_indic_q{p})")
(cut-with-single-formula "partition_q{p diff singleton{x},s diff x}")
(cut-with-single-formula "f_card{s diff x}=m*t")
(weaken (6))
(instantiate-universal-antecedent
"with(p:prop,forall(u:sets[ind_1],p))" ("x"))
(force-substitution "s" "(s diff x) union x" (0))
(apply-macete-with-minor-premises f-card-disjoint-union)
(backchain "with(m:nn,x:sets[ind_1],f_card{x}=m)")
(backchain "with(t:zz,m:nn,x,s:sets[ind_1],f_card{s diff x}=m*t)")
(weaken (0 1 2 3 4 5))
simplify
(weaken (0 1 2 3 4 5 6))
simplify-insistently
(apply-macete-with-minor-premises tr%diff-union-equal-whole)
(antecedent-inference-strategy (1))
insistent-direct-inference-strategy
(backchain "with(p,q:prop, forall(x:ind_1,p iff q))")
auto-instantiate-existential
(instantiate-universal-antecedent
"with(q:prop, forall(p:sets[sets[ind_1]], s:sets[ind_1],m:nn,q))"
("p diff singleton{x}" "s diff x" "m"))
(contrapose "with(p:prop, not(p))")
(cut-with-single-formula "f_indic_q{p diff singleton{x}}")
(cut-with-single-formula "f_card{singleton{x}}=1")
(cut-with-single-formula
"f_card{p}=f_card{p diff singleton{x}}+f_card{singleton{x}}")
(backchain "with(t:zz,p:sets[sets[ind_1]],f_card{p}=t+1)")
(incorporate-antecedent
"with(x:sets[ind_1],p:sets[sets[ind_1]],
f_card{p}=f_card{p diff singleton{x}}+f_card{singleton{x}})")
(backchain "with(t:zz,p:sets[sets[ind_1]],f_card{p}=t+1)")
(backchain "with(x:sets[ind_1],f_card{singleton{x}}=1)")
(weaken (0 1 2 3 4 5 6 7 8))
simplify
(force-substitution "p" "(p diff singleton{x}) union singleton{x}" (0))
(apply-macete-with-minor-premises tr%f-card-disjoint-union)
simplify
(weaken (0 1 2 3 4 5 6 7 8))
simplify-insistently
(apply-macete-with-minor-premises tr%diff-union-equal-whole)
insistent-direct-inference
beta-reduce-insistently
(case-split-on-conditionals (0))
(apply-macete-with-minor-premises tr%singleton-has-f-card-one)
(instantiate-existential ("x"))
(apply-macete-with-minor-premises tr%subset-of-finite-indic-is-finite)
(instantiate-existential ("p"))
insistent-direct-inference
beta-reduce-insistently
(case-split-on-conditionals (0))
(contrapose "with(p:prop, not(p))")
(backchain "with(p:prop, forall(u:sets[ind_1],p))")
(incorporate-antecedent "with(x:sets[ind_1],a:sets[sets[ind_1]], x in a)")
beta-reduce-insistently
(case-split-on-conditionals (0))
(apply-macete-with-minor-premises tr%decremented-partition-lemma)
(weaken (1 2 4 5))
(antecedent-inference-strategy (0))
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%rev%positive-f-card-iff-nonempty)
(weaken (0 2 3))
simplify
)))
```

```
(def-theorem finite-uniform-partition-theorem
"forall(p:sets[sets[ind_1]],s:sets[ind_1],m:nn,
(partition_q{p,s} and
f_indic_q{s} and
forall(u:sets[ind_1], (u in p) implies f_card{u} = m))
implies f_card{s} = m * f_card{p})"
(theory generic-theory-1)
(usages transportable-macete)
(proof
(
direct-inference-strategy
(antecedent-inference "with(p,q,r,s:prop, p and q and r)")
(cut-with-single-formula "f_indic_q{p}")
(instantiate-theorem finite-uniform-partition-lemma ("f_card{p}"))
(simplify-antecedent "with(p:prop, not(p))")
(backchain
"with(x:prop, forall(p:sets[sets[ind_1]],s:sets[ind_1],m:nn,x))")
auto-instantiate-existential
(apply-macete-with-minor-premises finiteness-of-a-partition)
(antecedent-inference
"with(s:sets[ind_1],p:sets[sets[ind_1]],partition_q{p,s})")
auto-instantiate-existential
)))
```