English
If f is right-commutative, then folding f over two permutation-related lists gives equal results for any initial accumulator.
Русский
Если f правосторонне коммутативна, то свёртка f по двум спискам, которые являются перестановками друг друга, даёт одинаковый результат для любого начального аккумулятора.
LaTeX
$$$\\text{Forall } b, \\ \\operatorname{foldl} f\\; b\\; l_1 = \\operatorname{foldl} f\\; b\\; l_2$ whenever $l_1 \\sim l_2$ and $f$ is right-commutative$$
Lean4
theorem foldl_eq {f : β → α → β} {l₁ l₂ : List α} [rcomm : RightCommutative f] (p : l₁ ~ l₂) :
∀ b, foldl f b l₁ = foldl f b l₂ :=
p.foldl_eq' fun x _hx y _hy z => rcomm.right_comm z x y
