---

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 :  all: x:A. B[x],  InitialSystem: InitialSystem(P.M[P]),  implies: P  Q,  sub-system: sub-system(P.M[P];S1;S2),  system-realizes: system-realizes
FDL editor aliases :  system-strongly-realizes

---

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: 2010_08_27-PM-08_00_44
Last ObjectModification: 2010_06_02-PM-03_09_54

Home Index