Nuprl - Pf P_causal_switchable0 3 1

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

1. E: EventStruct
2. x: |E| List
3. y: |E| List
4. z: |E| List
5. i:||x||. j:||x||. ji & is-send(E)(x[j]) & (x[j] =msg=(E) x[i])
6. i:||y||. j:||y||. ji & is-send(E)(y[j]) & (y[j] =msg=(E) y[i])
7. (xx.(yy.(x =msg=(E) y)))
8. z = (x @ y)
9. i: ||z||

j:||z||. ji & is-send(E)(z[j]) & (z[j] =msg=(E) z[i])

By: Inst Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs|| [|E|;x;y] THEN RevHypSubst -3 -1 THEN Decide (i < ||x||)

Generated subgoals:

1 10. ||z|| = ||x||+||y||
11. i < ||x||
j:||z||. ji & is-send(E)(z[j]) & (z[j] =msg=(E) z[i])

2 10. ||z|| = ||x||+||y||
11. i < ||x||
j:||z||. ji & is-send(E)(z[j]) & (z[j] =msg=(E) z[i])

About:

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

1	10. `\|\|z\|\| = \|\|x\|\|+\|\|y\|\|` 11. `i < \|\|x\|\|` `j:\|\|z\|\|. ji & is-send(E)(z[j]) & (z[j] =msg=(E) z[i])`
2	10. `\|\|z\|\| = \|\|x\|\|+\|\|y\|\|` 11. `i < \|\|x\|\|` `j:\|\|z\|\|. ji & is-send(E)(z[j]) & (z[j] =msg=(E) z[i])`