(6steps total)
PrintForm
Definitions
mb
event
system
1
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
firstn
all
L
:Top List,
n
:
. ||
L
||
n
(firstn(
n
;
L
) ~
L
)
By:
InductionOnList THEN Reduce 0 THEN Try (Complete Auto)
Generated subgoal:
1
1. Top List
2.
u
: Top
3.
v
: Top List
4.
n
:
. ||
v
||
n
(firstn(
n
;
v
) ~
v
)
n
:
. ||
v
||+1
n
(firstn(
n
;[
u
/
v
]) ~ [
u
/
v
])
5
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
mb
event
system
1
Sections
EventSystems
Doc
L:Top List, n:
. ||L||
n 
(firstn(n;L) ~ L) L:Top List, n:. ||L||n (firstn(n;L) ~ L)n:. ||v||n (firstn(n;v) ~ v)
n:. ||v||+1n (firstn(n;[u / v]) ~ [u / v])
