---

Step * 1 of Lemma normalize-constraints-eq


1. k : ℕ
2. A : (ℕ ⟶ ℚ × ℤ) List
3. map(λp.normalize-constraint(k;p);A) = A ∈ ((ℕ ⟶ ℚ × ℤ) List)
⊢ normalize-constraints(k;A) = A ∈ ((ℕ ⟶ ℚ × ℤ) List)
BY
{ (Assert map(λp.normalize-constraint(k;p);A) ∈ (ℕ ⟶ ℚ × ℤ) List BY
         Auto) }

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

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  A  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List
3.  map(\mlambda{}p.normalize-constraint(k;p);A)  =  A
\mvdash{}  normalize-constraints(k;A)  =  A


By

---

Latex:
(Assert  map(\mlambda{}p.normalize-constraint(k;p);A)  \mmember{}  (\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List  BY
              Auto)

---

Home Index