(14steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc
At:
switchable
induced
2
1.
E:
EventStruct
2.
A:
Type
3.
f:
A
|E|
4.
P:
(|E| List)
Prop
5.
x,y:|E| List. P(x)
(x memorylessR(E) y)
P(y)
x,y:A List. P(map(f;x))
(x memorylessR(induced_event_str(E;A;f)) y)
P(map(f;y))
By:
Auto
THEN
Using [`x',map(f;x)] BackThruSomeHyp
THEN
All (Unfold `R_memoryless`)
THEN
All Reduce
Generated subgoal:
1
5.
x,y:|E| List. P(x)
(
a:|E|. y = filter(
b.
(b =msg=(E) a);x))
P(y)
6.
x:
A List
7.
y:
A List
8.
P(map(f;x))
9.
a:A. y = filter(
b.
(b =msg=(induced_event_str(E;A;f)) a);x)
a:|E|. map(f;y) = filter(
b.
(b =msg=(E) a);map(f;x))
About:
(14steps)
PrintForm
Definitions
Lemmas
mb
hybrid
Sections
GenAutomata
Doc