Nuprl Lemma : type-of-message

Nuprl Lemma : type-of-message_wf

[T:Type].

[es:EO'].

[nm:Name].

[locs:Id List]. (type-of-message(es;nm;locs;T)

')

Proof not projected

Definitions occuring in Statement : type-of-message: type-of-message(es;nm;locs;T), Message: Message, event-ordering+: EO+(Info), Id: Id, name: Name, uall:

[x:A]. B[x], prop:

, member: t

T, list: type List, universe: Type
Definitions : so_lambda:

x.t[x], all:

x:A. B[x], type-of-message: type-of-message(es;nm;locs;T), prop:

, member: t

T, uall:

[x:A]. B[x], so_apply: x[s]
Lemmas : event-ordering+_wf, name_wf, Id_wf, msg-type_wf, Message_wf, es-E-interface_wf, all_wf

\mforall{}[T:Type]. \mforall{}[es:EO']. \mforall{}[nm:Name]. \mforall{}[locs:Id List]. (type-of-message(es;nm;locs;T) \mmember{} \mBbbP{}') Date html generated: 2012_01_23-PM-01_42_41 Last ObjectModification: 2011_12_11-PM-12_22_59 Home Index