(def-theorem a%even-a%odd-a%inf-cover-dom-of-f"a%even union a%odd union a%inf = dom{f}"lemma reverse (theory schroeder-bernstein-theory) (usages transportable-macete) (proof ( unfold-defined-constants extensionality direct-inference beta-reduce-repeatedly (raise-conditional (0)) simplify (case-split ("#(last%a%index(x_0))")) (apply-macete-with-minor-premises natural-numbers-are-even-or-odd) simplify )))

(def-theorem a%even-a%odd-disjoint"a%even disj a%odd"lemma (theory schroeder-bernstein-theory) (proof ( unfold-defined-constants simplify-insistently (apply-macete-with-minor-premises even-and-odd-natural-numbers-are-disjoint) simplify )))

(def-theorem a%even-a%inf-disjoint"a%even disj a%inf"lemma (theory schroeder-bernstein-theory) (proof ( unfold-defined-constants simplify-insistently )))

(def-theorem a%odd-a%inf-disjoint"a%odd disj a%inf"lemma (theory schroeder-bernstein-theory) (proof ( unfold-defined-constants simplify-insistently )))

(def-theorem ran-of-f-is-b%seq-at-1"ran{f}=b%seq(1)"lemma reverse (theory schroeder-bernstein-theory) (proof ( (unfold-single-defined-constant-globally b%seq) simplify (unfold-single-defined-constant-globally a%seq) simplify )))

(def-theorem a%seq-to-b%seq-step-by-f"forall(i:nn,x:ind_1, x in a%seq(i) iff f(x) in b%seq(1+i))"reverse lemma (theory schroeder-bernstein-theory) (proof ( (unfold-single-defined-constant-globally b%seq) simplify direct-and-antecedent-inference-strategy (instantiate-existential ("x")) (instantiate-theorem f-injectiveness ("x""x_$1")) (backchain"with(x_$1,x:ind_1,x=x_$1)") )))

(def-theorem a%seq-b%seq-hierarchies-lemma"forall(i:zz, 0<=i implies a%seq(1+i) subseteq a%seq(i) and b%seq(1+i) subseteq b%seq(i))"lemma (theory schroeder-bernstein-theory) (proof ( (induction integer-inductor ("i")) simplify-insistently (unfold-single-defined-constant (0) a%seq) simplify (unfold-single-defined-constant (2) b%seq) simplify (apply-macete-with-minor-premises tr%image-is-monotone-wrt-subseteq) direct-inference )))

(def-theorem a%seq-hierarchy"forall(i,j:nn, i<=j implies a%seq(j) subseteq a%seq(i))"lemma (theory schroeder-bernstein-theory) (proof ( (force-substitution"forall(i,j:nn,i<=j implies a%seq(j) subseteq a%seq(i))""forall(i:zz, forall(j:zz, i<=j implies (#(i,nn) and #(j,nn) implies a%seq(j) subseteq a%seq(i))))"(0)) (apply-macete-with-minor-premises integer-induction) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (contrapose"with(p:prop, not(p))") (weaken (0 2 4)) (incorporate-antecedent"with(i:zz,#(i,nn))") (apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic) simplify (cut-with-single-formula"#(t,nn)") (instantiate-theorem a%seq-b%seq-hierarchies-lemma ("t")) (contrapose"with(p:prop, not(p))") (apply-macete-with-minor-premises nn-in-quasi-sort_h-o-real-arithmetic) (force-substitution"t+1""1+t"(0)) (apply-macete-with-minor-premises tr%subseteq-transitivity) (instantiate-existential ("a%seq(t)")) simplify (weaken (0 2 4)) direct-and-antecedent-inference-strategy (backchain"with(p:prop, forall(i:zz,p))") )))

