---

{ [M:Type  Type]
    S1,S2,S3:System(P.M[P]).
      (sub-system(P.M[P];S1;S2)
       sub-system(P.M[P];S2;S3)
       sub-system(P.M[P];S1;S3)) }

{ Proof }

---

Definitions occuring in Statement :  sub-system: sub-system(P.M[P];S1;S2),  System: System(P.M[P]),  uall: [x:A]. B[x],  so_apply: x[s],  all: x:A. B[x],  implies: P  Q,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  so_apply: x[s],  implies: P  Q,  sub-system: sub-system(P.M[P];S1;S2),  and: P  Q,  member: t  T,  prop: ,  so_lambda: x.t[x],  System: System(P.M[P]),  ldag: LabeledDAG(T),  guard: {T}
Lemmas :  sublist_transitivity,  lg-contains_transitivity,  sublist_wf,  component_wf,  lg-contains_wf,  pInTransit_wf,  System_wf

---

\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}S1,S2,S3:System(P.M[P]).
        (sub-system(P.M[P];S1;S2)  {}\mRightarrow{}  sub-system(P.M[P];S2;S3)  {}\mRightarrow{}  sub-system(P.M[P];S1;S3))


Date html generated: 2011_08_17-PM-03_46_53
Last ObjectModification: 2011_06_18-AM-11_26_58

Home Index