[isabelle] extending well-founded partial orders to total well-founded orders

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 MHonArc.