E:TaggedEventStruct. safetyR(E) preserves AD-normal(E)l1,l2:T List. l1 
l2 
||l1||||l2|| & (i:
. i < ||l1|| 
l1[i] = l2[i])| Theorem | Name |
|
Thm* E:TaggedEventStruct. safetyR(E) preserves AD-normal(E) | [switch_normal_safety] |
| cites | |
|
Thm* l1,l2:T List. l1 l2 ||l1||||l2|| & (i:. i < ||l1|| l1[i] = l2[i]) | [iseg_select] |