(def-language indicator-pairs
(embedded-languages generic-theory-2)
(constants (a "sets[ind_1]") (b "sets[ind_2]")))
(def-theory indicator-pairs
(component-theories generic-theory-2)
(language indicator-pairs)
(axioms
(nonempty-a "nonempty_indic_q{a}")
(nonempty-b "nonempty_indic_q{b}")))
(def-translation generic-theory-2-to-indicator-pairs
(source generic-theory-2)
(target indicator-pairs)
(fixed-theories h-o-real-arithmetic)
(sort-pairs (ind_1 (indic "a")) (ind_2 (indic "b")))
(theory-interpretation-check using-simplification))
(def-theorem schroeder-bernstein-nonempty-case
"(a embeds b) and (b embeds a) implies (a equinumerous b)"
(home-theory indicator-pairs)
(theory generic-theory-2)
lemma
(proof
(
direct-and-antecedent-inference-strategy
(instantiate-transported-theorem schroeder-bernstein-for-types
generic-theory-2-to-indicator-pairs
("f_$1" "f_$0"))
(block
(script-comment "`instantiate-transported-theorem' at (0 0 0 0 0 0)")
(contrapose "with(p:prop,not(p));")
simplify
(backchain "with(f:sets[ind_1],f subseteq a);")
(apply-macete-with-minor-premises tr%range-domain-membership)
simplify)
(block
(script-comment "`instantiate-transported-theorem' at (0 0 0 0 1)")
(contrapose "with(p:prop,not(p));")
simplify
(backchain-backwards "with(f:sets[ind_2],f=b);")
simplify
(apply-macete-with-minor-premises tr%domain-membership-iff-defined))
(block
(script-comment "`instantiate-transported-theorem' at (0 0 1 0 0 0)")
(contrapose "with(p:prop,not(p));")
(backchain "with(f:sets[ind_2],f subseteq b);")
(apply-macete-with-minor-premises range-domain-membership)
simplify)
(block
(script-comment "`instantiate-transported-theorem' at (0 0 1 0 1)")
(contrapose "with(p:prop,not(p));")
(backchain-backwards "with(f:sets[ind_1],f=a);")
(apply-macete-with-minor-premises domain-membership-iff-defined))
(block
(script-comment "`instantiate-transported-theorem' at (0 1 0 0 0 0)")
(contrapose "with(x_$2:ind_1,x_$2 in a);")
(backchain-backwards "with(f:sets[ind_1],f=a);")
(apply-macete-with-minor-premises domain-membership-iff-defined))
(block
(script-comment "`instantiate-transported-theorem' at (0 1 0 1 0 0)")
(contrapose "with(x_$5:ind_2,x_$5 in b);")
(backchain-backwards "with(f:sets[ind_2],f=b);")
(apply-macete-with-minor-premises tr%domain-membership-iff-defined))
(block
(script-comment "`instantiate-transported-theorem' at (0 1 0 2 0 0 0)")
(contrapose "with(p:prop,not(p));")
simplify)
(block
(script-comment "`instantiate-transported-theorem' at (0 1 0 3 0 0 0)")
(contrapose "with(p:prop,not(p));")
simplify)
(block
(script-comment "`instantiate-transported-theorem' at (0 1 1 0 0 0 0)")
(instantiate-existential ("h"))
insistent-direct-inference
(block
(script-comment "`insistent-direct-inference' at (0)")
insistent-direct-inference
(block
(script-comment "`insistent-direct-inference' at (0)")
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
simplify-insistently
(instantiate-universal-antecedent "with(p:prop,forall(x_$0:ind_1,if_form(p, p, p)));"
("x")))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
simplify-insistently
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(f:sets[ind_1],a subseteq f);"
("x_$0"))
(contrapose "with(x_$0:ind_1,u:unit%sort,x_$0 in lambda(x_$3:ind_1,u));")
beta-reduce-repeatedly
simplify))
(block
(script-comment "`insistent-direct-inference' at (1)")
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
insistent-direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop,forall(x_$0:ind_1,if_form(p, p, p)));"
("x_$0"))
(backchain "with(i,x_$2:ind_2,x_$2=i);"))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
insistent-direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(f:sets[ind_2],b subseteq f);"
("x_$1"))
(contrapose "with(x_$1:ind_2,u:unit%sort,x_$1 in lambda(x_$6:ind_2,u));")
simplify)))
(block
(script-comment "`insistent-direct-inference' at (1)")
insistent-direct-inference
direct-and-antecedent-inference-strategy
simplify))
)))
(def-theorem schroeder-bernstein-theorem
Remark: This entry is multiply defined. See: [1] [2]
"forall(b:sets[ind_2],a:sets[ind_1],
(a embeds b and b embeds a implies a equinumerous b))"
(theory generic-theory-2)
(usages transportable-macete)
(proof
(
direct-inference
direct-inference
(antecedent-inference "with(p:prop,p);")
(case-split ("nonempty_indic_q{a}"))
(block
(script-comment "`case-split' at (1)")
(cut-with-single-formula "nonempty_indic_q{b}")
(block
(script-comment "`cut-with-single-formula' at (0)")
(apply-macete-with-minor-premises schroeder-bernstein-nonempty-case)
simplify)
(block
(script-comment "`cut-with-single-formula' at (1)")
(antecedent-inference "with(a:sets[ind_1],nonempty_indic_q{a});")
(antecedent-inference "with(b:sets[ind_2],a:sets[ind_1],a embeds b);")
(instantiate-existential ("f_$1(x)"))
(backchain "with(p:prop,p and p and p);")
(block
(script-comment "`backchain' at (0)")
(apply-macete-with-minor-premises range-domain-membership)
(backchain "with(p:prop,p and p and p);"))
simplify))
(block
(script-comment "`case-split' at (2)")
(cut-with-single-formula "not(nonempty_indic_q{b})")
(block
(script-comment "`cut-with-single-formula' at (0)")
(contrapose "with(b:sets[ind_2],not(nonempty_indic_q{b}));")
(contrapose "with(p:prop,forall(f:[ind_1,ind_2],p));")
(contrapose "with(p:prop,not(p));")
(contrapose "with(p:prop,forall(f:[ind_1,ind_2],p));")
(instantiate-existential ("with(x:ind_2, lambda(m:ind_1, if(m in a, x, ?ind_2)))"))
insistent-direct-inference
(block
(script-comment "`insistent-direct-inference' at (0)")
insistent-direct-inference
(block
(script-comment "`insistent-direct-inference' at (0)")
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
simplify-insistently)
(block
(script-comment "`insistent-direct-inference' at (1)")
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
simplify-insistently))
(block
(script-comment "`insistent-direct-inference' at (1)")
insistent-direct-inference
simplify
direct-and-antecedent-inference-strategy
simplify
(instantiate-universal-antecedent "with(a:sets[ind_1],empty_indic_q{a});"
("x_$4"))))
(block
(script-comment "`cut-with-single-formula' at (1)")
(contrapose "with(p:prop,not(p));")
(antecedent-inference "with(b:sets[ind_2],nonempty_indic_q{b});")
(antecedent-inference "with(a:sets[ind_1],b:sets[ind_2],b embeds a);")
(instantiate-existential ("f_$1(x)"))
(backchain "with(p:prop,p and p and p);")
(block
(script-comment "`backchain' at (0)")
(apply-macete-with-minor-premises tr%range-domain-membership)
(backchain "with(p:prop,p and p and p);"))
simplify))
)))