Nuprl Lemma : pv8_p2_out_tr_wf
[Cid,Op,RepState:ValueAllType].
(pv8_p2_out_tr(Cid;Op;RepState) 
A:
'
(A
RepState 
( Id Cid Op) List (( Id Cid Op) List)
(RepState ( Id Cid Op) List (( Id Cid Op) List)
bag(Id Message))
Id
A
RepState ( Id Cid Op) List (( Id Cid Op) List)
bag(Id Message)
(RepState ( Id Cid Op) List (( Id Cid Op) List)
bag(Id Message))))
Proof not projected
Definitions occuring in Statement :
pv8_p2_out_tr: pv8_p2_out_tr(Cid;Op;RepState),
Message: Message,
Id: Id,
uall: [x:A]. B[x],
member: t T,
isect: x:A. B[x],
function: x:A B[x],
product: x:A B[x],
list: type List,
int: ,
universe: Type,
bag: bag(T),
vatype: ValueAllType
Definitions :
pv8_p2_out_tr: pv8_p2_out_tr(Cid;Op;RepState),
member: t T,
vatype: ValueAllType,
uall: [x:A]. B[x]
Lemmas :
valueall-type_wf,
Message_wf,
bag_wf,
Id_wf
\mforall{}[Cid,Op,RepState:ValueAllType].
(pv8\_p2\_out\_tr(Cid;Op;RepState) \mmember{} \mcap{}A:\mBbbU{}'
(A
{}\mrightarrow{} RepState
\mtimes{} \mBbbZ{}
\mtimes{} (\mBbbZ{} \mtimes{} Id \mtimes{} Cid \mtimes{} Op) List
\mtimes{} ((\mBbbZ{} \mtimes{} Id \mtimes{} Cid \mtimes{} Op) List)
{}\mrightarrow{} (RepState
\mtimes{} \mBbbZ{}
\mtimes{} (\mBbbZ{} \mtimes{} Id \mtimes{} Cid \mtimes{} Op) List
\mtimes{} ((\mBbbZ{} \mtimes{} Id \mtimes{} Cid \mtimes{} Op) List) \mtimes{} bag(Id \mtimes{} Message))
{}\mrightarrow{} Id
{}\mrightarrow{} A
{}\mrightarrow{} RepState
\mtimes{} \mBbbZ{}
\mtimes{} (\mBbbZ{} \mtimes{} Id \mtimes{} Cid \mtimes{} Op) List
\mtimes{} ((\mBbbZ{} \mtimes{} Id \mtimes{} Cid \mtimes{} Op) List) \mtimes{} bag(Id \mtimes{} Message)
{}\mrightarrow{} (RepState
\mtimes{} \mBbbZ{}
\mtimes{} (\mBbbZ{} \mtimes{} Id \mtimes{} Cid \mtimes{} Op) List
\mtimes{} ((\mBbbZ{} \mtimes{} Id \mtimes{} Cid \mtimes{} Op) List) \mtimes{} bag(Id \mtimes{} Message))))
Date html generated:
2012_02_20-PM-07_36_19
Last ObjectModification:
2012_02_06-PM-03_14_44
Home
Index