Nuprl - Pf P_no_dup_strong

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

E:EventStruct. R_strong_safety(E) preserves No-dup-deliver(E)

By: Unfolds [`preserved_by`;`P_no_dup`;`R_strong_safety`] 0 THEN Unfold `sublist` 0 THEN Reduce 0 THEN ExRepD THEN InstHyp [f(i);f(j)] 4 THEN AllHyps (h.(InstHyp [j] h) THEN (RevHypSubst -1 0)) THEN AllHyps (h.(InstHyp [i] h) THEN (RevHypSubst -1 0))

Generated subgoal:

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

About:

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