---

Step * 2 of Lemma q-constraint-positive


1. x : ℕ ⟶ ℚ
2. r : ℤ
3. k : ℕ+
4. y : ℚ List
5. k ≤ ||y||
6. 0 < x k
7. ¬((x k) = 0 ∈ ℚ)
8. q-rel(r;y[k - 1] + ((1/x k) * q-linear(k - 1;j.x j;y)))
⊢ q-rel(r;q-linear(k - 1;j.x j;y) + ((x k) * y[k - 1]))
BY
{ ((MoveToConcl (-1))
   THEN Unfold `q-rel` 0
   THEN Repeat ((SplitOnConclITE THENA Auto))
   THEN Auto
   THEN (QMul ⌜x k⌝ (-1))⋅
   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.  0  <  x  k
7.  \mneg{}((x  k)  =  0)
8.  q-rel(r;y[k  -  1]  +  ((1/x  k)  *  q-linear(k  -  1;j.x  j;y)))
\mvdash{}  q-rel(r;q-linear(k  -  1;j.x  j;y)  +  ((x  k)  *  y[k  -  1]))


By

---

Latex:
((MoveToConcl  (-1))
  THEN  Unfold  `q-rel`  0
  THEN  Repeat  ((SplitOnConclITE  THENA  Auto))
  THEN  Auto
  THEN  (QMul  \mkleeneopen{}x  k\mkleeneclose{}  (-1))\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index