---

Step * 1 1 1 of Lemma decidable__q-constraints

.....decidable?..... 
1. k : ℕ
2. ∀k1:ℕk. ∀A:(ℕ ⟶ ℚ × ℤ) List.  Dec(∃y:ℚ List [q-constraints(k1;A;y)])
3. k = 0 ∈ ℤ
4. A : (ℕ ⟶ ℚ × ℤ) List
⊢ Dec(∃y:ℚ List [((||y|| = 0 ∈ ℤ) c∧ (∀xr∈A.q-rel(snd(xr);(fst(xr)) 0)))])
BY
{ (Assert ⌜Dec((∀xr∈A.q-rel(snd(xr);(fst(xr)) 0)))⌝⋅ THENA Auto) }

1
1. k : ℕ
2. ∀k1:ℕk. ∀A:(ℕ ⟶ ℚ × ℤ) List.  Dec(∃y:ℚ List [q-constraints(k1;A;y)])
3. k = 0 ∈ ℤ
4. A : (ℕ ⟶ ℚ × ℤ) List
5. Dec((∀xr∈A.q-rel(snd(xr);(fst(xr)) 0)))
⊢ Dec(∃y:ℚ List [((||y|| = 0 ∈ ℤ) c∧ (∀xr∈A.q-rel(snd(xr);(fst(xr)) 0)))])

---

Latex:

---

Latex:
.....decidable?..... 
1.  k  :  \mBbbN{}
2.  \mforall{}k1:\mBbbN{}k.  \mforall{}A:(\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List.    Dec(\mexists{}y:\mBbbQ{}  List  [q-constraints(k1;A;y)])
3.  k  =  0
4.  A  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List
\mvdash{}  Dec(\mexists{}y:\mBbbQ{}  List  [((||y||  =  0)  c\mwedge{}  (\mforall{}xr\mmember{}A.q-rel(snd(xr);(fst(xr))  0)))])


By

---

Latex:
(Assert  \mkleeneopen{}Dec((\mforall{}xr\mmember{}A.q-rel(snd(xr);(fst(xr))  0)))\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index