Nuprl - Pf P_no_dup_permutable 1

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

1. E: EventStruct
2. x: |E| List
3. No-dup-deliver(E)(x)
4. i: (||x||-1)
5. True

No-dup-deliver(E)(swap(x;i;i+1))

By: All (h.(Unfold `P_no_dup` h) THEN (Reduce h)) THEN Inst Thm* k:, i,j:k. Bij(k; k; (i, j)) [||x||;i;i+1] THEN Inst Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L|| [|E|;x;i;i+1] THEN Inst Thm* k:, i,j:k. (i, j) kk [||x||;i;i+1] THEN InstHyp [(i, i+1)(i@0);(i, i+1)(j)] 3 THEN Try (Complete Auto) THEN Try (RWO "swap_select < " 0)

Generated subgoal:

1 3. i,j:||x||. is-send(E)(x[i]) is-send(E)(x[j]) (x[j] =msg=(E) x[i]) loc(E)(x[i]) = loc(E)(x[j]) i = j
4. i: (||x||-1)
5. True
6. i@0: ||swap(x;i;i+1)||
7. j: ||swap(x;i;i+1)||
8. is-send(E)(swap(x;i;i+1)[i@0])
9. is-send(E)(swap(x;i;i+1)[j])
10. swap(x;i;i+1)[j] =msg=(E) swap(x;i;i+1)[i@0]
11. loc(E)(swap(x;i;i+1)[i@0]) = loc(E)(swap(x;i;i+1)[j])
12. Bij(||x||; ||x||; (i, i+1))
13. ||swap(x;i;i+1)|| = ||x||
14. (i, i+1) ||x||||x||
15. (i, i+1)(i@0) = (i, i+1)(j)
i@0 = j

About:

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