Nuprl - Pf P_no_dup

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

1. E: EventStruct
2. tr: |E| List
3. No-dup-deliver(E)(tr)
4. x: |E|
5. y: |E|
6. is-send(E)(x)
7. is-send(E)(y)
8. y =msg=(E) x
9. loc(E)(x) = loc(E)(y)
10. f: 2||tr||
11. increasing(f;2)
12. j:2. [x; y][j] = tr[(f(j))]
13. x = tr[(f(0))]
14. y = tr[(f(1))]

False

By: Unfold `P_no_dup` 3 THEN Reduce 3 THEN InstHyp [f(0);f(1)] 3 THEN Try (SubstFor tr[(f(0))] 0) THEN Try (SubstFor tr[(f(1))] 0) THEN Try Trivial

Generated subgoal:

1 3. i,j:||tr||. is-send(E)(tr[i]) is-send(E)(tr[j]) (tr[j] =msg=(E) tr[i]) loc(E)(tr[i]) = loc(E)(tr[j]) i = j
4. x: |E|
5. y: |E|
6. is-send(E)(x)
7. is-send(E)(y)
8. y =msg=(E) x
9. loc(E)(x) = loc(E)(y)
10. f: 2||tr||
11. increasing(f;2)
12. j:2. [x; y][j] = tr[(f(j))]
13. x = tr[(f(0))]
14. y = tr[(f(1))]
15. f(0) = f(1)
False

About:

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