Theory "toto"

Signature

Definitions

cpn_TY_DEF

|- ∃rep. TYPE_DEFINITION (λn. n < 3) rep

cpn_BIJ

|- (∀a. num2cpn (cpn2num a) = a) ∧
   ∀r. (λn. n < 3) r ⇔ (cpn2num (num2cpn r) = r)

cpn_size_def

|- ∀x. cpn_size x = 0

cpn_CASE

|- ∀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) (cpn2num x)

TotOrd

|- ∀c.
     TotOrd c ⇔
     (∀x y. (c x y = Equal) ⇔ (x = y)) ∧
     (∀x y. (c x y = Greater) ⇔ (c y x = Less)) ∧
     ∀x y z. (c x y = Less) ∧ (c y z = Less) ⇒ (c x z = Less)

TO_of_LinearOrder

|- ∀r x y.
     TO_of_LinearOrder r x y =
     if x = y then Equal else if r x y then Less else Greater

toto_TY_DEF

|- ∃rep. TYPE_DEFINITION TotOrd rep

to_bij

|- (∀a. TO (apto a) = a) ∧ ∀r. TotOrd r ⇔ (apto (TO r) = r)

WeakLinearOrder_of_TO

|- ∀c x y.
     WeakLinearOrder_of_TO c x y ⇔
     case c x y of Less => T | Equal => T | Greater => F

StrongLinearOrder_of_TO

|- ∀c x y.
     StrongLinearOrder_of_TO c x y ⇔
     case c x y of Less => T | Equal => F | Greater => F

toto_of_LinearOrder

|- ∀r. toto_of_LinearOrder r = TO (TO_of_LinearOrder r)

TO_inv

|- ∀c x y. TO_inv c x y = c y x

toto_inv

|- ∀c. toto_inv c = TO (TO_inv (apto c))

lexTO

|- ∀R V.
     R lexTO V =
     TO_of_LinearOrder
       (StrongLinearOrder_of_TO R LEX StrongLinearOrder_of_TO V)

lextoto

|- ∀c v. c lextoto v = TO (apto c lexTO apto v)

numOrd

|- numOrd = TO_of_LinearOrder $<

numto

|- numto = TO numOrd

num_dt_TY_DEF

|- ∃rep.
     TYPE_DEFINITION
       (λa0.
          ∀'num_dt' .
            (∀a0.
               (a0 = ind_type$CONSTR 0 ARB (λn. ind_type$BOTTOM)) ∨
               (∃a.
                  (a0 =
                   (λa.
                      ind_type$CONSTR (SUC 0) ARB
                        (ind_type$FCONS a (λn. ind_type$BOTTOM))) a) ∧
                  'num_dt' a) ∨
               (∃a.
                  (a0 =
                   (λa.
                      ind_type$CONSTR (SUC (SUC 0)) ARB
                        (ind_type$FCONS a (λn. ind_type$BOTTOM))) a) ∧
                  'num_dt' a) ⇒
               'num_dt' a0) ⇒
            'num_dt' a0) rep

num_dt_case_def

|- (∀v f f1. num_dt_CASE zer v f f1 = v) ∧
   (∀a v f f1. num_dt_CASE (bit1 a) v f f1 = f a) ∧
   ∀a v f f1. num_dt_CASE (bit2 a) v f f1 = f1 a

num_dt_size_def

|- (num_dt_size zer = 0) ∧ (∀a. num_dt_size (bit1 a) = 1 + num_dt_size a) ∧
   ∀a. num_dt_size (bit2 a) = 1 + num_dt_size a

num_to_dt_primitive

|- num_to_dt =
   WFREC
     (@R.
        WF R ∧ (∀n. n ≠ 0 ∧ ODD n ⇒ R (DIV2 (n − 1)) n) ∧
        ∀n. n ≠ 0 ∧ ¬ODD n ⇒ R (DIV2 (n − 2)) n)
     (λnum_to_dt n.
        I
          (if n = 0 then zer
           else if ODD n then bit1 (num_to_dt (DIV2 (n − 1)))
           else bit2 (num_to_dt (DIV2 (n − 2)))))

num_dtOrd_tupled_primitive

