assuming(env,r.A[env; r])
S |- eo.B[eo] ==
env:pEnvType(P.M[P]). let r = pRun(S;env;n2m;l2m) in A[env; r] 
B[EO(r)]
Definitions :
all: x:A. B[x],
pEnvType: pEnvType(T.M[T]),
let: let,
pRun: pRun(S0;env;nat2msg;loc2msg),
implies: P Q,
run-eo: EO(r)
FDL editor aliases :
system-realizes
assuming(env,r.A[env; r])
S |- eo.B[eo] ==
\mforall{}env:pEnvType(P.M[P]). let r = pRun(S;env;n2m;l2m) in A[env; r] {}\mRightarrow{} B[EO(r)]
Date html generated:
2010_08_27-PM-08_00_11
Last ObjectModification:
2010_06_02-PM-02_05_51
Home
Index