English
Red L (reduce L) expresses that reduce is related to L by the Red relation.
Русский
Отношение Red связывает слово L с его редуцированным образом reduce L.
LaTeX
$$$$\operatorname{Red}(L, \operatorname{reduce}(L)).$$$$
Lean4
/-- The first theorem that characterises the function `reduce`: a word reduces to its maximal
reduction. -/
@[to_additive /-- The first theorem that characterises the function `reduce`: a word reduces to its
maximal reduction. -/
]
theorem red : Red L (reduce L) := by
induction L with
| nil => constructor
| cons hd1 tl1 ih =>
dsimp
revert ih
generalize htl : reduce tl1 = TL
intro ih
cases TL with
| nil => exact Red.cons_cons ih
| cons hd2 tl2 =>
dsimp only
split_ifs with h
· cases hd1
cases hd2
cases h
dsimp at *
subst_vars
apply Red.trans (Red.cons_cons ih)
exact Red.Step.cons_not_rev.to_red
· exact Red.cons_cons ih