|- num_dtOrd_tupled =
   WFREC
     (@R.
        WF R ∧ (∀y x. R (x,y) (bit1 x,bit1 y)) ∧
        ∀y x. R (x,y) (bit2 x,bit2 y))
     (λnum_dtOrd_tupled a.
        case a of
          (zer,zer) => I Equal
        | (zer,bit1 x) => I Less
        | (zer,bit2 x') => I Less
        | (bit1 x'',zer) => I Greater
        | (bit1 x'',bit1 y'') => I (num_dtOrd_tupled (x'',y''))
        | (bit1 x'',bit2 y) => I Less
        | (bit2 x''',zer) => I Greater
        | (bit2 x''',bit1 y') => I Greater
        | (bit2 x''',bit2 y''') => I (num_dtOrd_tupled (x''',y''')))

num_dtOrd_curried

|- ∀x x1. num_dtOrd x x1 = num_dtOrd_tupled (x,x1)

qk_numOrd_def

|- ∀m n. qk_numOrd m n = num_dtOrd (num_to_dt m) (num_to_dt n)

qk_numto

|- qk_numto = TO qk_numOrd

charOrd

|- ∀a b. charOrd a b = numOrd (ORD a) (ORD b)

charto

|- charto = TO charOrd

listorder_tupled_primitive

|- listorder_tupled =
   WFREC (@R. WF R ∧ ∀s r m l V. R (V,l,m) (V,r::l,s::m))
     (λlistorder_tupled a.
        case a of
          (V,l,[]) => I F
        | (V,[],s::m) => I T
        | (V,r::l',s::m) => I (V r s ∨ (r = s) ∧ listorder_tupled (V,l',m)))

listorder_curried

|- ∀x x1 x2. listorder x x1 x2 ⇔ listorder_tupled (x,x1,x2)

ListOrd

|- ∀c.
     ListOrd c =
     TO_of_LinearOrder (listorder (StrongLinearOrder_of_TO (apto c)))

listoto

|- ∀c. listoto c = TO (ListOrd c)

stringto

|- stringto = listoto charto

imageOrd

|- ∀f cp a b. imageOrd f cp a b = cp (f a) (f b)

Theorems

StrongLinearOrderExists

|- ∃R. StrongLinearOrder R

num2cpn_cpn2num

|- ∀a. num2cpn (cpn2num a) = a

cpn2num_num2cpn

|- ∀r. r < 3 ⇔ (cpn2num (num2cpn r) = r)

num2cpn_11

|- ∀r r'. r < 3 ⇒ r' < 3 ⇒ ((num2cpn r = num2cpn r') ⇔ (r = r'))

cpn2num_11

|- ∀a a'. (cpn2num a = cpn2num a') ⇔ (a = a')

num2cpn_ONTO

|- ∀a. ∃r. (a = num2cpn r) ∧ r < 3

cpn2num_ONTO

|- ∀r. r < 3 ⇔ ∃a. r = cpn2num a

num2cpn_thm

|- (num2cpn 0 = Less) ∧ (num2cpn 1 = Equal) ∧ (num2cpn 2 = Greater)

cpn2num_thm

|- (cpn2num Less = 0) ∧ (cpn2num Equal = 1) ∧ (cpn2num Greater = 2)

cpn_EQ_cpn

|- ∀a a'. (a = a') ⇔ (cpn2num a = cpn2num a')

cpn_case_def

|- (∀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

datatype_cpn

|- DATATYPE (cpn Less Equal Greater)

cpn_distinct

|- Less ≠ Equal ∧ Less ≠ Greater ∧ Equal ≠ Greater

cpn_case_cong

|- ∀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')

cpn_nchotomy

|- ∀a. (a = Less) ∨ (a = Equal) ∨ (a = Greater)

cpn_Axiom

|- ∀x0 x1 x2. ∃f. (f Less = x0) ∧ (f Equal = x1) ∧ (f Greater = x2)

cpn_induction

|- ∀P. P Equal ∧ P Greater ∧ P Less ⇒ ∀a. P a

trichotomous_ALT

|- ∀R. trichotomous R ⇔ ∀x y. ¬R x y ∧ ¬R y x ⇒ (x = y)

TotOrd_TO_of_LO

|- ∀r. LinearOrder r ⇒ TotOrd (TO_of_LinearOrder r)

SPLIT_PAIRS

|- ∀x y. (x = y) ⇔ (FST x = FST y) ∧ (SND x = SND y)

all_cpn_distinct

|- (Less ≠ Equal ∧ Less ≠ Greater ∧ Equal ≠ Greater) ∧ Equal ≠ Less ∧
   Greater ≠ Less ∧ Greater ≠ Equal

TO_exists

|- ∃x. TotOrd x

TO_apto_ID

|- ∀a. TO (apto a) = a

TO_apto_TO_ID

|- ∀r. TotOrd r ⇔ (apto (TO r) = r)

TO_11

|- ∀r r'. TotOrd r ⇒ TotOrd r' ⇒ ((TO r = TO r') ⇔ (r = r'))

onto_apto

|- ∀r. TotOrd r ⇔ ∃a. r = apto a

TO_onto

|- ∀a. ∃r. (a = TO r) ∧ TotOrd r

TotOrd_apto

|- ∀c. TotOrd (apto c)

TO_apto_TO_IMP

|- ∀r. TotOrd r ⇒ (apto (TO r) = r)

toto_thm

|- ∀c.
     (∀x y. (apto c x y = Equal) ⇔ (x = y)) ∧
     (∀x y. (apto c x y = Greater) ⇔ (apto c y x = Less)) ∧
     ∀x y z. (apto c x y = Less) ∧ (apto c y z = Less) ⇒ (apto c x z = Less)

TO_equal_eq

|- ∀c. TotOrd c ⇒ ∀x y. (c x y = Equal) ⇔ (x = y)

toto_equal_eq

|- ∀c x y. (apto c x y = Equal) ⇔ (x = y)

toto_equal_imp_eq

|- ∀c x y. (apto c x y = Equal) ⇒ (x = y)

TO_refl

|- ∀c. TotOrd c ⇒ ∀x. c x x = Equal

toto_refl

|- ∀c x. apto c x x = Equal

toto_equal_sym

|- ∀c x y. (apto c x y = Equal) ⇔ (apto c y x = Equal)

TO_antisym

|- ∀c. TotOrd c ⇒ ∀x y. (c x y = Greater) ⇔ (c y x = Less)

toto_antisym

|- ∀c x y. (apto c x y = Greater) ⇔ (apto c y x = Less)

toto_not_less_refl

|- ∀cmp h. (apto cmp h h = Less) ⇔ F

toto_swap_cases

|- ∀c x y.
     apto c y x =
     case apto c x y of Less => Greater | Equal => Equal | Greater => Less

toto_glneq

|- (∀c x y. (apto c x y = Less) ⇒ x ≠ y) ∧
   ∀c x y. (apto c x y = Greater) ⇒ x ≠ y

toto_cpn_eqn

|- (∀c x y. (apto c x y = Equal) ⇒ (x = y)) ∧
   (∀c x y. (apto c x y = Less) ⇒ x ≠ y) ∧
   ∀c x y. (apto c x y = Greater) ⇒ x ≠ y

TO_cpn_eqn

|- ∀c.
     TotOrd c ⇒
     (∀x y. (c x y = Less) ⇒ x ≠ y) ∧ (∀x y. (c x y = Greater) ⇒ x ≠ y) ∧
     ∀x y. (c x y = Equal) ⇒ (x = y)

NOT_EQ_LESS_IMP

|- ∀cmp x y. apto cmp x y ≠ Less ⇒ (x = y) ∨ (apto cmp y x = Less)

totoEEtrans

|- ∀c x y z.
     ((apto c x y = Equal) ∧ (apto c y z = Equal) ⇒ (apto c x z = Equal)) ∧
     ((apto c x y = Equal) ∧ (apto c z y = Equal) ⇒ (apto c x z = Equal))

totoLLtrans

|- ∀c x y z. (apto c x y = Less) ∧ (apto c y z = Less) ⇒ (apto c x z = Less)

totoLGtrans

|- ∀c x y z.
     (apto c x y = Less) ∧ (apto c z y = Greater) ⇒ (apto c x z = Less)

totoGGtrans

|- ∀c x y z.
     (apto c y x = Greater) ∧ (apto c z y = Greater) ⇒ (apto c x z = Less)

totoGLtrans

|- ∀c x y z.
     (apto c y x = Greater) ∧ (apto c y z = Less) ⇒ (apto c x z = Less)

totoLEtrans

|- ∀c x y z. (apto c x y = Less) ∧ (apto c y z = Equal) ⇒ (apto c x z = Less)

totoELtrans

|- ∀c x y z. (apto c x y = Equal) ∧ (apto c y z = Less) ⇒ (apto c x z = Less)

toto_trans_less

|- (∀c x y z.
      (apto c x y = Less) ∧ (apto c y z = Less) ⇒ (apto c x z = Less)) ∧
   (∀c x y z.
      (apto c x y = Less) ∧ (apto c z y = Greater) ⇒ (apto c x z = Less)) ∧
   (∀c x y z.
      (apto c y x = Greater) ∧ (apto c z y = Greater) ⇒ (apto c x z = Less)) ∧
   (∀c x y z.
      (apto c y x = Greater) ∧ (apto c y z = Less) ⇒ (apto c x z = Less)) ∧
   (∀c x y z.
      (apto c x y = Less) ∧ (apto c y z = Equal) ⇒ (apto c x z = Less)) ∧
   ∀c x y z. (apto c x y = Equal) ∧ (apto c y z = Less) ⇒ (apto c x z = Less)

Weak_Weak_of

|- ∀c. WeakLinearOrder (WeakLinearOrder_of_TO (apto c))

STRORD_SLO

|- ∀R. WeakLinearOrder R ⇒ StrongLinearOrder (STRORD R)

Strongof_toto_STRORD

|- ∀c.
     StrongLinearOrder_of_TO (apto c) =
     STRORD (WeakLinearOrder_of_TO (apto c))

Strong_Strong_of

|- ∀c. StrongLinearOrder (StrongLinearOrder_of_TO (apto c))

Strong_Strong_of_TO

|- ∀c. TotOrd c ⇒ StrongLinearOrder (StrongLinearOrder_of_TO c)

TotOrd_TO_of_Weak

|- ∀r. WeakLinearOrder r ⇒ TotOrd (TO_of_LinearOrder r)

TotOrd_TO_of_Strong

|- ∀r. StrongLinearOrder r ⇒ TotOrd (TO_of_LinearOrder r)

toto_Weak_thm

|- ∀c. toto_of_LinearOrder (WeakLinearOrder_of_TO (apto c)) = c

toto_Strong_thm

|- ∀c. toto_of_LinearOrder (StrongLinearOrder_of_TO (apto c)) = c

Weak_toto_thm

|- ∀r.
     WeakLinearOrder r ⇒
     (WeakLinearOrder_of_TO (apto (toto_of_LinearOrder r)) = r)

Strong_toto_thm

|- ∀r.
     StrongLinearOrder r ⇒
     (StrongLinearOrder_of_TO (apto (toto_of_LinearOrder r)) = r)

TotOrd_inv

|- ∀c. TotOrd c ⇒ TotOrd (TO_inv c)

inv_TO

|- ∀r. TotOrd r ⇒ (toto_inv (TO r) = TO (TO_inv r))

apto_inv

|- ∀c. apto (toto_inv c) = TO_inv (apto c)

Weak_toto_inv

|- ∀c.
     WeakLinearOrder_of_TO (apto (toto_inv c)) =
     inv (WeakLinearOrder_of_TO (apto c))

Strong_toto_inv

|- ∀c.
     StrongLinearOrder_of_TO (apto (toto_inv c)) =
     inv (StrongLinearOrder_of_TO (apto c))

TO_inv_TO_inv

|- ∀c. TO_inv (TO_inv c) = c

toto_inv_toto_inv

|- ∀c. toto_inv (toto_inv c) = c

TO_inv_Ord

|- ∀r. TO_of_LinearOrder (inv r) = TO_inv (TO_of_LinearOrder r)

TO_of_less_rel

|- ∀r. StrongLinearOrder r ⇒ ∀x y. (TO_of_LinearOrder r x y = Less) ⇔ r x y

TO_of_greater_ler

|- ∀r. StrongLinearOrder r ⇒ ∀x y. (TO_of_LinearOrder r x y = Greater) ⇔ r y x

toto_equal_imp

|- ∀cmp phi.
     LinearOrder phi ∧ (cmp = toto_of_LinearOrder phi) ⇒
     ∀x y. ((x = y) ⇔ T) ⇒ (apto cmp x y = Equal)

toto_unequal_imp

|- ∀cmp phi.
     LinearOrder phi ∧ (cmp = toto_of_LinearOrder phi) ⇒
     ∀x y.
       ((x = y) ⇔ F) ⇒
       if phi x y then apto cmp x y = Less else apto cmp x y = Greater

StrongOrder_ALT

|- ∀Z. StrongOrder Z ⇔ irreflexive Z ∧ transitive Z

LEX_ALT

|- ∀R U c d.
     (R LEX U) c d ⇔ R (FST c) (FST d) ∨ (FST c = FST d) ∧ U (SND c) (SND d)

SLO_LEX

|- ∀R V.
     StrongLinearOrder R ∧ StrongLinearOrder V ⇒ StrongLinearOrder (R LEX V)

lexTO_thm

|- ∀R V.
     TotOrd R ∧ TotOrd V ⇒
     ∀x y.
       (R lexTO V) x y =
       case R (FST x) (FST y) of
         Less => Less
       | Equal => V (SND x) (SND y)
       | Greater => Greater

lexTO_ALT

|- ∀R V.
     TotOrd R ∧ TotOrd V ⇒
     ∀(r,u) (r',u').
       (R lexTO V) (r,u) (r',u') =
       case R r r' of Less => Less | Equal => V u u' | Greater => Greater

TO_lexTO

|- ∀R V. TotOrd R ∧ TotOrd V ⇒ TotOrd (R lexTO V)

pre_aplextoto

|- ∀c v x y.
     apto (c lextoto v) x y =
     case apto c (FST x) (FST y) of
       Less => Less
     | Equal => apto v (SND x) (SND y)
     | Greater => Greater

aplextoto

|- ∀c v x1 x2 y1 y2.
     apto (c lextoto v) (x1,x2) (y1,y2) =
     case apto c x1 y1 of
       Less => Less
     | Equal => apto v x2 y2
     | Greater => Greater

StrongLinearOrder_LESS

|- StrongLinearOrder $<

TO_numOrd

|- TotOrd numOrd

apnumto_thm

|- apto numto = numOrd

numeralOrd

|- ∀x y.
     (numOrd ZERO ZERO = Equal) ∧ (numOrd ZERO (BIT1 y) = Less) ∧
     (numOrd ZERO (BIT2 y) = Less) ∧ (numOrd (BIT1 x) ZERO = Greater) ∧
     (numOrd (BIT2 x) ZERO = Greater) ∧
     (numOrd (BIT1 x) (BIT1 y) = numOrd x y) ∧
     (numOrd (BIT2 x) (BIT2 y) = numOrd x y) ∧
     (numOrd (BIT1 x) (BIT2 y) =
      case numOrd x y of Less => Less | Equal => Less | Greater => Greater) ∧
     (numOrd (BIT2 x) (BIT1 y) =
      case numOrd x y of Less => Less | Equal => Greater | Greater => Greater)

datatype_num_dt

|- DATATYPE (num_dt zer bit1 bit2)

num_dt_11

|- (∀a a'. (bit1 a = bit1 a') ⇔ (a = a')) ∧
   ∀a a'. (bit2 a = bit2 a') ⇔ (a = a')

num_dt_distinct

|- (∀a. zer ≠ bit1 a) ∧ (∀a. zer ≠ bit2 a) ∧ ∀a' a. bit1 a ≠ bit2 a'

num_dt_case_cong

|- ∀M M' v f f1.
     (M = M') ∧ ((M' = zer) ⇒ (v = v')) ∧ (∀a. (M' = bit1 a) ⇒ (f a = f' a)) ∧
     (∀a. (M' = bit2 a) ⇒ (f1 a = f1' a)) ⇒
     (num_dt_CASE M v f f1 = num_dt_CASE M' v' f' f1')

num_dt_nchotomy

|- ∀nn. (nn = zer) ∨ (∃n. nn = bit1 n) ∨ ∃n. nn = bit2 n

num_dt_Axiom

|- ∀f0 f1 f2.
     ∃fn.
       (fn zer = f0) ∧ (∀a. fn (bit1 a) = f1 a (fn a)) ∧
       ∀a. fn (bit2 a) = f2 a (fn a)

num_dt_induction

|- ∀P. P zer ∧ (∀n. P n ⇒ P (bit1 n)) ∧ (∀n. P n ⇒ P (bit2 n)) ⇒ ∀n. P n

num_dtOrd_ind

|- ∀P.
     P zer zer ∧ (∀x. P zer (bit1 x)) ∧ (∀x. P zer (bit2 x)) ∧
     (∀x. P (bit1 x) zer) ∧ (∀x. P (bit2 x) zer) ∧
     (∀x y. P (bit1 x) (bit2 y)) ∧ (∀x y. P (bit2 x) (bit1 y)) ∧
     (∀x y. P x y ⇒ P (bit1 x) (bit1 y)) ∧
     (∀x y. P x y ⇒ P (bit2 x) (bit2 y)) ⇒
     ∀v v1. P v v1

num_dtOrd

|- (num_dtOrd zer zer = Equal) ∧ (∀x. num_dtOrd zer (bit1 x) = Less) ∧
   (∀x. num_dtOrd zer (bit2 x) = Less) ∧
   (∀x. num_dtOrd (bit1 x) zer = Greater) ∧
   (∀x. num_dtOrd (bit2 x) zer = Greater) ∧
   (∀y x. num_dtOrd (bit1 x) (bit2 y) = Less) ∧
   (∀y x. num_dtOrd (bit2 x) (bit1 y) = Greater) ∧
   (∀y x. num_dtOrd (bit1 x) (bit1 y) = num_dtOrd x y) ∧
   ∀y x. num_dtOrd (bit2 x) (bit2 y) = num_dtOrd x y

TO_qk_numOrd

|- TotOrd qk_numOrd

qk_numeralOrd

|- ∀x y.
     (qk_numOrd ZERO ZERO = Equal) ∧ (qk_numOrd ZERO (BIT1 y) = Less) ∧
     (qk_numOrd ZERO (BIT2 y) = Less) ∧ (qk_numOrd (BIT1 x) ZERO = Greater) ∧
     (qk_numOrd (BIT2 x) ZERO = Greater) ∧
     (qk_numOrd (BIT1 x) (BIT1 y) = qk_numOrd x y) ∧
     (qk_numOrd (BIT2 x) (BIT2 y) = qk_numOrd x y) ∧
     (qk_numOrd (BIT1 x) (BIT2 y) = Less) ∧
     (qk_numOrd (BIT2 x) (BIT1 y) = Greater)

ap_qk_numto_thm

|- apto qk_numto = qk_numOrd

TO_charOrd

|- TotOrd charOrd

apcharto_thm

|- apto charto = charOrd

charOrd_lt_lem

|- ∀a b.
     (numOrd a b = Less) ⇒ (b < 256 ⇔ T) ⇒ (charOrd (CHR a) (CHR b) = Less)

charOrd_gt_lem

|- ∀a b.
     (numOrd a b = Greater) ⇒
     (a < 256 ⇔ T) ⇒
     (charOrd (CHR a) (CHR b) = Greater)

charOrd_eq_lem

|- ∀a b. (numOrd a b = Equal) ⇒ (charOrd (CHR a) (CHR b) = Equal)

charOrd_thm

|- charOrd = TO_of_LinearOrder $<

listorder_ind

|- ∀P.
     (∀V l. P V l []) ∧ (∀V s m. P V [] (s::m)) ∧
     (∀V r l s m. P V l m ⇒ P V (r::l) (s::m)) ⇒
     ∀v v1 v2. P v v1 v2

listorder

|- (∀l V. listorder V l [] ⇔ F) ∧ (∀s m V. listorder V [] (s::m) ⇔ T) ∧
   ∀s r m l V. listorder V (r::l) (s::m) ⇔ V r s ∨ (r = s) ∧ listorder V l m

SLO_listorder

|- ∀V. StrongLinearOrder V ⇒ StrongLinearOrder (listorder V)

TO_ListOrd

|- ∀c. TotOrd (ListOrd c)

ListOrd_THM

|- ∀c.
     (ListOrd c [] [] = Equal) ∧ (∀b y. ListOrd c [] (b::y) = Less) ∧
     (∀a x. ListOrd c (a::x) [] = Greater) ∧
     ∀a x b y.
       ListOrd c (a::x) (b::y) =
       case apto c a b of
         Less => Less
       | Equal => ListOrd c x y
       | Greater => Greater

aplistoto

|- ∀c.
     (apto (listoto c) [] [] = Equal) ∧
     (∀b y. apto (listoto c) [] (b::y) = Less) ∧
     (∀a x. apto (listoto c) (a::x) [] = Greater) ∧
     ∀a x b y.
       apto (listoto c) (a::x) (b::y) =
       case apto c a b of
         Less => Less
       | Equal => apto (listoto c) x y
       | Greater => Greater

TO_injection

|- ∀cp. TotOrd cp ⇒ ∀f. ONE_ONE f ⇒ TotOrd (imageOrd f cp)