English
Same as above: if the initial state does not change in the accumulation, then mapAccumr₂ f xs ys s = (s, map₂ (λ x y, (f x y s).snd) xs ys).
Русский
То же самое: если начальное состояние не изменяется в ходе аккумуляции, тогда 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 b, (f a b s).fst = s) :
mapAccumr₂ f xs ys s = (s, (map₂ (fun x y => (f x y s).snd) xs ys)) := by
induction xs, ys using revInductionOn₂ <;> simp_all
