Nuprl - Pf switch_normal

(24steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

1. E: TaggedEventStruct
2. tr: |E| List
3. switch_inv(E)(tr)
4. No-dup-send(E)(tr)

x,y:|E|. R_ad_normal(tr)(x,y) R_ad_normal(tr)(y,x)

By: Inst Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2) [E] THEN Unfold `R_ad_normal` 0 THEN Reduce 0 THEN SupposeNot THEN Analyze 8 THEN SimpConcl THEN ExRepD

Generated subgoal:

1 5. EquivRel(|E|)(_1 =msg=(E) _2)
6. x: |E|
7. y: |E|
8. is-send(E)(y)
9. is-send(E)(x)
10. x1: ||tr||
11. y1: ||tr||
12. x1 < y1
13. is-send(E)(tr[x1])
14. is-send(E)(tr[y1])
15. tr[x1] =msg=(E) x
16. tr[y1] =msg=(E) y
17. loc(E)(y) = loc(E)(x)
18. x@0: ||tr||
19. y@0: ||tr||
20. x@0 < y@0
21. is-send(E)(tr[x@0])
22. is-send(E)(tr[y@0])
23. tr[x@0] =msg=(E) y
24. tr[y@0] =msg=(E) x
loc(E)(x) = loc(E)(y)

About:

(24steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc