论文标题
二元交叉点正式化
Binary intersection formalized
论文作者
论文摘要
我们通过juhanikarhumäki来对经典结果进行重新制定和形式化，以表征$ \ {x，y \}^*\ cap \ {u，v \}^*$的两种语言的交集。我们使用形态学的术语，可以以更短，更透明的方式制定结果，并在证明助手Isabelle/Hol中形式化结果。
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\}^*\cap \{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.
