A Proof of the Schröder-Bernstein Theorem in ACL2

The Schrder-Bernstein theorem states that, for any two sets P and Q, if there exists an injection from P to Q and an injection from Q to P, then there must exist a bijection between the two sets.Classically, it follows that the ordering of the cardinal numbers is antisymmetric.We describe a formulation and verification of the Schrder-Bernstein theorem in ACL2 following a well-known proof, introducing a theory of chains to define a non-computable witness.1 To generalize the argument to arbitrary sets, we need only tag elements reflecting their association with one of the two sets.Indeed, we employ this strategy in the ACL2 formalization.