(10steps total)
PrintForm
Definitions
Lemmas
mb
event
system
3
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
es-first-exists
es
:ES,
e'
:E.
e
:E. first(
e
) &
e
e'
By:
Analyze 0 THEN LocLessInd
Generated subgoal:
1
1.
es
: ES
2. WellFnd{i}(E;
x
,
y
.(
x
<loc
y
))
3.
j
: E
4.
k
:E. (
k
<loc
j
)
(
e
:E. first(
e
) &
e
k
)
e
:E. first(
e
) &
e
j
9
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(10steps total)
PrintForm
Definitions
Lemmas
mb
event
system
3
Sections
EventSystems
Doc
es:ES, e':E. 
e:E. first(e) & e 
e' es:ES, e':E. e:E. first(e) & e e' k:E. (k <loc j) 
(e:E. first(e) & e k )
e:E. first(e) & e j 
