---

Step * of Lemma q-constraint-zero

∀[x:ℕ ⟶ ℚ]. ∀[r:ℤ]. ∀[k:ℕ+]. ∀[y:ℚ List].
  (uiff(q-rel(r;q-linear(k;j.x j;y));q-rel(r;q-linear(k - 1;j.x j;y)))) supposing (((x k) = 0 ∈ ℚ) and (k ≤ ||y||))
BY
{ TACTIC:((UnivCD THENA Auto)
          THEN ((RW(AddrC [1;2] (LemmaC `q-linear-unroll`)) 0) THENA Auto)
          THEN (HypSubst' -1 0 THENA Auto)
          THEN QNorm 0
          THEN Auto) }

---

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;q-linear(k  -  1;j.x  j;y))))  supposing 
          (((x  k)  =  0)  and 
          (k  \mleq{}  ||y||))


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)
                THEN  ((RW(AddrC  [1;2]  (LemmaC  `q-linear-unroll`))  0)  THENA  Auto)
                THEN  (HypSubst'  -1  0  THENA  Auto)
                THEN  QNorm  0
                THEN  Auto)

---

Home Index