---

Step * 1 1 of Lemma system-strongly-realizes-and


1. M : Type ─→ Type
2. S3 : component(P.M[P]) List@i
3. S4 : LabeledDAG(pInTransit(P.M[P]))@i
4. std-initial(<S3, S4>)@i
5. S5 : component(P.M[P]) List@i
6. S6 : LabeledDAG(pInTransit(P.M[P]))@i
7. std-initial(<S5, S6>)@i
⊢ <S3, S4> @ <S5, S6> ∈ InitialSystem(P.M[P])
BY
{ (MemTypeCD⋅ THEN Auto THEN RepUR ``System`` 0 THEN Auto) }

1
.....set predicate..... 
1. M : Type ─→ Type
2. S3 : component(P.M[P]) List@i
3. S4 : LabeledDAG(pInTransit(P.M[P]))@i
4. std-initial(<S3, S4>)@i
5. S5 : component(P.M[P]) List@i
6. S6 : LabeledDAG(pInTransit(P.M[P]))@i
7. std-initial(<S5, S6>)@i
⊢ std-initial(<S3, S4> @ <S5, S6>)

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  S3  :  component(P.M[P])  List@i
3.  S4  :  LabeledDAG(pInTransit(P.M[P]))@i
4.  std-initial(<S3,  S4>)@i
5.  S5  :  component(P.M[P])  List@i
6.  S6  :  LabeledDAG(pInTransit(P.M[P]))@i
7.  std-initial(<S5,  S6>)@i
\mvdash{}  <S3,  S4>  @  <S5,  S6>  \mmember{}  InitialSystem(P.M[P])


By

---

Latex:
(MemTypeCD\mcdot{}  THEN  Auto  THEN  RepUR  ``System``  0  THEN  Auto)

---

Home Index