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