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)

sublist(|E|;[x; y];tr)

By: Analyze 0 THEN Unfold `sublist` -1 THEN Reduce -1 THEN ExRepD THEN InstHyp [0] -1 THEN Reduce -1 THEN InstHyp [1] -2 THEN Reduce -1

Generated subgoal:

1 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

About:

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