Nuprl - Pf P_causal_switchable0 4

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

1. E: EventStruct

send-enabledR(E) preserves Causal(E)

By: Unfolds [`preserved_by`;`P_causal`;`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 -3 -1 THEN Decide (i < ||x||)

Generated subgoals:

1 2. x: |E| List
3. y: |E| List
4. i:||x||. j:||x||. ji & is-send(E)(x[j]) & (x[j] =msg=(E) x[i])
5. x@0: |E|
6. is-send(E)(x@0)
7. y = (x @ [x@0])
8. i: ||y||
9. ||y|| = ||x||+||[x@0]||
10. i < ||x||
j:||y||. ji & is-send(E)(y[j]) & (y[j] =msg=(E) y[i])

2 2. x: |E| List
3. y: |E| List
4. i:||x||. j:||x||. ji & is-send(E)(x[j]) & (x[j] =msg=(E) x[i])
5. x@0: |E|
6. is-send(E)(x@0)
7. y = (x @ [x@0])
8. i: ||y||
9. ||y|| = ||x||+||[x@0]||
10. i < ||x||
j:||y||. ji & is-send(E)(y[j]) & (y[j] =msg=(E) y[i])

About:

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

1	2. `x:` `\|E\| List` 3. `y:` `\|E\| List` 4. `i:\|\|x\|\|. j:\|\|x\|\|. ji & is-send(E)(x[j]) & (x[j] =msg=(E) x[i])` 5. `x@0:` `\|E\|` 6. `is-send(E)(x@0)` 7. `y = (x @ [x@0])` 8. `i:` `\|\|y\|\|` 9. `\|\|y\|\| = \|\|x\|\|+\|\|[x@0]\|\|` 10. `i < \|\|x\|\|` `j:\|\|y\|\|. ji & is-send(E)(y[j]) & (y[j] =msg=(E) y[i])`
2	2. `x:` `\|E\| List` 3. `y:` `\|E\| List` 4. `i:\|\|x\|\|. j:\|\|x\|\|. ji & is-send(E)(x[j]) & (x[j] =msg=(E) x[i])` 5. `x@0:` `\|E\|` 6. `is-send(E)(x@0)` 7. `y = (x @ [x@0])` 8. `i:` `\|\|y\|\|` 9. `\|\|y\|\| = \|\|x\|\|+\|\|[x@0]\|\|` 10. `i < \|\|x\|\|` `j:\|\|y\|\|. ji & is-send(E)(y[j]) & (y[j] =msg=(E) y[i])`