---

Step * 3 2 of Lemma q-constraint-negative


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])
BY
{ (QMul ⌜-(x k)⌝ (-1)⋅ THEN Auto THEN Try ((ParallelOp -4 THEN RelRST ⋅ THEN Auto))) }

---

Latex:

---

Latex:

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)
11.  0  <  -(y[k  -  1])  +  ((-1/x  k)  *  q-linear(k  -  1;j.x  j;y))
\mvdash{}  0  <  q-linear(k  -  1;j.x  j;y)  +  ((x  k)  *  y[k  -  1])


By

---

Latex:
(QMul  \mkleeneopen{}-(x  k)\mkleeneclose{}  (-1)\mcdot{}  THEN  Auto  THEN  Try  ((ParallelOp  -4  THEN  RelRST  \mcdot{}  THEN  Auto)))

---

Home Index