---

Step * of Lemma lg-add_wf

∀[T:Type]. ∀[g:LabeledGraph(T)]. ∀[a,b:ℕlg-size(g)].  (lg-add(g;a;b) ∈ LabeledGraph(T))
BY
{ (ProveWfLemma
   THEN DepIsectHD 2
   THEN (Assert ||g|| ∈ ℤ BY
               (GenConcl ⌜g = L ∈ (Top List)⌝⋅ THEN Auto))
   THEN Unfold `labeled-graph` 0
   THEN DepIsectCD
   THEN RWW "mklist_length" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g:LabeledGraph(T)].  \mforall{}[a,b:\mBbbN{}lg-size(g)].    (lg-add(g;a;b)  \mmember{}  LabeledGraph(T))


By

---

Latex:
(ProveWfLemma
  THEN  DepIsectHD  2
  THEN  (Assert  ||g||  \mmember{}  \mBbbZ{}  BY
                          (GenConcl  \mkleeneopen{}g  =  L\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  Unfold  `labeled-graph`  0
  THEN  DepIsectCD
  THEN  RWW  "mklist\_length"  0
  THEN  Auto)

---

Home Index