---

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

{ Proof }

---

Definitions occuring in Statement :  system-append: S1 @ S2,  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],  and: P  Q,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  so_apply: x[s],  and: P  Q,  sub-system: sub-system(P.M[P];S1;S2),  system-append: S1 @ S2,  member: t  T,  so_lambda: x.t[x],  true: True,  System: System(P.M[P]),  ldag: LabeledDAG(T),  uimplies: b supposing a,  iff: P  Q,  implies: P  Q,  rev_implies: P  Q
Lemmas :  lg-append-contains,  pInTransit_wf,  sublist_append2,  component_wf,  System_wf,  sublist_weakening,  nil_sublist,  sublist_append1,  sublist_append

---

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


Date html generated: 2011_08_17-PM-03_47_17
Last ObjectModification: 2011_06_18-AM-11_27_32

Home Index