{ 
[M:Type 
Type]
[t:
]. [x:Id]. [m:pMsg(P.M[P])]. [S:System(P.M[P])].
[C:component(P.M[P])].
(deliver-msg-to-comp(t;m;x;S;C) 
System(P.M[P]))
supposing Continuous+(P.M[P]) }
{ Proof }
Definitions occuring in Statement :
deliver-msg-to-comp: deliver-msg-to-comp(t;m;x;S;C),
System: System(P.M[P]),
component: component(P.M[P]),
pMsg: pMsg(P.M[P]),
Id: Id,
strong-type-continuous: Continuous+(T.F[T]),
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
member: t T,
function: x:A B[x],
universe: Type
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
so_apply: x[s],
System: System(P.M[P]),
component: component(P.M[P]),
member: t T,
deliver-msg-to-comp: deliver-msg-to-comp(t;m;x;S;C),
so_lambda: 
x.t[x],
prop: 
Lemmas :
ifthenelse_wf,
eq_id_wf,
System_wf,
Process-apply_wf,
lg-append_wf_dag,
pInTransit_wf,
add-cause_wf,
component_wf,
pMsg_wf,
Id_wf,
nat_wf,
strong-type-continuous_wf
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}[t:\mBbbN{}]. \mforall{}[x:Id]. \mforall{}[m:pMsg(P.M[P])]. \mforall{}[S:System(P.M[P])]. \mforall{}[C:component(P.M[P])].
(deliver-msg-to-comp(t;m;x;S;C) \mmember{} System(P.M[P]))
supposing Continuous+(P.M[P])
Date html generated:
2011_08_16-PM-06_52_49
Last ObjectModification:
2011_06_18-AM-11_07_20
Home
Index