Nuprl Lemma : tagged-list-messages_wf

[S,V:Type]. ∀[M:Id ─→ Type]. ∀[s:S]. ∀[v:V]. ∀[L:(t:Id × (S ─→ V ─→ (M[t] List))) List].
  (tagged-list-messages(s;v;L) ∈ (t:Id × M[t]) List)


Proof




Definitions occuring in Statement :  tagged-list-messages: tagged-list-messages(s;v;L) Id: Id list: List uall: [x:A]. B[x] so_apply: x[s] member: t ∈ T function: x:A ─→ B[x] product: x:A × B[x] universe: Type
Lemmas :  concat_wf Id_wf map_wf list_wf
\mforall{}[S,V:Type].  \mforall{}[M:Id  {}\mrightarrow{}  Type].  \mforall{}[s:S].  \mforall{}[v:V].  \mforall{}[L:(t:Id  \mtimes{}  (S  {}\mrightarrow{}  V  {}\mrightarrow{}  (M[t]  List)))  List].
    (tagged-list-messages(s;v;L)  \mmember{}  (t:Id  \mtimes{}  M[t])  List)



Date html generated: 2015_07_17-AM-09_12_41
Last ObjectModification: 2015_01_28-AM-07_56_16

Home Index