---

Step * of Lemma bm_compare_int_wf

bm_compare_int() ∈ bm_compare(ℤ)
BY
{ (RepUR ``bm_compare_int bm_compare`` 0 THEN MemTypeCD THEN Reduce 0 THEN Auto) }

1
Trans(ℤ;x,y.0 ≤ if x <z y then -1
            if (x =z y) then 0
            else 1
            fi )

2
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 )

3
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 )

4
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 ∈ ℤ)

5
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 ∈ ℤ)

---

Latex:


bm\_compare\_int()  \mmember{}  bm\_compare(\mBbbZ{})


By

(RepUR  ``bm\_compare\_int  bm\_compare``  0  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index