---

Step * 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 ∈ ℤ
⊢ ∀A:(ℕ ⟶ ℚ × ℤ) List. Dec(∃y:ℚ List [q-constraints(0;A;y)])
BY
{ (RepUR ``q-constraints`` 0 THEN RWO "q-linear-base" 0 THEN Auto) }

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

---

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
\mvdash{}  \mforall{}A:(\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List.  Dec(\mexists{}y:\mBbbQ{}  List  [q-constraints(0;A;y)])


By

---

Latex:
(RepUR  ``q-constraints``  0  THEN  RWO  "q-linear-base"  0  THEN  Auto)

---

Home Index