---

Step * of Lemma lg-out-edges_wf

∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[x:ℕlg-size(g)].  (lg-out-edges(g;x) ∈ ℕlg-size(g) List)
BY
{ ((Auto THEN DVar `g') THEN All (Unfold `lg-size`) THEN ProveWfLemma)⋅ }

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  DVar  `g')  THEN  All  (Unfold  `lg-size`)  THEN  ProveWfLemma)\mcdot{}

---

Home Index