---

Step * 1 of Lemma decidable__q-constraints2


1. k : ℕ
2. A : (ℚ List × ℤ × (ℚ List)) List
3. ∀A:(ℕ ⟶ ℚ × ℤ) List. Dec(∃y:ℚ List [q-constraints(k;A;y)])
⊢ Dec(∃y:ℚ List [((||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
{ ((Assert λa.let F,r,G = a in 
              <λj.(G[j]?0 - F[j]?0), r> ∈ (ℚ List × ℤ × (ℚ List)) ⟶ (ℕ ⟶ ℚ × ℤ) BY
          (Auto THEN D -1 THEN D -1 THEN Reduce 0 THEN Auto))
   THEN ((InstHyp [⌜normalize-constraints(k;map(λa.let F,r,G = a in <λj.(G[j]?0 - F[j]?0), r>;A))⌝ ] (-2))⋅ THENA Auto)
   THEN (RWO "normalize-constraints-eq" (-1) THENA Auto)) }

1
1. k : ℕ
2. A : (ℚ List × ℤ × (ℚ List)) List
3. ∀A:(ℕ ⟶ ℚ × ℤ) List. Dec(∃y:ℚ List [q-constraints(k;A;y)])
4. λa.let F,r,G = a in 
      <λj.(G[j]?0 - F[j]?0), r> ∈ (ℚ List × ℤ × (ℚ List)) ⟶ (ℕ ⟶ ℚ × ℤ)
5. Dec(∃y:ℚ List [q-constraints(k;map(λa.let F,r,G = a in 
                                         <λj.(G[j]?0 - F[j]?0), r>;A);y)])
⊢ Dec(∃y:ℚ List [((||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 ))])

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  A  :  (\mBbbQ{}  List  \mtimes{}  \mBbbZ{}  \mtimes{}  (\mBbbQ{}  List))  List
3.  \mforall{}A:(\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List.  Dec(\mexists{}y:\mBbbQ{}  List  [q-constraints(k;A;y)])
\mvdash{}  Dec(\mexists{}y:\mBbbQ{}  List  [((||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:
((Assert  \mlambda{}a.let  F,r,G  =  a  in 
                        <\mlambda{}j.(G[j]?0  -  F[j]?0),  r>  \mmember{}  (\mBbbQ{}  List  \mtimes{}  \mBbbZ{}  \mtimes{}  (\mBbbQ{}  List))  {}\mrightarrow{}  (\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  BY
                (Auto  THEN  D  -1  THEN  D  -1  THEN  Reduce  0  THEN  Auto))
  THEN  ((InstHyp  [\mkleeneopen{}normalize-constraints(k;map(\mlambda{}a.let  F,r,G  =  a  in  <\mlambda{}j.(G[j]?0  -  F[j]?0),  r>A))\mkleeneclose{}  ]  (\000C-2))\mcdot{}  THENA  Auto)
  THEN  (RWO  "normalize-constraints-eq"  (-1)  THENA  Auto))

---

Home Index