English
A word L over α with a Boolean tagging is cyclically reduced if it is reduced and the first and last letters do not cancel; the empty word is cyclically reduced by convention.
Русский
Слово L над α с пометкой Bool циклически сокращено, если оно сокращено и первая и последняя буквы не аннулируются; пустое слово считается циклически сокращенным по соглашению.
LaTeX
$$$$ \\mathrm{IsCyclicallyReduced}(L) \\;\\equiv\\; \\mathrm{IsReduced}(L) \\land \\forall a \\in L.getLast?, \\forall b \\in L.head?, a.1 = b.1 \\rightarrow a.2 = b.2. $$$$
Lean4
/-- Predicate asserting that the word `L` is cyclically reduced, i.e., it is reduced and furthermore
the first and the last letter of the word do not cancel. The empty word is by convention also
cyclically reduced. -/
@[to_additive /-- Predicate asserting that the word `L` is cyclically reduced, i.e., it is reduced
and furthermore the first and the last letter of the word do not cancel. The empty word is by
convention also cyclically reduced. -/
]
def IsCyclicallyReduced (L : List (α × Bool)) : Prop :=
IsReduced L ∧ ∀ a ∈ L.getLast?, ∀ b ∈ L.head?, a.1 = b.1 → a.2 = b.2
