Nuprl - Pf P_no_dup_send

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

1. E: EventStruct

send-enabledR(E) preserves No-dup-deliver(E)

By: Unfolds [`preserved_by`;`P_no_dup`;`R_send_enabled`] 0 THEN Reduce 0 THEN ExRepD THEN Inst Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs|| [|E|;x;[x@0]] THEN RevHypSubst 7 -1 THEN Reduce -1

Generated subgoal:

1 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. x@0: |E|
6. is-send(E)(x@0)
7. y = (x @ [x@0])
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. ||y|| = ||x||+1
i = j

About:

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