Nuprl Lemma : pDVmsg_wf
∀[val:Name]. ∀[index:ℕ].  (pDVmsg(val;index) ∈ PiDataVal())
Proof
Definitions occuring in Statement : 
pDVmsg: pDVmsg(val;index)
, 
PiDataVal: PiDataVal()
, 
name: Name
, 
nat: ℕ
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
Definitions unfolded in proof : 
pDVmsg: pDVmsg(val;index)
, 
PiDataVal: PiDataVal()
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
Latex:
\mforall{}[val:Name].  \mforall{}[index:\mBbbN{}].    (pDVmsg(val;index)  \mmember{}  PiDataVal())
Date html generated:
2016_05_17-AM-11_26_36
Last ObjectModification:
2015_12_29-PM-06_52_27
Theory : event-logic-applications
Home
Index