---

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


1. k : ℕ
2. A1 : ℕ ⟶ ℚ
3. A2 : ℤ
4. x : ℕ
⊢ map(A1;upto(k))[x]?A1 x = (A1 x) ∈ ℚ
BY
{ xxx(Unfold `select?` 0 THEN SplitOnConclITE THEN Auto)xxx }

1
.....truecase..... 
1. k : ℕ
2. A1 : ℕ ⟶ ℚ
3. A2 : ℤ
4. x : ℕ
5. x < ||map(A1;upto(k))||
⊢ map(A1;upto(k))[x] = (A1 x) ∈ ℚ

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(Unfold  `select?`  0  THEN  SplitOnConclITE  THEN  Auto)xxx

---

Home Index