---

Step * 1 1 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
⊢ ∀x∈lg-append(S4;S6).(fst(fst(x))) = (-1) ∈ ℤ
BY
{ ((DVar `S4' THEN DVar `S6') THEN RWO "lg-all-append" 0 THEN Auto) }

---

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{}  \mforall{}x\mmember{}lg-append(S4;S6).(fst(fst(x)))  =  (-1)


By

---

Latex:
((DVar  `S4'  THEN  DVar  `S6')  THEN  RWO  "lg-all-append"  0  THEN  Auto)

---

Home Index