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

By:	FwdThru Thm* the_w:World, l:IdLnk, i:Id, a:Action(i). Thm* isrcv(l;a)  isnull(a) & isrcv(kind(a)) & lnk(kind(a)) = l [-2]

1

7. isnull(a(i;t)) & isrcv(kind(a(i;t))) & lnk(kind(a(i;t))) = l   msg(a(i;t))  Msg

2 steps

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