---

Step * 1 of Lemma bm_compare_int_wf


Trans(ℤ;x,y.0 ≤ if x <z y then -1
            if (x =z y) then 0
            else 1
            fi )
BY
{ (Unfold `trans` 0 THEN RepeatFor 3 ((D 0 THENA Auto)) THEN RepeatFor 5 (AutoSplit)) }

---

Latex:



Trans(\mBbbZ{};x,y.0  \mleq{}  if  x  <z  y  then  -1
                        if  (x  =\msubz{}  y)  then  0
                        else  1
                        fi  )


By

(Unfold  `trans`  0  THEN  RepeatFor  3  ((D  0  THENA  Auto))  THEN  RepeatFor  5  (AutoSplit))

---

Home Index