Re: [isabelle] extending well-founded partial orders to total well-founded orders
This obviously requires the axiom of choice (after all, the empty relation is well-founded), and is trivial with it (simply well-order the set of unrelated elements).
On 17 Jan 2013, at 06:55, Christian Sternagel <c.sternagel at gmail.com> wrote:
> Dear all,
> is anybody aware of an Isabelle formalization of the (apparently well-known) fact that every well-founded partial order can be extended to a total well-founded order (in particular a well-partial-order)?
> If not, any pointers to "informal" proofs (i.e., papers or textbooks ;)).
This archive was generated by a fusion of
Pipermail (Mailman edition) and