---

Step * 4 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 )
3. Connex(ℤ;x,y.0 ≤ if x <z y then -1
                if (x =z y) then 0
                else 1
                fi )
⊢ Refl(ℤ;x,y.if x <z y then -1 if (x =z y) then 0 else 1 fi  = 0 ∈ ℤ)
BY
{ (Unfold `refl` 0 THEN (D 0 THENA Auto) THEN 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  )
3.  Connex(\mBbbZ{};x,y.0  \mleq{}  if  x  <z  y  then  -1
                                if  (x  =\msubz{}  y)  then  0
                                else  1
                                fi  )
\mvdash{}  Refl(\mBbbZ{};x,y.if  x  <z  y  then  -1  if  (x  =\msubz{}  y)  then  0  else  1  fi    =  0)


By

(Unfold  `refl`  0  THEN  (D  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index