Nuprl - Pf switch_normal_exists 2 2 1 1 1 1 1

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

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]];L')
20. L' (swap adjacent[R_ad_normal(tr)(x,y)]^-1^*) tr

swap adjacent[R_ad_normal(tr)(x,y)]^-1 preserves L.sublist(|E|;[L'[x]; L'[y]];L)

By: Fold `l_before` 0 THEN Unfolds [`swap_adjacent`;`R_ad_normal`] 0 THEN Unfolds [`rel_inverse`;`preserved_by`] 0 THEN Reduce 0 THEN ExRepD THEN MoveToConcl -4 THEN SubstFor x@0 0 THEN FwdThru Thm* L:T List, i:(||L||-1), a,b:T. a before b swap(L;i;i+1) a before b L a = L[(i+1)] & b = L[i] [-1] THEN Analyze -1

Generated subgoal:

1 21. x@0: |E| List
22. y@0: |E| List
23. i1: (||y@0||-1)
24. ((is-send(E)(y@0[i1]) is-send(E)(y@0[(i1+1)]) (y@0[i1] =msg=(E) y@0[(i1+1)])) & (is-send(E)(y@0[i1]) is-send(E)(y@0[(i1+1)]) (x,y@1:||tr||. x < y@1 & is-send(E)(tr[x]) & is-send(E)(tr[y@1]) & (tr[x] =msg=(E) y@0[(i1+1)]) & (tr[y@1] =msg=(E) y@0[i1])) loc(E)(y@0[i1]) = loc(E)(y@0[(i1+1)])))
25. x@0 = swap(y@0;i1;i1+1)
26. L'[x] before L'[y] swap(y@0;i1;i1+1)
27. L'[x] = y@0[(i1+1)]
28. L'[y] = y@0[i1]
L'[x] before L'[y] y@0

About:

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