Binary intersection formalized

06/30/2020
by   Štěpán Holub, et al.
0

We provide a reformulation and a formalization of the classical result by Juhani Karhumäki characterizing intersections of two languages of the form {x,y}^*∩{u,v}^*. We use the terminology of morphisms which allows to formulate the result in a shorter and more transparent way, and we formalize the result in the proof assistant Isabelle/HOL.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset