(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: fair-fifo wf 1 1

1. the_w : World
2. i : Id
3. t : 
4. l : IdLnk
5. isrcv(l;a(i;t))
6. ||queue(l;t)||1
7. isnull(a(i;t)) & isrcv(kind(a(i;t))) & lnk(kind(a(i;t))) = l
  msg(a(i;t))  Msg


By: Using [`l',lnk(kind(a(i;t)))]
(BackThru
(Thm* the_w:World, i:Id, a:Action(i), l:IdLnk. isrcv(l;a msg(a Msg)


Generated subgoal:

1 7. isnull(a(i;t))
8. isrcv(kind(a(i;t)))
9. lnk(kind(a(i;t))) = l
  isrcv(lnk(kind(a(i;t)));a(i;t))

1 step

About:
assertnatural_numberequalmemberimpliesandall
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