---

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

.....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>)
BY
{ RepUR ``std-initial system-append`` 0⋅ }

1
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
⊢ ∀x∈lg-append(S4;S6).(fst(fst(x))) = (-1) ∈ ℤ

---

Latex:

---

Latex:
.....set  predicate..... 
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{}  std-initial(<S3,  S4>  @  <S5,  S6>)


By

---

Latex:
RepUR  ``std-initial  system-append``  0\mcdot{}

---

Home Index