English
Destruct on the mapped sequence corresponds to mapping and then destructing: destruct (map f s) = Computation.map (Option.map (Prod.map f (map f))) (destruct s).
Русский
Разложение для отображённой последовательности соответствует отображению и затем разложению: destruct (map f s) = Computation.map (Option.map (Prod.map f (map f))) (destruct s).
LaTeX
$$$$ \\operatorname{destruct}(\\operatorname{map} f s) = \\operatorname{Computation}.map (\\operatorname{Option.map} (\\operatorname{Prod.map} f (\\operatorname{map} f))) (\\operatorname{destruct} s) $$$$
Lean4
theorem destruct_map (f : α → β) (s : WSeq α) :
destruct (map f s) = Computation.map (Option.map (Prod.map f (map f))) (destruct s) :=
by
apply
Computation.eq_of_bisim fun c1 c2 =>
∃ s, c1 = destruct (map f s) ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s)
· intro c1 c2 h
obtain ⟨s, h⟩ := h
rw [h.left, h.right]
induction s using WSeq.recOn <;> simp
case think s => exact ⟨s, rfl, rfl⟩
· exact ⟨s, rfl, rfl⟩
