---

Step * of Lemma q-rel-decider_wf

∀r:ℤ. ∀x:ℚ.  (q-rel-decider(r;x) ∈ Dec(q-rel(r;x)))
BY
{ (Auto
   THEN RepUR ``q-rel q-rel-decider`` 0
   THEN (BoolCase ⌜(r =z 0)⌝⋅ THENA Auto)
   THEN (BoolCase ⌜(r =z 1)⌝⋅ THENA Auto)
   THEN RepUR ``decidable or not implies it`` 0
   THEN Repeat (AutoSplit)
   THEN Auto
   THEN Try ((BLemma `qle_witness` ORELSE BLemma `qless_witness`))
   THEN Auto
   THEN Try ((FLemma `qless_complement_qorder` [4] THEN Auto THEN RelRST THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}r:\mBbbZ{}.  \mforall{}x:\mBbbQ{}.    (q-rel-decider(r;x)  \mmember{}  Dec(q-rel(r;x)))


By

---

Latex:
(Auto
  THEN  RepUR  ``q-rel  q-rel-decider``  0
  THEN  (BoolCase  \mkleeneopen{}(r  =\msubz{}  0)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (BoolCase  \mkleeneopen{}(r  =\msubz{}  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepUR  ``decidable  or  not  implies  it``  0
  THEN  Repeat  (AutoSplit)
  THEN  Auto
  THEN  Try  ((BLemma  `qle\_witness`  ORELSE  BLemma  `qless\_witness`))
  THEN  Auto
  THEN  Try  ((FLemma  `qless\_complement\_qorder`  [4]  THEN  Auto  THEN  RelRST  THEN  Auto)))

---

Home Index