Structure sortingTheory

signature sortingTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val PART3_DEF : thm
    val PARTITION_DEF : thm
    val PART_DEF : thm
    val PERM_DEF : thm
    val PERM_SINGLE_SWAP_DEF : thm
    val SORTS_DEF : thm
    val STABLE_DEF : thm
  
  (*  Theorems  *)
    val ALL_DISTINCT_PERM : thm
    val ALL_DISTINCT_PERM_LIST_TO_SET_TO_LIST : thm
    val ALL_DISTINCT_SORTED_WEAKEN : thm
    val APPEND_PERM_SYM : thm
    val CONS_PERM : thm
    val FILTER_EQ_LENGTHS_EQ : thm
    val FILTER_EQ_REP : thm
    val FOLDR_PERM : thm
    val MEM_PERM : thm
    val PART3_FILTER : thm
    val PART_LENGTH : thm
    val PART_LENGTH_LEM : thm
    val PART_MEM : thm
    val PARTs_HAVE_PROP : thm
    val PERM3 : thm
    val PERM3_FILTER : thm
    val PERM_ALL_DISTINCT : thm
    val PERM_APPEND : thm
    val PERM_APPEND_IFF : thm
    val PERM_BIJ : thm
    val PERM_CONG : thm
    val PERM_CONG_2 : thm
    val PERM_CONG_APPEND_IFF : thm
    val PERM_CONG_APPEND_IFF2 : thm
    val PERM_CONS_EQ_APPEND : thm
    val PERM_CONS_IFF : thm
    val PERM_EQC : thm
    val PERM_EQUIVALENCE : thm
    val PERM_EQUIVALENCE_ALT_DEF : thm
    val PERM_EVERY : thm
    val PERM_FILTER : thm
    val PERM_FUN_APPEND : thm
    val PERM_FUN_APPEND_APPEND_1 : thm
    val PERM_FUN_APPEND_APPEND_2 : thm
    val PERM_FUN_APPEND_C : thm
    val PERM_FUN_APPEND_CONS : thm
    val PERM_FUN_APPEND_IFF : thm
    val PERM_FUN_CONG : thm
    val PERM_FUN_CONS : thm
    val PERM_FUN_CONS_11_APPEND : thm
    val PERM_FUN_CONS_11_SWAP_AT_FRONT : thm
    val PERM_FUN_CONS_APPEND_1 : thm
    val PERM_FUN_CONS_APPEND_2 : thm
    val PERM_FUN_CONS_IFF : thm
    val PERM_FUN_SPLIT : thm
    val PERM_FUN_SWAP_AT_FRONT : thm
    val PERM_IND : thm
    val PERM_INTRO : thm
    val PERM_LENGTH : thm
    val PERM_LIST_TO_SET : thm
    val PERM_MAP : thm
    val PERM_MEM_EQ : thm
    val PERM_MONO : thm
    val PERM_NIL : thm
    val PERM_QSORT3 : thm
    val PERM_REFL : thm
    val PERM_REVERSE : thm
    val PERM_REVERSE_EQ : thm
    val PERM_REWR : thm
    val PERM_RTC : thm
    val PERM_SET_TO_LIST_count_COUNT_LIST : thm
    val PERM_SING : thm
    val PERM_SINGLE_SWAP_APPEND : thm
    val PERM_SINGLE_SWAP_CONS : thm
    val PERM_SINGLE_SWAP_I : thm
    val PERM_SINGLE_SWAP_REFL : thm
    val PERM_SINGLE_SWAP_SYM : thm
    val PERM_SINGLE_SWAP_TC_CONS : thm
    val PERM_SPLIT : thm
    val PERM_SPLIT_IF : thm
    val PERM_STRONG_IND : thm
    val PERM_SUM : thm
    val PERM_SWAP_AT_FRONT : thm
    val PERM_SWAP_L_AT_FRONT : thm
    val PERM_SYM : thm
    val PERM_TC : thm
    val PERM_TO_APPEND_SIMPS : thm
    val PERM_TRANS : thm
    val PERM_alt : thm
    val PERM_lifts_equalities : thm
    val PERM_lifts_invariants : thm
    val PERM_lifts_monotonicities : thm
    val PERM_lifts_transitive_relations : thm
    val PERM_transitive : thm
    val QSORT3_DEF : thm
    val QSORT3_IND : thm
    val QSORT3_MEM : thm
    val QSORT3_SORTED : thm
    val QSORT3_SORTS : thm
    val QSORT3_SPLIT : thm
    val QSORT3_STABLE : thm
    val QSORT_DEF : thm
    val QSORT_IND : thm
    val QSORT_MEM : thm
    val QSORT_PERM : thm
    val QSORT_SORTED : thm
    val QSORT_SORTS : thm
    val QSORT_eq_if_PERM : thm
    val SORTED_ALL_DISTINCT : thm
    val SORTED_APPEND : thm
    val SORTED_APPEND_IFF : thm
    val SORTED_DEF : thm
    val SORTED_EL_LESS : thm
    val SORTED_EL_SUC : thm
    val SORTED_EQ : thm
    val SORTED_EQ_PART : thm
    val SORTED_FILTER : thm
    val SORTED_GENLIST_PLUS : thm
    val SORTED_IND : thm
    val SORTED_NIL : thm
    val SORTED_PERM_EQ : thm
    val SORTED_SING : thm
    val SORTED_TL : thm
    val SORTED_weaken : thm
    val SUM_IMAGE_count_MULT : thm
    val SUM_IMAGE_count_SUM_GENLIST : thm
    val less_sorted_eq : thm
    val sorted_count_list : thm
    val sorted_filter : thm
    val sorted_map : thm
    val sorted_perm_count_list : thm
    val sum_of_sums : thm
  
  val sorting_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [indexedLists] Parent theory of "sorting"
   
   [patternMatches] Parent theory of "sorting"
   
   [PART3_DEF]  Definition
      
      ⊢ (∀R h. PART3 R h [] = ([],[],[])) ∧
        ∀R h hd tl.
            PART3 R h (hd::tl) =
            if R h hd ∧ R hd h then (I ## CONS hd ## I) (PART3 R h tl)
            else if R hd h then (CONS hd ## I ## I) (PART3 R h tl)
            else (I ## I ## CONS hd) (PART3 R h tl)
   
   [PARTITION_DEF]  Definition
      
      ⊢ ∀P l. PARTITION P l = PART P l [] []
   
   [PART_DEF]  Definition
      
      ⊢ (∀P l1 l2. PART P [] l1 l2 = (l1,l2)) ∧
        ∀P h rst l1 l2.
            PART P (h::rst) l1 l2 =
            if P h then PART P rst (h::l1) l2 else PART P rst l1 (h::l2)
   
   [PERM_DEF]  Definition
      
      ⊢ ∀L1 L2. PERM L1 L2 ⇔ ∀x. FILTER ($= x) L1 = FILTER ($= x) L2
   
   [PERM_SINGLE_SWAP_DEF]  Definition
      
      ⊢ ∀l1 l2.
            PERM_SINGLE_SWAP l1 l2 ⇔
            ∃x1 x2 x3. l1 = x1 ⧺ x2 ⧺ x3 ∧ l2 = x1 ⧺ x3 ⧺ x2
   
   [SORTS_DEF]  Definition
      
      ⊢ ∀f R. SORTS f R ⇔ ∀l. PERM l (f R l) ∧ SORTED R (f R l)
   
   [STABLE_DEF]  Definition
      
      ⊢ ∀sort r.
            STABLE sort r ⇔
            SORTS sort r ∧
            ∀p.
                (∀x y. p x ∧ p y ⇒ r x y) ⇒
                ∀l. FILTER p l = FILTER p (sort r l)
   
   [ALL_DISTINCT_PERM]  Theorem
      
      ⊢ ∀l1 l2. PERM l1 l2 ⇒ (ALL_DISTINCT l1 ⇔ ALL_DISTINCT l2)
   
   [ALL_DISTINCT_PERM_LIST_TO_SET_TO_LIST]  Theorem
      
      ⊢ ∀ls. ALL_DISTINCT ls ⇔ PERM ls (SET_TO_LIST (set ls))
   
   [ALL_DISTINCT_SORTED_WEAKEN]  Theorem
      
      ⊢ ∀R R' ls.
            (∀x y. MEM x ls ∧ MEM y ls ∧ x ≠ y ⇒ (R x y ⇔ R' x y)) ∧
            ALL_DISTINCT ls ∧ SORTED R ls ⇒
            SORTED R' ls
   
   [APPEND_PERM_SYM]  Theorem
      
      ⊢ ∀A B C. PERM (A ⧺ B) C ⇒ PERM (B ⧺ A) C
   
   [CONS_PERM]  Theorem
      
      ⊢ ∀x L M N. PERM L (M ⧺ N) ⇒ PERM (x::L) (M ⧺ x::N)
   
   [FILTER_EQ_LENGTHS_EQ]  Theorem
      
      ⊢ LENGTH (FILTER ($= x) l1) = LENGTH (FILTER ($= x) l2) ⇒
        FILTER ($= x) l1 = FILTER ($= x) l2
   
   [FILTER_EQ_REP]  Theorem
      
      ⊢ FILTER ($= x) l = REPLICATE (LENGTH (FILTER ($= x) l)) x
   
   [FOLDR_PERM]  Theorem
      
      ⊢ ∀f l1 l2 e.
            ASSOC f ∧ COMM f ⇒ PERM l1 l2 ⇒ FOLDR f e l1 = FOLDR f e l2
   
   [MEM_PERM]  Theorem
      
      ⊢ ∀l1 l2. PERM l1 l2 ⇒ ∀a. MEM a l1 ⇔ MEM a l2
   
   [PART3_FILTER]  Theorem
      
      ⊢ ∀tl hd.
            PART3 R hd tl =
            (FILTER (λx. R x hd ∧ ¬R hd x) tl,
             FILTER (λx. R x hd ∧ R hd x) tl,FILTER (λx. ¬R x hd) tl)
   
   [PART_LENGTH]  Theorem
      
      ⊢ ∀P L l1 l2 p q.
            (p,q) = PART P L l1 l2 ⇒
            LENGTH L + LENGTH l1 + LENGTH l2 = LENGTH p + LENGTH q
   
   [PART_LENGTH_LEM]  Theorem
      
      ⊢ ∀P L l1 l2 p q.
            (p,q) = PART P L l1 l2 ⇒
            LENGTH p ≤ LENGTH L + LENGTH l1 + LENGTH l2 ∧
            LENGTH q ≤ LENGTH L + LENGTH l1 + LENGTH l2
   
   [PART_MEM]  Theorem
      
      ⊢ ∀P L a1 a2 l1 l2.
            (a1,a2) = PART P L l1 l2 ⇒
            ∀x. MEM x (L ⧺ (l1 ⧺ l2)) ⇔ MEM x (a1 ⧺ a2)
   
   [PARTs_HAVE_PROP]  Theorem
      
      ⊢ ∀P L A B l1 l2.
            (A,B) = PART P L l1 l2 ∧ (∀x. MEM x l1 ⇒ P x) ∧
            (∀x. MEM x l2 ⇒ ¬P x) ⇒
            (∀z. MEM z A ⇒ P z) ∧ ∀z. MEM z B ⇒ ¬P z
   
   [PERM3]  Theorem
      
      ⊢ ∀x a a' b b' c c'.
            (PERM a a' ∧ PERM b b' ∧ PERM c c') ∧ PERM x (a ⧺ b ⧺ c) ⇒
            PERM x (a' ⧺ b' ⧺ c')
   
   [PERM3_FILTER]  Theorem
      
      ⊢ ∀l h.
            PERM l
              (FILTER (λx. R x h ∧ ¬R h x) l ⧺
               FILTER (λx. R x h ∧ R h x) l ⧺ FILTER (λx. ¬R x h) l)
   
   [PERM_ALL_DISTINCT]  Theorem
      
      ⊢ ∀l1 l2.
            ALL_DISTINCT l1 ∧ ALL_DISTINCT l2 ∧ (∀x. MEM x l1 ⇔ MEM x l2) ⇒
            PERM l1 l2
   
   [PERM_APPEND]  Theorem
      
      ⊢ ∀l1 l2. PERM (l1 ⧺ l2) (l2 ⧺ l1)
   
   [PERM_APPEND_IFF]  Theorem
      
      ⊢ (∀l l1 l2. PERM (l ⧺ l1) (l ⧺ l2) ⇔ PERM l1 l2) ∧
        ∀l l1 l2. PERM (l1 ⧺ l) (l2 ⧺ l) ⇔ PERM l1 l2
   
   [PERM_BIJ]  Theorem
      
      ⊢ ∀l1 l2.
            PERM l1 l2 ⇒
            ∃f.
                f PERMUTES count (LENGTH l1) ∧
                l2 = GENLIST (λi. EL (f i) l1) (LENGTH l1)
   
   [PERM_CONG]  Theorem
      
      ⊢ ∀L1 L2 L3 L4. PERM L1 L3 ∧ PERM L2 L4 ⇒ PERM (L1 ⧺ L2) (L3 ⧺ L4)
   
   [PERM_CONG_2]  Theorem
      
      ⊢ ∀l1 l1' l2 l2'.
            PERM l1 l1' ⇒ PERM l2 l2' ⇒ (PERM l1 l2 ⇔ PERM l1' l2')
   
   [PERM_CONG_APPEND_IFF]  Theorem
      
      ⊢ ∀l l1 l1' l2 l2'.
            PERM l1 (l ⧺ l1') ⇒
            PERM l2 (l ⧺ l2') ⇒
            (PERM l1 l2 ⇔ PERM l1' l2')
   
   [PERM_CONG_APPEND_IFF2]  Theorem
      
      ⊢ ∀l1 l1' l1'' l2 l2' l2''.
            PERM l1 (l1' ⧺ l1'') ⇒
            PERM l2 (l2' ⧺ l2'') ⇒
            PERM l1' l2' ⇒
            (PERM l1 l2 ⇔ PERM l1'' l2'')
   
   [PERM_CONS_EQ_APPEND]  Theorem
      
      ⊢ ∀L h. PERM (h::t) L ⇔ ∃M N. L = M ⧺ h::N ∧ PERM t (M ⧺ N)
   
   [PERM_CONS_IFF]  Theorem
      
      ⊢ ∀x l2 l1. PERM (x::l1) (x::l2) ⇔ PERM l1 l2
   
   [PERM_EQC]  Theorem
      
      ⊢ PERM = PERM_SINGLE_SWAP^=
   
   [PERM_EQUIVALENCE]  Theorem
      
      ⊢ equivalence PERM
   
   [PERM_EQUIVALENCE_ALT_DEF]  Theorem
      
      ⊢ ∀x y. PERM x y ⇔ PERM x = PERM y
   
   [PERM_EVERY]  Theorem
      
      ⊢ ∀ls ls'. PERM ls ls' ⇒ (EVERY P ls ⇔ EVERY P ls')
   
   [PERM_FILTER]  Theorem
      
      ⊢ ∀P l1 l2. PERM l1 l2 ⇒ PERM (FILTER P l1) (FILTER P l2)
   
   [PERM_FUN_APPEND]  Theorem
      
      ⊢ ∀l1 l2. PERM (l1 ⧺ l2) = PERM (l2 ⧺ l1)
   
   [PERM_FUN_APPEND_APPEND_1]  Theorem
      
      ⊢ ∀l1 l2 l3 l4.
            PERM l1 = PERM (l2 ⧺ l3) ⇒
            PERM (l1 ⧺ l4) = PERM (l2 ⧺ (l3 ⧺ l4))
   
   [PERM_FUN_APPEND_APPEND_2]  Theorem
      
      ⊢ ∀l1 l2 l3 l4.
            PERM l1 = PERM (l2 ⧺ l3) ⇒
            PERM (l4 ⧺ l1) = PERM (l2 ⧺ (l4 ⧺ l3))
   
   [PERM_FUN_APPEND_C]  Theorem
      
      ⊢ ∀l1 l1' l2 l2'.
            PERM l1 = PERM l1' ⇒
            PERM l2 = PERM l2' ⇒
            PERM (l1 ⧺ l2) = PERM (l1' ⧺ l2')
   
   [PERM_FUN_APPEND_CONS]  Theorem
      
      ⊢ ∀x l1 l2. PERM (l1 ⧺ x::l2) = PERM (x::l1 ⧺ l2)
   
   [PERM_FUN_APPEND_IFF]  Theorem
      
      ⊢ ∀l l1 l2. PERM l1 = PERM l2 ⇒ PERM (l ⧺ l1) = PERM (l ⧺ l2)
   
   [PERM_FUN_CONG]  Theorem
      
      ⊢ ∀l1 l1' l2 l2'.
            PERM l1 = PERM l1' ⇒
            PERM l2 = PERM l2' ⇒
            (PERM l1 l2 ⇔ PERM l1' l2')
   
   [PERM_FUN_CONS]  Theorem
      
      ⊢ ∀x l1 l1'. PERM l1 = PERM l1' ⇒ PERM (x::l1) = PERM (x::l1')
   
   [PERM_FUN_CONS_11_APPEND]  Theorem
      
      ⊢ ∀y l1 l2 l3.
            PERM l1 = PERM (l2 ⧺ l3) ⇒ PERM (y::l1) = PERM (l2 ⧺ y::l3)
   
   [PERM_FUN_CONS_11_SWAP_AT_FRONT]  Theorem
      
      ⊢ ∀y l1 x l2. PERM l1 = PERM (x::l2) ⇒ PERM (y::l1) = PERM (x::y::l2)
   
   [PERM_FUN_CONS_APPEND_1]  Theorem
      
      ⊢ ∀l l1 x l2.
            PERM l1 = PERM (x::l2) ⇒ PERM (l1 ⧺ l) = PERM (x::(l2 ⧺ l))
   
   [PERM_FUN_CONS_APPEND_2]  Theorem
      
      ⊢ ∀l l1 x l2.
            PERM l1 = PERM (x::l2) ⇒ PERM (l ⧺ l1) = PERM (x::(l ⧺ l2))
   
   [PERM_FUN_CONS_IFF]  Theorem
      
      ⊢ ∀x l1 l2. PERM l1 = PERM l2 ⇒ PERM (x::l1) = PERM (x::l2)
   
   [PERM_FUN_SPLIT]  Theorem
      
      ⊢ ∀l l1 l1' l2. PERM l (l1 ⧺ l2) ⇒ PERM l1' l1 ⇒ PERM l (l1' ⧺ l2)
   
   [PERM_FUN_SWAP_AT_FRONT]  Theorem
      
      ⊢ ∀x y l. PERM (x::y::l) = PERM (y::x::l)
   
   [PERM_IND]  Theorem
      
      ⊢ ∀P.
            P [] [] ∧ (∀x l1 l2. P l1 l2 ⇒ P (x::l1) (x::l2)) ∧
            (∀x y l1 l2. P l1 l2 ⇒ P (x::y::l1) (y::x::l2)) ∧
            (∀l1 l2 l3. P l1 l2 ∧ P l2 l3 ⇒ P l1 l3) ⇒
            ∀l1 l2. PERM l1 l2 ⇒ P l1 l2
   
   [PERM_INTRO]  Theorem
      
      ⊢ ∀x y. x = y ⇒ PERM x y
   
   [PERM_LENGTH]  Theorem
      
      ⊢ ∀l1 l2. PERM l1 l2 ⇒ LENGTH l1 = LENGTH l2
   
   [PERM_LIST_TO_SET]  Theorem
      
      ⊢ ∀l1 l2. PERM l1 l2 ⇒ set l1 = set l2
   
   [PERM_MAP]  Theorem
      
      ⊢ ∀f l1 l2. PERM l1 l2 ⇒ PERM (MAP f l1) (MAP f l2)
   
   [PERM_MEM_EQ]  Theorem
      
      ⊢ ∀l1 l2. PERM l1 l2 ⇒ ∀x. MEM x l1 ⇔ MEM x l2
   
   [PERM_MONO]  Theorem
      
      ⊢ ∀l1 l2 x. PERM l1 l2 ⇒ PERM (x::l1) (x::l2)
   
   [PERM_NIL]  Theorem
      
      ⊢ ∀L. (PERM L [] ⇔ L = []) ∧ (PERM [] L ⇔ L = [])
   
   [PERM_QSORT3]  Theorem
      
      ⊢ ∀l R. PERM l (QSORT3 R l)
   
   [PERM_REFL]  Theorem
      
      ⊢ ∀L. PERM L L
   
   [PERM_REVERSE]  Theorem
      
      ⊢ PERM ls (REVERSE ls)
   
   [PERM_REVERSE_EQ]  Theorem
      
      ⊢ (PERM (REVERSE l1) l2 ⇔ PERM l1 l2) ∧
        (PERM l1 (REVERSE l2) ⇔ PERM l1 l2)
   
   [PERM_REWR]  Theorem
      
      ⊢ ∀l r l1 l2. PERM l r ⇒ (PERM (l ⧺ l1) l2 ⇔ PERM (r ⧺ l1) l2)
   
   [PERM_RTC]  Theorem
      
      ⊢ PERM = PERM_SINGLE_SWAP⃰
   
   [PERM_SET_TO_LIST_count_COUNT_LIST]  Theorem
      
      ⊢ PERM (SET_TO_LIST (count n)) (COUNT_LIST n)
   
   [PERM_SING]  Theorem
      
      ⊢ (PERM L [x] ⇔ L = [x]) ∧ (PERM [x] L ⇔ L = [x])
   
   [PERM_SINGLE_SWAP_APPEND]  Theorem
      
      ⊢ PERM_SINGLE_SWAP (x2 ⧺ x3) (x3 ⧺ x2)
   
   [PERM_SINGLE_SWAP_CONS]  Theorem
      
      ⊢ PERM_SINGLE_SWAP M N ⇒ PERM_SINGLE_SWAP (x::M) (x::N)
   
   [PERM_SINGLE_SWAP_I]  Theorem
      
      ⊢ PERM_SINGLE_SWAP (x1 ⧺ x2 ⧺ x3) (x1 ⧺ x3 ⧺ x2)
   
   [PERM_SINGLE_SWAP_REFL]  Theorem
      
      ⊢ ∀l. PERM_SINGLE_SWAP l l
   
   [PERM_SINGLE_SWAP_SYM]  Theorem
      
      ⊢ ∀l1 l2. PERM_SINGLE_SWAP l1 l2 ⇔ PERM_SINGLE_SWAP l2 l1
   
   [PERM_SINGLE_SWAP_TC_CONS]  Theorem
      
      ⊢ ∀M N. PERM_SINGLE_SWAP⁺ M N ⇒ PERM_SINGLE_SWAP⁺ (x::M) (x::N)
   
   [PERM_SPLIT]  Theorem
      
      ⊢ ∀P l. PERM l (FILTER P l ⧺ FILTER ($~ ∘ P) l)
   
   [PERM_SPLIT_IF]  Theorem
      
      ⊢ ∀P Q l. EVERY (λx. P x ⇔ ¬Q x) l ⇒ PERM l (FILTER P l ⧺ FILTER Q l)
   
   [PERM_STRONG_IND]  Theorem
      
      ⊢ ∀P.
            P [] [] ∧
            (∀x l1 l2. PERM l1 l2 ∧ P l1 l2 ⇒ P (x::l1) (x::l2)) ∧
            (∀x y l1 l2. PERM l1 l2 ∧ P l1 l2 ⇒ P (x::y::l1) (y::x::l2)) ∧
            (∀l1 l2 l3.
                 PERM l1 l2 ∧ P l1 l2 ∧ PERM l2 l3 ∧ P l2 l3 ⇒ P l1 l3) ⇒
            ∀l1 l2. PERM l1 l2 ⇒ P l1 l2
   
   [PERM_SUM]  Theorem
      
      ⊢ ∀l1 l2. PERM l1 l2 ⇒ SUM l1 = SUM l2
   
   [PERM_SWAP_AT_FRONT]  Theorem
      
      ⊢ PERM (x::y::l1) (y::x::l2) ⇔ PERM l1 l2
   
   [PERM_SWAP_L_AT_FRONT]  Theorem
      
      ⊢ ∀x y. PERM (x ⧺ y ⧺ l1) (y ⧺ x ⧺ l2) ⇔ PERM l1 l2
   
   [PERM_SYM]  Theorem
      
      ⊢ ∀l1 l2. PERM l1 l2 ⇔ PERM l2 l1
   
   [PERM_TC]  Theorem
      
      ⊢ PERM = PERM_SINGLE_SWAP⁺
   
   [PERM_TO_APPEND_SIMPS]  Theorem
      
      ⊢ (PERM (x::l) (x::r1 ⧺ r2) ⇔ PERM l (r1 ⧺ r2)) ∧
        (PERM (x::l) (r1 ⧺ x::r2) ⇔ PERM l (r1 ⧺ r2)) ∧
        (PERM (xs ⧺ ys ⧺ zs) r ⇔ PERM (xs ⧺ (ys ⧺ zs)) r) ∧
        (PERM (x::ys ⧺ zs) r ⇔ PERM (x::(ys ⧺ zs)) r) ∧
        (PERM ([] ⧺ l) r ⇔ PERM l r) ∧
        (PERM (xs ⧺ l) (xs ⧺ r1 ⧺ r2) ⇔ PERM l (r1 ⧺ r2)) ∧
        (PERM (xs ⧺ l) (r1 ⧺ (xs ⧺ r2)) ⇔ PERM l (r1 ⧺ r2)) ∧
        (PERM [] ([] ⧺ []) ⇔ T) ∧ (PERM xs (xs ⧺ [] ⧺ []) ⇔ T) ∧
        (PERM xs ([] ⧺ (xs ⧺ [])) ⇔ T)
   
   [PERM_TRANS]  Theorem
      
      ⊢ ∀x y z. PERM x y ∧ PERM y z ⇒ PERM x z
   
   [PERM_alt]  Theorem
      
      ⊢ ∀L1 L2.
            PERM L1 L2 ⇔
            ∀x. LENGTH (FILTER ($= x) L1) = LENGTH (FILTER ($= x) L2)
   
   [PERM_lifts_equalities]  Theorem
      
      ⊢ ∀f.
            (∀x1 x2 x3. f (x1 ⧺ x2 ⧺ x3) = f (x1 ⧺ x3 ⧺ x2)) ⇒
            ∀x y. PERM x y ⇒ f x = f y
   
   [PERM_lifts_invariants]  Theorem
      
      ⊢ ∀P.
            (∀x1 x2 x3. P (x1 ⧺ x2 ⧺ x3) ⇒ P (x1 ⧺ x3 ⧺ x2)) ⇒
            ∀x y. P x ∧ PERM x y ⇒ P y
   
   [PERM_lifts_monotonicities]  Theorem
      
      ⊢ ∀f.
            (∀x1 x2 x3.
                 ∃x1' x2' x3'.
                     f (x1 ⧺ x2 ⧺ x3) = x1' ⧺ x2' ⧺ x3' ∧
                     f (x1 ⧺ x3 ⧺ x2) = x1' ⧺ x3' ⧺ x2') ⇒
            ∀x y. PERM x y ⇒ PERM (f x) (f y)
   
   [PERM_lifts_transitive_relations]  Theorem
      
      ⊢ ∀f Q.
            (∀x1 x2 x3. Q (f (x1 ⧺ x2 ⧺ x3)) (f (x1 ⧺ x3 ⧺ x2))) ∧
            transitive Q ⇒
            ∀x y. PERM x y ⇒ Q (f x) (f y)
   
   [PERM_transitive]  Theorem
      
      ⊢ transitive PERM
   
   [QSORT3_DEF]  Theorem
      
      ⊢ (∀R. QSORT3 R [] = []) ∧
        ∀tl hd R.
            QSORT3 R (hd::tl) =
            (let
               (lo,eq,hi) = PART3 R hd tl
             in
               QSORT3 R lo ⧺ hd::eq ⧺ QSORT3 R hi)
   
   [QSORT3_IND]  Theorem
      
      ⊢ ∀P.
            (∀R. P R []) ∧
            (∀R hd tl.
                 (∀lo eq hi. (lo,eq,hi) = PART3 R hd tl ⇒ P R hi) ∧
                 (∀lo eq hi. (lo,eq,hi) = PART3 R hd tl ⇒ P R lo) ⇒
                 P R (hd::tl)) ⇒
            ∀v v1. P v v1
   
   [QSORT3_MEM]  Theorem
      
      ⊢ ∀R L x. MEM x (QSORT3 R L) ⇔ MEM x L
   
   [QSORT3_SORTED]  Theorem
      
      ⊢ ∀R L. transitive R ∧ total R ⇒ SORTED R (QSORT3 R L)
   
   [QSORT3_SORTS]  Theorem
      
      ⊢ ∀R. transitive R ∧ total R ⇒ SORTS QSORT3 R
   
   [QSORT3_SPLIT]  Theorem
      
      ⊢ ∀R.
            transitive R ∧ total R ⇒
            ∀l e.
                QSORT3 R l =
                QSORT3 R (FILTER (λx. R x e ∧ ¬R e x) l) ⧺
                FILTER (λx. R x e ∧ R e x) l ⧺
                QSORT3 R (FILTER (λx. ¬R x e) l)
   
   [QSORT3_STABLE]  Theorem
      
      ⊢ ∀R. transitive R ∧ total R ⇒ STABLE QSORT3 R
   
   [QSORT_DEF]  Theorem
      
      ⊢ (∀ord. QSORT ord [] = []) ∧
        ∀t ord h.
            QSORT ord (h::t) =
            (let
               (l1,l2) = PARTITION (λy. ord y h) t
             in
               QSORT ord l1 ⧺ [h] ⧺ QSORT ord l2)
   
   [QSORT_IND]  Theorem
      
      ⊢ ∀P.
            (∀ord. P ord []) ∧
            (∀ord h t.
                 (∀l1 l2. (l1,l2) = PARTITION (λy. ord y h) t ⇒ P ord l2) ∧
                 (∀l1 l2. (l1,l2) = PARTITION (λy. ord y h) t ⇒ P ord l1) ⇒
                 P ord (h::t)) ⇒
            ∀v v1. P v v1
   
   [QSORT_MEM]  Theorem
      
      ⊢ ∀R L x. MEM x (QSORT R L) ⇔ MEM x L
   
   [QSORT_PERM]  Theorem
      
      ⊢ ∀R L. PERM L (QSORT R L)
   
   [QSORT_SORTED]  Theorem
      
      ⊢ ∀R L. transitive R ∧ total R ⇒ SORTED R (QSORT R L)
   
   [QSORT_SORTS]  Theorem
      
      ⊢ ∀R. transitive R ∧ total R ⇒ SORTS QSORT R
   
   [QSORT_eq_if_PERM]  Theorem
      
      ⊢ ∀R.
            total R ∧ transitive R ∧ antisymmetric R ⇒
            ∀l1 l2. QSORT R l1 = QSORT R l2 ⇔ PERM l1 l2
   
   [SORTED_ALL_DISTINCT]  Theorem
      
      ⊢ irreflexive R ∧ transitive R ⇒ ∀ls. SORTED R ls ⇒ ALL_DISTINCT ls
   
   [SORTED_APPEND]  Theorem
      
      ⊢ ∀R L1 L2.
            transitive R ∧ SORTED R L1 ∧ SORTED R L2 ∧
            (∀x y. MEM x L1 ∧ MEM y L2 ⇒ R x y) ⇒
            SORTED R (L1 ⧺ L2)
   
   [SORTED_APPEND_IFF]  Theorem
      
      ⊢ ∀R L1 L2.
            SORTED R (L1 ⧺ L2) ⇔
            SORTED R L1 ∧ SORTED R L2 ∧
            (L1 = [] ∨ L2 = [] ∨ R (LAST L1) (HD L2))
   
   [SORTED_DEF]  Theorem
      
      ⊢ (∀R. SORTED R [] ⇔ T) ∧ (∀x R. SORTED R [x] ⇔ T) ∧
        ∀y x rst R. SORTED R (x::y::rst) ⇔ R x y ∧ SORTED R (y::rst)
   
   [SORTED_EL_LESS]  Theorem
      
      ⊢ ∀R.
            transitive R ⇒
            ∀ls.
                SORTED R ls ⇔
                ∀m n. m < n ∧ n < LENGTH ls ⇒ R (EL m ls) (EL n ls)
   
   [SORTED_EL_SUC]  Theorem
      
      ⊢ ∀R ls.
            SORTED R ls ⇔
            ∀n. SUC n < LENGTH ls ⇒ R (EL n ls) (EL (SUC n) ls)
   
   [SORTED_EQ]  Theorem
      
      ⊢ ∀R L x.
            transitive R ⇒
            (SORTED R (x::L) ⇔ SORTED R L ∧ ∀y. MEM y L ⇒ R x y)
   
   [SORTED_EQ_PART]  Theorem
      
      ⊢ ∀l R. transitive R ⇒ SORTED R (FILTER (λx. R x hd ∧ R hd x) l)
   
   [SORTED_FILTER]  Theorem
      
      ⊢ ∀R ls P. transitive R ∧ SORTED R ls ⇒ SORTED R (FILTER P ls)
   
   [SORTED_GENLIST_PLUS]  Theorem
      
      ⊢ ∀n k. SORTED $< (GENLIST ($+ k) n)
   
   [SORTED_IND]  Theorem
      
      ⊢ ∀P.
            (∀R. P R []) ∧ (∀R x. P R [x]) ∧
            (∀R x y rst. P R (y::rst) ⇒ P R (x::y::rst)) ⇒
            ∀v v1. P v v1
   
   [SORTED_NIL]  Theorem
      
      ⊢ ∀R. SORTED R []
   
   [SORTED_PERM_EQ]  Theorem
      
      ⊢ ∀R.
            transitive R ∧ antisymmetric R ⇒
            ∀l1 l2. SORTED R l1 ∧ SORTED R l2 ∧ PERM l1 l2 ⇒ l1 = l2
   
   [SORTED_SING]  Theorem
      
      ⊢ ∀R x. SORTED R [x]
   
   [SORTED_TL]  Theorem
      
      ⊢ SORTED R (x::xs) ⇒ SORTED R xs
   
   [SORTED_weaken]  Theorem
      
      ⊢ ∀R R' ls.
            SORTED R ls ∧ (∀x y. MEM x ls ∧ MEM y ls ∧ R x y ⇒ R' x y) ⇒
            SORTED R' ls
   
   [SUM_IMAGE_count_MULT]  Theorem
      
      ⊢ (∀m. m < n ⇒ g m = ∑ (λx. f (x + k * m)) (count k)) ⇒
        ∑ f (count (k * n)) = ∑ g (count n)
   
   [SUM_IMAGE_count_SUM_GENLIST]  Theorem
      
      ⊢ ∑ f (count n) = SUM (GENLIST f n)
   
   [less_sorted_eq]  Theorem
      
      ⊢ ∀L x. SORTED $< (x::L) ⇔ SORTED $< L ∧ ∀y. MEM y L ⇒ x < y
   
   [sorted_count_list]  Theorem
      
      ⊢ ∀n. SORTED $<= (COUNT_LIST n)
   
   [sorted_filter]  Theorem
      
      ⊢ ∀R ls. transitive R ⇒ SORTED R ls ⇒ SORTED R (FILTER P ls)
   
   [sorted_map]  Theorem
      
      ⊢ ∀R f l.
            transitive R ⇒ (SORTED R (MAP f l) ⇔ SORTED (inv_image R f) l)
   
   [sorted_perm_count_list]  Theorem
      
      ⊢ ∀y f l n.
            SORTED (inv_image $<= f) l ∧ PERM (MAP f l) (COUNT_LIST n) ⇒
            MAP f l = COUNT_LIST n
   
   [sum_of_sums]  Theorem
      
      ⊢ ∑ (λm. ∑ (f m) (count a)) (count b) =
        ∑ (λm. f (m DIV a) (m MOD a)) (count (a * b))
   
   
*)
end

HOL 4, Kananaskis-13