---

Step * 1 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. 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.  r  =  0
10.  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