{ 
[P:PiDataVal() 
]
((id:Id. P[pDVloc(id)])
(id:Id. name:Name. P[pDVloc_tag(id;name)])
(from:Id. preList:pi_prefix() List. P[pDVguards(from;preList)])
(val:Name. index:
. P[pDVmsg(val;index)])
P[pDVfire()]
P[pDVcontinue()]
(rndv1: 
Id Name. P[pDVselex(rndv1)])
(rndv2: Id Name. counter:. P[pDVrequest(rndv2;counter)])
{x:PiDataVal(). P[x]}) }
{ Proof }
Definitions occuring in Statement :
pDVmsg: pDVmsg(val;index),
PiDataVal: PiDataVal(),
pi_prefix: pi_prefix(),
Id: Id,
name: Name,
nat: ,
uall: [x:A]. B[x],
prop: ,
guard: {T},
so_apply: x[s],
all: x:A. B[x],
implies: P Q,
function: x:A B[x],
product: x:A B[x],
list: type List
Definitions :
uall: [x:A]. B[x],
prop: ,
implies: P Q,
all: x:A. B[x],
so_apply: x[s],
guard: {T},
member: t 
T,
PiDataVal: PiDataVal(),
pDVloc: pDVloc(id),
pDVloc_tag: pDVloc_tag(id;name),
pDVguards: pDVguards(from;preList),
pDVmsg: pDVmsg(val;index),
pDVfire: pDVfire(),
pDVcontinue: pDVcontinue(),
pDVselex: pDVselex(rndv1),
pDVrequest: pDVrequest(rndv2;counter),
unit: Unit,
it: 
Lemmas :
PiDataVal_wf,
nat_wf,
Id_wf,
name_wf,
pDVrequest_wf,
pDVselex_wf,
pDVcontinue_wf,
pDVfire_wf,
pDVmsg_wf,
pi_prefix_wf,
pDVguards_wf,
pDVloc_tag_wf,
pDVloc_wf
\mforall{}[P:PiDataVal() {}\mrightarrow{} \mBbbP{}]
((\mforall{}id:Id. P[pDVloc(id)])
{}\mRightarrow{} (\mforall{}id:Id. \mforall{}name:Name. P[pDVloc\_tag(id;name)])
{}\mRightarrow{} (\mforall{}from:Id. \mforall{}preList:pi\_prefix() List. P[pDVguards(from;preList)])
{}\mRightarrow{} (\mforall{}val:Name. \mforall{}index:\mBbbN{}. P[pDVmsg(val;index)])
{}\mRightarrow{} P[pDVfire()]
{}\mRightarrow{} P[pDVcontinue()]
{}\mRightarrow{} (\mforall{}rndv1:\mBbbN{} \mtimes{} Id \mtimes{} \mBbbN{} \mtimes{} Name. P[pDVselex(rndv1)])
{}\mRightarrow{} (\mforall{}rndv2:\mBbbN{} \mtimes{} Id \mtimes{} \mBbbN{} \mtimes{} Name. \mforall{}counter:\mBbbN{}. P[pDVrequest(rndv2;counter)])
{}\mRightarrow{} \{\mforall{}x:PiDataVal(). P[x]\})
Date html generated:
2011_08_17-PM-06_54_13
Last ObjectModification:
2011_06_18-PM-12_29_30
Home
Index