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

At: switchable induced 4
1. E: EventStruct
2. A: Type
3. f: A|E|
4. P: (|E| List)Prop
5. x,y:|E| List. P(x) (x send-enabledR(E) y) P(y)

x,y:A List. P(map(f;x)) (x send-enabledR(induced_event_str(E;A;f)) y) P(map(f;y))
By:
Auto
THEN
Using [`x',map(f;x);`y',map(f;y)] BackThruSomeHyp
THEN
All (h.(Unfold `R_send_enabled` h) THEN (Reduce h))
THEN
Unfold `induced_event_str` -1
THEN
Reduce -1
THEN
ExRepD
THEN
InstConcl [f(x@0)]
THEN
HypSubst -1 0
THEN
RW MapAppendC 0
THEN
Reduce 0
Generated subgoals:

None

About:
listapplyfunctionuniversepropimpliesall

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