---

Step * of Lemma bm_compare_connex_le

∀[K:Type]. ∀compare:bm_compare(K). ∀k1,k2:K.  ((0 ≤ (compare k1 k2)) ∨ (0 ≤ (compare k2 k1)))
BY
{ (Auto
   THEN (Decide ⌈0 ≤ (compare k1 k2)⌉⋅ THENA Auto)
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN (Decide ⌈0 ≤ (compare k2 k1)⌉⋅ THENA Auto)
   THEN Try (Complete ((OrRight THEN Auto)))
   THEN (Assert ⌈False⌉⋅ THEN Auto)
   THEN Unfold `bm_compare` 2
   THEN DVarSets
   THEN Assert ⌈(0 ≤ (compare k1 k2)) ∨ (0 ≤ (compare k2 k1))⌉⋅
   THEN Auto
   THEN D (-1)
   THEN Auto) }

1
1. K : Type
2. compare : K ─→ K ─→ ℤ@i
3. Trans(K;x,y.0 ≤ (compare x y))@i
4. AntiSym(K;x,y.0 ≤ (compare x y))@i
5. Connex(K;x,y.0 ≤ (compare x y))@i
6. Refl(K;x,y.(compare x y) = 0 ∈ ℤ)@i
7. Sym(K;x,y.(compare x y) = 0 ∈ ℤ)@i
8. k1 : K@i
9. k2 : K@i
10. ¬(0 ≤ (compare k1 k2))
⊢ 0 ≤ (compare k2 k1)

---

Latex:


\mforall{}[K:Type].  \mforall{}compare:bm\_compare(K).  \mforall{}k1,k2:K.    ((0  \mleq{}  (compare  k1  k2))  \mvee{}  (0  \mleq{}  (compare  k2  k1)))


By

(Auto
  THEN  (Decide  \mkleeneopen{}0  \mleq{}  (compare  k1  k2)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  (Decide  \mkleeneopen{}0  \mleq{}  (compare  k2  k1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (Complete  ((OrRight  THEN  Auto)))
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  Unfold  `bm\_compare`  2
  THEN  DVarSets
  THEN  Assert  \mkleeneopen{}(0  \mleq{}  (compare  k1  k2))  \mvee{}  (0  \mleq{}  (compare  k2  k1))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  D  (-1)
  THEN  Auto)

---

Home Index