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

At: switch normal exists 2 2 1 2
1. E: TaggedEventStruct
2. tr: |E| List
3. switch_inv(E)(tr)
4. No-dup-send(E)(tr)
5. L': |E| List
6. tr (swap adjacent[R_ad_normal(tr)(x,y)]^*) L'
7. i:(||L'||-1). R_ad_normal(tr)(L'[i],L'[(i+1)])
8. i: (||L'||-1)
9. is-send(E)(L'[i]) is-send(E)(L'[(i+1)]) (x,y:||tr||. x < y & is-send(E)(tr[x]) & is-send(E)(tr[y]) & (tr[x] =msg=(E) L'[(i+1)]) & (tr[y] =msg=(E) L'[i])) loc(E)(L'[i]) = loc(E)(L'[(i+1)])
10. x: ||L'||
11. y: ||L'||
12. x < y
13. is-send(E)(L'[x])
14. is-send(E)(L'[y])
15. L'[x] =msg=(E) L'[(i+1)]
16. is-send(E)(L'[(i+1)])
17. L'[y] =msg=(E) L'[i]
18. is-send(E)(L'[i])
19. sublist(|E|;[L'[x]; L'[y]];tr)

x,y:||tr||. x < y & is-send(E)(tr[x]) & is-send(E)(tr[y]) & (tr[x] =msg=(E) L'[(i+1)]) & (tr[y] =msg=(E) L'[i])
By:
Unfold `sublist` -1
THEN
Reduce -1
THEN
ExRepD
THEN
InstHyp [0] -1
THEN
Reduce -1
THEN
InstHyp [1] -2
THEN
Reduce -1
Generated subgoal:

119. f: 2||tr||
20. increasing(f;2)
21. j:2. [L'[x]; L'[y]][j] = tr[(f(j))]
22. L'[x] = tr[(f(0))]
23. L'[y] = tr[(f(1))]
x,y:||tr||. x < y & is-send(E)(tr[x]) & is-send(E)(tr[y]) & (tr[x] =msg=(E) L'[(i+1)]) & (tr[y] =msg=(E) L'[i])

About:
listconsnilassertnatural_numberaddsubtractless_than
applyequalimpliesandallexists

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