Nuprl - Pf switchable

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

1. E: EventStruct
2. A: Type
3. f: A|E|
4. P: (|E| List)Prop
5. x,y,z:|E| List. P(x) P(y) composableR(E)(x,y,z) P(z)
6. x: A List
7. y: A List
8. z: A List
9. P(map(f;x))
10. P(map(f;y))
11. composableR(induced_event_str(E;A;f))(x,y,z)

composableR(E)(map(f;x),map(f;y),map(f;z))

By: All (Unfold `R_composable`) THEN All Reduce

Generated subgoal:

1 5. x,y,z:|E| List. P(x) P(y) (xx.(yy.(x =msg=(E) y))) & z = (x @ y) P(z)
6. x: A List
7. y: A List
8. z: A List
9. P(map(f;x))
10. P(map(f;y))
11. (xx.(yy.(x =msg=(induced_event_str(E;A;f)) y))) & z = (x @ y)
(xmap(f;x).(ymap(f;y).(x =msg=(E) y))) & map(f;z) = (map(f;x) @ map(f;y))

About:

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