---

Step * 1 1 of Lemma decidable__q-constraints2


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 ))])
BY
{ (RepeatFor 2 ((Thin (-2))) THEN RepeatFor 3 (ParallelLast) THEN Try (ParallelLast)) }

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

2
.....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)

---

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)])
4.  \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{})
5.  Dec(\mexists{}y:\mBbbQ{}  List  [q-constraints(k;map(\mlambda{}a.let  F,r,G  =  a  in 
                                                                                  <\mlambda{}j.(G[j]?0  -  F[j]?0),  r>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:
(RepeatFor  2  ((Thin  (-2)))  THEN  RepeatFor  3  (ParallelLast)  THEN  Try  (ParallelLast))

---

Home Index