Abstract
We provide a reformulation and a formalization of the classical result by Juhani Karhumaki characterizing intersections of two languages of the form {x, y}* boolean AND {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. (C) 2021 Elsevier B.V.
All rights reserved.