(10steps total)
PrintForm
Definitions
Lemmas
mb
event
system
2
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
lpath
cons
1
1.
l
: IdLnk
2.
p
: IdLnk List
3. lpath([
l
/
p
])
lpath(
p
)
By:
ParallelOp -1 THEN Analyze 0 THEN InstHyp [
i
+1] -2
THEN
RWO
Thm*
a
:
T
,
as
:
T
List,
i
:
. 0<
i
i
||
as
||
[
a
/
as
][
i
] =
as
[(
i
-1)] -1
THEN
Subst ((
i
+1-1) ~
i
) -1
THENL
[Auto;Id]
THEN
Subst ((
i
+1+1-1) ~ (
i
+1)) -1
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(10steps total)
PrintForm
Definitions
Lemmas
mb
event
system
2
Sections
EventSystems
Doc
lpath(p) lpath(p)
a:T, as:T List, i:
. 0<i 
i
||as|| [a / as][i] = as[(i-1)] -1
