{ 
[Cs:Component List]. (mk-init-sys(Cs) 
InitSys) }
{ Proof }
Definitions occuring in Statement :
mk-init-sys: mk-init-sys(Cs),
InitSys: InitSys,
Component: Component,
uall: [x:A]. B[x],
member: t T,
list: type List
Definitions :
uall: [x:A]. B[x],
member: t T,
InitSys: InitSys,
Sys: Sys,
mk-init-sys: mk-init-sys(Cs),
System: System(P.M[P]),
so_lambda: 
x.t[x],
std-initial: std-initial(S),
lg-all: xG.P[x],
pi2: snd(t),
lg-nil: lg-nil(),
all: x:A. B[x],
int_seg: {i..j
},
lg-size: lg-size(g),
length: ||as||,
ycomb: Y,
lelt: i 
j < k,
and: P 
Q,
Component: Component,
Message: Message,
pMsg: pMsg(P.M[P]),
so_apply: x[s],
le: A B,
not: 
A,
implies: P 
Q,
false: False,
prop: 
Lemmas :
Component_wf,
lg-nil_wf_dag,
pInTransit_wf,
name_wf,
mData_wf,
pi1_wf_top,
top_wf,
lg-label_wf_dag,
le_wf,
int_seg_wf,
std-initial_wf
\mforall{}[Cs:Component List]. (mk-init-sys(Cs) \mmember{} InitSys)
Date html generated:
2011_08_17-PM-04_13_09
Last ObjectModification:
2011_06_18-AM-11_31_14
Home
Index