Nuprl - Pf switchable_induced 2 1 1

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

At: switchable induced 2 1 1

1. E: EventStruct
2. A: Type
3. f: A|E|
4. P: (|E| List)Prop
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
10. y = filter(b.(b =msg=(induced_event_str(E;A;f)) a);x)

map(f;filter(b.(b =msg=(induced_event_str(E;A;f)) a);x)) = map(f;filter((b.(b =msg=(E) (f(a)))) o f;x))

By: Unfolds [`compose`;`induced_event_str`] 0 THEN Reduce 0 THEN All (Unfold `event_msg_eq`) THEN All Reduce

Generated subgoals:

None

About:

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