if 0 < 
x+1
u.firstn(x+1-1;v) else nil fi = (if 0 < x u.firstn(x-1;v) else nil fi @ [(u.v)[x]])
as:T*. x-1 < ||as|| 
firstn(x-1+1;as) = (firstn(x-1;as) @ [as[(x-1)]]) firstn(x+1;u.v) = (firstn(x;u.v) @ [(u.v)[x]])| 1 | if 0 < x+1 u.firstn(x+1-1;v) else nil fi = (if 0 < x u.firstn(x-1;v) else nil fi @ [(u.v)[x]]) |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |