English
A bi-accumulation identity for two vectors indicates the rightmost composition matches the direct accumulation result.
Русский
Би-аккумуляционная идентичность для двух векторов: правая композиция совпадает с прямым результатом аккумуляции.
LaTeX
$$$\forall xs:\mathrm{List.Vector}\;\alpha\;n,\; \forall ys:\mathrm{List.Vector}\;\beta\;n,\; \forall f_1,f_2,\; \mathrm{...}$$$
Lean4
@[simp]
theorem mapAccumr_mapAccumr₂ (f₁ : γ → σ₁ → σ₁ × ζ) (f₂ : α → β → σ₂ → σ₂ × γ) :
(mapAccumr f₁ (mapAccumr₂ f₂ xs ys s₂).snd s₁) =
let m :=
mapAccumr₂
(fun x y s =>
let r₂ := f₂ x y s.snd
let r₁ := f₁ r₂.snd s.fst
((r₁.fst, r₂.fst), r₁.snd))
xs ys (s₁, s₂)
(m.fst.fst, m.snd) :=
by induction xs, ys using Vector.revInductionOn₂ generalizing s₁ s₂ <;> simp_all
