as:T*, i:{0...||as||}, j:{i...||as||}, k:{j...||as||}.
((as[i..j
]) @ (as[j..k])) = (as[i..k])
append_segment
| i
k & kj }
Thm* as:T*, i:{0...||as||}, j:{i...||as||}, k:{j...||as||}.
((as[i..j]) @ (as[j..k])) = (as[i..k])
append_segment