---

Step * 2 of Lemma bm_compare_int_wf


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

---

Latex:



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


By

(Unfold  `anti\_sym`  0  THEN  RepeatFor  2  ((D  0  THENA  Auto))  THEN  RepeatFor  3  (AutoSplit))

---

Home Index