Nuprl - Pf firstn_lem1 1 2 2 1 1 1 1

PrintForm Definitions list 3 autom Sections AutomataTheory Doc

1. T: Type
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. u: T
7. v: T*
8. x < ||v||+1
9. 0 < x+1
10. 0 < x

u.firstn(x+1-1;v) = ((u.firstn(x-1;v)) @ [(u.v)[x]])

By: ArithSimp 0 THEN ArithSimp 4

Generated subgoals:

1 x < ||u.v||

2 4. as:T*. -1+x < ||as|| firstn(x;as) = (firstn(-1+x;as) @ [as[(-1+x)]])
5. as: T*
6. u: T
7. v: T*
8. x < ||v||+1
9. 0 < x+1
10. 0 < x
u.firstn(x;v) = ((u.firstn(-1+x;v)) @ [(u.v)[x]])

About:

1	`x < \|\|u.v\|\|`
2	4. `as:T. -1+x < \|\|as\|\| firstn(x;as) = (firstn(-1+x;as) @ [as[(-1+x)]])` 5. `as:` `T` 6. `u:` `T` 7. `v:` `T*` 8. `x < \|\|v\|\|+1` 9. `0 < x+1` 10. `0 < x` `u.firstn(x;v) = ((u.firstn(-1+x;v)) @ [(u.v)[x]])`