[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
This is a variant on the Schroeder-Bernstein (aka Cantor-Bernstein)
Theorem (which would have injective? rather than surjective?). The
reason it's a famous theorem is that it's quite hard to prove (in the
transfinite cases). You can look up a proof in a set theory book and
transcribe it into PVS; this will take about a day for a PVS expert
(PVS's automation is no help in these cases). Alternatively, it's a
corollary to the Knaster-Tarski Theorem, so if you already have a PVS
proof of that, you're nearly done.
Google can find PVS proofs of these theorems on the web.
John Rushby and Sam Owre