Nuprl - Pf switch_inv_swap 1 1 2 1 2 1 1 2

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

1. E: TaggedEventStruct
2. x: |E| List
3. i: (||x||-1)
4. is-send(E)(x[(i+1)])
5. loc(E)(x[i]) = loc(E)(x[(i+1)])
6. ||swap(x;i;i+1)|| = ||x||
7. i,j,k:||x||. i < j is-send(E)(x[i]) is-send(E)(x[j]) tag(E)(x[i]) = tag(E)(x[j]) (x[j] =msg=(E) x[k]) & is-send(E)(x[k]) (k':||x||. k' < k & (x[i] =msg=(E) x[k']) & is-send(E)(x[k']) & loc(E)(x[k']) = loc(E)(x[k]))
8. i@0: ||swap(x;i;i+1)||
9. j: ||swap(x;i;i+1)||
10. k: ||swap(x;i;i+1)||
11. f: ||x||||x||
12. (i, i+1) = f ||x||||x||
13. i@0 < j
14. is-send(E)(x[(f(i@0))])
15. is-send(E)(x[(f(j))])
16. tag(E)(x[(f(i@0))]) = tag(E)(x[(f(j))])
17. x[(f(j))] =msg=(E) x[(f(k))]
18. is-send(E)(x[(f(k))])
19. k': ||x||
20. x[(f(i@0))] =msg=(E) x[k']
21. is-send(E)(x[k'])
22. loc(E)(x[k']) = loc(E)(x[(f(k))])
23. k = i
24. k = i+1
25. k' = i
26. k' = i+1
27. k' < i+1

i+1 < k

By: SubstFor k' -6 THEN Subst' (f(k) = i+1) -6

Generated subgoals:

1 22. loc(E)(x[i]) = loc(E)(x[(f(k))])
23. k = i
24. k = i+1
25. k' = i
26. k' = i+1
27. k' < i+1
28. x,y:. x = y (x ~ y)
f(k) = i+1

2 22. loc(E)(x[i]) = loc(E)(x[(i+1)])
23. k = i
24. k = i+1
25. k' = i
26. k' = i+1
27. k' < i+1
i+1 < k

About:

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

1	22. `loc(E)(x[i]) = loc(E)(x[(f(k))])` 23. `k = i` 24. `k = i+1` 25. `k' = i` 26. `k' = i+1` 27. `k' < i+1` 28. `x,y:. x = y (x ~ y)` `f(k) = i+1`
2	22. `loc(E)(x[i]) = loc(E)(x[(i+1)])` 23. `k = i` 24. `k = i+1` 25. `k' = i` 26. `k' = i+1` 27. `k' < i+1` `i+1 < k`