(def-theorem last%a%index-to-last%b%index-step-by-f"forall(x:ind_1, last%b%index(f(x)) == (1 + last%a%index(x)))"lemma (theory schroeder-bernstein-theory) (proof; 116 nodes ( unfold-defined-constants insistent-direct-inference-strategy (antecedent-inference"with(p,q:prop, p or q)") (eliminate-defined-iota-expression 0 w) (cut-with-single-formula"#([-1]+w,nn)") (eliminate-iota 0) (instantiate-existential ("[-1]+w")) (incorporate-antecedent"with(x:ind_2,a:sets[ind_2], x in a)") (apply-macete-with-minor-premises tr%membership-in-diff) (apply-macete-with-minor-premises a%seq-to-b%seq-step-by-f) simplify (instantiate-universal-antecedent"with(p:prop,forall(w_1:nn,p))"("1+z%iota_$0")) (contrapose"with(p:prop, not(p))") (weaken (0 2 3 4 5)) (incorporate-antecedent"with(x:ind_1,a:sets[ind_1], x in a)") (apply-macete-with-minor-premises tr%membership-in-diff) (apply-macete-with-minor-premises a%seq-to-b%seq-step-by-f) (weaken (1 2 3 4 5)) simplify simplify (cut-with-single-formula"w=0 or 0<w") (antecedent-inference"with(p,q:prop, p or q)") (contrapose"with(x:ind_2,a:sets[ind_2], x in a)") (backchain"with(w:nn,w=0)") (unfold-single-defined-constant (0) b%seq) simplify (weaken (0 1 2 3)) (apply-macete-with-minor-premises rev%ran-of-f-is-b%seq-at-1) (apply-macete-with-minor-premises range-domain-membership) (apply-macete-with-minor-premises domain-membership-iff-defined) (apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic) simplify simplify (eliminate-defined-iota-expression 1 w) (eliminate-iota 0) (instantiate-existential ("1+w")) (incorporate-antecedent"with(x:ind_1,a:sets[ind_1], x in a)") (apply-macete-with-minor-premises tr%membership-in-diff) (apply-macete-with-minor-premises a%seq-to-b%seq-step-by-f) (cut-with-single-formula"#([-1]+z%iota_$0,nn)") (instantiate-universal-antecedent"with(p:prop,forall(w_1:nn,p))"("[-1]+z%iota_$0")) (contrapose"with(p:prop, not(p))") (weaken (0 3 4 5)) (incorporate-antecedent"with(x:ind_2,a:sets[ind_2], x in a)") (apply-macete-with-minor-premises tr%membership-in-diff) (apply-macete-with-minor-premises a%seq-to-b%seq-step-by-f) simplify simplify (cut-with-single-formula"z%iota_$0=0 or 0<z%iota_$0") (antecedent-inference"with(p,q:prop, p or q)") (contrapose"with(x:ind_2,a:sets[ind_2], x in a)") (backchain"with(w:nn,z%iota_$0=0)") (unfold-single-defined-constant (0) b%seq) simplify (apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic) simplify simplify )))

(def-theorem b%odd-subseteq-of-ran-of-f"b%odd subseteq ran{f}"lemma (theory schroeder-bernstein-theory) (proof ( (apply-macete-with-minor-premises ran-of-f-is-b%seq-at-1) (unfold-single-defined-constant-globally b%odd) (unfold-single-defined-constant-globally last%b%index) insistent-direct-inference simplify direct-inference (cut-with-single-formula"#(iota(i_$0:nn, x_$0 in b%seq(i_$0) and not(x_$0 in b%seq(1+i_$0))))") (incorporate-antecedent"with(m:nn, odd(m))") (eliminate-defined-iota-expression 0 w) direct-inference (cut-with-single-formula"1<=w") (instantiate-transported-theorem a%seq-hierarchy schroeder-bernstein-symmetry ("1""w")) (instantiate-universal-antecedent"with(a,b:sets[ind_2], a subseteq b)"("x_$0")) (case-split ("0=w")) (contrapose"with(w:nn,odd(w))") (backchain-backwards"with(w:nn,0=w)") (apply-macete-with-minor-premises even-and-odd-natural-numbers-are-disjoint) (unfold-single-defined-constant-globally even) simplify simplify )))

(def-theorem b%inf-subseteq-of-ran-of-f"b%inf subseteq ran{f}"lemma (theory schroeder-bernstein-theory) (proof ( (apply-macete-with-minor-premises ran-of-f-is-b%seq-at-1) insistent-direct-inference (unfold-single-defined-constant-globally b%inf) (unfold-single-defined-constant-globally last%b%index) simplify direct-inference (cut-with-single-formula"x_$0 in (b%seq(0) diff b%seq(1)) or x_$0 in b%seq(1)") (antecedent-inference"with(p,q:prop, p or q)") (contrapose"with(p:prop, not(p))") (apply-macete-with-minor-premises eliminate-iota-macete) (instantiate-existential ("0")) simplify (incorporate-antecedent"with(x_$0:ind_2,x_$0 in b%seq(0) diff b%seq(1))") (apply-macete-with-minor-premises tr%membership-in-diff) direct-and-antecedent-inference-strategy simplify (cut-with-single-formula"j=0 or 1<=j") (antecedent-inference"with(p,q:prop, p or q)") (instantiate-transported-theorem a%seq-hierarchy schroeder-bernstein-symmetry ("1""j")) (instantiate-universal-antecedent"with(j:nn,b%seq(j) subseteq b%seq(1))"("x_$0")) simplify (apply-macete-with-minor-premises tr%membership-in-diff) direct-and-antecedent-inference-strategy (contrapose"with(p:prop, not(p))") (unfold-single-defined-constant-globally b%seq) simplify )))

