---

Step * of Lemma normalize-constraints_wf

∀[k:ℕ]. ∀[A:(ℕ ⟶ ℚ × ℤ) List].  (normalize-constraints(k;A) ∈ (ℕ ⟶ ℚ × ℤ) List)
BY
{ (BasicUniformUnivCD Auto
   THEN Unhide
   THEN (Assert map(λp.normalize-constraint(k;p);A) ∈ (ℕ ⟶ ℚ × ℤ) List BY
               Auto)
   THEN (Assert ↓∃:ℕ. value-type(ℚ) BY
               (D 0 THEN With ⌜0⌝ (D 0)⋅ THEN Auto))) }

1
1. k : ℕ
2. A : (ℕ ⟶ ℚ × ℤ) List
3. map(λp.normalize-constraint(k;p);A) ∈ (ℕ ⟶ ℚ × ℤ) List
4. ↓∃:ℕ. value-type(ℚ)
⊢ normalize-constraints(k;A) ∈ (ℕ ⟶ ℚ × ℤ) List

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[A:(\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List].    (normalize-constraints(k;A)  \mmember{}  (\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List)


By

---

Latex:
(BasicUniformUnivCD  Auto
  THEN  Unhide
  THEN  (Assert  map(\mlambda{}p.normalize-constraint(k;p);A)  \mmember{}  (\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List  BY
                          Auto)
  THEN  (Assert  \mdownarrow{}\mexists{}:\mBbbN{}.  value-type(\mBbbQ{})  BY
                          (D  0  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)))

---

Home Index