Nuprl - Pf switch_theorem 1 1

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

1. E: EventStruct
2. P: (|E| List)Prop
3. A: Type
4. evt: A|E|
5. tg: ALabel
6. tr: A List
7. switchable(E)(P)
8. No-dup-send(E)(map(evt;tr))
9. switch_inv( < A,evt,tg > (E))(tr)
10. m:Label. P(map(evt; < tr > _m))
11. switchable( < A,evt,tg > (E))(P o evt)
12. tr:Trace( < A,evt,tg > (E)). (m:Label. P(map(evt; < tr > _m))) (switch_inv( < A,evt,tg > (E)) No-dup-send( < A,evt,tg > (E)))(tr) P(map(evt;tr))

No-dup-send( < A,evt,tg > (E))(tr)

By: BackThruLemma' Thm* E:EventStruct, A:Type, evt:(A|E|), tg:(ALabel), tr_l:A List. No-dup-send(E)(map(evt;tr_l)) No-dup-send( < A,evt,tg > (E))(tr_l)

Generated subgoals:

None

About:

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