[isabelle] extending well-founded partial orders to total well-founded orders
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] extending well-founded partial orders to total well-founded orders
- From: Christian Sternagel <c.sternagel at gmail.com>
- Date: Thu, 17 Jan 2013 15:55:36 +0900
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130110 Thunderbird/17.0.2
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