---

Step * 1 1 2 1 of Lemma decidable__q-constraints2


1. k : ℕ
2. A : (ℚ List × ℤ × (ℚ List)) List
3. y : ℚ List
4. ||y|| = k ∈ ℤ
5. ||y|| = k ∈ ℤ
6. i : ℕ||A||
7. v1 : ℚ List
8. v3 : ℤ
9. v4 : ℚ List
10. A[i] = <v1, v3, v4> ∈ (ℚ List × ℤ × (ℚ List))
⊢ if (v3 =z 0) then q-linear(k;j.v1[j]?0;y) = q-linear(k;j.v4[j]?0;y) ∈ ℚ
if (v3 =z 1) then q-linear(k;j.v1[j]?0;y) ≤ q-linear(k;j.v4[j]?0;y)
else q-linear(k;j.v1[j]?0;y) < q-linear(k;j.v4[j]?0;y)
fi 
⇒ q-rel(v3;q-linear(k;j.v4[j]?0 - v1[j]?0;y))
BY
{ (Subst' q-linear(k;j.v4[j]?0 - v1[j]?0;y) = (q-linear(k;j.v4[j]?0;y) - q-linear(k;j.v1[j]?0;y)) ∈ ℚ 0 THENA Auto)⋅ }

1
.....equality..... 
1. k : ℕ
2. A : (ℚ List × ℤ × (ℚ List)) List
3. y : ℚ List
4. ||y|| = k ∈ ℤ
5. ||y|| = k ∈ ℤ
6. i : ℕ||A||
7. v1 : ℚ List
8. v3 : ℤ
9. v4 : ℚ List
10. A[i] = <v1, v3, v4> ∈ (ℚ List × ℤ × (ℚ List))
⊢ q-linear(k;j.v4[j]?0 - v1[j]?0;y) = (q-linear(k;j.v4[j]?0;y) - q-linear(k;j.v1[j]?0;y)) ∈ ℚ

2
1. k : ℕ
2. A : (ℚ List × ℤ × (ℚ List)) List
3. y : ℚ List
4. ||y|| = k ∈ ℤ
5. ||y|| = k ∈ ℤ
6. i : ℕ||A||
7. v1 : ℚ List
8. v3 : ℤ
9. v4 : ℚ List
10. A[i] = <v1, v3, v4> ∈ (ℚ List × ℤ × (ℚ List))
⊢ if (v3 =z 0) then q-linear(k;j.v1[j]?0;y) = q-linear(k;j.v4[j]?0;y) ∈ ℚ
if (v3 =z 1) then q-linear(k;j.v1[j]?0;y) ≤ q-linear(k;j.v4[j]?0;y)
else q-linear(k;j.v1[j]?0;y) < q-linear(k;j.v4[j]?0;y)
fi 
⇒ q-rel(v3;q-linear(k;j.v4[j]?0;y) - q-linear(k;j.v1[j]?0;y))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  A  :  (\mBbbQ{}  List  \mtimes{}  \mBbbZ{}  \mtimes{}  (\mBbbQ{}  List))  List
3.  y  :  \mBbbQ{}  List
4.  ||y||  =  k
5.  ||y||  =  k
6.  i  :  \mBbbN{}||A||
7.  v1  :  \mBbbQ{}  List
8.  v3  :  \mBbbZ{}
9.  v4  :  \mBbbQ{}  List
10.  A[i]  =  <v1,  v3,  v4>
\mvdash{}  if  (v3  =\msubz{}  0)  then  q-linear(k;j.v1[j]?0;y)  =  q-linear(k;j.v4[j]?0;y)
if  (v3  =\msubz{}  1)  then  q-linear(k;j.v1[j]?0;y)  \mleq{}  q-linear(k;j.v4[j]?0;y)
else  q-linear(k;j.v1[j]?0;y)  <  q-linear(k;j.v4[j]?0;y)
fi 
{}\mRightarrow{}  q-rel(v3;q-linear(k;j.v4[j]?0  -  v1[j]?0;y))


By

---

Latex:
(Subst'  q-linear(k;j.v4[j]?0  -  v1[j]?0;y)  =  (q-linear(k;j.v4[j]?0;y)  -  q-linear(k;j.v1[j]?0;y))  0
  THENA  Auto
  )\mcdot{}

---

Home Index