English
Destruct on the join of S equals the bind of destruct on S with the auxiliary function destruct_join.aux.
Русский
Разложение для объединения join S равно связыванию разложения над S с вспомогательной функцией destruct_join.aux.
LaTeX
$$$$ \\operatorname{destruct}(\\mathrm{join} S) = (\\operatorname{destruct} S).bind \\operatorname{destruct\\_join}.aux $$$$
Lean4
theorem destruct_join (S : WSeq (WSeq α)) : destruct (join S) = (destruct S).bind destruct_join.aux :=
by
apply
Computation.eq_of_bisim
(fun c1 c2 => c1 = c2 ∨ ∃ S, c1 = destruct (join S) ∧ c2 = (destruct S).bind destruct_join.aux) _
(Or.inr ⟨S, rfl, rfl⟩)
intro c1 c2 h
exact
match c1, c2, h with
| c, _, Or.inl <| rfl => by cases c.destruct <;> simp
| _, _, Or.inr ⟨S, rfl, rfl⟩ => by
induction S using WSeq.recOn <;> simp
case think S => refine Or.inr ⟨S, rfl, rfl⟩
