mb
hybrid
Sections
GenAutomata
Doc
Theorem
Name
Thm*
E:TaggedEventStruct. safetyR(E) preserves switch_inv(E)
[switch_inv_safety]
cites
Thm*
l1,l2:T List. l1
l2
||l1||
||l2|| & (
i:
. i < ||l1||
l1[i] = l2[i])
[iseg_select]
mb
hybrid
Sections
GenAutomata
Doc