---

Step * of Lemma norm-lg_wf

∀[T:Type]. ∀[N:id-fun(T)]. (norm-lg(N) ∈ id-fun(LabeledGraph(T))) supposing value-type(T)
BY
{ (Auto
   THEN (Assert norm-lg(N) ∈ id-fun((T × ℤ List × (ℤ List)) List) BY
               (ProveWfLemma
                THEN Try ((BLemma `product-value-type` THEN Auto))
                THEN (Try ((BLemma `list-value-type` THEN Auto))
                      THEN Try ((BLemma `int-value-type` THEN Auto))
                      THEN Unfold `id-fun` 0
                      THEN Auto)⋅))
   ) }

1
1. T : Type
2. value-type(T)
3. N : id-fun(T)
4. norm-lg(N) ∈ id-fun((T × ℤ List × (ℤ List)) List)
⊢ norm-lg(N) ∈ id-fun(LabeledGraph(T))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[N:id-fun(T)].  (norm-lg(N)  \mmember{}  id-fun(LabeledGraph(T)))  supposing  value-type(T)


By

---

Latex:
(Auto
  THEN  (Assert  norm-lg(N)  \mmember{}  id-fun((T  \mtimes{}  \mBbbZ{}  List  \mtimes{}  (\mBbbZ{}  List))  List)  BY
                          (ProveWfLemma
                            THEN  Try  ((BLemma  `product-value-type`  THEN  Auto))
                            THEN  (Try  ((BLemma  `list-value-type`  THEN  Auto))
                                        THEN  Try  ((BLemma  `int-value-type`  THEN  Auto))
                                        THEN  Unfold  `id-fun`  0
                                        THEN  Auto)\mcdot{}))
  )

---

Home Index