English
For two vectors v1, v2 of the same length n and a function f with three arguments, mapping with a state over both components preserves the head-tail structure analogous to mapAccumr_cons.
Русский
Для двух векторов v1, v2 одинаковой длины n и функции f с тремя аргументами отображение с состоянием над парами сохраняет структуру головы и хвоста аналогично mapAccumr_cons.
LaTeX
$$$\\mathrm{mapAccumr}\\!\\_2\\; f\\; (x \\;::ᵥ\\; xs)\\;(y \\;::ᵥ\\; ys)\\; s = \\n let r := \\mathrm{mapAccumr}\\!\\_2\\; f\\; xs\\; ys\\; s\\n let q := f\\ x\\ y\\ r.1\\n (q.1, q.2 ::ᵥ r.2)$$$
Lean4
@[simp]
theorem mapAccumr₂_cons {f : α → β → σ → σ × φ} :
mapAccumr₂ f (x ::ᵥ xs) (y ::ᵥ ys) s =
let r := mapAccumr₂ f xs ys s
let q := f x y r.1
(q.1, q.2 ::ᵥ r.2) :=
rfl
