Nuprl - Pf causal_fusion 1 1 2

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

1. E: TaggedEventStruct
2. tr: |E| List
3. m:Label. Causal(E)( < tr > _m)
4. True
5. tr': |E| List
6. tr' tr
7. x: |E|
8. (x tr')
9. tr':|E| List. tr' < tr > _tag(E)(x) (xtr'.(ytr'.is-send(E)(y) & (y =msg=(E) x)))
10. (x@0 < tr' > _tag(E)(x).(y < tr' > _tag(E)(x).is-send(E)(y) & (y =msg=(E) x@0)))

(ytr'.is-send(E)(y) & (y =msg=(E) x))

By: Unfold `l_all` -1 THEN InstHyp [x] -1

Generated subgoals:

1 10. x@0:|E|. (x@0 < tr' > _tag(E)(x)) (y < tr' > _tag(E)(x).is-send(E)(y) & (y =msg=(E) x@0))
(x < tr' > _tag(E)(x))

2 10. x@0:|E|. (x@0 < tr' > _tag(E)(x)) (y < tr' > _tag(E)(x).is-send(E)(y) & (y =msg=(E) x@0))
11. (y < tr' > _tag(E)(x).is-send(E)(y) & (y =msg=(E) x))
(ytr'.is-send(E)(y) & (y =msg=(E) x))

About:

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

1	10. `x@0:\|E\|. (x@0 < tr' > _tag(E)(x)) (y < tr' > _tag(E)(x).is-send(E)(y) & (y =msg=(E) x@0))` `(x < tr' > _tag(E)(x))`
2	10. `x@0:\|E\|. (x@0 < tr' > _tag(E)(x)) (y < tr' > _tag(E)(x).is-send(E)(y) & (y =msg=(E) x@0))` 11. `(y < tr' > _tag(E)(x).is-send(E)(y) & (y =msg=(E) x))` `(ytr'.is-send(E)(y) & (y =msg=(E) x))`