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

At: P no dup iff 1 1 1
1. E: EventStruct
2. tr: |E| List
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
By: AllHyps (h.(Unfold `increasing` h) THEN (InstHyp [0] h))
Generated subgoals:

None

About:
listconsnilassertintnatural_numberapply
functionequalimpliesfalseall

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