---

Step * of Lemma is-dag-remove

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

1
1. T : Type
2. g : LabeledGraph(T)
3. x : ℕlg-size(g)
4. ∀a,b:ℕlg-size(g).  (lg-edge(g;a;b) ⇒ a < b)
5. a : ℕlg-size(lg-remove(g;x))@i
6. b : ℕlg-size(lg-remove(g;x))@i
7. lg-edge(g;if a <z x then a else a + 1 fi ;if b <z x then b else b + 1 fi )
8. lg-size(lg-remove(g;x)) = (lg-size(g) - 1) ∈ ℤ
9. if a <z x then a else a + 1 fi  < if b <z x then b else b + 1 fi 
⊢ a < b

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  All  (Unfold  `is-dag`)
  THEN  Auto
  THEN  InstLemma  `lg-size-remove`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RWO  "lg-edge-remove"  (-2)
  THEN  Auto
  THEN  FHyp  4  [-2]
  THEN  Auto)

---

Home Index