Nuprl - Pf P_causal_switchable0 6 1 1 1 1

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

1. E: EventStruct
2. x: |E| List
3. y: |E| List
4. i:||x||. j:||x||. ji & is-send(E)(x[j]) & (x[j] =msg=(E) x[i])
5. i1: (||x||-1)
6. (x[i1] =msg=(E) x[(i1+1)])
7. is-send(E)(x[i1]) & is-send(E)(x[(i1+1)]) is-send(E)(x[i1]) & is-send(E)(x[(i1+1)])
8. y = swap(x;i1;i1+1)
9. i: ||y||
10. ||swap(x;i1;i1+1)|| = ||x||
11. ||y|| = ||x||
12. ||swap(y;i1;i1+1)|| = ||y||
13. (i1, i1+1) ||x||||x||
14. j: ||x||
15. is-send(E)(x[j])
16. x[j] =msg=(E) x[((i1, i1+1)(i))]
17. i = i1
18. ji1+1
19. j = i1

i1+1i

By: Analyze 6 THEN NthHypSq -4 THEN HypSubstSq -1 0 THEN HypSubstSq -3 0 THEN Subst' ((i1, i1+1)(i1) = i1+1) 0

Generated subgoal:

1 6. is-send(E)(x[i1]) & is-send(E)(x[(i1+1)]) is-send(E)(x[i1]) & is-send(E)(x[(i1+1)])
7. y = swap(x;i1;i1+1)
8. i: ||y||
9. ||swap(x;i1;i1+1)|| = ||x||
10. ||y|| = ||x||
11. ||swap(y;i1;i1+1)|| = ||y||
12. (i1, i1+1) ||x||||x||
13. j: ||x||
14. is-send(E)(x[j])
15. x[j] =msg=(E) x[((i1, i1+1)(i))]
16. i = i1
17. ji1+1
18. j = i1
19. x,y:. x = y (x ~ y)
(i1, i1+1)(i1) = i1+1

About:

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