Nuprl - Pf firstn

PrintForm Definitions list 3 autom Sections AutomataTheory Doc

1. T: Type
2. as: T*
3. 0 < ||as||

firstn(0+1;as) = (firstn(0;as) @ [as[0]])

By: RecUnfold `firstn` 0 THEN Reduce 0 THEN ListInd 2

Generated subgoals:

1 0 < ||nil|| (Case of nil; nil nil ; a.as' a.firstn(0;as')) = ((Case of nil; nil nil ; a.as' nil) @ [nil[0]]) T*

2 3. u: T
4. v: T*
5. 0 < ||v|| (Case of v; nil nil ; a.as' a.firstn(0;as')) = ((Case of v; nil nil ; a.as' nil) @ [v[0]])
0 < ||u.v|| (Case of u.v; nil nil ; a.as' a.firstn(0;as')) = ((Case of u.v; nil nil ; a.as' nil) @ [(u.v)[0]])

About:

1	`0 < \|\|nil\|\| (Case of nil; nil nil ; a.as' a.firstn(0;as')) = ((Case of nil; nil nil ; a.as' nil) @ [nil[0]]) T*`
2	3. `u:` `T` 4. `v:` `T*` 5. `0 < \|\|v\|\| (Case of v; nil nil ; a.as' a.firstn(0;as')) = ((Case of v; nil nil ; a.as' nil) @ [v[0]])` `0 < \|\|u.v\|\| (Case of u.v; nil nil ; a.as' a.firstn(0;as')) = ((Case of u.v; nil nil ; a.as' nil) @ [(u.v)[0]])`