---

{ [S1,S2:Sys].  (S1  S2  ') }

{ Proof }

---

Definitions occuring in Statement :  subsys: S1  S2,  Sys: Sys,  uall: [x:A]. B[x],  prop: ,  member: t  T
Definitions :  uall: [x:A]. B[x],  Sys: Sys,  member: t  T,  subsys: S1  S2,  System: System(P.M[P]),  so_lambda: x.t[x],  so_apply: x[s]
Lemmas :  sub-system_wf,  name_wf,  mData_wf,  Sys_wf

---

\mforall{}[S1,S2:Sys].    (S1  \msubseteq{}  S2  \mmember{}  \mBbbP{}')


Date html generated: 2011_08_17-PM-04_13_18
Last ObjectModification: 2011_06_18-AM-11_31_27

Home Index