---

Step * of Lemma norm-factors_wf

∀[L:ℕ List]. (norm-factors(L) ∈ ℕ List)
BY
{ xxx(Unfold `norm-factors` 0
      THEN Auto
      THEN GenConclAtAddrType ⌜ℕ List × ℕ × ℕ⌝ [2;1]⋅
      THEN Auto
      THEN (RepeatFor 2 (D (-2)) THEN Reduce 0)⋅
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[L:\mBbbN{}  List].  (norm-factors(L)  \mmember{}  \mBbbN{}  List)


By

---

Latex:
xxx(Unfold  `norm-factors`  0
        THEN  Auto
        THEN  GenConclAtAddrType  \mkleeneopen{}\mBbbN{}  List  \mtimes{}  \mBbbN{}  \mtimes{}  \mBbbN{}\mkleeneclose{}  [2;1]\mcdot{}
        THEN  Auto
        THEN  (RepeatFor  2  (D  (-2))  THEN  Reduce  0)\mcdot{}
        THEN  Auto)xxx

---

Home Index