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