L:Knd List, l:IdLnk, tg:Id.
@source(l): only L sends on (l with tg) 
Dsys
& (D:Dsys.
& (@source(l): only L sends on (l with tg) 
D
& (
& (D
& (realizes es.e:E.
& (realizes es.loc(e) = destination(l) Id
& (realizes es.
& (realizes es.kind(e) = rcv(l; tg) Knd (kind(sender(e)) L))| By: |
THEN Analyze 0 THEN Try Trivial THEN ParallelOp -2 THEN RepeatFor 7 ParallelLast THEN BackThruSomeHyp THEN MaAuto |
| 1 |
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.
5. realizes es.loc(e) = source(l) Id  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) null(sends(l,tg,sender(e))) | 16 steps |
About:
 |  |  |  |  |  |