---

Step * 1 of Lemma sub-system_weakening


1. [M] : Type ─→ Type
2. S3 : component(P.M[P]) List@i
3. S4 : LabeledDAG(pInTransit(P.M[P]))@i
4. S5 : component(P.M[P]) List@i
5. S6 : LabeledDAG(pInTransit(P.M[P]))@i
6. S3 = S5 ∈ (component(P.M[P]) List)
7. S4 = S6 ∈ LabeledDAG(pInTransit(P.M[P]))
8. S3 ⊆ S5
⊢ S6 ⊆ S6
BY
{ EAuto 1 }

---

Latex:

---

Latex:

1.  [M]  :  Type  {}\mrightarrow{}  Type
2.  S3  :  component(P.M[P])  List@i
3.  S4  :  LabeledDAG(pInTransit(P.M[P]))@i
4.  S5  :  component(P.M[P])  List@i
5.  S6  :  LabeledDAG(pInTransit(P.M[P]))@i
6.  S3  =  S5
7.  S4  =  S6
8.  S3  \msubseteq{}  S5
\mvdash{}  S6  \msubseteq{}  S6


By

---

Latex:
EAuto  1

---

Home Index