---

{ S1,S2,S3:Sys.  (S1  S2  S2  S3  S1  S3) }

{ Proof }

---

Definitions occuring in Statement :  subsys: S1  S2,  Sys: Sys,  all: x:A. B[x],  implies: P  Q
Definitions :  sub-system: sub-system(P.M[P];S1;S2),  member: t  T,  Sys: Sys,  System: System(P.M[P]),  list: type List,  equal: s = t,  subtype_rel: A r B,  function: x:A  B[x],  all: x:A. B[x],  universe: Type,  lambda: x.A[x],  implies: P  Q,  subsys: S1  S2,  strong-subtype: strong-subtype(A;B),  spread: spread def,  set: {x:A| B[x]} ,  ldag: LabeledDAG(T),  prop: ,  Auto: Error :Auto,  mData: mData,  name: Name,  product: x:A  B[x],  so_lambda: x.t[x],  parameter: parm{i},  CollapseTHEN: Error :CollapseTHEN,  tactic: Error :tactic
Lemmas :  subsys_wf,  Sys_wf,  sub-system_transitivity,  name_wf,  mData_wf,  System_wf,  member_wf

---

\mforall{}S1,S2,S3:Sys.    (S1  \msubseteq{}  S2  {}\mRightarrow{}  S2  \msubseteq{}  S3  {}\mRightarrow{}  S1  \msubseteq{}  S3)


Date html generated: 2010_08_27-PM-08_04_30
Last ObjectModification: 2010_06_09-PM-11_42_31

Home Index