English
If f never changes the state component, i.e., (f a s).fst = s for all a and s, then mapAccumr₂ f xs ys s equals (s, map₂ (λ x y, (f x y s).snd) xs ys).
Русский
Если функция f не изменяет состояние, то есть (f a s).fst = s для всех a, s, тогда mapAccumr₂ f xs ys s = (s, map₂ (λ x y, (f x y s).snd) xs ys).
LaTeX
$$$$ \operatorname{mapAccumr_2} f\, xs\, ys\, s = \left( s, \operatorname{map}_2\bigl(\lambda x\, y, (f x y s).snd\bigr) xs\ ys \right) $$$$
Lean4
/-- If an accumulation function `f`, given an initial state `s`, produces `s` as its output state
for all possible input bits, then the state is redundant and can be optimized out.
-/
@[simp]
theorem mapAccumr_eq_map_of_constant_state (f : α → σ → σ × β) (s : σ) (h : ∀ a, (f a s).fst = s) :
mapAccumr f xs s = (s, (map (fun x => (f x s).snd) xs)) := by induction xs using revInductionOn <;> simp_all
