---

Step * 1 1 2 of Lemma decidable__q-constraints2

.....set predicate..... 
1. k : ℕ
2. A : (ℚ List × ℤ × (ℚ List)) List
3. y : ℚ List
4. (||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 )
⊢ q-constraints(k;map(λa.let F,r,G = a in 
                         <λj.(G[j]?0 - F[j]?0), r>;A);y)
BY
{ (D -1
   THEN D 0
   THEN Auto
   THEN (D 0 THENA (RWO "length-map" 0 THEN Auto))
   THEN (RWO "select-map" 0 THENA Auto)
   THEN (Reduce 0 THEN ∀h:hyp. (RWO "length-map" h THENA Auto)  THEN Auto)
   THEN (With ⌜i⌝ (D (-3))⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [1;1]
   THEN RepeatFor 2 (D (-2))
   THEN Reduce 0) }

1
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))

---

Latex:

---

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


By

---

Latex:
(D  -1
  THEN  D  0
  THEN  Auto
  THEN  (D  0  THENA  (RWO  "length-map"  0  THEN  Auto))
  THEN  (RWO  "select-map"  0  THENA  Auto)
  THEN  (Reduce  0  THEN  \mforall{}h:hyp.  (RWO  "length-map"  h  THENA  Auto)    THEN  Auto)
  THEN  (With  \mkleeneopen{}i\mkleeneclose{}  (D  (-3))\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [1;1]
  THEN  RepeatFor  2  (D  (-2))
  THEN  Reduce  0)

---

Home Index