---

Step * of Lemma q-constraint-times

∀[x:ℕ ⟶ ℚ]. ∀[r:ℤ]. ∀[a:ℚ]. ∀[k:ℕ]. ∀[y:ℚ List].
  (q-rel(r;q-linear(k;j.a * (x j);y))) supposing 
     (q-rel(r;q-linear(k;j.x j;y)) and 
     ((r = 0 ∈ ℤ) ∨ 0 < a ∨ ((0 ≤ a) ∧ (r = 1 ∈ ℤ))) and 
     (k ≤ ||y||))
BY
{ xxx(Auto
      THEN (RWO "q-linear-times" 0 THENA Auto)
      THEN SplitOrHyps
      THEN Auto
      THEN (MoveToConcl (-1))
      THEN Try (HypSubst' -1 0)
      THEN Unfold `q-rel` 0
      THEN Repeat ((SplitOnConclITE THENA Auto))
      THEN Auto
      THEN ThinVar `r'
      THEN Try (((QMul ⌜a⌝ (-1))⋅ THEN All QNorm THEN Complete (Auto))))xxx }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[r:\mBbbZ{}].  \mforall{}[a:\mBbbQ{}].  \mforall{}[k:\mBbbN{}].  \mforall{}[y:\mBbbQ{}  List].
    (q-rel(r;q-linear(k;j.a  *  (x  j);y)))  supposing 
          (q-rel(r;q-linear(k;j.x  j;y))  and 
          ((r  =  0)  \mvee{}  0  <  a  \mvee{}  ((0  \mleq{}  a)  \mwedge{}  (r  =  1)))  and 
          (k  \mleq{}  ||y||))


By

---

Latex:
xxx(Auto
        THEN  (RWO  "q-linear-times"  0  THENA  Auto)
        THEN  SplitOrHyps
        THEN  Auto
        THEN  (MoveToConcl  (-1))
        THEN  Try  (HypSubst'  -1  0)
        THEN  Unfold  `q-rel`  0
        THEN  Repeat  ((SplitOnConclITE  THENA  Auto))
        THEN  Auto
        THEN  ThinVar  `r'
        THEN  Try  (((QMul  \mkleeneopen{}a\mkleeneclose{}  (-1))\mcdot{}  THEN  All  QNorm  THEN  Complete  (Auto))))xxx

---

Home Index