---

Step * of Lemma q-constraint-negative

No Annotations
∀[x:ℕ ⟶ ℚ]. ∀[r:ℤ]. ∀[k:ℕ+]. ∀[y:ℚ List].
  (uiff(q-rel(r;q-linear(k;j.x j;y));q-rel(r;-(y[k - 1]) + ((-1/x k) * q-linear(k - 1;j.x j;y))))) supposing 
     (x k < 0 and 
     (k ≤ ||y||))
BY
{ (RepeatFor 6 ((D 0 THENA Auto))
   THEN (Assert ¬((x k) = 0 ∈ ℚ) BY
               (RelRST THEN Auto))
   THEN (Assert 0 < -(x k) BY
               (QMul ⌜-1⌝ 0⋅ THEN Auto))
   THEN ((RW (AddrC [1; 2] (LemmaC `q-linear-unroll`)) 0) THENA Auto)
   THEN Unfold `q-rel` 0
   THEN Repeat ((SplitOnConclITE THENA Auto))) }

1
.....truecase..... 
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 ∈ ℤ
⊢ 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)))
∈ ℚ)

2
.....truecase..... 
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))))

3
.....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)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x:\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[r:\mBbbZ{}].  \mforall{}[k:\mBbbN{}\msupplus{}].  \mforall{}[y:\mBbbQ{}  List].
    (uiff(q-rel(r;q-linear(k;j.x  j;y));q-rel(r;-(y[k  -  1])
          +  ((-1/x  k)  *  q-linear(k  -  1;j.x  j;y)))))  supposing 
          (x  k  <  0  and 
          (k  \mleq{}  ||y||))


By

---

Latex:
(RepeatFor  6  ((D  0  THENA  Auto))
  THEN  (Assert  \mneg{}((x  k)  =  0)  BY
                          (RelRST  THEN  Auto))
  THEN  (Assert  0  <  -(x  k)  BY
                          (QMul  \mkleeneopen{}-1\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  ((RW  (AddrC  [1;  2]  (LemmaC  `q-linear-unroll`))  0)  THENA  Auto)
  THEN  Unfold  `q-rel`  0
  THEN  Repeat  ((SplitOnConclITE  THENA  Auto)))

---

Home Index