---

Step * of Lemma q-constraint-sum

∀[x,x':ℕ ⟶ ℚ]. ∀[r1,r2:ℤ]. ∀[k:ℕ]. ∀[y:ℚ List].
  (q-rel(q-rel-lub(r1;r2);q-linear(k;j.(x j) + (x' j);y))) supposing 
     (q-rel(r2;q-linear(k;j.x' j;y)) and 
     q-rel(r1;q-linear(k;j.x j;y)) and 
     (k ≤ ||y||))
BY
{ TACTIC:(Auto THEN RWO "q-linear-sum" 0 THEN Auto) }

1
1. x : ℕ ⟶ ℚ
2. x' : ℕ ⟶ ℚ
3. r1 : ℤ
4. r2 : ℤ
5. k : ℕ
6. y : ℚ List
7. k ≤ ||y||
8. q-rel(r1;q-linear(k;j.x j;y))
9. q-rel(r2;q-linear(k;j.x' j;y))
⊢ q-rel(q-rel-lub(r1;r2);q-linear(k;j.x j;y) + q-linear(k;j.x' j;y))

---

Latex:

---

Latex:
\mforall{}[x,x':\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[r1,r2:\mBbbZ{}].  \mforall{}[k:\mBbbN{}].  \mforall{}[y:\mBbbQ{}  List].
    (q-rel(q-rel-lub(r1;r2);q-linear(k;j.(x  j)  +  (x'  j);y)))  supposing 
          (q-rel(r2;q-linear(k;j.x'  j;y))  and 
          q-rel(r1;q-linear(k;j.x  j;y))  and 
          (k  \mleq{}  ||y||))


By

---

Latex:
TACTIC:(Auto  THEN  RWO  "q-linear-sum"  0  THEN  Auto)

---

Home Index