---

Step * 1 2 1 1 1 1 2 1 of Lemma decidable__q-constraints


1. k : ℕ
2. 0 < k
3. ∀A:(ℕ ⟶ ℚ × ℤ) List. Dec(∃y:ℚ List [q-constraints(k - 1;A;y)])
4. A : (ℕ ⟶ ℚ × ℤ) List
5. ¬(∃xr:ℕ ⟶ ℚ × ℤ. ((xr ∈ A) ∧ ((snd(xr)) = 0 ∈ ℤ) ∧ (¬(((fst(xr)) k) = 0 ∈ ℚ))))
⊢ Dec(∃y:ℚ List [q-constraints(k;A;y)])
BY
{ Assert ⌜∃B:(ℕ ⟶ ℚ × ℤ) List
           ∀a:ℕ ⟶ ℚ × ℤ
             ((a ∈ B)
             ⇐⇒ ((a ∈ A) ∧ (((fst(a)) k) = 0 ∈ ℚ))
                 ∨ (∃b:ℕ ⟶ ℚ × ℤ
                     ((b ∈ A)
                     ∧ (∃c:ℕ ⟶ ℚ × ℤ
                         ((c ∈ A)
                         ∧ 0 < (fst(b)) k
                         ∧ (fst(c)) k < 0
                         ∧ (a
                           = <λj.((((fst(b)) k) * ((fst(c)) j)) - ((fst(c)) k) * ((fst(b)) j))
                             , q-rel-lub(snd(b);snd(c))
                             >
                           ∈ (ℕ ⟶ ℚ × ℤ)))))))⌝⋅ }

1
.....assertion..... 
1. k : ℕ
2. 0 < k
3. ∀A:(ℕ ⟶ ℚ × ℤ) List. Dec(∃y:ℚ List [q-constraints(k - 1;A;y)])
4. A : (ℕ ⟶ ℚ × ℤ) List
5. ¬(∃xr:ℕ ⟶ ℚ × ℤ. ((xr ∈ A) ∧ ((snd(xr)) = 0 ∈ ℤ) ∧ (¬(((fst(xr)) k) = 0 ∈ ℚ))))
⊢ ∃B:(ℕ ⟶ ℚ × ℤ) List
   ∀a:ℕ ⟶ ℚ × ℤ
     ((a ∈ B)
     ⇐⇒ ((a ∈ A) ∧ (((fst(a)) k) = 0 ∈ ℚ))
         ∨ (∃b:ℕ ⟶ ℚ × ℤ
             ((b ∈ A)
             ∧ (∃c:ℕ ⟶ ℚ × ℤ
                 ((c ∈ A)
                 ∧ 0 < (fst(b)) k
                 ∧ (fst(c)) k < 0
                 ∧ (a
                   = <λj.((((fst(b)) k) * ((fst(c)) j)) - ((fst(c)) k) * ((fst(b)) j)), q-rel-lub(snd(b);snd(c))>
                   ∈ (ℕ ⟶ ℚ × ℤ)))))))

2
1. k : ℕ
2. 0 < k
3. ∀A:(ℕ ⟶ ℚ × ℤ) List. Dec(∃y:ℚ List [q-constraints(k - 1;A;y)])
4. A : (ℕ ⟶ ℚ × ℤ) List
5. ¬(∃xr:ℕ ⟶ ℚ × ℤ. ((xr ∈ A) ∧ ((snd(xr)) = 0 ∈ ℤ) ∧ (¬(((fst(xr)) k) = 0 ∈ ℚ))))
6. ∃B:(ℕ ⟶ ℚ × ℤ) List
    ∀a:ℕ ⟶ ℚ × ℤ
      ((a ∈ B)
      ⇐⇒ ((a ∈ A) ∧ (((fst(a)) k) = 0 ∈ ℚ))
          ∨ (∃b:ℕ ⟶ ℚ × ℤ
              ((b ∈ A)
              ∧ (∃c:ℕ ⟶ ℚ × ℤ
                  ((c ∈ A)
                  ∧ 0 < (fst(b)) k
                  ∧ (fst(c)) k < 0
                  ∧ (a
                    = <λj.((((fst(b)) k) * ((fst(c)) j)) - ((fst(c)) k) * ((fst(b)) j)), q-rel-lub(snd(b);snd(c))>
                    ∈ (ℕ ⟶ ℚ × ℤ)))))))
⊢ Dec(∃y:ℚ List [q-constraints(k;A;y)])

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  0  <  k
3.  \mforall{}A:(\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List.  Dec(\mexists{}y:\mBbbQ{}  List  [q-constraints(k  -  1;A;y)])
4.  A  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List
5.  \mneg{}(\mexists{}xr:\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{}.  ((xr  \mmember{}  A)  \mwedge{}  ((snd(xr))  =  0)  \mwedge{}  (\mneg{}(((fst(xr))  k)  =  0))))
\mvdash{}  Dec(\mexists{}y:\mBbbQ{}  List  [q-constraints(k;A;y)])


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}B:(\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List
                  \mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{}
                      ((a  \mmember{}  B)
                      \mLeftarrow{}{}\mRightarrow{}  ((a  \mmember{}  A)  \mwedge{}  (((fst(a))  k)  =  0))
                              \mvee{}  (\mexists{}b:\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{}
                                      ((b  \mmember{}  A)
                                      \mwedge{}  (\mexists{}c:\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{}
                                              ((c  \mmember{}  A)
                                              \mwedge{}  0  <  (fst(b))  k
                                              \mwedge{}  (fst(c))  k  <  0
                                              \mwedge{}  (a
                                                  =  <\mlambda{}j.((((fst(b))  k)  *  ((fst(c))  j))  -  ((fst(c))  k)  *  ((fst(b))  j))
                                                      ,  q-rel-lub(snd(b);snd(c))
                                                      >))))))\mkleeneclose{}\mcdot{}

---

Home Index