English
Let L be a word in the free group on α. The predicate IsReduced(L) holds exactly when no two consecutive symbols cancel, i.e. for every consecutive pair (a1, s1), (a2, s2) in L, if a1 = a2 then s1 = s2.
Русский
Пусть L — слово в свободной группе на α. Соотношение IsReduced(L) верно тогда и только тогда, когда две соседние буквы не отменяют друг друга, т.е. для каждой соседней пары (a1, s1), (a2, s2) в L, если a1 = a2, то s1 = s2.
LaTeX
$$$\operatorname{IsReduced}(L) \iff \forall i,\ 0 \le i < |L|-1:\ \text{fst}(L_i) = \text{fst}(L_{i+1}) \Rightarrow \text{snd}(L_i) = \text{snd}(L_{i+1}).$$$
Lean4
/-- Predicate asserting that the word `L` admits no reduction steps, i.e., no two neighboring
elements of the word cancel. -/
@[to_additive /-- Predicate asserting the word `L` admits no reduction steps,
i.e., no two neighboring elements of the word cancel. -/
]
def IsReduced (L : List (α × Bool)) : Prop :=
L.IsChain fun a b ↦ a.1 = b.1 → a.2 = b.2
