---

Step * 1 of Lemma q-constraint-sum


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))
BY
{ (RepeatFor 2 ((MoveToConcl (-1)))
   THEN Unfolds ``q-rel q-rel-lub`` 0
   THEN Repeat (((SplitOnConclITE THENA Auto) THEN All Reduce))
   THEN Auto
   THEN (QAdd q-linear(k;j.x j;y) (-1))⋅
   THEN Try ((RelRST THEN Auto))) }

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbQ{}
2.  x'  :  \mBbbN{}  {}\mrightarrow{}  \mBbbQ{}
3.  r1  :  \mBbbZ{}
4.  r2  :  \mBbbZ{}
5.  k  :  \mBbbN{}
6.  y  :  \mBbbQ{}  List
7.  k  \mleq{}  ||y||
8.  q-rel(r1;q-linear(k;j.x  j;y))
9.  q-rel(r2;q-linear(k;j.x'  j;y))
\mvdash{}  q-rel(q-rel-lub(r1;r2);q-linear(k;j.x  j;y)  +  q-linear(k;j.x'  j;y))


By

---

Latex:
(RepeatFor  2  ((MoveToConcl  (-1)))
  THEN  Unfolds  ``q-rel  q-rel-lub``  0
  THEN  Repeat  (((SplitOnConclITE  THENA  Auto)  THEN  All  Reduce))
  THEN  Auto
  THEN  (QAdd  q-linear(k;j.x  j;y)  (-1))\mcdot{}
  THEN  Try  ((RelRST  THEN  Auto)))

---

Home Index