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:|E| List. P(x) (x delayableR(E) y) P(y)

x,y:A List. P(map(f;x)) (x delayableR(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.(Unfolds [`induced_event_str`;`R_delayable`] h) THEN (Reduce h)) THEN BackThru Thm* P:(AAProp), f:(BA), x,y:B List. (x swap adjacent[P(f(x),f(y))] y) (map(f;x) swap adjacent[P(x,y)] map(f;y)) THEN All (Unfold `event_msg_eq`) THEN All Reduce THEN Trivial

Generated subgoals:

None

About:

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