[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: hlp



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