mapAccumr₂_mapAccumr₂_left_left

English

A left-left accumulation identity for mapAccumr₂ over two vectors holds.

Русский

Лево-левое накопление mapAccumr₂ по двум векторам сохраняет равенство.

LaTeX

$$$\forall xs,\forall ys,\; (\mathrm{mapAccumr\_2}\; f\; xs\; ys)\; =\; \ldots$$$

Lean4

@[simp]
theorem mapAccumr₂_mapAccumr₂_left_left (f₁ : γ → α → σ₁ → σ₁ × φ) (f₂ : α → β → σ₂ → σ₂ × γ) :
    (mapAccumr₂ f₁ (mapAccumr₂ f₂ xs ys s₂).snd xs s₁) =
      let m :=
        mapAccumr₂
          (fun x y (s₁, s₂) =>
            let r₂ := f₂ x y s₂
            let r₁ := f₁ r₂.snd x s₁
            ((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

Похожие утверждения