(def-theorem image-of-a%even-under-f"image{f,a%even}=b%odd"lemma reverse (theory schroeder-bernstein-theory) (usages transportable-macete) (proof ( unfold-defined-constants (apply-macete-with-minor-premises tr%subseteq-antisymmetry) direct-inference insistent-direct-inference simplify direct-and-antecedent-inference-strategy (backchain"with(x,y:ind_2, x=y)") (incorporate-antecedent"with(x:ind_1,even(last%a%index(x)))") (apply-macete-with-minor-premises last%a%index-to-last%b%index-step-by-f) (apply-macete-with-minor-premises even-iff-suc-is-odd) simplify (weaken (0)) insistent-direct-inference simplify (instantiate-theorem b%odd-subseteq-of-ran-of-f ("x_$1")) (incorporate-antecedent"with(p:prop, not(p))") (unfold-single-defined-constant-globally b%odd) simplify (incorporate-antecedent"with(p:prop, p)") simplify direct-inference (antecedent-inference"with(p:prop, forsome(x:ind_1,p))") (backchain"with(x,y:ind_2, x=y)") (apply-macete-with-minor-premises last%a%index-to-last%b%index-step-by-f) direct-inference auto-instantiate-existential (apply-macete-with-minor-premises even-iff-suc-is-odd) simplify )))

(def-theorem image-of-a%odd-under-inverse-of-g"image{inverse{g},a%odd}=b%even"lemma reverse (theory schroeder-bernstein-theory) (usages transportable-macete) (proof ( (apply-macete-with-minor-premises tr%image-under-inverse-of-injective-mapping) (apply-macete-with-minor-premises g-injectiveness) (apply-macete-with-minor-premises tr%image-of-a%even-under-f) direct-inference (apply-macete-with-minor-premises tr%rev%a%even-a%odd-a%inf-cover-dom-of-f) simplify-insistently )))

(def-theorem image-of-a%inf-under-f"image{f,a%inf}=b%inf"lemma reverse (theory schroeder-bernstein-theory) (usages transportable-macete) (proof ( unfold-defined-constants (apply-macete-with-minor-premises tr%subseteq-antisymmetry) direct-inference insistent-direct-inference simplify direct-and-antecedent-inference-strategy (backchain"with(x,y:ind_2, x=y)") (apply-macete-with-minor-premises last%a%index-to-last%b%index-step-by-f) simplify (weaken (0)) insistent-direct-inference simplify (instantiate-theorem b%inf-subseteq-of-ran-of-f ("x_$1")) (incorporate-antecedent"with(p:prop, not(p))") (unfold-single-defined-constant-globally b%inf) simplify (incorporate-antecedent"with(p:prop, p)") simplify direct-inference (antecedent-inference"with(p:prop, forsome(x:ind_1,p))") (backchain"with(x,y:ind_2, x=y)") (apply-macete-with-minor-premises last%a%index-to-last%b%index-step-by-f) direct-inference auto-instantiate-existential (simplify-antecedent"with(p:prop, not(p))") )))

(def-theorem h-injectiveness-lemma"forall(x_1,x_2:ind_1, (x_1 in a%inf or x_1 in a%even) and f(x_1)=iota(y:ind_2,g(y)=x_2) and not(x_2 in a%inf or x_2 in a%even) implies x_1=x_2)"lemma (theory schroeder-bernstein-theory) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"x_2 in a%odd") (cut-with-single-formula"f(x_1) in b%inf") (cut-with-single-formula"f(x_1) in b%even") (instantiate-transported-theorem a%even-a%inf-disjoint schroeder-bernstein-symmetry ("f(x_1)")) (apply-macete-with-minor-premises rev%image-of-a%odd-under-inverse-of-g) (weaken (0 2 4)) simplify auto-instantiate-existential (apply-macete-with-minor-premises rev%image-of-a%inf-under-f) (weaken (0 3)) simplify auto-instantiate-existential (weaken (0 1)) (assume-theorem a%even-a%odd-a%inf-cover-dom-of-f) (contrapose"a%even union a%odd union a%inf=dom{f}") extensionality (instantiate-existential ("x_2")) simplify (cut-with-single-formula"x_2 in a%odd") (cut-with-single-formula"f(x_1) in b%odd") (cut-with-single-formula"f(x_1) in b%even") (instantiate-transported-theorem a%even-a%odd-disjoint schroeder-bernstein-symmetry ("f(x_1)")) (apply-macete-with-minor-premises rev%image-of-a%odd-under-inverse-of-g) (weaken (0 2 4)) (apply-macete-with-minor-premises rev%image-of-a%even-under-f) (weaken (0 3)) simplify auto-instantiate-existential (weaken (0 1)) )))

