Theory sorting

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

⊢ ∀P l. PARTITION P l = PART P l [] []

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

⊢ ∀L1 L2. PERM L1 L2 ⇔ ∀x. FILTER ($= x) L1 = FILTER ($= x) L2

⊢ ∀l1 l2.
    PERM_SINGLE_SWAP l1 l2 ⇔
    ∃x1 x2 x3. l1 = x1 ⧺ x2 ⧺ x3 ∧ l2 = x1 ⧺ x3 ⧺ x2

⊢ ∀f R. SORTS f R ⇔ ∀l. PERM l (f R l) ∧ SORTED R (f R l)

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

⊢ ∀l1 l2. PERM l1 l2 ⇒ (ALL_DISTINCT l1 ⇔ ALL_DISTINCT l2)

⊢ ∀ls. ALL_DISTINCT ls ⇔ PERM ls (SET_TO_LIST (set ls))

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

⊢ ∀A B C. PERM (A ⧺ B) C ⇒ PERM (B ⧺ A) C

⊢ ∀x L M N. PERM L (M ⧺ N) ⇒ PERM (x::L) (M ⧺ x::N)

⊢ ∀n i.
    i < LENGTH (FILTER P (COUNT_LIST n)) ⇒
    (FILTER P (COUNT_LIST n))❲i❳ =
    LEAST j. (0 < i ⇒ (FILTER P (COUNT_LIST n))❲i − 1❳ < j) ∧ j < n ∧ P j

⊢ LENGTH (FILTER ($= x) l1) = LENGTH (FILTER ($= x) l2) ⇒
  FILTER ($= x) l1 = FILTER ($= x) l2

⊢ FILTER ($= x) l = REPLICATE (LENGTH (FILTER ($= x) l)) x

⊢ ∀f l1 l2 e. ASSOC f ∧ COMM f ⇒ PERM l1 l2 ⇒ FOLDR f e l1 = FOLDR f e l2

⊢ LENGTH (QSORT R l) = LENGTH l

⊢ ∀l1 l2 l3.
    LIST_REL P l1 l2 ∧ PERM l2 l3 ⇒ ∃l4. PERM l1 l4 ∧ LIST_REL P l4 l3

⊢ ∀l1 l2. PERM l1 l2 ⇒ ∀a. MEM a l1 ⇔ MEM a l2

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

⊢ ∀P L l1 l2 p q.
    (p,q) = PART P L l1 l2 ⇒
    LENGTH L + LENGTH l1 + LENGTH l2 = LENGTH p + LENGTH q

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

⊢ ∀P L a1 a2 l1 l2.
    (a1,a2) = PART P L l1 l2 ⇒ ∀x. MEM x (L ⧺ (l1 ⧺ l2)) ⇔ MEM x (a1 ⧺ a2)

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

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

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

⊢ ∀l1 l2.
    ALL_DISTINCT l1 ∧ ALL_DISTINCT l2 ∧ (∀x. MEM x l1 ⇔ MEM x l2) ⇒
    PERM l1 l2

⊢ ∀l1 l2. PERM (l1 ⧺ l2) (l2 ⧺ l1)

⊢ (∀l l1 l2. PERM (l ⧺ l1) (l ⧺ l2) ⇔ PERM l1 l2) ∧
  ∀l l1 l2. PERM (l1 ⧺ l) (l2 ⧺ l) ⇔ PERM l1 l2

⊢ ∀l1 l2.
    PERM l1 l2 ⇒
    ∃f. f PERMUTES count (LENGTH l1) ∧
        l2 = GENLIST (λi. l1❲f i❳) (LENGTH l1)

⊢ PERM l1 l2 ⇔
  ∃p. p PERMUTES count (LENGTH l1) ∧ l2 = GENLIST (λi. l1❲p i❳) (LENGTH l1)

⊢ ∀f s1 s2.
    FINITE s1 ∧ FINITE s2 ∧ BIJ f s1 s2 ⇒
    PERM (MAP f (SET_TO_LIST s1)) (SET_TO_LIST s2)

⊢ ∀L1 L2 L3 L4. PERM L1 L3 ∧ PERM L2 L4 ⇒ PERM (L1 ⧺ L2) (L3 ⧺ L4)

⊢ ∀l1 l1' l2 l2'. PERM l1 l1' ⇒ PERM l2 l2' ⇒ (PERM l1 l2 ⇔ PERM l1' l2')

⊢ ∀l l1 l1' l2 l2'.
    PERM l1 (l ⧺ l1') ⇒ PERM l2 (l ⧺ l2') ⇒ (PERM l1 l2 ⇔ PERM l1' l2')

