---

Step * 2 of Lemma lg-size-nil


1. T : Type
2. g : LabeledGraph(T)
3. g = [] ∈ LabeledGraph(T)
⊢ ||g|| = 0 ∈ ℤ
BY
{ (DVar `g' THEN HypSubst (-1) 0 THEN (Reduce 0 THENA (D (-1) THEN Auto)) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  g  :  LabeledGraph(T)
3.  g  =  []
\mvdash{}  ||g||  =  0


By

---

Latex:
(DVar  `g'  THEN  HypSubst  (-1)  0  THEN  (Reduce  0  THENA  (D  (-1)  THEN  Auto))  THEN  Auto)\mcdot{}

---

Home Index