(3steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc

At: delivered before somewhere lemma 1
1. E: EventStruct
2. a: |E|
3. b: |E|
4. c: |E|
5. tr: |E| List
6. a somewhere delivered before b
7. a somewhere delivered before c
8. c somewhere delivered before b

False
By:
AllHyps (RWO "not_delivered_before_somewhere")
THEN
AllHyps (Unfold `delivered_before_somewhere`)
THEN
ExRepD
Generated subgoal:

16. k: ||tr||
7. a delivered at time k
8. k':||tr||. b delivered at time k' loc(E)(tr[k']) = loc(E)(tr[k]) kk'
9. k:||tr||. a delivered at time k (k':||tr||. k' < k & c delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k]))
10. k:||tr||. c delivered at time k (k':||tr||. k' < k & b delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k]))
False

About:
listfalse

(3steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc