(3steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc

At: delivered before somewhere lemma 1 1
1. E: EventStruct
2. a: |E|
3. b: |E|
4. c: |E|
5. tr: |E| List
6. 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
By:
InstHyp [k] -2
THEN
ExRepD
THEN
InstHyp [k'] -5
THEN
ExRepD
THEN
InstHyp [k'@0] -11
Generated subgoals:

None

About:
listnatural_numberless_thanapplyequalimpliesandfalseallexists

(3steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc