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).
Larry Paulson


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 ;)).
> 
> cheers
> 
> chris
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.