---

Step * of Lemma lg-label_wf

∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[x:ℕlg-size(g)].  (lg-label(g;x) ∈ T)
BY
{ (RepUR ``labeled-graph lg-size lg-label`` 0
   THEN Auto
   THEN Try (Complete (((Fold `labeled-graph` 2 THEN Fold `lg-size` 0) THEN Auto)))) }

1
1. T : Type
2. g : self:Top List ∩ (T × ℕ||self|| List × (ℕ||self|| List)) List
3. x : ℕ||g||
⊢ g ∈ (T × Top) List

---

Latex:

---

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


By

---

Latex:
(RepUR  ``labeled-graph  lg-size  lg-label``  0
  THEN  Auto
  THEN  Try  (Complete  (((Fold  `labeled-graph`  2  THEN  Fold  `lg-size`  0)  THEN  Auto))))

---

Home Index