---

Step * of Lemma sub-system-append

∀[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))
BY
{ (Auto THEN DVar `S1' THEN DVar `S2' THEN RepUR ``sub-system system-append`` 0 THEN Auto) }

---

Latex:

---

Latex:
\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))


By

---

Latex:
(Auto  THEN  DVar  `S1'  THEN  DVar  `S2'  THEN  RepUR  ``sub-system  system-append``  0  THEN  Auto)

---

Home Index