Package hol-sort: HOL sorting theories

Information

namehol-sort
version1.0
descriptionHOL sorting theories
authorHOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
licenseMIT
checksum2a19552fa096e1ae820a442a23ebdf3cf7723373
requiresbase
hol-base
showData.Bool
Data.List
Data.Pair
Function
HOL4
Number.Natural
Relation

Files

Defined Constants

Theorems

relation.equivalence sorting.PERM

transitive sorting.PERM

sorting.PERM = relation.EQC sorting.PERM_SINGLE_SWAP

sorting.PERM = relation.RTC sorting.PERM_SINGLE_SWAP

sorting.PERM = transitiveClosure sorting.PERM_SINGLE_SWAP

sorting.PERM ls (reverse ls)

L. sorting.PERM L L

l. sorting.PERM_SINGLE_SWAP l l

R. sorting.SORTED R []

n. sorting.SORTED () (rich_list.COUNT_LIST n)

sorting.PERM (list.SET_TO_LIST (pred_set.count n))
    (rich_list.COUNT_LIST n)

sorting.PERM_SINGLE_SWAP (x2 @ x3) (x3 @ x2)

l R. sorting.PERM l (sorting.QSORT3 R l)

R x. sorting.SORTED R (x :: [])

R l. sorting.PERM l (mergesort.mergesort R l)

R L. sorting.PERM L (sorting.QSORT R L)

n k. sorting.SORTED (<) (list.GENLIST ((+) k) n)

pred_set.SUM_IMAGE f (pred_set.count n) = list.SUM (list.GENLIST f n)

sorting.SORTED R (x :: xs) sorting.SORTED R xs

ls.
    list.ALL_DISTINCT ls
    sorting.PERM ls (list.SET_TO_LIST (list.LIST_TO_SET ls))

l1 l2. sorting.PERM l1 l2 sorting.PERM l2 l1

l1 l2. sorting.PERM_SINGLE_SWAP l1 l2 sorting.PERM_SINGLE_SWAP l2 l1

x y. x = y sorting.PERM x y

l1 l2. sorting.PERM (l1 @ l2) (l2 @ l1)

R. transitive R relation.total R sorting.SORTS sorting.QSORT R

R. transitive R relation.total R sorting.SORTS sorting.QSORT3 R

R.
    transitive R relation.total R sorting.STABLE mergesort.mergesort R

R. transitive R relation.total R sorting.STABLE sorting.QSORT3 R

x x1. sorting.SORTED x x1 sorting.SORTED_tupled (x, x1)

x x1. sorting.QSORT x x1 = sorting.QSORT_tupled (x, x1)

x x1. sorting.QSORT3 x x1 = sorting.QSORT3_tupled (x, x1)

sorting.PERM_SINGLE_SWAP M N sorting.PERM_SINGLE_SWAP (x :: M) (x :: N)

sorting.PERM_SINGLE_SWAP ((x1 @ x2) @ x3) ((x1 @ x3) @ x2)

x y. sorting.PERM x y sorting.PERM x = sorting.PERM y

l1 l2.
    sorting.PERM l1 l2 (list.ALL_DISTINCT l1 list.ALL_DISTINCT l2)

l1 l2. sorting.PERM l1 l2 length l1 = length l2

l1 l2. sorting.PERM l1 l2 list.LIST_TO_SET l1 = list.LIST_TO_SET l2

l1 l2. sorting.PERM (l1 @ l2) = sorting.PERM (l2 @ l1)

l1 l2. sorting.PERM l1 l2 list.SUM l1 = list.SUM l2

P l. sorting.PARTITION P l = sorting.PART P l [] []

R l. mergesort.mergesort R l = mergesort.mergesortN R (length l) l

filter ((=) x) l = rich_list.REPLICATE (length (filter ((=) x) l)) x

R n l. sorting.PERM (list.TAKE n l) (mergesort.mergesortN R n l)

R l1 l2. sorting.PERM (l1 @ l2) (mergesort.merge R l1 l2)

R l.
    mergesort.mergesort_tail R l =
    mergesort.mergesortN_tail R (length l) l

R x y. relation.total R sorting.SORTED R (mergesort.sort2 R x y)

irreflexive R transitive R
  ls. sorting.SORTED R ls list.ALL_DISTINCT ls

P l. sorting.PERM l (filter P l @ filter ((¬) P) l)

%%genvar%%7817 l.
    transitive %%genvar%%7817 relation.total %%genvar%%7817
    sorting.SORTED %%genvar%%7817 (mergesort.mergesort %%genvar%%7817 l)

R L.
    transitive R relation.total R sorting.SORTED R (sorting.QSORT R L)

R L.
    transitive R relation.total R sorting.SORTED R (sorting.QSORT3 R L)

R x y. sorting.PERM (x :: y :: []) (mergesort.sort2 R x y)

R ls.
    transitive R sorting.SORTED R ls sorting.SORTED R (filter P ls)

%%genvar%%9194 l.
    transitive %%genvar%%9194 relation.total %%genvar%%9194
    mergesort.stable %%genvar%%9194 l
      (mergesort.mergesort %%genvar%%9194 l)

sorting.PERM (x :: y :: l1) (y :: x :: l2) sorting.PERM l1 l2

x l2 l1. sorting.PERM (x :: l1) (x :: l2) sorting.PERM l1 l2

l1 l2 x. sorting.PERM l1 l2 sorting.PERM (x :: l1) (x :: l2)

A B C. sorting.PERM (A @ B) C sorting.PERM (B @ A) C

%%genvar%%648 y z.
    sorting.PERM %%genvar%%648 y sorting.PERM y z
    sorting.PERM %%genvar%%648 z

f l1 l2. sorting.PERM l1 l2 sorting.PERM (map f l1) (map f l2)

P l1 l2. sorting.PERM l1 l2 sorting.PERM (filter P l1) (filter P l2)

R x y. mergesort.stable R (x :: y :: []) (mergesort.sort2 R x y)

x x1 x2.
    mergesort.mergesortN x x1 x2 = mergesort.mergesortN_tupled (x, x1, x2)

%%genvar%%9316 L x.
    bool.IN x (list.LIST_TO_SET (mergesort.mergesort %%genvar%%9316 L))
    bool.IN x (list.LIST_TO_SET L)

R L x.
    bool.IN x (list.LIST_TO_SET (sorting.QSORT R L))
    bool.IN x (list.LIST_TO_SET L)

R L x.
    bool.IN x (list.LIST_TO_SET (sorting.QSORT3 R L))
    bool.IN x (list.LIST_TO_SET L)

x x1 x2. mergesort.merge x x1 x2 = mergesort.merge_tupled (x, x1, x2)

M N.
    transitiveClosure sorting.PERM_SINGLE_SWAP M N
    transitiveClosure sorting.PERM_SINGLE_SWAP (x :: M) (x :: N)

R x y z. relation.total R sorting.SORTED R (mergesort.sort3 R x y z)

R l.
    relation.total R transitive R
    mergesort.mergesort_tail R l = mergesort.mergesort R l

L. (sorting.PERM L [] L = []) (sorting.PERM [] L L = [])

R n l.
    relation.total R transitive R
    sorting.SORTED R (mergesort.mergesortN R n l)

R ls P.
    transitive R sorting.SORTED R ls sorting.SORTED R (filter P ls)

(sorting.PERM (reverse l1) l2 sorting.PERM l1 l2)
  (sorting.PERM l1 (reverse l2) sorting.PERM l1 l2)

x y l. sorting.PERM (x :: y :: l) = sorting.PERM (y :: x :: l)

%%genvar%%4417 l1 l2.
    sorting.PERM (l1 @ %%genvar%%4417 :: l2) =
    sorting.PERM ((%%genvar%%4417 :: l1) @ l2)

L1 L2. sorting.PERM L1 L2 x. filter ((=) x) L1 = filter ((=) x) L2

l1 l2.
    sorting.PERM l1 l2
    a. bool.IN a (list.LIST_TO_SET l1) bool.IN a (list.LIST_TO_SET l2)

