---

Step * 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. 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)))])
BY
{ Repeat ParallelLast⋅ }

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

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

---

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


By

---

Latex:
Repeat  ParallelLast\mcdot{}

---

Home Index