---

Step * 1 of Lemma normalize-constraints_wf


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

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  A  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List
3.  map(\mlambda{}p.normalize-constraint(k;p);A)  \mmember{}  (\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List
4.  \mdownarrow{}\mexists{}:\mBbbN{}.  value-type(\mBbbQ{})
\mvdash{}  normalize-constraints(k;A)  \mmember{}  (\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List


By

---

Latex:
ProveWfLemma

---

Home Index