---

Step * 1 1 1 1 1 1 of Lemma normalize-constraint-eq

.....truecase..... 
1. k : ℕ
2. A1 : ℕ ⟶ ℚ
3. A2 : ℤ
4. x : ℕ
5. x < ||map(A1;upto(k))||
⊢ map(A1;upto(k))[x] = (A1 x) ∈ ℚ
BY
{ xxx((DupHyp (-1))
      THEN ((RWO "length-map" (-1)) THENA Auto)
      THEN (RWO "map_select" 0 THENA Auto)
      THEN Reduce 0
      THEN EqCD
      THEN Auto)xxx }

---

Latex:

---

Latex:
.....truecase..... 
1.  k  :  \mBbbN{}
2.  A1  :  \mBbbN{}  {}\mrightarrow{}  \mBbbQ{}
3.  A2  :  \mBbbZ{}
4.  x  :  \mBbbN{}
5.  x  <  ||map(A1;upto(k))||
\mvdash{}  map(A1;upto(k))[x]  =  (A1  x)


By

---

Latex:
xxx((DupHyp  (-1))
        THEN  ((RWO  "length-map"  (-1))  THENA  Auto)
        THEN  (RWO  "map\_select"  0  THENA  Auto)
        THEN  Reduce  0
        THEN  EqCD
        THEN  Auto)xxx

---

Home Index