### Abstract

This article provides a formalization of the classification of intersection \( \{x,y\}^* \cap \{u,v\}^*\) of two monoids generated by two element codes. Namely, the intersection has one of the following forms \( \{\beta,\gamma\}^* \quad \text{ or } \quad \left(\beta_0 + \beta(\gamma(1+\delta+ \cdots + \delta^t))^*\epsilon\right)^*.\) Note that it can be infinitely generated. The result is due to [Karhumäki, 84]. Our proof uses the terminology of morphisms which allows us to formulate the result in a shorter and more transparent way.

### License

BSD License

### History

August 17, 2023
  Updated to version v1.10.1.

### Topics

- Computer science/Automata and formal languages

### Related publications

- Karhumäki, J. (n.d.). A note on intersections of free submonoids of a free monoid. Lecture Notes in Computer Science, 397–407. https://doi.org/10.1007/bfb0036924
- Development repository

### Session Two_Generated_Word_Monoids_Intersection

- Two_Generated_Word_Monoids_Intersection

### Depends on

- Combinatorics on Words Basics
- Graph Lemma

## Cite

×

Two_Generated_Word_Monoids_Intersection-AFP

    @article{Two_Generated_Word_Monoids_Intersection-AFP,
      author  = {Štěpán Holub and Štěpán Starosta},
      title   = {Intersection of two monoids generated by two element codes},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Two_Generated_Word_Monoids_Intersection.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Mar 16, 2023 : Isabelle2022