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

At: switchable induced 7
1. E: EventStruct
2. A: Type
3. f: A|E|
4. P: (|E| List)Prop
5. tr:|E| List. P(tr) Causal(E)(tr)

tr:A List. P(map(f;tr)) Causal(induced_event_str(E;A;f))(tr)
By:
All (h.(Unfolds [`induced_event_str`;`P_causal`] h) THEN (Reduce h))
THEN
InstHyp [map(f;tr);i] -4
THEN
Try (RWO "map_length" 0)
THEN
All (h.(Unfold `event_msg_eq` h) THEN (Reduce h))
THEN
ParallelOp -1
THEN
Try (RWO "map_select" -1)
Generated subgoals:

None

About:
listapplyfunctionuniversepropimpliesall

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