(12steps 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-match-unique 2
1. the_w:World, e:E, t,t':.
1. FairFifo
1. 
1. isrcv(kind(e))
1. 
1. t<t'  match(lnk(kind(e));t;time(e))  match(lnk(kind(e));t';time(e))
  the_w:World, e:E, t,t':.
  FairFifo
  
  isrcv(kind(e))
  
  match(lnk(kind(e));t;time(e))  match(lnk(kind(e));t';time(e))  t = t'
By: Auto THEN Decide (t<t')

Generated subgoals:

1 2. the_w : World
3. e : E
4. t : 
5. t' : 
6. FairFifo
7. isrcv(kind(e))
8. match(lnk(kind(e));t;time(e))
9. match(lnk(kind(e));t';time(e))
10. t<t'
  t = t'
1 step
2 2. the_w : World
3. e : E
4. t : 
5. t' : 
6. FairFifo
7. isrcv(kind(e))
8. match(lnk(kind(e));t;time(e))
9. match(lnk(kind(e));t';time(e))
10. t<t'
  t = t'
2 steps

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

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