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

At: switch inv swap 1 1
1. E: TaggedEventStruct
2. x: |E| List
3. i: (||x||-1)
4. is-send(E)(x[(i+1)])
5. is-send(E)(x[i]) 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)||

i@0 < j is-send(E)(x[((i, i+1)(i@0))]) is-send(E)(x[((i, i+1)(j))]) tag(E)(x[((i, i+1)(i@0))]) = tag(E)(x[((i, i+1)(j))]) (x[((i, i+1)(j))] =msg=(E) x[((i, i+1)(k))]) & is-send(E)(x[((i, i+1)(k))]) (k':||swap(x;i;i+1)||. k' < k & (x[((i, i+1)(i@0))] =msg=(E) x[((i, i+1)(k'))]) & is-send(E)(x[((i, i+1)(k'))]) & loc(E)(x[((i, i+1)(k'))]) = loc(E)(x[((i, i+1)(k))]))
By:
GenConcl ((i, i+1) = f)
THEN
AllHyps (h.InstHyp [f(i@0);f(j);f(k)] h)
Generated subgoals:

111. 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))])
f(i@0) < f(j)
211. 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||. k' < f(k) & (x[(f(i@0))] =msg=(E) x[k']) & is-send(E)(x[k']) & loc(E)(x[k']) = loc(E)(x[(f(k))])
k':||swap(x;i;i+1)||. k' < k & (x[(f(i@0))] =msg=(E) x[(f(k'))]) & is-send(E)(x[(f(k'))]) & loc(E)(x[(f(k'))]) = loc(E)(x[(f(k))])

About:
listassertintnatural_numberaddsubtractless_thanapplyfunction
equalimpliesandorallexists

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