mapAccumr₂_mapAccumr₂_right_right

English

Right-right bisimulation identity for mapAccumr₂.

Русский

Правая справа бисимуляция для mapAccumr₂.

LaTeX

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

Lean4

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

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