---

Step * 3 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 )
2. AntiSym(ℤ;x,y.0 ≤ if x <z y then -1
                 if (x =z y) then 0
                 else 1
                 fi )
⊢ Connex(ℤ;x,y.0 ≤ if x <z y then -1
               if (x =z y) then 0
               else 1
               fi )
BY
{ (Unfold `connex` 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  )
2.  AntiSym(\mBbbZ{};x,y.0  \mleq{}  if  x  <z  y  then  -1
                                  if  (x  =\msubz{}  y)  then  0
                                  else  1
                                  fi  )
\mvdash{}  Connex(\mBbbZ{};x,y.0  \mleq{}  if  x  <z  y  then  -1
                              if  (x  =\msubz{}  y)  then  0
                              else  1
                              fi  )


By

(Unfold  `connex`  0  THEN  RepeatFor  2  ((D  0  THENA  Auto))  THEN  RepeatFor  3  (AutoSplit))

---

Home Index