mb
event
system
3
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
the_es
:ES,
e
:E. before(
e
)
E List
[es-before_wf]
cites the following:
Thm*
the_es
:ES,
j
:E.
first(
j
)
(pred(
j
) <loc
j
)
[es-pred-locl]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
event
system
3
Sections
EventSystems
Doc
the_es:ES, e:E. before(e) 
E Listthe_es:ES, j:E. 
first(j) 
(pred(j) <loc j)the_es:ES, e:E. before(e) E Listthe_es:ES, j:E. first(j) (pred(j) <loc j)