(2steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc
At:
P
causal
safety
E:EventStruct. safetyR(E) preserves Causal(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:
1
1.
E:
EventStruct
2.
x:
|E| List
3.
y:
|E| List
4.
y
x
5.
||y||
||x||
6.
i:
. i < ||y||
y[i] = x[i]
7.
Causal(E)(x)
Causal(E)(y)
About:
(2steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc