(3steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc

At: not delivered before somewhere 1
1. E: EventStruct
2. a: |E|
3. b: |E|
4. tr: |E| List
5. a somewhere delivered before b
6. k: ||tr||
7. a delivered at time k

k':||tr||. k' < k & b delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k])
By:
Unfold `delivered_at` 0
THEN
SupposeNot
THEN
Fold `delivered_at` -1
THEN
Analyze -4
THEN
Unfold `delivered_before_somewhere` 0
THEN
InstConcl [k]
THEN
SupposeNot
THEN
Analyze -5
THEN
InstConcl [k']
Generated subgoals:

None

About:
listnatural_numberless_thanapplyequalandexists

(3steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc