---

Step * of Lemma q-constraint-positive

∀[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 
     (0 < x k and 
     (k ≤ ||y||))
BY
{ (RepeatFor 6 (((D 0 THENA Auto) THEN Try (((Assert ¬((x k) = 0 ∈ ℚ) BY (RelRST THEN Auto)) THEN Trivial))))
   THEN (Assert ¬((x k) = 0 ∈ ℚ) BY
               (RelRST THEN Auto))
   THEN (RW (AddrC [1; 2] (LemmaC `q-linear-unroll`)) 0)
   THEN Auto) }

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

---

Latex:

---

Latex:
\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 
          (0  <  x  k  and 
          (k  \mleq{}  ||y||))


By

---

Latex:
(RepeatFor  6  (((D  0  THENA  Auto)
                              THEN  Try  (((Assert  \mneg{}((x  k)  =  0)  BY  (RelRST  THEN  Auto))  THEN  Trivial))
                              ))
  THEN  (Assert  \mneg{}((x  k)  =  0)  BY
                          (RelRST  THEN  Auto))
  THEN  (RW  (AddrC  [1;  2]  (LemmaC  `q-linear-unroll`))  0)
  THEN  Auto)

---

Home Index