Nuprl - Proof: world-event-system 1

(248steps 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: world-event-system 1

1. the_w : World
2. FairFifo

e,e':E. loc(e) = loc(e')

e <c e'

e = e'

e' <c e

By:	Auto THEN Assert (e <c e' e <loc e')

Generated subgoals:

1 3. e : E
4. e' : E
5. loc(e) = loc(e')  Id
  e <c e'  e <loc e'
1 step

2 3. e : E
4. e' : E
5. loc(e) = loc(e')  Id
6. e <c e'  e <loc e'
  e <c e'  e = e'  e' <c e
6 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(248steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc

1	3. e : E 4. e' : E 5. loc(e) = loc(e') Id e <c e' e <loc e'	1 step
2	3. e : E 4. e' : E 5. loc(e) = loc(e') Id 6. e <c e' e <loc e' e <c e' e = e' e' <c e	6 steps