l R. transitive R sorting.SORTED R (filter (λx. R x hd R hd x) l)

R l acc. mergesort.merge R l [] = l mergesort.merge R [] l = l

x y. sorting.PERM ((x @ y) @ l1) ((y @ x) @ l2) sorting.PERM l1 l2

R f l.
    transitive R
    (sorting.SORTED R (map f l)
     sorting.SORTED (relation.inv_image R f) l)

R x y z. sorting.PERM (x :: y :: z :: []) (mergesort.sort3 R x y z)

x l1 l2.
    sorting.PERM l1 = sorting.PERM l2
    sorting.PERM (x :: l1) = sorting.PERM (x :: l2)

l l1 l2.
    sorting.PERM l1 = sorting.PERM l2
    sorting.PERM (l @ l1) = sorting.PERM (l @ l2)

L1 L2.
    sorting.PERM L1 L2
    x. length (filter ((=) x) L1) = length (filter ((=) x) L2)

R n l.
    relation.total R transitive R
    mergesort.stable R (list.TAKE n l) (mergesort.mergesortN R n l)

f R.
    sorting.SORTS f R
    l. sorting.PERM l (f R l) sorting.SORTED R (f R l)

x x1 x2 x3.
    mergesort.mergesortN_tail x x1 x2 x3 =
    mergesort.mergesortN_tail_tupled (x, x1, x2, x3)

R l1 l2 l3.
    mergesort.stable R l1 l2 mergesort.stable R l2 l3
    mergesort.stable R l1 l3

R l1 l2.
    transitive R sorting.SORTED R l1
    mergesort.stable R (l1 @ l2) (mergesort.merge R l1 l2)

x L M N. sorting.PERM L (M @ N) sorting.PERM (x :: L) (M @ x :: N)

%%genvar%%4726 l1' l2 l2'.
    sorting.PERM %%genvar%%4726 l1' sorting.PERM l2 l2'
    (sorting.PERM %%genvar%%4726 l2 sorting.PERM l1' l2')

l r l1 l2.
    sorting.PERM l r
    (sorting.PERM (l @ l1) l2 sorting.PERM (r @ l1) l2)