(def-theorem h-injectiveness"injective_q{h}"lemma (theory schroeder-bernstein-theory) (proof ( (unfold-single-defined-constant-globally h) insistent-direct-inference beta-reduce-repeatedly (raise-conditional (0)) (raise-conditional (0)) (raise-conditional (0)) direct-and-antecedent-inference-strategy (instantiate-theorem f-injectiveness ("x_1""x_2")) (instantiate-theorem f-injectiveness ("x_1""x_2")) (instantiate-theorem f-injectiveness ("x_1""x_2")) (instantiate-theorem f-injectiveness ("x_1""x_2")) (apply-macete-with-minor-premises h-injectiveness-lemma) direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises h-injectiveness-lemma) direct-and-antecedent-inference-strategy (force-substitution"x_1=x_2""x_2=x_1"(0)) (apply-macete-with-minor-premises h-injectiveness-lemma) direct-and-antecedent-inference-strategy (weaken (0 1 2)) simplify (force-substitution"x_1=x_2""x_2=x_1"(0)) (apply-macete-with-minor-premises h-injectiveness-lemma) direct-and-antecedent-inference-strategy (instantiate-transported-theorem inverse-is-injective () ("g")) (backchain"injective_q{inverse{g}}") simplify )))

(def-theorem dom-of-h"total_q{dom{h},sets[ind_1]}"lemma (theory schroeder-bernstein-theory) (proof ( (unfold-single-defined-constant-globally h) insistent-direct-inference simplify (raise-conditional (0)) direct-and-antecedent-inference-strategy (cut-with-single-formula"x_0 in a%odd") (instantiate-transported-theorem b%odd-subseteq-of-ran-of-f schroeder-bernstein-symmetry ("x_0")) (incorporate-antecedent"with(x_0:ind_1,x_0 in ran{g})") simplify direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises eliminate-iota-macete) (instantiate-existential ("x")) (instantiate-theorem g-injectiveness ("j""x")) (assume-theorem a%even-a%odd-a%inf-cover-dom-of-f) (contrapose"a%even union a%odd union a%inf=dom{f}") extensionality (instantiate-existential ("x_0")) simplify )))

(def-theorem ran-of-h-lemma-1"forall(x_0:ind_2, x_0 in b%inf implies forsome(x:ind_1, x_0 =if(x in a%inf or x in a%even, f(x), iota(y:ind_2,g(y)=x))))"lemma (theory schroeder-bernstein-theory) (proof ( direct-and-antecedent-inference-strategy (instantiate-theorem b%inf-subseteq-of-ran-of-f ("x_0")) (contrapose"with(x_0:ind_2,x_0 in ran{f})") simplify direct-inference (contrapose"with(p:prop, forall(x:ind_1,p))") (instantiate-existential ("inverse{f}(x_0)")) (cut-with-single-formula"inverse{f}(x_0) in a%inf") (incorporate-antecedent"with(x_0:ind_2,inverse{f}(x_0) in a%inf)") (raise-conditional (0)) simplify direct-inference (eliminate-defined-iota-expression 0 w) (contrapose"with(x_0:ind_2,x_0 in b%inf)") (apply-macete-with-minor-premises rev%image-of-a%inf-under-f) simplify direct-and-antecedent-inference-strategy (contrapose"with(x_0:ind_2,not(inverse{f}(x_0) in a%inf))") simplify (eliminate-iota 0) (instantiate-existential ("x_$0")) (instantiate-theorem f-injectiveness ("z%iota""x_$0")) (eliminate-iota 0) (instantiate-existential ("x")) (instantiate-theorem f-injectiveness ("z%iota""x")) )))

