Nuprl - Pf switch_inv_rel_closure

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

At: switch inv rel closure lemma1 1 1 2 1 1

1. E: EventStruct
2. tr: |E| List
3. ls: ||tr||
4. is-send(E)(tr[ls])
5. j:||tr||. ls < j is-send(E)(tr[j])
6. n:
7. 0 < n
8. i,j:||tr||. ij is-send(E)(tr[i]) is-send(E)(tr[j]) (i switchR(tr)^n-1 ls) (j (switchR(tr)^*) ls)
9. i: ||tr||
10. j: ||tr||
11. ij
12. is-send(E)(tr[i])
13. is-send(E)(tr[j])
14. i switchR(tr)^n ls
15. n = 0
16. z: ||tr||
17. i switchR(tr) z
18. z switchR(tr)^n-1 ls
19. i (switchR(tr)^*) ls
20. z (switchR(tr)^*) ls

j (switchR(tr)^*) ls

By: Unfold `switch_inv_rel` -4 THEN Reduce -4 THEN ExRepD THEN Decide (zj)

Generated subgoals:

1 17. is-send(E)(tr[i])
18. is-send(E)(tr[z])
19. i < z & tr[z] somewhere delivered before tr[i] z < i & tr[i] somewhere delivered before tr[z]
20. z switchR(tr)^n-1 ls
21. i (switchR(tr)^*) ls
22. z (switchR(tr)^*) ls
23. zj
j (switchR(tr)^*) ls

2 17. is-send(E)(tr[i])
18. is-send(E)(tr[z])
19. i < z & tr[z] somewhere delivered before tr[i] z < i & tr[i] somewhere delivered before tr[z]
20. z switchR(tr)^n-1 ls
21. i (switchR(tr)^*) ls
22. z (switchR(tr)^*) ls
23. zj
j (switchR(tr)^*) ls

About:

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

1	17. `is-send(E)(tr[i])` 18. `is-send(E)(tr[z])` 19. `i < z & tr[z] somewhere delivered before tr[i] z < i & tr[i] somewhere delivered before tr[z]` 20. `z switchR(tr)^n-1 ls` 21. `i (switchR(tr)^) ls` 22. `z (switchR(tr)^) ls` 23. `zj` `j (switchR(tr)^*) ls`
2	17. `is-send(E)(tr[i])` 18. `is-send(E)(tr[z])` 19. `i < z & tr[z] somewhere delivered before tr[i] z < i & tr[i] somewhere delivered before tr[z]` 20. `z switchR(tr)^n-1 ls` 21. `i (switchR(tr)^) ls` 22. `z (switchR(tr)^) ls` 23. `zj` `j (switchR(tr)^*) ls`