Re: [isabelle] Well-foundedness of Relational Composition

Please find attached a formalization (thanks to Bertram for pointless induction having a point ;)), alas, it still relies on Regexp. Maybe someone would like to rectify this?



On 04/27/2015 01:45 PM, Tjark Weber wrote:

Thank you for the detailed literature search. Of course, I am all for
adding the much more general lemma to Wellfounded.thy.

I can try to complete the formal proof later this week. (If somebody
else wants to go ahead with this right now, I certainly don't mind.)


Attachment: Bla.thy
Description: application/extension-thy

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