---

Step * of Lemma decidable__less_than'

∀i,j:ℤ.  Dec(less_than'(i;j))
BY
{ TACTIC:(Auto
          THEN UseWitness ⌜if (i) < (j)  then inl Ax  else (inr (λx.Ax) )⌝⋅
          THEN RepUR ``decidable or less_than\' not`` 0
          THEN Refine_lessCases `x' ⌜i⌝ ⌜j⌝ `u' `v'⋅
          THEN Try (Declaration)
          THEN RWO "-1" 0
          THEN Auto) }

---

Latex:

---

Latex:
\mforall{}i,j:\mBbbZ{}.    Dec(less\_than'(i;j))


By

---

Latex:
TACTIC:(Auto
                THEN  UseWitness  \mkleeneopen{}if  (i)  <  (j)    then  inl  Ax    else  (inr  (\mlambda{}x.Ax)  )\mkleeneclose{}\mcdot{}
                THEN  RepUR  ``decidable  or  less\_than\mbackslash{}'  not``  0
                THEN  Refine\_lessCases  `x'  \mkleeneopen{}i\mkleeneclose{}  \mkleeneopen{}j\mkleeneclose{}  `u'  `v'\mcdot{}
                THEN  Try  (Declaration)
                THEN  RWO  "-1"  0
                THEN  Auto)

---

Home Index