(def-theorem ran-of-h-lemma-2"forall(x_0:ind_2, x_0 in b%odd implies forsome(x:ind_1, x_0 =if(x in a%inf or x in a%even, f(x), iota(y:ind_2,g(y)=x))))"lemma (theory schroeder-bernstein-theory) (proof ( direct-and-antecedent-inference-strategy (instantiate-theorem b%odd-subseteq-of-ran-of-f ("x_0")) (contrapose"with(x_0:ind_2,x_0 in ran{f})") simplify direct-inference (contrapose"with(p:prop, forall(x:ind_1,p))") (instantiate-existential ("inverse{f}(x_0)")) (cut-with-single-formula"inverse{f}(x_0) in a%even") (incorporate-antecedent"with(x_0:ind_2,inverse{f}(x_0) in a%even);") (raise-conditional (0)) simplify direct-inference (eliminate-defined-iota-expression 0 w) (contrapose"with(x_0:ind_2,x_0 in b%odd);") (apply-macete-with-minor-premises rev%image-of-a%even-under-f) simplify direct-and-antecedent-inference-strategy (contrapose"with(x_0:ind_2,not(inverse{f}(x_0) in a%even));") simplify (eliminate-iota 0) (instantiate-existential ("x_$0")) (instantiate-theorem f-injectiveness ("z%iota""x_$0")) (eliminate-iota 0) (instantiate-existential ("x")) (instantiate-theorem f-injectiveness ("z%iota""x")) )))

(def-theorem ran-of-h-lemma-3"forall(x_0:ind_2, x_0 in b%even implies forsome(x:ind_1, x_0 =if(x in a%inf or x in a%even, f(x), iota(y:ind_2,g(y)=x))))"lemma (theory schroeder-bernstein-theory) (proof ( direct-and-antecedent-inference-strategy (instantiate-existential ("g(x_0)")) (raise-conditional (0)) direct-and-antecedent-inference-strategy (contrapose"with(x_0:ind_2,g(x_0) in a%inf)") (apply-macete-with-minor-premises tr%rev%image-of-a%inf-under-f) simplify direct-and-antecedent-inference-strategy (instantiate-theorem g-injectiveness ("x_0""x")) (instantiate-transported-theorem a%even-a%inf-disjoint schroeder-bernstein-symmetry ("x")) (simplify-antecedent"with(x:ind_2,not(x in b%even))") (assume-transported-theorem image-of-a%even-under-f schroeder-bernstein-symmetry) (contrapose"image{g,b%even}=a%odd") extensionality (instantiate-existential ("g(x_0)")) simplify direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop, forall(x:ind_2,p))"("x_0")) (raise-conditional (0)) simplify direct-and-antecedent-inference-strategy (instantiate-theorem a%even-a%odd-disjoint ("g(x_0)")) (simplify-antecedent"with(x_0:ind_2,not(g(x_0) in a%odd))") (instantiate-theorem a%even-a%odd-disjoint ("g(x_0)")) (apply-macete-with-minor-premises eliminate-iota-macete) direct-and-antecedent-inference-strategy (instantiate-theorem g-injectiveness ("b""x_0")) )))

(def-theorem ran-of-h"total_q{ran{h},sets[ind_2]}"lemma (theory schroeder-bernstein-theory) (proof ( (unfold-single-defined-constant-globally h) insistent-direct-inference simplify (cut-with-single-formula"x_0 in b%inf or x_0 in b%odd or x_0 in b%even") (antecedent-inference"with(p,q,r:prop, p or q or r)") (apply-macete-with-minor-premises ran-of-h-lemma-1) (apply-macete-with-minor-premises ran-of-h-lemma-2) (apply-macete-with-minor-premises ran-of-h-lemma-3) (assume-transported-theorem a%even-a%odd-a%inf-cover-dom-of-f schroeder-bernstein-symmetry) (contrapose"b%even union b%odd union b%inf=dom{g}") extensionality (instantiate-existential ("x_0")) simplify )))

(def-theorem h-surjectiveness"surjective_q{h}"lemma (theory schroeder-bernstein-theory) (proof ( insistent-direct-inference (apply-macete-with-minor-premises dom-of-h) (apply-macete-with-minor-premises ran-of-h) )))

(def-theorem h-bijectiveness ; first proved by r. givan"bijective_q{h}"lemma (theory schroeder-bernstein-theory) (proof ( insistent-direct-inference (apply-macete-with-minor-premises h-surjectiveness) (apply-macete-with-minor-premises h-injectiveness) )))