(17steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: better-sframe-rule 1

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(ltg)
  null(sends(l,tg,sender(e)))


By: RW assert_pushdownC 0 THEN MaAuto


Generated subgoal:

1   sends(l,tg,sender(e)) = nil  (Msg on l) List
15 steps

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

(17steps total) PrintForm Definitions Lemmas mb event system 7 Sections EventSystems Doc