---

Step * of Lemma is-dag-append

∀[T:Type]. ∀[g1,g2:LabeledGraph(T)].  (is-dag(lg-append(g1;g2))) supposing (is-dag(g2) and is-dag(g1))
BY
{ (Auto THEN All (Unfold `is-dag`) THEN Auto) }

1
1. T : Type
2. g1 : LabeledGraph(T)
3. g2 : LabeledGraph(T)
4. ∀a,b:ℕlg-size(g1).  (lg-edge(g1;a;b) ⇒ a < b)
5. ∀a,b:ℕlg-size(g2).  (lg-edge(g2;a;b) ⇒ a < b)
6. a : ℕlg-size(lg-append(g1;g2))@i
7. b : ℕlg-size(lg-append(g1;g2))@i
8. lg-edge(lg-append(g1;g2);a;b)@i
⊢ a < b

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g1,g2:LabeledGraph(T)].
    (is-dag(lg-append(g1;g2)))  supposing  (is-dag(g2)  and  is-dag(g1))


By

---

Latex:
(Auto  THEN  All  (Unfold  `is-dag`)  THEN  Auto)

---

Home Index