```(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_difference
Remark: 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)))
)))
```