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

By: RWW "l_all_map" 0 THEN ParallelOp -1 THEN Try ((HypSubst -1 0) THEN (RW MapAppendC 0)) THEN RepeatFor 2 (ParallelOp -1) THEN All (Fold `l_all`) THEN RWO "l_all_map" 0

Generated subgoal:

1 11. (x@0x.(y@0y.(x@0 =msg=(induced_event_str(E;A;f)) y@0)))
12. x@0: A
13. (x@0 x) (y@0y.(x@0 =msg=(induced_event_str(E;A;f)) y@0))
(x@0 x) (y@0y.((f(x@0)) =msg=(E) (f(y@0))))

About:

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