---

Step * of Lemma lg-size-nil

∀[T:Type]. ∀[g:LabeledGraph(T)].  uiff(lg-size(g) = 0 ∈ ℤ;g = lg-nil() ∈ LabeledGraph(T))
BY
{ (Auto THEN All (RepUR ``lg-nil lg-size``)) }

1
1. T : Type
2. g : LabeledGraph(T)
3. ||g|| = 0 ∈ ℤ
⊢ g = [] ∈ LabeledGraph(T)

2
1. T : Type
2. g : LabeledGraph(T)
3. g = [] ∈ LabeledGraph(T)
⊢ ||g|| = 0 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g:LabeledGraph(T)].    uiff(lg-size(g)  =  0;g  =  lg-nil())


By

---

Latex:
(Auto  THEN  All  (RepUR  ``lg-nil  lg-size``))

---

Home Index