English
Reduction of inverse-reverse with left cancellation yields the empty word: reduce (invRev L ++ L) = [].
Русский
Редукция invRev(L) с левой стороны от L даёт пустое слово: reduce (invRev L ++ L) = [].
LaTeX
$$$\forall L : List(Prod\;\alpha\;Bool),\; \mathrm{reduce}(\mathrm{invRev} L ++ L) = []$$$
Lean4
instance decidableRel : DecidableRel (@Red α)
| [], [] => isTrue Red.refl
| [], _hd2 :: _tl2 => isFalse fun H => List.noConfusion (Red.nil_iff.1 H)
| (x, b) :: tl, [] =>
match Red.decidableRel tl [(x, not b)] with
| isTrue H => isTrue <| Red.trans (Red.cons_cons H) <| (@Red.Step.not _ [] [] _ _).to_red
| isFalse H => isFalse fun H2 => H <| Red.cons_nil_iff_singleton.1 H2
| (x1, b1) :: tl1, (x2, b2) :: tl2 =>
if h : (x1, b1) = (x2, b2) then
match Red.decidableRel tl1 tl2 with
| isTrue H => isTrue <| h ▸ Red.cons_cons H
| isFalse H => isFalse fun H2 => H <| (Red.cons_cons_iff _).1 <| h.symm ▸ H2
else
match Red.decidableRel tl1 ((x1, !b1) :: (x2, b2) :: tl2) with
| isTrue H => isTrue <| (Red.cons_cons H).tail Red.Step.cons_not
| isFalse H => isFalse fun H2 => H <| Red.inv_of_red_of_ne h H2
