{ 
[M:Type 
Type]
[S:InitialSystem(P.M[P])]. [n2m:
pMsg(P.M[P])].
[l2m:Id pMsg(P.M[P])]. [A:pEnvType(P.M[P]) pRunType(P.M[P]) 
].
[B:EO+(pMsg(P.M[P])) ].
(assuming(env,r.A[env;r])
S |- eo.B[eo] 
)
supposing Continuous+(P.M[P]) }
{ Proof }
Definitions occuring in Statement :
system-realizes: system-realizes,
InitialSystem: InitialSystem(P.M[P]),
pEnvType: pEnvType(T.M[T]),
pRunType: pRunType(T.M[T]),
pMsg: pMsg(P.M[P]),
event-ordering+: EO+(Info),
Id: Id,
strong-type-continuous: Continuous+(T.F[T]),
nat: ,
uimplies: b supposing a,
uall: [x:A]. B[x],
prop: ,
so_apply: x[s1;s2],
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],
pRunType: pRunType(T.M[T]),
prop: ,
member: t T,
system-realizes: system-realizes,
so_apply: x[s1;s2],
all: x:A. B[x],
let: let,
implies: P 
Q,
so_lambda: 
x.t[x],
fulpRunType: fulpRunType(T.M[T]),
top: Top,
InitialSystem: InitialSystem(P.M[P]),
System: System(P.M[P])
Lemmas :
pEnvType_wf,
pRun_wf2,
pRun_wf,
subtype_rel_function,
nat_wf,
Id_wf,
pMsg_wf,
unit_wf,
System_wf,
top_wf,
ldag_wf,
pInTransit_wf,
subtype_rel_self,
subtype_rel_simple_product,
fulpRunType_wf,
pRunType_wf,
run-eo_wf,
run-initialization-property,
std-initial-property,
runEvents_wf,
event-ordering+_wf,
InitialSystem_wf,
strong-type-continuous_wf
\mforall{}[M:Type {}\mrightarrow{} Type]
\mforall{}[S:InitialSystem(P.M[P])]. \mforall{}[n2m:\mBbbN{} {}\mrightarrow{} pMsg(P.M[P])]. \mforall{}[l2m:Id {}\mrightarrow{} pMsg(P.M[P])].
\mforall{}[A:pEnvType(P.M[P]) {}\mrightarrow{} pRunType(P.M[P]) {}\mrightarrow{} \mBbbP{}]. \mforall{}[B:EO+(pMsg(P.M[P])) {}\mrightarrow{} \mBbbP{}].
(assuming(env,r.A[env;r])
S |- eo.B[eo] \mmember{} \mBbbP{})
supposing Continuous+(P.M[P])
Date html generated:
2011_08_17-PM-03_46_36
Last ObjectModification:
2011_06_18-AM-11_26_35
Home
Index