Nuprl Lemma : pDVrequest_wf
∀[rndv2:ℕ × Id × ℕ × Name]. ∀[counter:ℕ].  (pDVrequest(rndv2;counter) ∈ PiDataVal())
Proof
Definitions occuring in Statement : 
pDVrequest: pDVrequest(rndv2;counter)
, 
PiDataVal: PiDataVal()
, 
Id: Id
, 
name: Name
, 
nat: ℕ
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
product: x:A × B[x]
Definitions unfolded in proof : 
pDVrequest: pDVrequest(rndv2;counter)
, 
PiDataVal: PiDataVal()
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
Latex:
\mforall{}[rndv2:\mBbbN{}  \mtimes{}  Id  \mtimes{}  \mBbbN{}  \mtimes{}  Name].  \mforall{}[counter:\mBbbN{}].    (pDVrequest(rndv2;counter)  \mmember{}  PiDataVal())
Date html generated:
2016_05_17-AM-11_27_01
Last ObjectModification:
2015_12_29-PM-06_52_16
Theory : event-logic-applications
Home
Index