Theory ternaryComparisons

⊢ invert_comparison GREATER = LESS ∧ invert_comparison LESS = GREATER ∧
  invert_comparison EQUAL = EQUAL

⊢ ∀n1 n2.
    num_compare n1 n2 =
    if n1 = n2 then EQUAL else if n1 < n2 then LESS else GREATER

⊢ (∀a. num2ordering (ordering2num a) = a) ∧
  ∀r. (λn. n < 3) r ⇔ ordering2num (num2ordering r) = r

⊢ ∀x v0 v1 v2.
    (case x of LESS => v0 | EQUAL => v1 | GREATER => v2) =
    (λm. if m < 1 then v0 else if m = 1 then v1 else v2) (ordering2num x)

⊢ ∃rep. TYPE_DEFINITION (λn. n < 3) rep

⊢ ∀x. ordering_size x = 0

⊢ ∀c1 c2 a b x y.
    pair_compare c1 c2 (a,b) (x,y) =
    case c1 a x of LESS => LESS | EQUAL => c2 b y | GREATER => GREATER

⊢ bool_compare T T = EQUAL ∧ bool_compare F F = EQUAL ∧
  bool_compare T F = GREATER ∧ bool_compare F T = LESS

⊢ ∀P. P T T ∧ P F F ∧ P T F ∧ P F T ⇒ ∀v v1. P v v1

⊢ (∀x y. cmp x y = EQUAL ⇔ x = y) ⇒
  ∀l1 l2. list_compare cmp l1 l2 = EQUAL ⇔ l1 = l2

⊢ DATATYPE (ordering LESS EQUAL GREATER)

⊢ ∀x. invert_comparison x = EQUAL ⇔ x = EQUAL

⊢ (∀cmp. list_compare cmp [] [] = EQUAL) ∧
  (∀v9 v8 cmp. list_compare cmp [] (v8::v9) = LESS) ∧
  (∀v5 v4 cmp. list_compare cmp (v4::v5) [] = GREATER) ∧
  ∀y x l2 l1 cmp.
    list_compare cmp (x::l1) (y::l2) =
    case cmp x y of
      LESS => LESS
    | EQUAL => list_compare cmp l1 l2
    | GREATER => GREATER

⊢ ∀P. (∀cmp. P cmp [] []) ∧ (∀cmp v8 v9. P cmp [] (v8::v9)) ∧
      (∀cmp v4 v5. P cmp (v4::v5) []) ∧
      (∀cmp x l1 y l2.
         (cmp x y = EQUAL ⇒ P cmp l1 l2) ⇒ P cmp (x::l1) (y::l2)) ⇒
      ∀v v1 v2. P v v1 v2

⊢ (∀l1 a_lt. list_merge a_lt l1 [] = l1) ∧
  (∀v5 v4 a_lt. list_merge a_lt [] (v4::v5) = v4::v5) ∧
  ∀y x l2 l1 a_lt.
    list_merge a_lt (x::l1) (y::l2) =
    if a_lt x y then x::list_merge a_lt l1 (y::l2)
    else y::list_merge a_lt (x::l1) l2

⊢ ∀P. (∀a_lt l1. P a_lt l1 []) ∧ (∀a_lt v4 v5. P a_lt [] (v4::v5)) ∧
      (∀a_lt x l1 y l2.
         (¬a_lt x y ⇒ P a_lt (x::l1) l2) ∧ (a_lt x y ⇒ P a_lt l1 (y::l2)) ⇒
         P a_lt (x::l1) (y::l2)) ⇒
      ∀v v1 v2. P v v1 v2

⊢ ∀r r'. r < 3 ⇒ r' < 3 ⇒ (num2ordering r = num2ordering r' ⇔ r = r')

⊢ ∀a. ∃r. a = num2ordering r ∧ r < 3

⊢ ∀a. num2ordering (ordering2num a) = a

⊢ num2ordering 0 = LESS ∧ num2ordering 1 = EQUAL ∧ num2ordering 2 = GREATER

⊢ option_compare c NONE NONE = EQUAL ∧
  option_compare c NONE (SOME v0) = LESS ∧
  option_compare c (SOME v3) NONE = GREATER ∧
  option_compare c (SOME v1) (SOME v2) = c v1 v2

⊢ ∀P. (∀c. P c NONE NONE) ∧ (∀c v0. P c NONE (SOME v0)) ∧
      (∀c v3. P c (SOME v3) NONE) ∧ (∀c v1 v2. P c (SOME v1) (SOME v2)) ⇒
      ∀v v1 v2. P v v1 v2

⊢ ∀a a'. ordering2num a = ordering2num a' ⇔ a = a'

⊢ ∀r. r < 3 ⇔ ∃a. r = ordering2num a

⊢ ∀r. r < 3 ⇔ ordering2num (num2ordering r) = r

⊢ ordering2num LESS = 0 ∧ ordering2num EQUAL = 1 ∧ ordering2num GREATER = 2

⊢ ∀x0 x1 x2. ∃f. f LESS = x0 ∧ f EQUAL = x1 ∧ f GREATER = x2

⊢ ∀a a'. a = a' ⇔ ordering2num a = ordering2num a'

⊢ ∀M M' v0 v1 v2.
    M = M' ∧ (M' = LESS ⇒ v0 = v0') ∧ (M' = EQUAL ⇒ v1 = v1') ∧
    (M' = GREATER ⇒ v2 = v2') ⇒
    (case M of LESS => v0 | EQUAL => v1 | GREATER => v2) =
    case M' of LESS => v0' | EQUAL => v1' | GREATER => v2'

⊢ (∀v0 v1 v2. (case LESS of LESS => v0 | EQUAL => v1 | GREATER => v2) = v0) ∧
  (∀v0 v1 v2. (case EQUAL of LESS => v0 | EQUAL => v1 | GREATER => v2) = v1) ∧
  ∀v0 v1 v2.
    (case GREATER of LESS => v0 | EQUAL => v1 | GREATER => v2) = v2

⊢ (case x of LESS => v0 | EQUAL => v1 | GREATER => v2) = v ⇔
  x = LESS ∧ v0 = v ∨ x = EQUAL ∧ v1 = v ∨ x = GREATER ∧ v2 = v

⊢ LESS ≠ EQUAL ∧ LESS ≠ GREATER ∧ EQUAL ≠ GREATER

⊢ EQUAL ≠ LESS

⊢ GREATER ≠ EQUAL

⊢ (∀x. x = x ⇔ T) ∧ (LESS = EQUAL ⇔ F) ∧ (LESS = GREATER ⇔ F) ∧
  (EQUAL = GREATER ⇔ F) ∧ (EQUAL = LESS ⇔ F) ∧ (GREATER = LESS ⇔ F) ∧
  (GREATER = EQUAL ⇔ F) ∧ (∀x. ordering_size x = 0) ∧
  (ordering2num LESS = 0 ∧ ordering2num EQUAL = 1 ∧
   ordering2num GREATER = 2) ∧ num2ordering 0 = LESS ∧
  num2ordering 1 = EQUAL ∧ num2ordering 2 = GREATER

⊢ ∀P. P EQUAL ∧ P GREATER ∧ P LESS ⇒ ∀a. P a

⊢ ∀a. a = LESS ∨ a = EQUAL ∨ a = GREATER