Nuprl Definition : system-strongly-realizes
assuming(env,r.A[env; r])
S |= eo.B[eo] ==
∀S2:InitialSystem(P.M[P]). (sub-system(P.M[P];S;S2) ⇒ assuming(env,r.A[env; r]) S2 |- eo.B[eo])
Definitions occuring in Statement :
sub-system: sub-system(P.M[P];S1;S2),
system-realizes: system-realizes,
InitialSystem: InitialSystem(P.M[P]),
all: ∀x:A. B[x],
implies: P ⇒ Q
FDL editor aliases :
system-strongly-realizes
Latex:
assuming(env,r.A[env; r])
S |= eo.B[eo] ==
\mforall{}S2:InitialSystem(P.M[P]). (sub-system(P.M[P];S;S2) {}\mRightarrow{} assuming(env,r.A[env; r]) S2 |- eo.B[eo])
Date html generated:
2015_07_23-AM-11_19_52
Last ObjectModification:
2012_02_25-PM-03_46_32
Home
Index