English
Joining the concatenation of streams distributes over joining: join (append S T) = append (join S) (join T).
Русский
Объединение конкатенации потоков распределяется над объединением: join (append S T) = append (join S) (join T).
LaTeX
$$$\forall S\, T : Seq (Seq1 \alpha),\; join (append S T) = append (join S) (join T)$$$
Lean4
@[simp]
theorem join_append (S T : Seq (Seq1 α)) : join (append S T) = append (join S) (join T) :=
by
apply eq_of_bisim fun s1 s2 => ∃ s S T, s1 = append s (join (append S T)) ∧ s2 = append s (append (join S) (join T))
· intro s1 s2 h
exact
match s1, s2, h with
| _, _, ⟨s, S, T, rfl, rfl⟩ => by
cases s <;> simp
case nil =>
cases S <;> simp
case nil =>
cases T with
| nil => simp
| cons s T =>
obtain ⟨a, s⟩ := s; simp only [join_cons, destruct_cons, true_and]
refine ⟨s, nil, T, ?_, ?_⟩ <;> simp
case cons s S =>
obtain ⟨a, s⟩ := s
simpa using ⟨s, S, T, rfl, rfl⟩
case cons _ s => exact ⟨s, S, T, rfl, rfl⟩
· refine ⟨nil, S, T, ?_, ?_⟩ <;> simp
