Nuprl - Pf P_causal_non

1. E: EventStruct
2. L: |E| List
3. L = nil
4. Causal(E)(L)
5. x: |E|
6. (x L)

i:||L||. is-send(E)(L[i])

By: AllHyps (Unfold `l_member`) THEN ExRepD THEN AllHyps (h.(Unfold `P_causal` h) THEN (Reduce h) THEN (InstHyp [i] h)) THEN ParallelOp -1

Generated subgoals:

None

About: