(3steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: switch normal safety


E:TaggedEventStruct. safetyR(E) preserves AD-normal(E)

By:
Unfolds [`preserved_by`;`R_safety`] 0
THEN
Reduce 0
THEN
Try (Fold `trace_property` 0)
THEN
Inst Thm* l1,l2:T List. l1 l2 ||l1||||l2|| & (i:. i < ||l1|| l1[i] = l2[i]) [|E|;y;x]
THEN
SimpHyp -1
THEN
ExRepD
THEN
MoveToHyp 0 -4


Generated subgoal:

11. E: TaggedEventStruct
2. x: |E| List
3. y: |E| List
4. y x
5. ||y||||x||
6. i:. i < ||y|| y[i] = x[i]
7. AD-normal(E)(x)
AD-normal(E)(y)


About:
listapplyall

(3steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc