---

Step * of Lemma decidable__q-constraints-squash

∀k:ℕ. ∀A:(ℕ ⟶ ℚ × ℤ) List.  Dec(∃y:{ℚ List| q-constraints(k;A;y)})
BY
{ (InstLemma `decidable__q-constraints` [] THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}A:(\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}  \mtimes{}  \mBbbZ{})  List.    Dec(\mexists{}y:\{\mBbbQ{}  List|  q-constraints(k;A;y)\})


By

---

Latex:
(InstLemma  `decidable\_\_q-constraints`  []  THEN  Trivial)

---

Home Index