---

Step * 1 of Lemma lg-size-nil


1. T : Type
2. g : LabeledGraph(T)
3. ||g|| = 0 ∈ ℤ
⊢ g = [] ∈ LabeledGraph(T)
BY
{ (Unfold `labeled-graph` 0
   THEN DepIsectCD⋅
   THEN MoveToConcl (-1)
   THEN ((GenConcl ⌈g = G ∈ (Top List)⌉⋅ THENA Auto) THEN Thin (-1) THEN D -1 THEN Reduce 0 THEN Auto')⋅)⋅ }

---

Latex:

---

Latex:

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


By

---

Latex:
(Unfold  `labeled-graph`  0
  THEN  DepIsectCD\mcdot{}
  THEN  MoveToConcl  (-1)
  THEN  ((GenConcl  \mkleeneopen{}g  =  G\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Thin  (-1)  THEN  D  -1  THEN  Reduce  0  THEN  Auto')\mcdot{})\mcdot{}

---

Home Index