---

Step * of Lemma lg-remove_wf_dag

∀[T:Type]. ∀[g:LabeledDAG(T)]. ∀[x:ℕ].  (lg-remove(g;x) ∈ LabeledDAG(T))
BY
{ (Auto THEN DVar `g' THEN Auto THEN MemTypeCD THEN Auto THEN (Decide x < lg-size(g) THENA Auto)) }

1
1. T : Type
2. g : LabeledGraph(T)
3. is-dag(g)
4. x : ℕ
5. x < lg-size(g)
⊢ is-dag(lg-remove(g;x))

2
1. T : Type
2. g : LabeledGraph(T)
3. is-dag(g)
4. x : ℕ
5. ¬x < lg-size(g)
⊢ is-dag(lg-remove(g;x))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g:LabeledDAG(T)].  \mforall{}[x:\mBbbN{}].    (lg-remove(g;x)  \mmember{}  LabeledDAG(T))


By

---

Latex:
(Auto  THEN  DVar  `g'  THEN  Auto  THEN  MemTypeCD  THEN  Auto  THEN  (Decide  x  <  lg-size(g)  THENA  Auto))

---

Home Index