{ 
[f:Id List 
Id]. [l_server,l_choose,l_comm,l_pi:Id].
(pi-system(f;l_server;l_choose;l_comm;l_pi) 
Pi_term System(P.piM(P))) }
{ Proof }
Definitions occuring in Statement :
pi-system: pi-system(f;l_server;l_choose;l_comm;l_pi),
piM: piM(T),
pi_term: Pi_term,
System: System(P.M[P]),
Id: Id,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
list: type List
Definitions :
uall: [x:A]. B[x],
member: t T,
pi-system: pi-system(f;l_server;l_choose;l_comm;l_pi),
System: System(P.M[P]),
component: component(P.M[P]),
nat: 
,
le: A 
B,
not: 
A,
implies: P 
Q,
false: False,
so_lambda: 
x.t[x],
pInTransit: pInTransit(P.M[P]),
piM: piM(T),
pCom: pCom(P.M[P]),
Com: Com(P.M[P]),
tagged+: T |+ z:B,
tag-case: z:T,
isect2: T1 
T2,
ifthenelse: if b then t else f fi ,
btrue: tt,
eq_atom: x =a y,
top: Top,
bfalse: ff,
prop: 
,
so_apply: x[s],
unit: Unit,
bool: 
,
pi-process: pi-process(),
it: 
Lemmas :
pi_term_wf,
Id_wf,
loc-Server_wf2,
le_wf,
processChoose_wf2,
processComm_wf2,
pi-trans_wf,
nat-to-incomparable_wf,
pi-names_wf,
pi-process_wf,
make-lg_wf_dag,
pInTransit_wf,
piM_wf,
pDVfire_wf,
PiDataVal_wf,
ifthenelse_wf,
eq_atom_wf,
top_wf,
Process_wf,
unit_wf,
bool_wf
\mforall{}[f:Id List {}\mrightarrow{} Id]. \mforall{}[l$_{server}$,l$_{choose}$,l$_\mbackslash{}\000Cff7bcomm}$,l$_{pi}$:Id].
(pi-system(f;l$_{server}$;l$_{choose}$;l$_{com\000Cm}$;l$_{pi}$) \mmember{} Pi\_term {}\mrightarrow{} System(P.piM(P)))
Date html generated:
2011_08_17-PM-07_04_34
Last ObjectModification:
2011_06_18-PM-12_46_51
Home
Index