---

Step * 3 of Lemma q-constraint-negative

.....falsecase..... 
1. x : ℕ ⟶ ℚ
2. r : ℤ
3. k : ℕ+
4. y : ℚ List
5. k ≤ ||y||
6. x k < 0
7. ¬((x k) = 0 ∈ ℚ)
8. 0 < -(x k)
9. ¬(r = 0 ∈ ℤ)
10. ¬(r = 1 ∈ ℤ)
⊢ uiff(0 < q-linear(k - 1;j.x j;y) + ((x k) * y[k - 1]);0 < -(y[k - 1]) + ((-1/x k) * q-linear(k - 1;j.x j;y)))
BY
{ Auto }

1
1. x : ℕ ⟶ ℚ
2. r : ℤ
3. k : ℕ+
4. y : ℚ List
5. k ≤ ||y||
6. x k < 0
7. ¬((x k) = 0 ∈ ℚ)
8. 0 < -(x k)
9. ¬(r = 0 ∈ ℤ)
10. ¬(r = 1 ∈ ℤ)
11. 0 < q-linear(k - 1;j.x j;y) + ((x k) * y[k - 1])
⊢ 0 < -(y[k - 1]) + ((-1/x k) * q-linear(k - 1;j.x j;y))

2
1. x : ℕ ⟶ ℚ
2. r : ℤ
3. k : ℕ+
4. y : ℚ List
5. k ≤ ||y||
6. x k < 0
7. ¬((x k) = 0 ∈ ℚ)
8. 0 < -(x k)
9. ¬(r = 0 ∈ ℤ)
10. ¬(r = 1 ∈ ℤ)
11. 0 < -(y[k - 1]) + ((-1/x k) * q-linear(k - 1;j.x j;y))
⊢ 0 < q-linear(k - 1;j.x j;y) + ((x k) * y[k - 1])

---

Latex:

---

Latex:
.....falsecase..... 
1.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbQ{}
2.  r  :  \mBbbZ{}
3.  k  :  \mBbbN{}\msupplus{}
4.  y  :  \mBbbQ{}  List
5.  k  \mleq{}  ||y||
6.  x  k  <  0
7.  \mneg{}((x  k)  =  0)
8.  0  <  -(x  k)
9.  \mneg{}(r  =  0)
10.  \mneg{}(r  =  1)
\mvdash{}  uiff(0  <  q-linear(k  -  1;j.x  j;y)  +  ((x  k)  *  y[k  -  1]);0  <  -(y[k  -  1])
                                                                                                                +  ((-1/x  k)  *  q-linear(k  -  1;j.x  j;y)))


By

---

Latex:
Auto

---

Home Index