- λsrc,sig,n,is_startc,is_endc.λt: Vector (tape sig) (S n).
- ∃start,xs,end.
- nth src (tape sig) t (niltape sig) = midtape ? [] start (xs@[end]) ∧
- is_startc start = true ∧
- (∀c.c ∈ (xs@[end]) = true → is_startc c = false) ∧
- (∀c.c ∈ (start::xs) = true → is_endc c = false) ∧
- is_endc end = true.
+ λsrc,sig,n.λt: Vector (tape sig) (S n).
+ ∃x,xs.
+ nth src (tape sig) t (niltape sig) = midtape ? [] x xs.