---

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


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

---

Latex:

---

Latex:

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
5.  (\mforall{}xr\mmember{}A.q-rel(snd(xr);(fst(xr))  0))
\mvdash{}  \mexists{}y:\mBbbQ{}  List  [((||y||  =  0)  c\mwedge{}  (\mforall{}xr\mmember{}A.q-rel(snd(xr);(fst(xr))  0)))]


By

---

Latex:
(InstConcl  [\mkleeneopen{}[]\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index