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)

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: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html