---

Step * 1 of Lemma normalize-constraint-eq


1. k : ℕ
2. A : ℕ ⟶ ℚ × ℤ
⊢ normalize-constraint(k;A) = A ∈ (ℕ ⟶ ℚ × ℤ)
BY
{ xxx(D -1 THEN RepUR ``normalize-constraint`` 0)xxx }

1
1. k : ℕ
2. A1 : ℕ ⟶ ℚ
3. A2 : ℤ
⊢ eval r = A2 in let as ⟵ map(A1;upto(k)) in <λn.as[n]?A1 n, r> = <A1, A2> ∈ (ℕ ⟶ ℚ × ℤ)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{}
\mvdash{}  normalize-constraint(k;A)  =  A


By

---

Latex:
xxx(D  -1  THEN  RepUR  ``normalize-constraint``  0)xxx

---

Home Index