---

Step * 1 1 of Lemma normalize-constraints-eq


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)
BY
{ ((Assert ↓∃:ℕ. value-type(ℚ) BY
          (D 0 THEN With ⌜0⌝ (D 0)⋅ THEN Auto))
   THEN (Unfold `normalize-constraints` 0 THEN (CallByValueReduce 0 THENA Auto) THEN Trivial)⋅
   ) }

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  \mdownarrow{}\mexists{}:\mBbbN{}.  value-type(\mBbbQ{})  BY
                (D  0  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  THEN  (Unfold  `normalize-constraints`  0  THEN  (CallByValueReduce  0  THENA  Auto)  THEN  Trivial)\mcdot{}
  )

---

Home Index