---

Step * 5 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 )
4. Refl(ℤ;x,y.if x <z y then -1 if (x =z y) then 0 else 1 fi  = 0 ∈ ℤ)
⊢ Sym(ℤ;x,y.if x <z y then -1 if (x =z y) then 0 else 1 fi  = 0 ∈ ℤ)
BY
{ (Unfold `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  )
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  )
4.  Refl(\mBbbZ{};x,y.if  x  <z  y  then  -1  if  (x  =\msubz{}  y)  then  0  else  1  fi    =  0)
\mvdash{}  Sym(\mBbbZ{};x,y.if  x  <z  y  then  -1  if  (x  =\msubz{}  y)  then  0  else  1  fi    =  0)


By

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

---

Home Index