(def-language schroeder-bernstein-language
    (embedded-language generic-theory-2)
    (constants
        (f "[ind_1,ind_2]")
        (g "[ind_2,ind_1]")))

(def-theory schroeder-bernstein-theory 
    (language schroeder-bernstein-language)
    (component-theories generic-theory-2)
    (axioms
      (f-totality "total_q{f,[ind_1,ind_2]}" d-r-convergence)
      (g-totality "total_q{g,[ind_2,ind_1]}" d-r-convergence)
      (f-injectiveness "injective_q{f}")
      (g-injectiveness "injective_q{g}")))

(def-recursive-constant (a%seq b%seq) 
    ("lambda(a%seq_0:[nn,sets[ind_1]],b%seq_0:[nn,sets[ind_2]],
            lambda(i:nn,
                if(i=0, 
                      dom{f},
                      lambda(dummy:sets[ind_2],
                          if(#(dummy), image{g, dummy}, ?[ind_1,unit%sort]))
                      (b%seq_0(i-1)))))"
      "lambda(a%seq_0:[nn,sets[ind_1]],b%seq_0:[nn,sets[ind_2]],
            lambda(i:nn,
                if(i=0, 
                      dom{g},
                      lambda(dummy:sets[ind_1],
                          if(#(dummy), image{f, dummy}, ?[ind_2,unit%sort]))
                      (a%seq_0(i-1)))))")
  (theory schroeder-bernstein-theory)
  (definition-name schroeder-bernstein-set-functions))

(def-translation schroeder-bernstein-symmetry 
    (source schroeder-bernstein-theory)
    (target schroeder-bernstein-theory)
    (fixed-theories h-o-real-arithmetic)
    (sort-pairs
      (ind_1 ind_2)
      (ind_2 ind_1))
    (constant-pairs
      (f "g")
      (g "f")
      (a%seq "b%seq")
      (b%seq "a%seq"))
    force-under-quick-load)

(def-constant last%a%index 
    "lambda(x:ind_1, iota(i:nn, x in (a%seq(i) diff a%seq(1+i))))"
    (theory schroeder-bernstein-theory))

(def-constant a%inf 
    "indic(x:ind_1, not(#(last%a%index(x))))"
    (theory schroeder-bernstein-theory))

(def-constant a%even 
    "indic(x:ind_1, even(last%a%index(x)))"
    (theory schroeder-bernstein-theory))

(def-constant a%odd 
    "indic(x:ind_1, odd(last%a%index(x)))"
    (theory schroeder-bernstein-theory))

(def-transported-symbols 
    (last%a%index a%inf a%even a%odd)
    (translation schroeder-bernstein-symmetry)
    (renamer sb-renamer))

(def-constant h 
    "lambda(x:ind_1, 
          if(x in a%inf or x in a%even,
                f(x),
                inverse(g)(x)))"
    (theory schroeder-bernstein-theory))

(def-theorem a-seq-b-seq-definedness 
    "forall(n:zz, 0<=n implies #(a%seq(n),sets[ind_1]) and #(b%seq(n),sets[ind_2]))"
    lemma
    (theory schroeder-bernstein-theory)
    (proof ((induction integer-inductor ("n")))))

(def-theorem a-seq-definedness 
    "total_q{a%seq,[nn,sets[ind_1]]}"
    lemma
    (theory schroeder-bernstein-theory)
    (usages d-r-convergence)
    (proof
      (
        insistent-direct-inference
        (instantiate-theorem a-seq-b-seq-definedness ("x_0"))
        (simplify-antecedent "with(x_0:nn,not(0<=x_0))")
        )))

(def-theorem b-seq-definedness 
    "total_q{b%seq,[nn,sets[ind_2]]}"
    lemma
    (theory schroeder-bernstein-theory)
    (usages d-r-convergence)
    (proof
      (
        insistent-direct-inference
        (instantiate-theorem a-seq-b-seq-definedness ("x_0"))
        (simplify-antecedent "with(x_0:nn,not(0<=x_0))")
        )))

(def-translation schroeder-bernstein->generic-theory-2 
    (source schroeder-bernstein-theory)
    (target generic-theory-2)
    (fixed-theories h-o-real-arithmetic)
    (assumptions
      "with(a:sets[ind_1],nonempty_indic_q{a})"
      "with(b:sets[ind_2],nonempty_indic_q{b})"
      "with(u:[ind_1,ind_2],a:sets[ind_1],dom{u}=a)"
      "with(v:[ind_2,ind_1],b:sets[ind_2],dom{v}=b)"
      "with(u:[ind_1,ind_2],b:sets[ind_2],ran{u} subseteq b)"
      "with(v:[ind_2,ind_1],a:sets[ind_1],ran{v} subseteq a)"
      "with(u:[ind_1,ind_2],a:sets[ind_1],injective_on_q{u,a})"
      "with(v:[ind_2,ind_1],b:sets[ind_2],injective_on_q{v,b})")
    (sort-pairs
      (ind_1 (indic "with(a:sets[ind_1],a)"))
      (ind_2 (indic "with(b:sets[ind_2],b)")))
    (constant-pairs
      (f "with(u:[ind_1,ind_2],u)")
      (g "with(v:[ind_2,ind_1],v)"))
    dont-enrich
    force-under-quick-load
    (theory-interpretation-check using-simplification))

(def-theorem sb-theorem-lemma-1 
    "forsome(h_0:[ind_1,ind_2], bijective_q{h_0})"
    lemma
    (theory generic-theory-2)
    (translation schroeder-bernstein->generic-theory-2)
    (proof
      (
        (assume-theorem h-bijectiveness)
        auto-instantiate-existential
        )))

(def-theorem sb-theorem-lemma-2 
    "forall(a:sets[ind_1], b:sets[ind_2], 
          (a=empty_indic{ind_1} or b=empty_indic{ind_2}) 
              implies
          ((a embeds b) and (b embeds a) implies (a equinumerous b)))"
    lemma
    (theory generic-theory-2)
    (proof
      (
        direct-inference
        direct-inference
        (antecedent-inference "with(p,q:prop, p or q)")
        (force-substitution "a" "empty_indic{ind_1}" (1))
        (apply-macete-with-minor-premises tr%embeds-in-empty-indic)
        direct-inference
        (backchain "with(p,q:prop, p and q)")
        (apply-macete-with-minor-premises equinumerous-to-empty-indic)
        (force-substitution "b" "empty_indic{ind_2}" (0))
        (apply-macete-with-minor-premises embeds-in-empty-indic)
        direct-inference
        (backchain "with(p,q:prop, p and q)")
        (apply-macete-with-minor-premises tr%equinumerous-is-symmetric)
        (apply-macete-with-minor-premises tr%equinumerous-to-empty-indic)
        )))

(def-theorem schroeder-bernstein-theorem 
  Remark: This entry is multiply defined. See:  [1] [2]
    "forall(a:sets[ind_1], b:sets[ind_2],
          (a embeds b) and (b embeds a) implies (a equinumerous b))"
    (theory generic-theory-2)
    (usages transportable-macete)
    (proof
      (
        direct-inference-strategy
        (case-split ("a=empty_indic{ind_1} or b=empty_indic{ind_2}"))
        (apply-macete-with-minor-premises sb-theorem-lemma-2)
        direct-inference
        (antecedent-inference-strategy (1))
        (instantiate-theorem sb-theorem-lemma-1 ("f_$1" "f_$0" "b" "a"))
        (weaken (1 2 3 4 5 6))
        (contrapose "with(p:prop, not(p))")
        (instantiate-transported-theorem equals-empty-indic-iff-empty () ("a"))
        simplify
        (weaken (1 2 3 4 5 6))
        (contrapose "with(p:prop, not(p))")
        (instantiate-transported-theorem equals-empty-indic-iff-empty () ("b"))
        simplify
        (weaken (4 5 6 7 8 9 10))
        (instantiate-existential ("h_0"))
        insistent-direct-and-antecedent-inference-strategy
        (weaken (1 3))
        extensionality
        direct-inference
        (instantiate-universal-antecedent 
          "with(a,b:sets[ind_1],  a subseteq b)" ("x_0"))
        (instantiate-universal-antecedent 
          "with(p:prop, forall(x_$0:ind_1,p))" ("x_0"))
        beta-reduce-repeatedly
        simplify
        (weaken (1))
        (incorporate-antecedent "with(p:prop, p)")
        simplify-insistently
        (weaken (0 2 3))
        extensionality
        direct-inference
        (instantiate-universal-antecedent 
          "with(a,b:sets[ind_2],  a subseteq b)" ("x_0"))
        beta-reduce-repeatedly
        (raise-conditional (0))
        simplify
        direct-inference
        (instantiate-universal-antecedent 
          "with(p:prop, forall(x_$0:ind_1,p))" ("x_$0"))
        (weaken (1 2))
        simplify
        (contrapose "with(p:prop, not(p))")
        simplify
        (weaken (1 2))
        (weaken (1))
        (incorporate-antecedent "with(p:prop, p)")
        simplify-insistently
        direct-and-antecedent-inference-strategy
        (raise-conditional (0))
        simplify
        auto-instantiate-existential
        (weaken (0 1 5 7 8))
        (backchain "with(p:prop, forall(x_1,x_2:ind_1,p))")
        direct-and-antecedent-inference-strategy
        )))