3. 0 < ||as||
firstn(0+1;as) = (firstn(0;as) @ [as[0]])
3. 0 < x
4.
as:T*. x-1 < ||as|| 
firstn(x-1+1;as) = (firstn(x-1;as) @ [as[(x-1)]])5. as: T*
6. x < ||as||
firstn(x+1;as) = (firstn(x;as) @ [as[x]])
as:T*. x < ||as|| firstn(x+1;as) = (firstn(x;as) @ [as[x]])| 1 | 2. as: T* 3. 0 < ||as|| firstn(0+1;as) = (firstn(0;as) @ [as[0]]) |
| 2 | 2. x: 3. 0 < x 4. as:T*. x-1 < ||as|| firstn(x-1+1;as) = (firstn(x-1;as) @ [as[(x-1)]])5. as: T* 6. x < ||as|| firstn(x+1;as) = (firstn(x;as) @ [as[x]]) |
About:
 |  |  |  |  |
 |  |  |  |  |