PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: decidable delivered before somewhere

E:EventStruct, tr:|E| List, x,y:|E|. Dec(x somewhere delivered before y)
By:
Auto
THEN
Unfold `delivered_before_somewhere` 0
THEN
Unfold `delivered_at` 0
THEN
Repeat (First [(BackThru Thm* Dec(P) Dec(Q) Dec(P & Q)) THENL [Complete Auto;Id] ;(BackThru Thm* i,j:, F:({i..j}Prop). (k:{i..j}. Dec(F(k))) Dec(k:{i..j}. F(k))) THEN (Reduce 0) THEN (Analyze 0) ;(BackThru Thm* i,j:, F:({i..j}Prop). (k:{i..j}. Dec(F(k))) Dec(k:{i..j}. F(k))) THEN (Reduce 0) THEN (Analyze 0)])
Generated subgoals:

None

About:
listdecidableall

PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc