(7steps total)
PrintForm
Definitions
list
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
length
firstn
2
1.
A
: Type
2.
A
List
3.
u
:
A
4.
v
:
A
List
5.
n
:{0...||
v
||}. ||firstn(
n
;
v
)|| =
n
6.
n
: {0...||
u
.
v
||}
||firstn(
n
;
u
.
v
)|| =
n
By:
RecCaseSplit `firstn`
Generated subgoals:
1
7. 0<
n
||firstn(
n
-1;
v
)||+1 =
n
1
step
2
7.
n
0
0 =
n
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
list
1
Sections
StandardLIB
Doc
n:{0...||v||}. ||firstn(n;v)|| = n
||firstn(n;u.v)|| = n
0
