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