---

Step * 1 1 1 1 of Lemma decidable__q-constraints2


1. k : ℕ
2. A : (ℚ List × ℤ × (ℚ List)) List
3. y : ℚ List
4. ||y|| = k ∈ ℤ
5. ∀i:ℕ||map(λa.let F,r,G = a in 
                <λj.(G[j]?0 - F[j]?0), r>;A)||
     q-rel(snd(map(λa.let F,r,G = a in 
                      <λj.(G[j]?0 - F[j]?0), r>;A)[i]);q-linear(k;j.(fst(map(λa.let F,r,G = a in 
                                                                                <λj.(G[j]?0 - F[j]?0), r>;A)[i])) 
                                                                    j;y))
⊢ ∀i:ℕ||A||
    let F,r,G = A[i] in 
    if (r =z 0) then q-linear(k;j.F[j]?0;y) = q-linear(k;j.G[j]?0;y) ∈ ℚ
    if (r =z 1) then q-linear(k;j.F[j]?0;y) ≤ q-linear(k;j.G[j]?0;y)
    else q-linear(k;j.F[j]?0;y) < q-linear(k;j.G[j]?0;y)
    fi 
BY
{ xxx((RWO "length-map" (-1) THENA Auto)
      THEN ParallelLast
      THEN RepUR ``q-rel`` (-1)
      THEN (RWO "select-map" (-1) THENA Auto)
      THEN Reduce (-1)
      THEN MoveToConcl (-1)
      THEN GenConclAtAddr [2;1]
      THEN RepeatFor 2 (D (-2))
      THEN Reduce 0)xxx }

1
1. k : ℕ
2. A : (ℚ List × ℤ × (ℚ List)) List
3. y : ℚ List
4. ||y|| = k ∈ ℤ
5. ∀i:ℕ||A||
     q-rel(snd(map(λa.let F,r,G = a in 
                      <λj.(G[j]?0 - F[j]?0), r>;A)[i]);q-linear(k;j.(fst(map(λa.let F,r,G = a in 
                                                                                <λj.(G[j]?0 - F[j]?0), r>;A)[i])) 
                                                                    j;y))
6. i : ℕ||A||
7. v1 : ℚ List
8. v3 : ℤ
9. v4 : ℚ List
10. A[i] = <v1, v3, v4> ∈ (ℚ List × ℤ × (ℚ List))
⊢ if (v3 =z 0) then 0 = q-linear(k;j.v4[j]?0 - v1[j]?0;y) ∈ ℚ
if (v3 =z 1) then 0 ≤ q-linear(k;j.v4[j]?0 - v1[j]?0;y)
else 0 < q-linear(k;j.v4[j]?0 - v1[j]?0;y)
fi 
⇒ 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 

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  A  :  (\mBbbQ{}  List  \mtimes{}  \mBbbZ{}  \mtimes{}  (\mBbbQ{}  List))  List
3.  y  :  \mBbbQ{}  List
4.  ||y||  =  k
5.  \mforall{}i:\mBbbN{}||map(\mlambda{}a.let  F,r,G  =  a  in 
                                <\mlambda{}j.(G[j]?0  -  F[j]?0),  r>A)||
          q-rel(snd(map(\mlambda{}a.let  F,r,G  =  a  in 
                                            <\mlambda{}j.(G[j]?0  -  F[j]?0),  r>A)[i]);q-linear(k;j.(fst(map(\mlambda{}a.let  F,r,G  =  a  in 
                                                                                                                                                                <\mlambda{}j.(G[j]?0 
                                                                                                                                                                        -  F[j]?0)
                                                                                                                                                                ,  r
                                                                                                                                                                >A)[i])) 
                                                                                                                                        j;y))
\mvdash{}  \mforall{}i:\mBbbN{}||A||
        let  F,r,G  =  A[i]  in 
        if  (r  =\msubz{}  0)  then  q-linear(k;j.F[j]?0;y)  =  q-linear(k;j.G[j]?0;y)
        if  (r  =\msubz{}  1)  then  q-linear(k;j.F[j]?0;y)  \mleq{}  q-linear(k;j.G[j]?0;y)
        else  q-linear(k;j.F[j]?0;y)  <  q-linear(k;j.G[j]?0;y)
        fi 


By

---

Latex:
xxx((RWO  "length-map"  (-1)  THENA  Auto)
        THEN  ParallelLast
        THEN  RepUR  ``q-rel``  (-1)
        THEN  (RWO  "select-map"  (-1)  THENA  Auto)
        THEN  Reduce  (-1)
        THEN  MoveToConcl  (-1)
        THEN  GenConclAtAddr  [2;1]
        THEN  RepeatFor  2  (D  (-2))
        THEN  Reduce  0)xxx

---

Home Index