Nuprl - Pf strong_switch_inv_decomposable 1 2 1 1 2 2 1 2 1 1 1 1 1 2 1 2 1

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

At: strong switch inv decomposable 1 2 1 1 2 2 1 2 1 1 1 1 1 2 1 2 1

1. E: TaggedEventStruct
2. tr: |E| List
3. ...
4. AD-normal(E)(tr)
5. No-dup-deliver(E)(tr)
6. tr = nil
7. ls: ||tr||
8. is-send(E)(tr[ls])
9. ...
10. ...
11. EquivRel(|E|)(_1 =msg=(E) _2)
12. ...
13. d:
14. 0 < d
15. ...
16. i: ||tr||
17. j: ||tr||
18. d = j-i
19. i (switchR(tr)^*) ls
20. ij
21. is-send(E)(tr[i])
22. is-send(E)(tr[j])
23. ij-1
24. is-send(E)(tr[(j-1)])
25. k: ||tr||
26. k (switchR(tr)^*) ls
27. tr[k] =msg=(E) tr[(j-1)]
28. j@0: ||tr||
29. j@0j
30. is-send(E)(tr[j@0])
31. tr[j@0] =msg=(E) tr[j]
32. j@0 < k
33. k': ||tr||
34. tr[j@0] delivered at time k'
35. loc(E)(tr[k']) = loc(E)(tr[(j-1)])
36. j-1k'

j-1k'

By: Unfold `delivered_at` -3 THEN Analyze -3 THEN AllHyps (h.(Unfold `P_no_dup` h) THEN (Reduce h) THEN (InstHyp [j;k'] h))

Generated subgoals:

1 5. i,j:||tr||. is-send(E)(tr[i]) is-send(E)(tr[j]) (tr[j] =msg=(E) tr[i]) loc(E)(tr[i]) = loc(E)(tr[j]) i = j
6. tr = nil
7. ls: ||tr||
8. is-send(E)(tr[ls])
9. ...
10. ...
11. EquivRel(|E|)(_1 =msg=(E) _2)
12. ...
13. d:
14. 0 < d
15. ...
16. i: ||tr||
17. j: ||tr||
18. d = j-i
19. i (switchR(tr)^*) ls
20. ij
21. is-send(E)(tr[i])
22. is-send(E)(tr[j])
23. ij-1
24. is-send(E)(tr[(j-1)])
25. k: ||tr||
26. k (switchR(tr)^*) ls
27. tr[k] =msg=(E) tr[(j-1)]
28. j@0: ||tr||
29. j@0j
30. is-send(E)(tr[j@0])
31. tr[j@0] =msg=(E) tr[j]
32. j@0 < k
33. k': ||tr||
34. tr[j@0] =msg=(E) tr[k']
35. is-send(E)(tr[k'])
36. loc(E)(tr[k']) = loc(E)(tr[(j-1)])
37. j-1k'
tr[k'] =msg=(E) tr[j]

2 5. i,j:||tr||. is-send(E)(tr[i]) is-send(E)(tr[j]) (tr[j] =msg=(E) tr[i]) loc(E)(tr[i]) = loc(E)(tr[j]) i = j
6. tr = nil
7. ls: ||tr||
8. is-send(E)(tr[ls])
9. ...
10. ...
11. EquivRel(|E|)(_1 =msg=(E) _2)
12. ...
13. d:
14. 0 < d
15. ...
16. i: ||tr||
17. j: ||tr||
18. d = j-i
19. i (switchR(tr)^*) ls
20. ij
21. is-send(E)(tr[i])
22. is-send(E)(tr[j])
23. ij-1
24. is-send(E)(tr[(j-1)])
25. k: ||tr||
26. k (switchR(tr)^*) ls
27. tr[k] =msg=(E) tr[(j-1)]
28. j@0: ||tr||
29. j@0j
30. is-send(E)(tr[j@0])
31. tr[j@0] =msg=(E) tr[j]
32. j@0 < k
33. k': ||tr||
34. tr[j@0] =msg=(E) tr[k']
35. is-send(E)(tr[k'])
36. loc(E)(tr[k']) = loc(E)(tr[(j-1)])
37. j-1k'
loc(E)(tr[j]) = loc(E)(tr[k'])

About:

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