English
Joining a stream with a head a and tail s yields a stream whose head is a and whose tail is the join of s with the tail context.
Русский
Объединение потока с головой a и хвостом s даёт поток с головой a и хвостом, равным объединению.
LaTeX
$$$\forall a\, s\, S,\; join (cons (a, s) S) = cons a (append s (join S))$$$
Lean4
@[simp]
theorem join_cons (a : α) (s S) : join (cons (a, s) S) = cons a (append s (join S)) :=
by
apply
eq_of_bisim (fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = join (cons (a, s) S) ∧ s2 = cons a (append s (join S))) _
(Or.inr ⟨a, s, S, rfl, rfl⟩)
intro s1 s2 h
exact
match s1, s2, h with
| s, _, Or.inl <| Eq.refl s => by
cases s; · trivial
· rw [destruct_cons]
exact ⟨rfl, Or.inl rfl⟩
| _, _, Or.inr ⟨a, s, S, rfl, rfl⟩ => by
cases s
· simp [join_cons_nil]
· simpa [join_cons_cons, join_cons_nil] using Or.inr ⟨_, _, S, rfl, rfl⟩
