English
Describes how reduce behaves with a leading element: reduce(x :: L) equals the case analysis of reduce(L) with a conditional elimination of adjacent inverse pairs.
Русский
Характеризуется поведение редукции при добавлении слева элемента: reduce(x :: L) выражается через разбор reduce(L) с условным удалением соседних взаимно противоположных пар.
LaTeX
$$$$\operatorname{reduce}(x :: L) = \mathrm{List}.\mathrm{casesOn}(\operatorname{reduce}L) [x] (\lambda hd\ tl \to \text{if } x.1 = hd.1 \land x.2 = \lnot hd.2 \text{ then } tl \text{ else } x :: hd :: tl).$$$$
Lean4
@[to_additive (attr := simp)]
theorem cons (x) :
reduce (x :: L) =
List.casesOn (reduce L) [x] fun hd tl => if x.1 = hd.1 ∧ x.2 = not hd.2 then tl else x :: hd :: tl :=
rfl
