English
If FreeGroup.Red.Step L1 L2 holds, then |L1| = |L2| + 2.
Русский
Если выполняется Red.Step L1 L2, то длина L1 равна длине L2 плюс 2.
LaTeX
$$$ \\text{Step}(L_1,L_2) \\Rightarrow |L_1| = |L_2| + 2.$$$
Lean4
/-- Predicate asserting that the word `w₁` can be reduced to `w₂` in one step, i.e. there are words
`w₃ w₄` and letter `x` such that `w₁ = w₃xx⁻¹w₄` and `w₂ = w₃w₄` -/
@[to_additive /-- Predicate asserting that the word `w₁` can be reduced to `w₂` in one step, i.e.
there are words `w₃ w₄` and letter `x` such that `w₁ = w₃ + x + (-x) + w₄` and `w₂ = w₃w₄` -/
]
theorem length : ∀ {L₁ L₂ : List (α × Bool)}, Step L₁ L₂ → L₂.length + 2 = L₁.length
| _, _, @Red.Step.not _ L1 L2 x b => by rw [List.length_append, List.length_append]; rfl
