English
Concatenation of streams is associative: (s ++ t) ++ u = s ++ (t ++ u).
Русский
Объединение последовательностей по конкатенации ассоциативно: (s ++ t) ++ u = s ++ (t ++ u).
LaTeX
$$$\forall s\, t\, u,\; append (append s t) u = append s (append t u)$$$
Lean4
@[simp]
theorem append_assoc (s t u : Seq α) : append (append s t) u = append s (append t u) :=
by
apply eq_of_bisim fun s1 s2 => ∃ s t u, s1 = append (append s t) u ∧ s2 = append s (append t u)
· intro s1 s2 h
exact
match s1, s2, h with
| _, _, ⟨s, t, u, rfl, rfl⟩ => by
cases s <;> simp
case nil =>
cases t <;> simp
case nil =>
cases u <;> simp
case cons _ u => refine ⟨nil, nil, u, ?_, ?_⟩ <;> simp
case cons _ t => refine ⟨nil, t, u, ?_, ?_⟩ <;> simp
case cons _ s => exact ⟨s, t, u, rfl, rfl⟩
· exact ⟨s, t, u, rfl, rfl⟩
