mapAccumr₂_mapAccumr₂_left_right

English

A left-right bisimulation identity for mapAccumr₂ over two vectors.

Русский

Бисимуляция слева направо для mapAccumr₂ по двум векторам.

LaTeX

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

Lean4

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

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