Nuprl - Pf not_delivered_before

(3steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc

1. E: EventStruct
2. a: |E|
3. b: |E|
4. tr: |E| List
5. k:||tr||. a delivered at time k (k':||tr||. k' < k & b delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k]))

a somewhere delivered before b

By: Analyze 0 THEN Unfold `delivered_before_somewhere` -1 THEN ExRepD THEN InstHyp [k] -4 THEN ExRepD THEN InstHyp [k'] -5

Generated subgoals:

None

About:

(3steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc