i:Id, L:Knd List, l:IdLnk, tg:Id.
  @i: only L sends on (l with tg) 
  realizes es.e:E. loc(e) = i  Id  null(sends(l,tg,e))  (kind(e)  L)

By:	Auto THEN Try (ParallelOp 1) THEN BackThru Thm* D:Dsys, P:({es:ES| es is an event system of D }Prop{i'}). Thm* D realizes2 es.P(es)  D realizes es.P(es) THENA Try (Complete Auto)

1

1. i : Id 2. L : Knd List 3. l : IdLnk 4. tg : Id   @i: only L sends on (l with tg) realizes2 es.e:E.    loc(e) = i  Id  null(sends(l,tg,e))  (kind(e)  L)

15 steps

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