%%genvar%%4749 l1 l1' l2.
    sorting.PERM %%genvar%%4749 (l1 @ l2) sorting.PERM l1' l1
    sorting.PERM %%genvar%%4749 (l1' @ l2)

L1 L2 L3 L4.
    sorting.PERM L1 L3 sorting.PERM L2 L4
    sorting.PERM (L1 @ L2) (L3 @ L4)

length (filter ((=) x) l1) = length (filter ((=) x) l2)
  filter ((=) x) l1 = filter ((=) x) l2

pred_set.SUM_IMAGE (λm. pred_set.SUM_IMAGE (f m) (pred_set.count a))
    (pred_set.count b) =
  pred_set.SUM_IMAGE (λm. f (m div a) (m mod a)) (pred_set.count (a * b))

L x.
    sorting.SORTED (<) (x :: L)
    sorting.SORTED (<) L y. bool.IN y (list.LIST_TO_SET L) x < y

R ls.
    sorting.SORTED R ls
    n. suc n < length ls R (list.EL n ls) (list.EL (suc n) ls)

neg R x y.
    mergesort.sort2_tail neg R x y =
    if neg then reverse (mergesort.sort2 R x y) else mergesort.sort2 R x y

P Q l. all (λx. P x ¬Q x) l sorting.PERM l (filter P l @ filter Q l)

(sorting.PERM L (x :: []) L = x :: [])
  (sorting.PERM (x :: []) L L = x :: [])

l1 l2.
    list.ALL_DISTINCT l1 list.ALL_DISTINCT l2
    (a.
       bool.IN a (list.LIST_TO_SET l1) bool.IN a (list.LIST_TO_SET l2))
    sorting.PERM l1 l2

R x y.
    mergesort.sort2 R x y = if R x y then x :: y :: [] else y :: x :: []

x x1 x2 x3 x4.
    mergesort.merge_tail x x1 x2 x3 x4 =
    mergesort.merge_tail_tupled (x, x1, x2, x3, x4)

R l1 l2.
    transitive R relation.total R sorting.SORTED R l1
    sorting.SORTED R l2 sorting.SORTED R (mergesort.merge R l1 l2)

R.
    relation.total R transitive R relation.antisymmetric R
    l1 l2. sorting.QSORT R l1 = sorting.QSORT R l2 sorting.PERM l1 l2

y l1 x l2.
    sorting.PERM l1 = sorting.PERM (x :: l2)
    sorting.PERM (y :: l1) = sorting.PERM (x :: y :: l2)

y l1 l2 l3.
    sorting.PERM l1 = sorting.PERM (l2 @ l3)
    sorting.PERM (y :: l1) = sorting.PERM (l2 @ y :: l3)

y f l n.
    sorting.SORTED (relation.inv_image () f) l
    sorting.PERM (map f l) (rich_list.COUNT_LIST n)
    map f l = rich_list.COUNT_LIST n

L h.
    sorting.PERM (h :: t) L M N. L = M @ h :: N sorting.PERM t (M @ N)

l l1 x l2.
    sorting.PERM l1 = sorting.PERM (x :: l2)
    sorting.PERM (l @ l1) = sorting.PERM (x :: l @ l2)

l l1 x l2.
    sorting.PERM l1 = sorting.PERM (x :: l2)
    sorting.PERM (l1 @ l) = sorting.PERM (x :: l2 @ l)

%%genvar%%4718 l1' l2 l2'.
    sorting.PERM %%genvar%%4718 = sorting.PERM l1'
    sorting.PERM l2 = sorting.PERM l2'
    (sorting.PERM %%genvar%%4718 l2 sorting.PERM l1' l2')

l1 l2 l3 l4.
    sorting.PERM l1 = sorting.PERM (l2 @ l3)
    sorting.PERM (l1 @ l4) = sorting.PERM (l2 @ l3 @ l4)

l1 l2 l3 l4.
    sorting.PERM l1 = sorting.PERM (l2 @ l3)
    sorting.PERM (l4 @ l1) = sorting.PERM (l2 @ l4 @ l3)

f l1 l2 e.
    combin.ASSOC f combin.COMM f sorting.PERM l1 l2
    list.FOLDR f e l1 = list.FOLDR f e l2

neg R l1 l2 acc.
    (neg )
    mergesort.merge_tail neg R l1 l2 acc =
    reverse (mergesort.merge R l1 l2) @ acc

R l1 l2 l3 l4.
    mergesort.stable R l1 l2 mergesort.stable R l3 l4
    mergesort.stable R (l1 @ l3) (l2 @ l4)

R.
    transitive R relation.antisymmetric R
    l1 l2.
      sorting.SORTED R l1 sorting.SORTED R l2 sorting.PERM l1 l2
      l1 = l2

R x y z.
    relation.total R transitive R
    mergesort.stable R (x :: y :: z :: []) (mergesort.sort3 R x y z)

%%genvar%%4734 l1 l1' l2 l2'.
    sorting.PERM l1 (%%genvar%%4734 @ l1')
    sorting.PERM l2 (%%genvar%%4734 @ l2')
    (sorting.PERM l1 l2 sorting.PERM l1' l2')

l1 l2.
    sorting.PERM_SINGLE_SWAP l1 l2
    x1 x2 x3. l1 = (x1 @ x2) @ x3 l2 = (x1 @ x3) @ x2

l1 l1' l2 l2'.
    sorting.PERM l1 = sorting.PERM l1'
    sorting.PERM l2 = sorting.PERM l2'
    sorting.PERM (l1 @ l2) = sorting.PERM (l1' @ l2')

R L x.
    transitive R
    (sorting.SORTED R (x :: L)
     sorting.SORTED R L y. bool.IN y (list.LIST_TO_SET L) R x y)

neg R x y z.
    mergesort.sort3_tail neg R x y z =
    if neg then reverse (mergesort.sort3 R x y z)
    else mergesort.sort3 R x y z

neg R x y.
    mergesort.sort2_tail neg R x y =
    if ¬(R x y neg) then x :: y :: [] else y :: x :: []

negate R n l.
    relation.total R transitive R
    mergesort.mergesortN_tail negate R n l =
    if negate then reverse (mergesort.mergesortN R n l)
    else mergesort.mergesortN R n l

R.
    transitive R
    ls.
      sorting.SORTED R ls
      m n. m < n n < length ls R (list.EL m ls) (list.EL n ls)

(m.
     m < n
     g m = pred_set.SUM_IMAGE (λx. f (x + k * m)) (pred_set.count k))
  pred_set.SUM_IMAGE f (pred_set.count (k * n)) =
  pred_set.SUM_IMAGE g (pred_set.count n)

R l1 l2.
    mergesort.stable R l1 l2
    p. (x y. p x p y R x y) filter p l1 = filter p l2

R L1 L2.
    sorting.SORTED R (L1 @ L2)
    sorting.SORTED R L1 sorting.SORTED R L2
    (L1 = [] L2 = [] R (last L1) (head L2))

f.
    (x1 x2 x3. f ((x1 @ x2) @ x3) = f ((x1 @ x3) @ x2))
    x y. sorting.PERM x y f x = f y

P.
    (x1 x2 x3. P ((x1 @ x2) @ x3) P ((x1 @ x3) @ x2))
    x y. P x sorting.PERM x y P y

(l l1 l2. sorting.PERM (l @ l1) (l @ l2) sorting.PERM l1 l2)
  l l1 l2. sorting.PERM (l1 @ l) (l2 @ l) sorting.PERM l1 l2

R R' ls.
    sorting.SORTED R ls
    (x y.
       bool.IN x (list.LIST_TO_SET ls) bool.IN y (list.LIST_TO_SET ls)
       R x y R' x y) sorting.SORTED R' ls

P L l1 l2 p q.
    (p, q) = sorting.PART P L l1 l2
    length L + length l1 + length l2 = length p + length q

l h.
    sorting.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)

P L a1 a2 l1 l2.
    (a1, a2) = sorting.PART P L l1 l2
    x.
      bool.IN x (list.LIST_TO_SET (L @ l1 @ l2))
      bool.IN x (list.LIST_TO_SET (a1 @ a2))

sort r.
    sorting.STABLE sort r
    sorting.SORTS sort r
    p. (x y. p x p y r x y) l. filter p l = filter p (sort r l)

tl hd.
    sorting.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)

f Q.
    (x1 x2 x3. Q (f ((x1 @ x2) @ x3)) (f ((x1 @ x3) @ x2)))
    transitive Q x y. sorting.PERM x y Q (f x) (f y)

x a a' b b' c c'.
    (sorting.PERM a a' sorting.PERM b b' sorting.PERM c c')
    sorting.PERM x ((a @ b) @ c) sorting.PERM x ((a' @ b') @ c')

R L1 L2.
    transitive R sorting.SORTED R L1 sorting.SORTED R L2
    (x y.
       bool.IN x (list.LIST_TO_SET L1) bool.IN y (list.LIST_TO_SET L2)
       R x y) sorting.SORTED R (L1 @ L2)

(ord. sorting.QSORT ord [] = [])
  t ord h.
    sorting.QSORT ord (h :: t) =
    bool.LET
      (pair.UNCURRY
         (λl1 l2. (sorting.QSORT ord l1 @ h :: []) @ sorting.QSORT ord l2))
      (sorting.PARTITION (λy. ord y h) t)

(R. sorting.QSORT3 R [] = [])
  tl hd R.
    sorting.QSORT3 R (hd :: tl) =
    bool.LET
      (pair.UNCURRY
         (λlo.
            pair.UNCURRY
              (λeq hi.
                 (sorting.QSORT3 R lo @ hd :: eq) @ sorting.QSORT3 R hi)))
      (sorting.PART3 R hd tl)

P R l1 l2.
    transitive R (x y. P x P y R x y) sorting.SORTED R l1
    filter P (mergesort.merge R l1 l2) = filter P (l1 @ l2)

neg R l1 l2 acc.
    (neg ) transitive R sorting.SORTED R (reverse l1)
    sorting.SORTED R (reverse l2)
    mergesort.merge_tail neg R l1 l2 acc =
    mergesort.merge R (reverse l1) (reverse l2) @ acc

(R. sorting.SORTED R [] ) (x R. sorting.SORTED R (x :: []) )
  y x rst R.
    sorting.SORTED R (x :: y :: rst) R x y sorting.SORTED R (y :: rst)

P L l1 l2 p q.
    (p, q) = sorting.PART P L l1 l2
    length p length L + length l1 + length l2
    length q length L + length l1 + length l2

P.
    (R. P R []) (R x. P R (x :: []))
    (R x y rst. P R (y :: rst) P R (x :: y :: rst)) R ls. P R ls

R.
    transitive R relation.total R
    l e.
      sorting.QSORT3 R l =
      (sorting.QSORT3 R (filter (λx. R x e ¬R e x) l) @
       filter (λx. R x e R e x) l) @
      sorting.QSORT3 R (filter (λx. ¬R x e) l)

(P l1 l2. sorting.PART P [] l1 l2 = (l1, l2))
  P h rst l1 l2.
    sorting.PART P (h :: rst) l1 l2 =
    if P h then sorting.PART P rst (h :: l1) l2
    else sorting.PART P rst l1 (h :: l2)

f.
    (x1 x2 x3.
       x1' x2' x3'.
         f ((x1 @ x2) @ x3) = (x1' @ x2') @ x3'
         f ((x1 @ x3) @ x2) = (x1' @ x3') @ x2')
    x y. sorting.PERM x y sorting.PERM (f x) (f y)

sorting.SORTED_tupled =
  relation.WFREC
    (select R'.
       wellFounded R' x rst y R. R' (R, y :: rst) (R, x :: y :: rst))
    (λSORTED_tupled a.
       pair.pair_CASE a
         (λR v1.
            list.list_CASE v1 (id )
              (λx v3.
                 list.list_CASE v3 (id )
                   (λy rst. id (R x y SORTED_tupled (R, y :: rst))))))

P L A B l1 l2.
    (A, B) = sorting.PART P L l1 l2
    (x. bool.IN x (list.LIST_TO_SET l1) P x)
    (x. bool.IN x (list.LIST_TO_SET l2) ¬P x)
    (z. bool.IN z (list.LIST_TO_SET A) P z)
    z. bool.IN z (list.LIST_TO_SET B) ¬P z

P.
    (R. P R [])
    (ord h t.
       (l1 l2. (l1, l2) = sorting.PARTITION (λy. ord y h) t P ord l2)
       (l1 l2. (l1, l2) = sorting.PARTITION (λy. ord y h) t P ord l1)
       P ord (h :: t)) R ls. P R ls

P.
    (R. P R [])
    (R hd tl.
       (lo eq hi. (lo, eq, hi) = sorting.PART3 R hd tl P R hi)
       (lo eq hi. (lo, eq, hi) = sorting.PART3 R hd tl P R lo)
       P R (hd :: tl)) R ls. P R ls

(R h. sorting.PART3 R h [] = ([], [], []))
  R h hd tl.
    sorting.PART3 R h (hd :: tl) =
    if R h hd R hd h then
      pair.## id (pair.## ((::) hd) id) (sorting.PART3 R h tl)
    else if R hd h then
      pair.## ((::) hd) (pair.## id id) (sorting.PART3 R h tl)
    else pair.## id (pair.## id ((::) hd)) (sorting.PART3 R h tl)

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. sorting.PERM l1 l2 P l1 l2

R x y z.
    mergesort.sort3 R x y z =
    if R x y then
      if R y z then x :: y :: z :: []
      else if R x z then x :: z :: y :: []
      else z :: x :: y :: []
    else if R y z then
      if R x z then y :: x :: z :: [] else y :: z :: x :: []
    else z :: y :: x :: []

(R. mergesort.merge R [] [] = [])
  (v9 v8 R. mergesort.merge R (v8 :: v9) [] = v8 :: v9)
  (v5 v4 R. mergesort.merge R [] (v4 :: v5) = v4 :: v5)
  y x l2 l1 R.
    mergesort.merge R (x :: l1) (y :: l2) =
    if R x y then x :: mergesort.merge R l1 (y :: l2)
    else y :: mergesort.merge R (x :: l1) l2

P.
    (R. P R [] []) (R v8 v9. P R (v8 :: v9) [])
    (R v4 v5. P R [] (v4 :: v5))
    (R x l1 y l2.
       (¬R x y P R (x :: l1) l2) (R x y P R l1 (y :: l2))
       P R (x :: l1) (y :: l2)) R l1 l2. P R l1 l2

P.
    P [] []
    (x l1 l2. sorting.PERM l1 l2 P l1 l2 P (x :: l1) (x :: l2))
    (x y l1 l2.
       sorting.PERM l1 l2 P l1 l2 P (x :: y :: l1) (y :: x :: l2))
    (l1 l2 l3.
       sorting.PERM l1 l2 P l1 l2 sorting.PERM l2 l3 P l2 l3
       P l1 l3) l1 l2. sorting.PERM l1 l2 P l1 l2

neg R x y z.
    mergesort.sort3_tail neg R x y z =
    if ¬(R x y neg) then
      if ¬(R y z neg) then x :: y :: z :: []
      else if ¬(R x z neg) then x :: z :: y :: []
      else z :: x :: y :: []
    else if ¬(R y z neg) then
      if ¬(R x z neg) then y :: x :: z :: [] else y :: z :: x :: []
    else z :: y :: x :: []

sorting.QSORT_tupled =
  relation.WFREC
    (select R.
       wellFounded R
       (t h ord l1 l2.
          (l1, l2) = sorting.PARTITION (λy. ord y h) t
          R (ord, l2) (ord, h :: t))
       t h ord l1 l2.
         (l1, l2) = sorting.PARTITION (λy. ord y h) t
         R (ord, l1) (ord, h :: t))
    (λQSORT_tupled a.
       pair.pair_CASE a
         (λord v1.
            list.list_CASE v1 (id [])
              (λh t.
                 id
                   (bool.LET
                      (pair.UNCURRY
                         (λl1 l2.
                            (QSORT_tupled (ord, l1) @ h :: []) @
                            QSORT_tupled (ord, l2)))
                      (sorting.PARTITION (λy. ord y h) t)))))

sorting.QSORT3_tupled =
  relation.WFREC
    (select R'.
       wellFounded R'
       (tl hd R lo eq hi.
          (lo, eq, hi) = sorting.PART3 R hd tl
          R' (R, hi) (R, hd :: tl))
       tl hd R lo eq hi.
         (lo, eq, hi) = sorting.PART3 R hd tl R' (R, lo) (R, hd :: tl))
    (λQSORT3_tupled a.
       pair.pair_CASE a
         (λR v1.
            list.list_CASE v1 (id [])
              (λhd tl.
                 id
                   (bool.LET
                      (pair.UNCURRY
                         (λlo.
                            pair.UNCURRY
                              (λeq hi.
                                 (QSORT3_tupled (R, lo) @ hd :: eq) @
                                 QSORT3_tupled (R, hi))))
                      (sorting.PART3 R hd tl)))))

(negate acc R. mergesort.merge_tail negate R [] [] acc = acc)
  (v13 v12 negate acc R.
     mergesort.merge_tail negate R (v12 :: v13) [] acc =
     list.REV (v12 :: v13) acc)
  (v9 v8 negate acc R.
     mergesort.merge_tail negate R [] (v8 :: v9) acc =
     list.REV (v8 :: v9) acc)
  y x negate l2 l1 acc R.
    mergesort.merge_tail negate R (x :: l1) (y :: l2) acc =
    if ¬(R x y negate) then
      mergesort.merge_tail negate R l1 (y :: l2) (x :: acc)
    else mergesort.merge_tail negate R (x :: l1) l2 (y :: acc)

mergesort.merge_tupled =
  relation.WFREC
    (select R'.
       wellFounded R'
       (l2 l1 y x R. ¬R x y R' (R, x :: l1, l2) (R, x :: l1, y :: l2))
       l2 l1 y x R. R x y R' (R, l1, y :: l2) (R, x :: l1, y :: l2))
    (λmerge_tupled a.
       pair.pair_CASE a
         (λR v1.
            pair.pair_CASE v1
              (λv2 v3.
                 list.list_CASE v3
                   (list.list_CASE v2 (id []) (λv10 v11. id (v10 :: v11)))
                   (λy l2.
                      list.list_CASE v2 (id (y :: l2))
                        (λx l1.
                           id
                             (if R x y then
                                x :: merge_tupled (R, l1, y :: l2)
                              else y :: merge_tupled (R, x :: l1, l2)))))))

P.
    (negate R acc. P negate R [] [] acc)
    (negate R v12 v13 acc. P negate R (v12 :: v13) [] acc)
    (negate R v8 v9 acc. P negate R [] (v8 :: v9) acc)
    (negate R x l1 y l2 acc.
       (¬¬(R x y negate) P negate R (x :: l1) l2 (y :: acc))
       (¬(R x y negate) P negate R l1 (y :: l2) (x :: acc))
       P negate R (x :: l1) (y :: l2) acc)
    neg R l1 l2 acc. P neg R l1 l2 acc

mergesort.merge_tail_tupled =
  relation.WFREC
    (select R'.
       wellFounded R'
       (acc l2 l1 negate y x R.
          ¬¬(R x y negate)
          R' (negate, R, x :: l1, l2, y :: acc)
            (negate, R, x :: l1, y :: l2, acc))
       acc l2 l1 negate y x R.
         ¬(R x y negate)
         R' (negate, R, l1, y :: l2, x :: acc)
           (negate, R, x :: l1, y :: l2, acc))
    (λmerge_tail_tupled a.
       pair.pair_CASE a
         (λnegate v1.
            pair.pair_CASE v1
              (λR v3.
                 pair.pair_CASE v3
                   (λv4 v5.
                      pair.pair_CASE v5
                        (λv6 acc.
                           list.list_CASE v6
                             (list.list_CASE v4 (id acc)
                                (λv14 v15. id (list.REV (v14 :: v15) acc)))
                             (λy l2.
                                list.list_CASE v4
                                  (id (list.REV (y :: l2) acc))
                                  (λx l1.
                                     id
                                       (if ¬(R x y negate) then
                                          merge_tail_tupled
                                            (negate, R, l1, y :: l2,
                                             x :: acc)
                                        else
                                          merge_tail_tupled
                                            (negate, R, x :: l1, l2,
                                             y :: acc)))))))))

mergesort.mergesortN_tupled =
  relation.WFREC
    (select R'.
       wellFounded R'
       (l R v4 len1.
          ¬(v4 = 0) ¬(v4 = 1) ¬(v4 = arithmetic.BIT2 0) ¬(v4 = 3)
          len1 = arithmetic.DIV2 v4
          R' (R, arithmetic.DIV2 v4, l) (R, v4, l))
       l R v4 len1.
         ¬(v4 = 0) ¬(v4 = 1) ¬(v4 = arithmetic.BIT2 0) ¬(v4 = 3)
         len1 = arithmetic.DIV2 v4
         R' (R, arithmetic.- v4 len1, list.DROP len1 l) (R, v4, l))
    (λmergesortN_tupled a.
       pair.pair_CASE a
         (λR v1.
            pair.pair_CASE v1
              (λv2 l.
                 bool.literal_case
                   (λn.
                      if n = 0 then id []
                      else if n = 1 then
                        list.list_CASE l (id []) (λx l'. id (x :: []))
                      else if n = arithmetic.BIT2 0 then
                        list.list_CASE l (id [])
                          (λx' v17.
                             list.list_CASE v17 (id (x' :: []))
                               (λy l''. id (mergesort.sort2 R x' y)))
                      else if n = 3 then
                        list.list_CASE l (id [])
                          (λx'' v25.
                             list.list_CASE v25 (id (x'' :: []))
                               (λy' v29.
                                  list.list_CASE v29
                                    (id (mergesort.sort2 R x'' y'))
                                    (λz l'''.
                                       id (mergesort.sort3 R x'' y' z))))
                      else
                        id
                          (bool.LET
                             (λlen1.
                                mergesort.merge R
                                  (mergesortN_tupled
                                     (R, arithmetic.DIV2 n, l))
                                  (mergesortN_tupled
                                     (R, arithmetic.- n len1,
                                      list.DROP len1 l)))
                             (arithmetic.DIV2 n))) v2)))

P.
    (R l. P R 0 l) (R x l. P R 1 (x :: l)) (R. P R 1 [])
    (R x y l. P R (arithmetic.BIT2 0) (x :: y :: l))
    (R x. P R (arithmetic.BIT2 0) (x :: []))
    (R. P R (arithmetic.BIT2 0) [])
    (R x y z l. P R 3 (x :: y :: z :: l))
    (R x y. P R 3 (x :: y :: [])) (R x. P R 3 (x :: []))
    (R. P R 3 [])
    (R v4 l.
       (len1.
          ¬(v4 = 0) ¬(v4 = 1) ¬(v4 = arithmetic.BIT2 0) ¬(v4 = 3)
          len1 = arithmetic.DIV2 v4 P R (arithmetic.DIV2 v4) l)
       (len1.
          ¬(v4 = 0) ¬(v4 = 1) ¬(v4 = arithmetic.BIT2 0) ¬(v4 = 3)
          len1 = arithmetic.DIV2 v4
          P R (arithmetic.- v4 len1) (list.DROP len1 l)) P R v4 l)
    v v1 v2. P v v1 v2

(l R. mergesort.mergesortN R 0 l = [])
  (x l R. mergesort.mergesortN R 1 (x :: l) = x :: [])
  (R. mergesort.mergesortN R 1 [] = [])
  (y x l R.
     mergesort.mergesortN R (arithmetic.BIT2 0) (x :: y :: l) =
     mergesort.sort2 R x y)
  (x R. mergesort.mergesortN R (arithmetic.BIT2 0) (x :: []) = x :: [])
  (R. mergesort.mergesortN R (arithmetic.BIT2 0) [] = [])
  (z y x l R.
     mergesort.mergesortN R 3 (x :: y :: z :: l) =
     mergesort.sort3 R x y z)
  (y x R.
     mergesort.mergesortN R 3 (x :: y :: []) = mergesort.sort2 R x y)
  (x R. mergesort.mergesortN R 3 (x :: []) = x :: [])
  (R. mergesort.mergesortN R 3 [] = [])
  v4 l R.
    mergesort.mergesortN R v4 l =
    if v4 = 0 then []
    else if v4 = 1 then list.list_CASE l [] (λx l'. x :: [])
    else if v4 = arithmetic.BIT2 0 then
      list.list_CASE l []
        (λx' v17.
           list.list_CASE v17 (x' :: []) (λy l''. mergesort.sort2 R x' y))
    else if v4 = 3 then
      list.list_CASE l []
        (λx'' v25.
           list.list_CASE v25 (x'' :: [])
             (λy' v29.
                list.list_CASE v29 (mergesort.sort2 R x'' y')
                  (λz l'''. mergesort.sort3 R x'' y' z)))
    else
      bool.LET
        (λlen1.
           mergesort.merge R
             (mergesort.mergesortN R (arithmetic.DIV2 v4) l)
             (mergesort.mergesortN R (arithmetic.- v4 len1)
                (list.DROP len1 l))) (arithmetic.DIV2 v4)

mergesort.mergesortN_tail_tupled =
  relation.WFREC
    (select R'.
       wellFounded R'
       (l R negate v6 len1 neg.
          ¬(v6 = 0) ¬(v6 = 1) ¬(v6 = arithmetic.BIT2 0) ¬(v6 = 3)
          len1 = arithmetic.DIV2 v6 (neg ¬negate)
          R' (neg, R, arithmetic.DIV2 v6, l) (negate, R, v6, l))
       l R negate v6 len1 neg.
         ¬(v6 = 0) ¬(v6 = 1) ¬(v6 = arithmetic.BIT2 0) ¬(v6 = 3)
         len1 = arithmetic.DIV2 v6 (neg ¬negate)
         R' (neg, R, arithmetic.- v6 len1, list.DROP len1 l)
           (negate, R, v6, l))
    (λmergesortN_tail_tupled a.
       pair.pair_CASE a
         (λnegate v1.
            pair.pair_CASE v1
              (λR v3.
                 pair.pair_CASE v3
                   (λv4 l.
                      bool.literal_case
                        (λn.
                           if n = 0 then id []
                           else if n = 1 then
                             list.list_CASE l (id []) (λx l'. id (x :: []))
                           else if n = arithmetic.BIT2 0 then
                             list.list_CASE l (id [])
                               (λx' v19.
                                  list.list_CASE v19 (id (x' :: []))
                                    (λy l''.
                                       id
                                         (mergesort.sort2_tail negate R x'
                                            y)))
                           else if n = 3 then
                             list.list_CASE l (id [])
                               (λx'' v27.
                                  list.list_CASE v27 (id (x'' :: []))
                                    (λy' v31.
                                       list.list_CASE v31
                                         (id
                                            (mergesort.sort2_tail negate R
                                               x'' y'))
                                         (λz l'''.
                                            id
                                              (mergesort.sort3_tail negate
                                                 R x'' y' z))))
                           else
                             id
                               (bool.LET
                                  (λlen1.
                                     bool.LET
                                       (λneg.
                                          mergesort.merge_tail neg R
                                            (mergesortN_tail_tupled
                                               (neg, R, arithmetic.DIV2 n,
                                                l))
                                            (mergesortN_tail_tupled
                                               (neg, R,
                                                arithmetic.- n len1,
                                                list.DROP len1 l)) [])
                                       (¬negate)) (arithmetic.DIV2 n)))
                        v4))))

P.
    (negate R l. P negate R 0 l)
    (negate R x l. P negate R 1 (x :: l)) (negate R. P negate R 1 [])
    (negate R x y l. P negate R (arithmetic.BIT2 0) (x :: y :: l))
    (negate R x. P negate R (arithmetic.BIT2 0) (x :: []))
    (negate R. P negate R (arithmetic.BIT2 0) [])
    (negate R x y z l. P negate R 3 (x :: y :: z :: l))
    (negate R x y. P negate R 3 (x :: y :: []))
    (negate R x. P negate R 3 (x :: [])) (negate R. P negate R 3 [])
    (negate R v6 l.
       (len1 neg.
          ¬(v6 = 0) ¬(v6 = 1) ¬(v6 = arithmetic.BIT2 0) ¬(v6 = 3)
          len1 = arithmetic.DIV2 v6 (neg ¬negate)
          P neg R (arithmetic.DIV2 v6) l)
       (len1 neg.
          ¬(v6 = 0) ¬(v6 = 1) ¬(v6 = arithmetic.BIT2 0) ¬(v6 = 3)
          len1 = arithmetic.DIV2 v6 (neg ¬negate)
          P neg R (arithmetic.- v6 len1) (list.DROP len1 l))
       P negate R v6 l) negate R n l. P negate R n l

(negate l R. mergesort.mergesortN_tail negate R 0 l = [])
  (x negate l R.
     mergesort.mergesortN_tail negate R 1 (x :: l) = x :: [])
  (negate R. mergesort.mergesortN_tail negate R 1 [] = [])
  (y x negate l R.
     mergesort.mergesortN_tail negate R (arithmetic.BIT2 0) (x :: y :: l) =
     mergesort.sort2_tail negate R x y)
  (x negate R.
     mergesort.mergesortN_tail negate R (arithmetic.BIT2 0) (x :: []) =
     x :: [])
  (negate R.
     mergesort.mergesortN_tail negate R (arithmetic.BIT2 0) [] = [])
  (z y x negate l R.
     mergesort.mergesortN_tail negate R 3 (x :: y :: z :: l) =
     mergesort.sort3_tail negate R x y z)
  (y x negate R.
     mergesort.mergesortN_tail negate R 3 (x :: y :: []) =
     mergesort.sort2_tail negate R x y)
  (x negate R. mergesort.mergesortN_tail negate R 3 (x :: []) = x :: [])
  (negate R. mergesort.mergesortN_tail negate R 3 [] = [])
  v6 negate l R.
    mergesort.mergesortN_tail negate R v6 l =
    if v6 = 0 then []
    else if v6 = 1 then list.list_CASE l [] (λx l'. x :: [])
    else if v6 = arithmetic.BIT2 0 then
      list.list_CASE l []
        (λx' v19.
           list.list_CASE v19 (x' :: [])
             (λy l''. mergesort.sort2_tail negate R x' y))
    else if v6 = 3 then
      list.list_CASE l []
        (λx'' v27.
           list.list_CASE v27 (x'' :: [])
             (λy' v31.
                list.list_CASE v31 (mergesort.sort2_tail negate R x'' y')
                  (λz l'''. mergesort.sort3_tail negate R x'' y' z)))
    else
      bool.LET
        (λlen1.
           bool.LET
             (λneg.
                mergesort.merge_tail neg R
                  (mergesort.mergesortN_tail neg R (arithmetic.DIV2 v6) l)
                  (mergesort.mergesortN_tail neg R (arithmetic.- v6 len1)
                     (list.DROP len1 l)) []) (¬negate))
        (arithmetic.DIV2 v6)

External Type Operators

External Constants

Assumptions

transitive (<)

wellFounded (<)

prim_rec.measure = relation.inv_image (<)

pred_set.count 0 = pred_set.EMPTY

x. x = x

t. t

n. pred_set.FINITE (pred_set.count n)

n. 0 n

l. pred_set.FINITE (list.LIST_TO_SET l)

m. wellFounded (prim_rec.measure m)

R. relation.equivalence (relation.EQC R)

list.TAKE 0 l = []

¬¬p p

x. ¬bool.IN x pred_set.EMPTY

x. id x = x

t. t ¬t

x. marker.Abbrev x x

n. ¬(n < 0)

n. 0 < suc n

(¬) = λt. t

() = λP. P ((select) P)

a. x. x = a

t. (x. t) t

t. (λx. t x) = t

() = λP. P = λx.

¬(p q) p

x. x = x

t. ¬¬t t

c. arithmetic.- c c = 0

n. n * 0 = 0

m. m + 0 = m

l. reverse (reverse l) = l

l. l @ [] = l

flip = λf x y. f y x

¬(p q) ¬q

¬(p q) ¬p

¬(p q) ¬q

A. A ¬A

t. ¬t t

t. (t ) ¬t

n. rich_list.COUNT_LIST n = list.GENLIST id n

l. length (reverse l) = length l

l. list.TAKE (length l) l = l

s. pred_set.FINITE s list.ALL_DISTINCT (list.SET_TO_LIST s)

Combinator.s = λf g x. f x (g x)

lab argument. marker.:- lab argument argument

m n. m m + n

() = λp q. p q p

() (pair.UNCURRY f) () (() f)

t. t t

t. (t ) (t )

n. arithmetic.DIV2 n = n div arithmetic.BIT2 0

n. suc n = 1 + n

x. (fst x, snd x) = x

R. relation.EQC R = relation.RC (transitiveClosure (relation.SC R))

R. transitive R transitiveClosure R = R

x y. fst (x, y) = x

x y. snd (x, y) = y

h t. head (h :: t) = h

a1 a0. ¬([] = a0 :: a1)

a1 a0. ¬(a0 :: a1 = [])

f x. bool.literal_case f x = f x

f x. bool.LET f x = f x

P x. P x P ((select) P)

¬( ) ¬( )

f (λx. g x) = λx. f (g x)

flip (λx. f x) y = λx. f x y

pair.pair_CASE (x, y) f = f x y

x. q r. x = (q, r)

x y. x = y y = x

x y. x = y y = x

t1 t2. t1 t2 t2 t1

A B. A B B A

m n. m * n = n * m

m n. m + n = n + m

R f. transitive R transitive (relation.inv_image R f)

R. irreflexive R x. ¬R x x

R f. wellFounded R wellFounded (relation.inv_image R f)

P (bool.LET f v) = bool.LET (P f) v

bool.LET f v x = bool.LET (flip f x) v

f pair.UNCURRY g = pair.UNCURRY (() f g)

(¬A ) (A )

Combinator.s f (λx. g x) = λx. f x (g x)

f g. f g = λx. f (g x)

m n. m < n suc m n

m n. m < n m < suc n

m n. ¬(m < n) n m

m n. bool.IN m (pred_set.count n) m < n

m. m = 0 n. m = suc n

L1 L2. list.REV L1 L2 = reverse L1 @ L2

() = λp q. (λf. f p q) = λf. f

flip (pair.UNCURRY f) x = pair.UNCURRY (flip (flip f) x)

P. ¬(x. P x) y. ¬P y

P. ¬(x. P x) y. ¬P y

() = λP. q. (x. P x q) q

x l. list.SNOC x l = l @ x :: []

m n. ¬(m n) suc n m

m n. bool.IN m (list.LIST_TO_SET (rich_list.COUNT_LIST n)) m < n

m n. suc m = suc n m = n

m n. suc m < suc n m < n

n m. suc n suc m n m

m n. arithmetic.- m n = 0 m n

x l. list.SUM (list.SNOC x l) = list.SUM l + x

n. 0 < n k. k div n k

l P. filter P (reverse l) = reverse (filter P l)

pred_set.FINITE s
  pred_set.SUM_IMAGE f s = list.SUM (map f (list.SET_TO_LIST s))

c l. all (λx. c) l l = [] c

f g x. (f g) x = f (g x)

f. id f = f f id = f

R x y. R x y transitiveClosure R x y

f x y. flip f x y = f y x

m n. m * suc n = m + m * n

l x.
    bool.IN x (list.LIST_TO_SET (reverse l))
    bool.IN x (list.LIST_TO_SET l)

l1 l2. length (l1 @ l2) = length l1 + length l2

l1 l2. reverse (l1 @ l2) = reverse l2 @ reverse l1

l1 l2.
    list.LIST_TO_SET (l1 @ l2) =
    pred_set.UNION (list.LIST_TO_SET l1) (list.LIST_TO_SET l2)

l1 l2. list.SUM (l1 @ l2) = list.SUM l1 + list.SUM l2

P l. ¬all P l any ((¬) P) l

R f. relation.inv_image R f = λx y. R (f x) (f y)

list.GENLIST f (suc n) = f 0 :: list.GENLIST (f suc) n

l. l = [] h t. l = h :: t

f g. f = g x. f x = g x

f v. (y. y = v f y) f v

P a. (x. x = a P x) P a

f x y. pair.UNCURRY f (x, y) = f x y

() = λt1 t2. t. (t1 t) (t2 t) t

t1 t2. (t1 t2) (t1 t2) (t2 t1)

t1 t2. (t1 t2) (t2 t1) (t1 t2)

m n. m = n m n n m

bool.LET f v () (Combinator.s (() (marker.Abbrev flip (=) v)) f)

(p ¬q) (p q) (¬q ¬p)

Combinator.s f (pair.UNCURRY g) =
  pair.UNCURRY (Combinator.s (Combinator.s (() f ,)) g)

list.LIST_TO_SET [] = pred_set.EMPTY
  list.LIST_TO_SET (h :: t) = pred_set.INSERT h (list.LIST_TO_SET t)

list.GENLIST f 0 = [] list.GENLIST f n = list.GENLIST_AUX f n []

(l. l @ [] = l) l. [] @ l = l

¬(¬A B) A ¬B

P l. filter P l = [] all (λx. ¬P x) l

f. combin.COMM f x y. f x y = f y x

R. relation.total R x y. R x y R y x

R.
    relation.RC (transitiveClosure R) = relation.RTC R
    transitiveClosure (relation.RC R) = relation.RTC R

rich_list.COUNT_LIST 0 = []
  n. rich_list.COUNT_LIST (suc n) = list.SNOC n (rich_list.COUNT_LIST n)

P Q. (x. P Q x) P y. Q y

P Q. (y. P Q y) P y. Q y

Q P. (x. P x Q) (x. P x) Q

P Q. (y. P Q y) P y. Q y

P Q. P (y. Q y) y. P Q y

P Q. P (y. Q y) y. P Q y

P Q. (x. P x Q) (x. P x) Q

P Q. (y. P y Q) (x. P x) Q

P Q. (x. P x) Q y. P y Q

P Q. (x. P x) Q x. P x Q

s.
    pred_set.FINITE s
    x. bool.IN x (list.LIST_TO_SET (list.SET_TO_LIST s)) bool.IN x s

list.EL 0 = head list.EL (suc n) (l :: ls) = list.EL n ls

¬(A B) (A ) ¬B

(x y) (z w) x z y w

x y z. x = y y = z x = z

t1 t2 t3. t1 t2 t3 (t1 t2) t3

t1 t2 t3. t1 t2 t3 t1 t2 t3

A B C. A B C (A B) C

m n p. arithmetic.- m n p m n + p

m n p. m + (n + p) = m + n + p

m n p. m + p = n + p m = n

m n p. m + p < n + p m < n

m n p. m + n m + p n p

m n p. m n n p m p

l1 l2 l3. l1 @ l2 @ l3 = (l1 @ l2) @ l3

f g n. map f (list.GENLIST g n) = list.GENLIST (f g) n

P l. any P l e. bool.IN e (list.LIST_TO_SET l) P e

s t. s = t x. bool.IN x s bool.IN x t

P. (x. y. P x y) f. x. P x (f x)

t1 t2. (if then t1 else t2) = t1 (if then t1 else t2) = t2

t1 t2. (t1 t2) t1 t2 ¬t1 ¬t2

n m. arithmetic.- n m = if m < n then numeral.iSUB n m else 0

length [] = 0 h t. length (h :: t) = suc (length t)

f g p. pair.## f g p = (f (fst p), g (snd p))

P. P 0 (n. P n P (suc n)) n. P n

R x y. relation.RC R x y x = y R x y

R x y. relation.SC R x y R x y R y x

R. relation.equivalence R x y. R x y R x = R y

rich_list.COUNT_LIST 0 = []
  n. rich_list.COUNT_LIST (suc n) = 0 :: map suc (rich_list.COUNT_LIST n)

bool.IN x (list.LIST_TO_SET (list.GENLIST f n)) m. m < n x = f m

(t. ¬¬t t) (¬ ) (¬ )

m n. ¬(m = n) suc m n suc n m

n d. 0 < n 1 < d n div d < n

R f x y. relation.inv_image R f x y R (f x) (f y)

list.SUM [] = 0 h t. list.SUM (h :: t) = h + list.SUM t

x y s. bool.IN x (pred_set.INSERT y s) x = y bool.IN x s

A B C. B C A (B A) (C A)

n r. r < n q. (q * n + r) div n = q

n r. r < n q. (q * n + r) mod n = r

f l1 l2. map f (l1 @ l2) = map f l1 @ map f l2

P L M. filter P (L @ M) = filter P L @ filter P M

s t x. bool.IN x (pred_set.UNION s t) bool.IN x s bool.IN x t

b f g x. (if b then f else g) x = if b then f x else g x

f b x y. f (if b then x else y) = if b then f x else f y

f R y z. R y z relation.RESTRICT f R z y = f y

P. (n. (m. m < n P m) P n) n. P n

P L x.
    bool.IN x (list.LIST_TO_SET (filter P L))
    P x bool.IN x (list.LIST_TO_SET L)

P Q. (x. P x Q x) (x. P x) y. Q y

P Q. (y. P y Q y) (x. P x) y. Q y

R. relation.antisymmetric R x y. R x y R y x x = y

l.
    list.ALL_DISTINCT l
    x. bool.IN x (list.LIST_TO_SET l) filter ((=) x) l = x :: []

P. P [] (t. P t h. P (h :: t)) l. P l

reverse [] = [] h t. reverse (h :: t) = reverse t @ h :: []

(t1 t2. (if then t1 else t2) = t1)
  t1 t2. (if then t1 else t2) = t2

m n p. arithmetic.- m n < p m < n + p 0 < p

l x. bool.IN x (list.LIST_TO_SET l) n. n < length l x = list.EL n l

s.
    pred_set.FINITE s
    (pred_set.SUM_IMAGE f s = 0 x. bool.IN x s f x = 0)

f. combin.ASSOC f x y z. f x (f y z) = f (f x y) z

R. transitive R x y z. R x y R y z R x z

(x y. R x y Q x y) transitiveClosure R x y transitiveClosure Q x y

e l1 l2.
    bool.IN e (list.LIST_TO_SET (l1 @ l2))
    bool.IN e (list.LIST_TO_SET l1) bool.IN e (list.LIST_TO_SET l2)

(x. rich_list.REPLICATE 0 x = [])
  n x. rich_list.REPLICATE (suc n) x = x :: rich_list.REPLICATE n x

x y a b. (x, y) = (a, b) x = a y = b

a0 a1 a0' a1'. a0 :: a1 = a0' :: a1' a0 = a0' a1 = a1'

f a b.
    list.GENLIST f (a + b) =
    list.GENLIST f b @ list.GENLIST (λt. f (t + b)) a

(list.ALL_DISTINCT [] )
  h t.
    list.ALL_DISTINCT (h :: t)
    ¬bool.IN h (list.LIST_TO_SET t) list.ALL_DISTINCT t

n.
    numeral.iDUB (bit1 n) = arithmetic.BIT2 (numeral.iDUB n)
    numeral.iDUB (arithmetic.BIT2 n) = arithmetic.BIT2 (bit1 n)
    numeral.iDUB 0 = 0

(f. list.GENLIST f 0 = [])
  f n. list.GENLIST f (suc n) = list.SNOC (f n) (list.GENLIST f n)

l f x.
    bool.IN x (list.LIST_TO_SET (map f l))
    y. x = f y bool.IN y (list.LIST_TO_SET l)

(p q r) (p q) (p ¬r) (¬q r ¬p)

(p q r) (p ¬q) (p ¬r) (q r ¬p)

f0 f1. fn. fn [] = f0 a0 a1. fn (a0 :: a1) = f1 a0 a1 (fn a1)

x y z. 0 < z (x < y div z (x + 1) * z y)

R. wellFounded R P. (x. (y. R y x P y) P x) x. P x

s1 = s2 (x. bool.IN x s2 f1 x = f2 x)
  pred_set.SUM_IMAGE f1 s1 = pred_set.SUM_IMAGE f2 s2

x x' y y'. (x x') (x' (y y')) (x y x' y')

(p q r) (p ¬q ¬r) (q ¬p) (r ¬p)

suc 0 = 1 (n. suc (bit1 n) = arithmetic.BIT2 n)
  n. suc (arithmetic.BIT2 n) = bit1 (suc n)

(l. [] @ l = l) l1 l2 h. (h :: l1) @ l2 = h :: l1 @ l2

n m l.
    m n
    list.TAKE m l @ list.TAKE (arithmetic.- n m) (list.DROP m l) =
    list.TAKE n l

A B. (¬(A B) ¬A ¬B) (¬(A B) ¬A ¬B)

M R f.
    f = relation.WFREC R M wellFounded R
    x. f x = M (relation.RESTRICT f R x) x

(f. map f [] = []) f h t. map f (h :: t) = f h :: map f t

(P. all P [] ) P h t. all P (h :: t) P h all P t

(x. last (x :: []) = x) x y z. last (x :: y :: z) = last (y :: z)

P P' Q Q'. (Q (P P')) (P' (Q Q')) (P Q P' Q')

list.ALL_DISTINCT (list.GENLIST f n)
  m1 m2. m1 < n m2 < n f m1 = f m2 m1 = m2

l1 l2.
    list.ALL_DISTINCT (l1 @ l2)
    list.ALL_DISTINCT l1 list.ALL_DISTINCT l2
    e. bool.IN e (list.LIST_TO_SET l1) ¬bool.IN e (list.LIST_TO_SET l2)

(v f. list.list_CASE [] v f = v)
  a0 a1 v f. list.list_CASE (a0 :: a1) v f = f a0 a1

(x y. R x y f x = f y) x y. transitiveClosure R x y f x = f y

(x y. P x R x y P y) x y. P x transitiveClosure R x y P y

t. (( t) t) ((t ) t) (( t) ¬t) ((t ) ¬t)

(f. list.list_size f [] = 0)
  f a0 a1. list.list_size f (a0 :: a1) = 1 + (f a0 + list.list_size f a1)

f.
    pred_set.SUM_IMAGE f pred_set.EMPTY = 0
    e s.
      pred_set.FINITE s
      pred_set.SUM_IMAGE f (pred_set.INSERT e s) =
      f e + pred_set.SUM_IMAGE f (pred_set.DELETE s e)

(x. bool.IN x (list.LIST_TO_SET []) )
  x h t.
    bool.IN x (list.LIST_TO_SET (h :: t))
    x = h bool.IN x (list.LIST_TO_SET t)

f g M N. M = N (x. x = N f x = g x) bool.LET f M = bool.LET g N

(P. filter P [] = [])
  P h t. filter P (h :: t) = if P h then h :: filter P t else filter P t

(f e. list.FOLDR f e [] = e)
  f e x l. list.FOLDR f e (x :: l) = f x (list.FOLDR f e l)

(x y. R x y Q (f x) (f y)) transitive Q
  x y. transitiveClosure R x y Q (f x) (f y)

t. ( t t) (t t) ( t ) (t ) (t t t)

t. ( t ) (t ) ( t t) (t t) (t t t)

(n. list.TAKE n [] = [])
  n x xs.
    list.TAKE n (x :: xs) =
    if n = 0 then [] else x :: list.TAKE (arithmetic.- n 1) xs

t. ( t t) (t ) ( t ) (t t ) (t ¬t)

R.
    (x y. R x y transitiveClosure R x y)
    x y z.
      transitiveClosure R x y transitiveClosure R y z
      transitiveClosure R x z

(l1 l2 l3. l1 @ l2 = l1 @ l3 l2 = l3)
  l1 l2 l3. l2 @ l1 = l3 @ l1 l2 = l3

P Q x x' y y'.
    (P Q) (Q x = x') (¬Q y = y')
    (if P then x else y) = if Q then x' else y'

(p q r) (p q r) (p ¬r ¬q) (q ¬r ¬p) (r ¬q ¬p)

R P.
    (x y. R x y P x y) (x y z. P x y P y z P x z)
    u v. transitiveClosure R u v P u v

(p if q then r else s)
  (p q ¬s) (p ¬r ¬q) (p ¬r ¬s) (¬q r ¬p)
  (q s ¬p)

m n.
    0 * m = 0 m * 0 = 0 1 * m = m m * 1 = m suc m * n = m * n + n
    m * suc n = m + m * n

(l1 l2 l1' l2'.
     length l1 = length l1'
     (l1 @ l2 = l1' @ l2' l1 = l1' l2 = l2'))
  l1 l2 l1' l2'.
    length l2 = length l2' (l1 @ l2 = l1' @ l2' l1 = l1' l2 = l2')

n m.
    (0 n ) (bit1 n 0 ) (arithmetic.BIT2 n 0 )
    (bit1 n bit1 m n m) (bit1 n arithmetic.BIT2 m n m)
    (arithmetic.BIT2 n bit1 m ¬(m n))
    (arithmetic.BIT2 n arithmetic.BIT2 m n m)

n m.
    (0 < bit1 n ) (0 < arithmetic.BIT2 n ) (n < 0 )
    (bit1 n < bit1 m n < m)
    (arithmetic.BIT2 n < arithmetic.BIT2 m n < m)
    (bit1 n < arithmetic.BIT2 m ¬(m < n))
    (arithmetic.BIT2 n < bit1 m n < m)

n m.
    (0 = bit1 n ) (bit1 n = 0 ) (0 = arithmetic.BIT2 n )
    (arithmetic.BIT2 n = 0 ) (bit1 n = arithmetic.BIT2 m )
    (arithmetic.BIT2 n = bit1 m ) (bit1 n = bit1 m n = m)
    (arithmetic.BIT2 n = arithmetic.BIT2 m n = m)

b n m.
    numeral.iSUB b 0 x = 0 numeral.iSUB n 0 = n
    numeral.iSUB (bit1 n) 0 = numeral.iDUB n
    numeral.iSUB (bit1 n) (bit1 m) = numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (bit1 n) (bit1 m) = bit1 (numeral.iSUB n m)
    numeral.iSUB (bit1 n) (arithmetic.BIT2 m) =
    bit1 (numeral.iSUB n m)
    numeral.iSUB (bit1 n) (arithmetic.BIT2 m) =
    numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) 0 = bit1 n
    numeral.iSUB (arithmetic.BIT2 n) (bit1 m) =
    bit1 (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) (bit1 m) =
    numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) (arithmetic.BIT2 m) =
    numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) (arithmetic.BIT2 m) =
    bit1 (numeral.iSUB n m)

n m.
    numeral.iZ (0 + n) = n numeral.iZ (n + 0) = n
    numeral.iZ (bit1 n + bit1 m) = arithmetic.BIT2 (numeral.iZ (n + m))
    numeral.iZ (bit1 n + arithmetic.BIT2 m) = bit1 (suc (n + m))
    numeral.iZ (arithmetic.BIT2 n + bit1 m) = bit1 (suc (n + m))
    numeral.iZ (arithmetic.BIT2 n + arithmetic.BIT2 m) =
    arithmetic.BIT2 (suc (n + m)) suc (0 + n) = suc n
    suc (n + 0) = suc n suc (bit1 n + bit1 m) = bit1 (suc (n + m))
    suc (bit1 n + arithmetic.BIT2 m) = arithmetic.BIT2 (suc (n + m))
    suc (arithmetic.BIT2 n + bit1 m) = arithmetic.BIT2 (suc (n + m))
    suc (arithmetic.BIT2 n + arithmetic.BIT2 m) =
    bit1 (numeral.iiSUC (n + m))
    numeral.iiSUC (0 + n) = numeral.iiSUC n
    numeral.iiSUC (n + 0) = numeral.iiSUC n
    numeral.iiSUC (bit1 n + bit1 m) = arithmetic.BIT2 (suc (n + m))
    numeral.iiSUC (bit1 n + arithmetic.BIT2 m) =
    bit1 (numeral.iiSUC (n + m))
    numeral.iiSUC (arithmetic.BIT2 n + bit1 m) =
    bit1 (numeral.iiSUC (n + m))
    numeral.iiSUC (arithmetic.BIT2 n + arithmetic.BIT2 m) =
    arithmetic.BIT2 (numeral.iiSUC (n + m))

(m. 0 + m = m) (m. m + 0 = m) (n m. n + m = numeral.iZ (n + m))
  (n. 0 * n = 0) (n. n * 0 = 0) (n m. n * m = n * m)
  (n. arithmetic.- 0 n = 0) (n. arithmetic.- n 0 = n)
  (n m. arithmetic.- n m = arithmetic.- n m) (n. 0 bit1 n = 0)
  (n. 0 arithmetic.BIT2 n = 0) (n. n 0 = 1)
  (n m. n m = n m) suc 0 = 1 (n. suc n = suc n)
  prim_rec.PRE 0 = 0 (n. prim_rec.PRE n = prim_rec.PRE n)
  (n. n = 0 n = 0) (n. 0 = n n = 0) (n m. n = m n = m)
  (n. n < 0 ) (n. 0 < n 0 < n) (n m. n < m n < m)
  (n. 0 > n ) (n. n > 0 0 < n) (n m. n > m m < n)
  (n. 0 n ) (n. n 0 n 0) (n m. n m n m)
  (n. n 0 ) (n. 0 n n = 0) (n m. n m m n)
  (n. odd n odd n) (n. even n even n) ¬odd 0 even 0