Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The number of primitive words of unbounded exponent in the language of an HD0L-system is finite

Karel Klouda, Štěpán Starosta

Abstract

Let $H$ be an HD0L-system. We show that there are only finitely many primitive words $v$ with the property that $v^k$, for all integers $k$, is an element of the factorial language of $H$. In particular, this result applies to the set of all factors of a morphic word. We provide a formalized proof in the proof assistant Isabelle/HOL as part of the Combinatorics on Words Formalized project.

The number of primitive words of unbounded exponent in the language of an HD0L-system is finite

Abstract

Let be an HD0L-system. We show that there are only finitely many primitive words with the property that , for all integers , is an element of the factorial language of . In particular, this result applies to the set of all factors of a morphic word. We provide a formalized proof in the proof assistant Isabelle/HOL as part of the Combinatorics on Words Formalized project.

Paper Structure

This paper contains 9 sections, 11 theorems, 15 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. References to the formalization
  4. The language $L_G$
  5. The language $L_H$
  6. Notes on the formalization
  7. Final remarks
  8. The case of $\Psi$ erasing
  9. An algorithm to count primitive words of unbounded exponents of $L_H$

Key Result

theorem \oldthetheorem

There exist finite sets $W$ and $U$ such that every bounded $w \in L_G$ is of the form where $w_1,w_2,w_3 \in W$, $u_1, u_2 \in U$, and $k_1,k_2 \in \mathbb{N}$.

Theorems & Definitions (23)

  • theorem \oldthetheorem: long_bounded_factor
  • Lemma \oldthetheorem: non_pushy_subset_unbounded_image
  • proof
  • Lemma \oldthetheorem: bound_occ_prim_unb_exp
  • proof
  • Definition \oldthetheorem
  • Lemma \oldthetheorem: pow_subalph_l_ev_per_all
  • proof
  • Lemma \oldthetheorem: inv_sub_bot_pow_subalph
  • proof
  • ...and 13 more