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?

cheers

chris

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

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

Best,
Tjark



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



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