---

Step * of Lemma is-dag-add

∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[y:ℕlg-size(g)]. ∀[x:ℕy].  is-dag(lg-add(g;x;y)) supposing is-dag(g)
BY
{ (Auto
   THEN All (Unfold `is-dag`)
   THEN Auto
   THEN (InstLemma `lg-size-add` [⌜T⌝;⌜g⌝;⌜x⌝;⌜y⌝]⋅ THENA Auto)
   THEN RWO "lg-edge-add" (-2)
   THEN Auto'
   THEN D -2
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g:LabeledGraph(T)].  \mforall{}[y:\mBbbN{}lg-size(g)].  \mforall{}[x:\mBbbN{}y].
    is-dag(lg-add(g;x;y))  supposing  is-dag(g)


By

---

Latex:
(Auto
  THEN  All  (Unfold  `is-dag`)
  THEN  Auto
  THEN  (InstLemma  `lg-size-add`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "lg-edge-add"  (-2)
  THEN  Auto'
  THEN  D  -2
  THEN  Auto')

---

Home Index