---

Step * 1 1 1 of Lemma decidable__q-constraints2

.....set predicate..... 
1. k : ℕ
2. A : (ℚ List × ℤ × (ℚ List)) List
3. y : ℚ List
4. q-constraints(k;map(λa.let F,r,G = a in 
                          <λj.(G[j]?0 - F[j]?0), r>;A);y)
⊢ (||y|| = k ∈ ℤ)
c∧ (∀a∈A.let F,r,G = a 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
{ (D -1 THEN Auto THEN Thin (-1) THEN ParallelLast) }

1
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 

---

Latex:

---

Latex:
.....set  predicate..... 
1.  k  :  \mBbbN{}
2.  A  :  (\mBbbQ{}  List  \mtimes{}  \mBbbZ{}  \mtimes{}  (\mBbbQ{}  List))  List
3.  y  :  \mBbbQ{}  List
4.  q-constraints(k;map(\mlambda{}a.let  F,r,G  =  a  in 
                                                    <\mlambda{}j.(G[j]?0  -  F[j]?0),  r>A);y)
\mvdash{}  (||y||  =  k)
c\mwedge{}  (\mforall{}a\mmember{}A.let  F,r,G  =  a  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:
(D  -1  THEN  Auto  THEN  Thin  (-1)  THEN  ParallelLast)

---

Home Index