Binary intersection formalized
2020-06-30Code Available0· sign in to hype
Štěpán Holub, Štěpán Starosta
Code Available — Be the first to reproduce this paper.
ReproduceCode
- gitlab.com/formalcow/combinatorics-on-words-formalizedOfficialIn papernone★ 0
Abstract
We provide a reformulation and a formalization of the classical result by Juhani Karhum\"aki characterizing intersections of two languages of the form ,y\^* ,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.