⊢ ∀l1 l1' l1'' l2 l2' l2''.
    PERM l1 (l1' ⧺ l1'') ⇒
    PERM l2 (l2' ⧺ l2'') ⇒
    PERM l1' l2' ⇒
    (PERM l1 l2 ⇔ PERM l1'' l2'')

⊢ ∀L h. PERM (h::t) L ⇔ ∃M N. L = M ⧺ h::N ∧ PERM t (M ⧺ N)

⊢ ∀x l2 l1. PERM (x::l1) (x::l2) ⇔ PERM l1 l2

⊢ PERM = PERM_SINGLE_SWAP^=

⊢ equivalence PERM

⊢ ∀x y. PERM x y ⇔ PERM x = PERM y

⊢ ∀ls ls'. PERM ls ls' ⇒ (EVERY P ls ⇔ EVERY P ls')

⊢ ∀P l1 l2. PERM l1 l2 ⇒ PERM (FILTER P l1) (FILTER P l2)

⊢ ∀l1 l2. PERM l1 l2 ⇒ PERM (FLAT l1) (FLAT l2)

⊢ ∀h t ls. PERM (FLAT (MAP (λx. h x::t x) ls)) (MAP h ls ⧺ FLAT (MAP t ls))

⊢ ∀f l1 l2.
    PERM (FLAT (MAP (λx. MAP (f x) l2) l1))
      (FLAT (MAP (λx. MAP (flip f x) l1) l2))

⊢ ∀l1 l2. PERM (l1 ⧺ l2) = PERM (l2 ⧺ l1)

⊢ ∀l1 l2 l3 l4.
    PERM l1 = PERM (l2 ⧺ l3) ⇒ PERM (l1 ⧺ l4) = PERM (l2 ⧺ (l3 ⧺ l4))

⊢ ∀l1 l2 l3 l4.
    PERM l1 = PERM (l2 ⧺ l3) ⇒ PERM (l4 ⧺ l1) = PERM (l2 ⧺ (l4 ⧺ l3))

⊢ ∀l1 l1' l2 l2'.
    PERM l1 = PERM l1' ⇒
    PERM l2 = PERM l2' ⇒
    PERM (l1 ⧺ l2) = PERM (l1' ⧺ l2')

⊢ ∀x l1 l2. PERM (l1 ⧺ x::l2) = PERM (x::l1 ⧺ l2)

⊢ ∀l l1 l2. PERM l1 = PERM l2 ⇒ PERM (l ⧺ l1) = PERM (l ⧺ l2)

⊢ ∀l1 l1' l2 l2'.
    PERM l1 = PERM l1' ⇒ PERM l2 = PERM l2' ⇒ (PERM l1 l2 ⇔ PERM l1' l2')

⊢ ∀x l1 l1'. PERM l1 = PERM l1' ⇒ PERM (x::l1) = PERM (x::l1')

⊢ ∀y l1 l2 l3. PERM l1 = PERM (l2 ⧺ l3) ⇒ PERM (y::l1) = PERM (l2 ⧺ y::l3)

⊢ ∀y l1 x l2. PERM l1 = PERM (x::l2) ⇒ PERM (y::l1) = PERM (x::y::l2)

⊢ ∀l l1 x l2. PERM l1 = PERM (x::l2) ⇒ PERM (l1 ⧺ l) = PERM (x::(l2 ⧺ l))

⊢ ∀l l1 x l2. PERM l1 = PERM (x::l2) ⇒ PERM (l ⧺ l1) = PERM (x::(l ⧺ l2))

⊢ ∀x l1 l2. PERM l1 = PERM l2 ⇒ PERM (x::l1) = PERM (x::l2)

⊢ ∀l l1 l1' l2. PERM l (l1 ⧺ l2) ⇒ PERM l1' l1 ⇒ PERM l (l1' ⧺ l2)

⊢ ∀x y l. PERM (x::y::l) = PERM (y::x::l)

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

⊢ ∀x y. x = y ⇒ PERM x y

⊢ ∀l1 l2. PERM l1 l2 ⇒ LENGTH l1 = LENGTH l2

⊢ ∀l1 l2. PERM l1 l2 ⇒ set l1 = set l2

⊢ ∀f l1 l2. PERM l1 l2 ⇒ PERM (MAP f l1) (MAP f l2)

⊢ ∀s. FINITE s ⇒
      ∀f. (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
          PERM (MAP f (SET_TO_LIST s)) (SET_TO_LIST (IMAGE f s))

⊢ ∀l1 l2. PERM l1 l2 ⇒ ∀x. MEM x l1 ⇔ MEM x l2

⊢ ∀l1 l2 x. PERM l1 l2 ⇒ PERM (x::l1) (x::l2)

⊢ ∀L. (PERM L [] ⇔ L = []) ∧ (PERM [] L ⇔ L = [])

⊢ ∀l1 l2. PERM l1 l2 ⇒ (NULL l1 ⇔ NULL l2)

⊢ ∀l R. PERM l (QSORT3 R l)

⊢ ∀L. PERM L L

⊢ PERM ls (REVERSE ls)

⊢ (PERM (REVERSE l1) l2 ⇔ PERM l1 l2) ∧ (PERM l1 (REVERSE l2) ⇔ PERM l1 l2)

⊢ ∀l r l1 l2. PERM l r ⇒ (PERM (l ⧺ l1) l2 ⇔ PERM (r ⧺ l1) l2)

⊢ PERM = PERM_SINGLE_SWAP꙳

⊢ ∀s1 s2.
    FINITE s1 ∧ FINITE s2 ∧ DISJOINT s1 s2 ⇒
    PERM (SET_TO_LIST (s1 ∪ s2)) (SET_TO_LIST s1 ⧺ SET_TO_LIST s2)

⊢ FINITE s ⇒
  PERM (SET_TO_LIST (x INSERT s))
    (if x ∈ s then SET_TO_LIST s else x::SET_TO_LIST s)

⊢ PERM (SET_TO_LIST (count n)) (COUNT_LIST n)

⊢ (PERM L [x] ⇔ L = [x]) ∧ (PERM [x] L ⇔ L = [x])

⊢ PERM_SINGLE_SWAP (x2 ⧺ x3) (x3 ⧺ x2)

⊢ PERM_SINGLE_SWAP M N ⇒ PERM_SINGLE_SWAP (x::M) (x::N)

⊢ PERM_SINGLE_SWAP (x1 ⧺ x2 ⧺ x3) (x1 ⧺ x3 ⧺ x2)

⊢ ∀l. PERM_SINGLE_SWAP l l

⊢ ∀l1 l2. PERM_SINGLE_SWAP l1 l2 ⇔ PERM_SINGLE_SWAP l2 l1

⊢ ∀M N. PERM_SINGLE_SWAP⁺ M N ⇒ PERM_SINGLE_SWAP⁺ (x::M) (x::N)

⊢ ∀P l. PERM l (FILTER P l ⧺ FILTER ($¬ ∘ P) l)

⊢ ∀P Q l. EVERY (λx. P x ⇔ ¬Q x) l ⇒ PERM l (FILTER P l ⧺ FILTER Q l)

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

⊢ ∀l1 l2. PERM l1 l2 ⇒ SUM l1 = SUM l2

⊢ PERM (x::y::l1) (y::x::l2) ⇔ PERM l1 l2

⊢ ∀x y. PERM (x ⧺ y ⧺ l1) (y ⧺ x ⧺ l2) ⇔ PERM l1 l2

⊢ ∀l1 l2. PERM l1 l2 ⇔ PERM l2 l1

⊢ PERM = PERM_SINGLE_SWAP⁺

⊢ (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)

⊢ ∀x y z. PERM x y ∧ PERM y z ⇒ PERM x z

⊢ ∀L1 L2.
    PERM L1 L2 ⇔ ∀x. LENGTH (FILTER ($= x) L1) = LENGTH (FILTER ($= x) L2)

⊢ ∀f. (∀x1 x2 x3. f (x1 ⧺ x2 ⧺ x3) = f (x1 ⧺ x3 ⧺ x2)) ⇒
      ∀x y. PERM x y ⇒ f x = f y

⊢ ∀P. (∀x1 x2 x3. P (x1 ⧺ x2 ⧺ x3) ⇒ P (x1 ⧺ x3 ⧺ x2)) ⇒
      ∀x y. P x ∧ PERM x y ⇒ P y

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

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

⊢ transitive PERM

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

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

⊢ ∀R L x. MEM x (QSORT3 R L) ⇔ MEM x L

⊢ ∀R L. transitive R ∧ total R ⇒ SORTED R (QSORT3 R L)

⊢ ∀R. transitive R ∧ total R ⇒ SORTS QSORT3 R

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

⊢ ∀R. transitive R ∧ total R ⇒ STABLE QSORT3 R

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

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

⊢ ∀R L x. MEM x (QSORT R L) ⇔ MEM x L

⊢ ∀R L. PERM L (QSORT R L)

⊢ ∀R L. transitive R ∧ total R ⇒ SORTED R (QSORT R L)

⊢ ∀R. transitive R ∧ total R ⇒ SORTS QSORT R

⊢ ∀R. total R ∧ transitive R ∧ antisymmetric R ⇒
      ∀l1 l2. QSORT R l1 = QSORT R l2 ⇔ PERM l1 l2

⊢ transitive R ∧ antisymmetric R ∧ total R ⇒
  QSORT R (nub ls) = nub (QSORT R ls)

⊢ irreflexive R ∧ transitive R ⇒ ∀ls. SORTED R ls ⇒ ALL_DISTINCT ls

⊢ ∀R. transitive R ∧ antisymmetric R ⇒
      ∀l1 l2.
        SORTED R l1 ∧ SORTED R l2 ∧ ALL_DISTINCT l1 ∧ ALL_DISTINCT l2 ∧
        set l1 = set l2 ⇒
        l1 = l2

⊢ ∀R L1 L2.
    transitive R ⇒
    (SORTED R (L1 ⧺ L2) ⇔
     SORTED R L1 ∧ SORTED R L2 ∧ ∀x y. MEM x L1 ⇒ MEM y L2 ⇒ R x y)

⊢ ∀R L1 L2.
    SORTED R (L1 ⧺ L2) ⇔
    SORTED R L1 ∧ SORTED R L2 ∧ (L1 = [] ∨ L2 = [] ∨ R (LAST L1) (HD L2))

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

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

⊢ ∀R. transitive R ⇒
      ∀ls. SORTED R ls ⇔ ∀m n. m < n ∧ n < LENGTH ls ⇒ R ls❲m❳ ls❲n❳

⊢ ∀R ls. SORTED R ls ⇔ ∀n. SUC n < LENGTH ls ⇒ R ls❲n❳ ls❲SUC n❳

⊢ ∀R L x.
    transitive R ⇒ (SORTED R (x::L) ⇔ SORTED R L ∧ ∀y. MEM y L ⇒ R x y)

⊢ ∀l R. transitive R ⇒ SORTED R (FILTER (λx. R x hd ∧ R hd x) l)

⊢ ∀R ls P. transitive R ∧ SORTED R ls ⇒ SORTED R (FILTER P ls)

⊢ SORTED R (FILTER P (COUNT_LIST m)) ⇔
  ∀i j. i < j ∧ j < m ∧ P i ∧ P j ∧ (∀k. i < k ∧ k < j ⇒ ¬P k) ⇒ R i j

⊢ ∀R ls rs.
    SORTED R ls ∧ LENGTH ls = LENGTH rs ⇒
    SORTED (λx y. R (FST x) (FST y)) (ZIP (ls,rs))

⊢ ∀n k. SORTED $< (GENLIST ($+ k) n)

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

⊢ ∀R. SORTED R []

⊢ ∀R. transitive R ∧ antisymmetric R ⇒
      ∀l1 l2. SORTED R l1 ∧ SORTED R l2 ∧ PERM l1 l2 ⇒ l1 = l2

⊢ ∀R x. SORTED R [x]

⊢ SORTED R (x::xs) ⇒ SORTED R xs

⊢ SORTED R L ⇔ adjacent L ⊆ᵣ R

⊢ transitive R ∧ SORTED R ls ⇒ SORTED R (nub ls)

⊢ ∀R R' ls.
    SORTED R ls ∧ (∀x y. MEM x ls ∧ MEM y ls ∧ R x y ⇒ R' x y) ⇒
    SORTED R' ls

⊢ ∀R. transitive R ∧ antisymmetric R ∧ SORTS f R ⇒
      ∀l1 l2. f R l1 = f R l2 ⇔ PERM l1 l2

⊢ SORTED $> (x::L) ⇔ SORTED $> L ∧ ∀y. MEM y L ⇒ y < x

⊢ PERM l1 l2 ⇒ lcp l1 = lcp l2

⊢ ∀L x. SORTED $< (x::L) ⇔ SORTED $< L ∧ ∀y. MEM y L ⇒ x < y

⊢ (permdef :-
     ∀l1 l2.
       perm l1 l2 ⇔
       ∀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) ⇒
           P l1 l2) ⇒
  perm [] [] ∧ (∀x l1 l2. perm l1 l2 ⇒ perm (x::l1) (x::l2)) ∧
  (∀x y l1 l2. perm l1 l2 ⇒ perm (x::y::l1) (y::x::l2)) ∧
  ∀l1 l2 l3. perm l1 l2 ∧ perm l2 l3 ⇒ perm l1 l3

⊢ ∀n. SORTED $<= (COUNT_LIST n)

⊢ ∀R ls. transitive R ⇒ SORTED R ls ⇒ SORTED R (FILTER P ls)

⊢ ∀n. SORTED $< (COUNT_LIST n)

⊢ ∀R f l. SORTED R (MAP f l) ⇔ SORTED (inv_image R f) l

⊢ ∀y f l n.
    SORTED (inv_image $<= f) l ∧ PERM (MAP f l) (COUNT_LIST n) ⇒
    MAP f l = COUNT_LIST n