Nuprl - Proof: w-locl-iff

(4steps 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: w-locl-iff

the_w:World, e,e':E.

FairFifo

(e <loc e'

loc(e) = loc(e')

Id & e <c e')

By:

Auto

Generated subgoals:

1 1. the_w : World
2. e : E
3. e' : E
4. FairFifo
5. e <loc e'
  loc(e) = loc(e')  Id
1 step

2 1. the_w : World
2. e : E
3. e' : E
4. FairFifo
5. e <loc e'
  e <c e'
1 step

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

About:

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

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

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