Nuprl - Pf no_duplicate_send

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

E:EventStruct. safetyR(E) preserves No-dup-send(E)

By: Unfolds [`preserved_by`;`R_safety`;`no_duplicate_send`] 0 THEN Reduce 0 THEN Inst Thm* l1,l2:T List. l1 l2 ||l1||||l2|| & (i:. i < ||l1|| l1[i] = l2[i]) [|E|;y;x] THEN SimpHyp -1 THEN ExRepD

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[i] =msg=(E) x[j]) i = j
5. y x
6. i: ||y||
7. j: ||y||
8. is-send(E)(y[i])
9. is-send(E)(y[j])
10. y[i] =msg=(E) y[j]
11. ||y||||x||
12. i:. i < ||y|| y[i] = x[i]
i = j

About:

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