---

Step * 1 of Lemma decidable__q-rel


1. r : ℤ@i
2. x : ℚ@i
⊢ Dec(q-rel(r;x))
BY
{ (UseWitness ⌜q-rel-decider(r;x)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  \mBbbZ{}@i
2.  x  :  \mBbbQ{}@i
\mvdash{}  Dec(q-rel(r;x))


By

---

Latex:
(UseWitness  \mkleeneopen{}q-rel-decider(r;x)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index