Binary intersection formalized

Abstract

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{\}}^{\ast }\cap \{u,v{\}}^{\ast }$. 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.