---

Step * of Lemma decidable__q-constraints

No Annotations
∀k:ℕ. ∀A:(ℕ ⟶ ℚ × ℤ) List.  Dec(∃y:ℚ List [q-constraints(k;A;y)])
BY
{ ((GeneralInductionOnNat THENA Auto)
   THEN (cbvaAllIntro THENA (Auto THEN D 0 THEN With ⌜0⌝ (D 0)⋅ THEN Auto))
   THEN MoveToConcl (-1)) }

1
1. k : ℕ
2. ∀k1:ℕk. ∀A:(ℕ ⟶ ℚ × ℤ) List.  Dec(∃y:ℚ List [q-constraints(k1;A;y)])
⊢ ∀A:(ℕ ⟶ ℚ × ℤ) List. Dec(∃y:ℚ List [q-constraints(k;A;y)])

---

Latex:

---

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


By

---

Latex:
((GeneralInductionOnNat  THENA  Auto)
  THEN  (cbvaAllIntro  THENA  (Auto  THEN  D  0  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  THEN  MoveToConcl  (-1))

---

Home Index