1. L : Knd List
2. l : IdLnk
3. tg : Id
4. @source(l): only L sends on (l with tg)  Dsys
5. D:Dsys. 
5. @source(l): only L sends on (l with tg)  D
5. 
5. D 
5. realizes es.e:E. loc(e) = source(l)  null(sends(l,tg,e))  (kind(e)  L)
6. @source(l): only L sends on (l with tg)  Dsys
7. D : Dsys
8. @source(l): only L sends on (l with tg)  D
9. D' : Dsys
10. D  D'
11. w : World
12. p : FairFifo
13. PossibleWorld(D';w)
14. e:E. loc(e) = source(l)  null(sends(l,tg,e))  (kind(e)  L)
15. e : E
16. loc(e) = destination(l)
17. kind(e) = rcv(l; tg)
18. sends(l,tg,sender(e)) = nil
19. sends(lnk(e);sender(e))[index(e)] = msg(lnk(e);tag(e);val(e))
  (msg(lnk(e);tag(e);val(e))  sends(l,tg,sender(e)))

By:	Unfold `es-tg-sends` 0 THEN RWO Thm* P:(T), L:T List, x:T. (x  filter(P;L))  (x  L) & P(x) 0 THEN MaAuto

1	(msg(lnk(e);tag(e);val(e))  sends(l;sender(e)))	5 steps
2	(m.mtag(m) = tg)(msg(lnk(e);tag(e);val(e)))	3 steps

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