English
If Red( reduce(L1) , L2 ), then reduce(L1) equals L2; i.e., the maximal reduction of L1 equals L2 when L2 is a maximal reduction of L1.
Русский
Если Red( уменьшаемое(L1) , L2 ), то reduce(L1) = L2; т.е. максимальное редуцирование L1 совпадает с L2.
LaTeX
$$$$\text{If } \operatorname{Red}(\operatorname{reduce}(L_1), L_2) \text{ then } \operatorname{reduce}(L_1) = L_2.$$$$
Lean4
/-- The second theorem that characterises the function `reduce`: the maximal reduction of a word
only reduces to itself. -/
@[to_additive /-- The second theorem that characterises the function `reduce`: the maximal
reduction of a word only reduces to itself. -/
]
theorem min (H : Red (reduce L₁) L₂) : reduce L₁ = L₂ := by
induction H with
| refl => rfl
| tail _ H1 H2 =>
obtain ⟨L4, L5, x, b⟩ := H1
exact reduce.not H2
