Email Gateway (Sep 17 2026 at 16:11): Email Gateway (Sep 17 2026 at 16:11):From: Dmitriy Traytel <cl-isabelle-users@lists.cam.ac.uk>
Subject: [isabelle] New in the AFP: Greibach's Hardest Context-Free Language
Tobias Nipkow continues his context-free conquest and now he has formalized a hardest of them all.
Greibach's Hardest Context-Free Language
Formalization of Greibach’s hardest context-free language theorem: There is a “hardest” context-free language L_0 such that every context-free language is an inverse homomorphic image of L_0.
https://isa-afp.org/entries/Greibach_Hardest.html
Enjoy!
Last updated: Sep 17 2026 at 22:43 UTC