(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:

15. 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:
listlambdaapplyfunctionuniverseequalpropimpliesallexists

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