English
For f: α → β → σ → σ × γ with s0, if S, h0, closure, and out hold as in the invariant lemma, then (mapAccumr₂ f xs ys s0).snd = map₂ (λ x y, (f x y s0).snd) xs ys.
Русский
Для f: α → β → σ → σ × γ с состоянием s0, если выполняются условия S, h0, closure, и out как в лемме инвариантности, то (mapAccumr₂ f xs ys s0).snd = map₂ (λ x y, (f x y s0).snd) xs ys.
LaTeX
$$$$ (\operatorname{mapAccumr_2} f xs ys s_0).snd = \operatorname{map}_2\bigl(\lambda x y, (f x y s_0).snd\bigr) xs ys $$$$
Lean4
/-- If `f` takes a pair of states, but always returns the same value for both elements of the
pair, then we can simplify to just a single element of state.
-/
@[simp]
theorem mapAccumr₂_redundant_pair (f : α → β → (σ × σ) → (σ × σ) × γ)
(h :
∀ x y s,
let s' := (f x y (s, s)).fst;
s'.fst = s'.snd) :
(mapAccumr₂ f xs ys (s, s)).snd =
(mapAccumr₂ (fun x y (s : σ) => (f x y (s, s) |>.fst.fst, f x y (s, s) |>.snd)) xs ys s).snd :=
mapAccumr₂_bisim_tail <| by
use fun (s₁, s₂) s => s₂ = s ∧ s₁ = s
simp_all
