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