Overlap-free words
DefinitionOverlaps in words#✓fully proved
MetaMathlibExt.IsWordOverlap
A finite word \(o\) over an alphabet \(\alpha\) is an overlap if \(o = xyxyx\) for some finite words \(x\) and \(y\) over \(\alpha\) with \(x\) nonempty; \(y\) may be empty.
Here \(x\) may have any positive length, not only length one.
public def IsWordOverlap {α : Type*} (o : List α) : Prop :=
∃ x y : List α, x ≠ [] ∧ o = x ++ y ++ x ++ y ++ xUsed by 1
Used byOverlap-free binary words
DefinitionOverlap-free binary words#✓fully proved
MetaMathlibExt.IsOverlapFreeBinaryWord
A finite binary word is overlap-free when none of its contiguous factors is an overlap.
public def IsOverlapFreeBinaryWord (w : List Bool) : Prop :=
∀ o : List Bool, o.IsInfix w → ¬ IsWordOverlap opublic def IsWordOverlap {α : Type*} (o : List α) : Prop :=
∃ x y : List α, x ≠ [] ∧ o = x ++ y ++ x ++ y ++ xMathlibExt/Combinatorics/InfiniteWord/OverlapFreeBinaryWord.lean:29
Uses 1
Statement usesOverlaps in words
2 fully proved
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.