Nuprl - Pf firstn_lem1 1 2 2 1 1 1 1 2 2

PrintForm Definitions list 3 autom Sections AutomataTheory Doc

1. T: Type
2. x:
3. 0 < x
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

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

By: InstHyp [v] 4 THEN RWH (HypC -1) 0

Generated subgoals:

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

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

About:

1	11. `firstn(x;v) = (firstn(-1+x;v) @ [v[(-1+x)]])` `x < \|\|u.v\|\|`
2	11. `firstn(x;v) = (firstn(-1+x;v) @ [v[(-1+x)]])` `(firstn(-1+x;v) @ [v[(-1+x)]]) = (firstn(-1+x;v) @ [(u.v)[x]])`