Nuprl Definition : system-realizes
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 occuring in Statement :
run-eo: EO(r),
pRun: pRun(S0;env;nat2msg;loc2msg),
pEnvType: pEnvType(T.M[T]),
let: let,
all: ∀x:A. B[x],
implies: P ⇒ Q
FDL editor aliases :
system-realizes
Latex:
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:
2015_07_23-AM-11_19_28
Last ObjectModification:
2012_02_25-PM-03_46_02
Home
Index