mb
hybrid
Sections
GenAutomata
Doc
Theorem
Name
Thm*
E:EventStruct. safetyR(E) preserves Causal(E)
[P_causal_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