Nuprl - Pf no_dup_fusion 1 1 1 2

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

1. E: TaggedEventStruct
2. tr: |E| List
3. m:Label. No-dup-deliver(E)( < tr > _m)
4. Tag-by-msg(E)(tr)
5. x: |E|
6. y: |E|
7. is-send(E)(x)
8. is-send(E)(y)
9. y =msg=(E) x
10. loc(E)(x) = loc(E)(y)
11. x1,y:|E|. is-send(E)(x1) is-send(E)(y) (y =msg=(E) x1) loc(E)(x1) = loc(E)(y) sublist(|E|;[x1; y]; < tr > _tag(E)(x))
12. sublist(|E|;[x; y];tr)
13. x1: |E|
14. x1 = y

tag(E)(y) = tag(E)(x)

By: Unfold `sublist` -3 THEN Reduce -3 THEN ExRepD THEN InstHyp [0] -3 THEN Reduce -1 THEN InstHyp [1] -4 THEN Reduce -1 THEN AllHyps (h.(Unfold `P_tag_by_msg` h) THEN (Reduce h) THEN (InstHyp [f(0);f(1)] h))

Generated subgoals:

1 4. i,j:||tr||. (tr[i] =msg=(E) tr[j]) tag(E)(tr[i]) = tag(E)(tr[j])
5. x: |E|
6. y: |E|
7. is-send(E)(x)
8. is-send(E)(y)
9. y =msg=(E) x
10. loc(E)(x) = loc(E)(y)
11. x1,y:|E|. is-send(E)(x1) is-send(E)(y) (y =msg=(E) x1) loc(E)(x1) = loc(E)(y) sublist(|E|;[x1; y]; < tr > _tag(E)(x))
12. f: 2||tr||
13. increasing(f;2)
14. j:2. [x; y][j] = tr[(f(j))]
15. x1: |E|
16. x1 = y
17. x = tr[(f(0))]
18. y = tr[(f(1))]
tr[(f(0))] =msg=(E) tr[(f(1))]

2 4. i,j:||tr||. (tr[i] =msg=(E) tr[j]) tag(E)(tr[i]) = tag(E)(tr[j])
5. x: |E|
6. y: |E|
7. is-send(E)(x)
8. is-send(E)(y)
9. y =msg=(E) x
10. loc(E)(x) = loc(E)(y)
11. x1,y:|E|. is-send(E)(x1) is-send(E)(y) (y =msg=(E) x1) loc(E)(x1) = loc(E)(y) sublist(|E|;[x1; y]; < tr > _tag(E)(x))
12. f: 2||tr||
13. increasing(f;2)
14. j:2. [x; y][j] = tr[(f(j))]
15. x1: |E|
16. x1 = y
17. x = tr[(f(0))]
18. y = tr[(f(1))]
19. tag(E)(tr[(f(0))]) = tag(E)(tr[(f(1))])
tag(E)(y) = tag(E)(x)

About:

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