---

Step * of Lemma lg-remove_wf

∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[x:ℕ].  (lg-remove(g;x) ∈ LabeledGraph(T))
BY
{ (Auto THEN Unfold `labeled-graph` 0 THEN DepIsectCD⋅ THEN DLabeledGraph 2) }

1
1. T : Type
2. g : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
3. g ∈ Top List
4. g ∈ (T × ℕ||g|| List × (ℕ||g|| List)) List
5. ||g|| ∈ ℕ
6. x : ℕ
⊢ lg-remove(g;x) ∈ Top List

2
1. T : Type
2. g : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
3. g ∈ Top List
4. g ∈ (T × ℕ||g|| List × (ℕ||g|| List)) List
5. ||g|| ∈ ℕ
6. x : ℕ
⊢ lg-remove(g;x) ∈ (T × ℕ||lg-remove(g;x)|| List × (ℕ||lg-remove(g;x)|| List)) List

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Unfold  `labeled-graph`  0  THEN  DepIsectCD\mcdot{}  THEN  DLabeledGraph  2)

---

Home Index