PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: decidable switch inv rel

E:EventStruct, x:|E| List, j,z:||x||. Dec(j switchR(x) z)
By:
Auto
THEN
Unfold `switch_inv_rel` 0
THEN
Reduce 0
THEN
Repeat (First [(BackThru Thm* Dec(P) Dec(Q) Dec(P & Q)) THENL [Complete Auto;Id] ;BackThru Thm* Dec(P) Dec(Q) Dec(P Q)])
Generated subgoals:

None

About:
listdecidablenatural_numberall

PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc