(14steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc
At:
switchable
induced
1
1.
E:
EventStruct
2.
A:
Type
3.
f:
A
|E|
4.
P:
(|E| List)
Prop
5.
x,y:|E| List. P(x)
(x safetyR(E) y)
P(y)
x,y:A List. P(map(f;x))
(x safetyR(induced_event_str(E;A;f)) y)
P(map(f;y))
By:
Auto
THEN
Using [`x',map(f;x)] BackThruSomeHyp
THEN
All (Unfold `R_safety`)
THEN
All Reduce
THEN
Easy
Generated subgoals:
None
About:
(14steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc