Theory rich_list

⊢ AND_EL = EVERY I

⊢ ∀n xs. BUTLASTN n xs = REVERSE (DROP n (REVERSE xs))

⊢ (∀l. COUNT_LIST_AUX 0 l = l) ∧
  ∀n l. COUNT_LIST_AUX (SUC n) l = COUNT_LIST_AUX n (n::l)

⊢ COUNT_LIST 0 = [] ∧ ∀n. COUNT_LIST (SUC n) = 0::MAP SUC (COUNT_LIST n)

⊢ (∀e. DELETE_ELEMENT e [] = []) ∧
  ∀e x l.
    DELETE_ELEMENT e (x::l) =
    if e = x then DELETE_ELEMENT e l else x::DELETE_ELEMENT e l

⊢ (∀l. ELL 0 l = LAST l) ∧ ∀n l. ELL (SUC n) l = ELL n (FRONT l)

⊢ (∀l. IS_SUBLIST l [] ⇔ T) ∧ (∀x l. IS_SUBLIST [] (x::l) ⇔ F) ∧
  ∀x1 l1 x2 l2.
    IS_SUBLIST (x1::l1) (x2::l2) ⇔
    x1 = x2 ∧ l2 ≼ l1 ∨ IS_SUBLIST l1 (x2::l2)

⊢ (∀l. IS_SUFFIX l [] ⇔ T) ∧ (∀x l. IS_SUFFIX [] (SNOC x l) ⇔ F) ∧
  ∀x1 l1 x2 l2.
    IS_SUFFIX (SNOC x1 l1) (SNOC x2 l2) ⇔ x1 = x2 ∧ IS_SUFFIX l1 l2

⊢ ∀n xs. LASTN n xs = REVERSE (TAKE n (REVERSE xs))

⊢ ∀e l. LIST_ELEM_COUNT e l = LENGTH (FILTER (λx. x = e) l)

⊢ MAX_LIST [] = 0 ∧ ∀h t. MAX_LIST (h::t) = MAX h (MAX_LIST t)

⊢ ∀h t. MIN_LIST (h::t) = if t = [] then h else MIN h (MIN_LIST t)

⊢ OR_EL = EXISTS I

⊢ ∀P l. PREFIX P l = FST (SPLITP ($¬ ∘ P) l)

⊢ (∀x. REPLICATE 0 x = []) ∧ ∀n x. REPLICATE (SUC n) x = x::REPLICATE n x

⊢ (∀f e. SCANL f e [] = [e]) ∧
  ∀f e x l. SCANL f e (x::l) = e::SCANL f (f e x) l

⊢ (∀f e. SCANR f e [] = [e]) ∧
  ∀f e x l. SCANR f e (x::l) = f x (HD (SCANR f e l))::SCANR f e l

⊢ (∀k l. SEG 0 k l = []) ∧ (∀m x l. SEG (SUC m) 0 (x::l) = x::SEG m 0 l) ∧
  ∀m k x l. SEG (SUC m) (SUC k) (x::l) = SEG (SUC m) k l

⊢ ∀P. SPLITL P = SPLITP ($¬ ∘ P)

⊢ (∀P. SPLITP P [] = ([],[])) ∧
  ∀P x l.
    SPLITP P (x::l) =
    if P x then ([],x::l) else (x::FST (SPLITP P l),SND (SPLITP P l))

⊢ (∀acc P. SPLITP_TAILREC acc P [] = (REVERSE acc,[])) ∧
  ∀acc P h t.
    SPLITP_TAILREC acc P (h::t) =
    if P h then (REVERSE acc,h::t) else SPLITP_TAILREC (h::acc) P t

⊢ ∀P l.
    SPLITR P l =
    (let (a,b) = SPLITP ($¬ ∘ P) (REVERSE l) in (REVERSE b,REVERSE a))

⊢ ∀P l. SUFFIX P l = FOLDL (λl' x. if P x then SNOC x l' else []) [] l

⊢ ∀l. UNZIP_FST l = FST (UNZIP l)

⊢ ∀l. UNZIP_SND l = SND (UNZIP l)

⊢ ∀n ls.
    chunks_tr n ls = if n = 0 then [ls] else chunks_tr_aux (n − 1) ls []

⊢ ∀s. common_prefixes s = {p | ∀m. m ∈ s ⇒ p ≼ m}

⊢ ∀x y. lcp2 x y = longest_prefix {x; y}

⊢ ∀ls. lcp ls = longest_prefix (set ls)

⊢ ∀s. longest_prefix s =
      if s = ∅ then []
      else @x. is_measure_maximal LENGTH (common_prefixes s) x

⊢ ∀l1 x l2. ALL_DISTINCT (l1 ⧺ [x] ⧺ l2) ⇔ ALL_DISTINCT (x::(l1 ⧺ l2))

⊢ ∀ls l1 l2 j.
    ALL_DISTINCT ls ∧ j < LENGTH ls ∧ ls = l1 ⧺ [ls❲j❳] ⧺ l2 ⇒
    j = LENGTH l1

⊢ ∀l. l ≠ [] ∧ ALL_DISTINCT l ⇒ ALL_DISTINCT (FRONT l)

⊢ ∀ls j.
    ALL_DISTINCT ls ∧ ls ≠ [] ∧ j < LENGTH ls ⇒
    (ls❲j❳ = LAST ls ⇔ j + 1 = LENGTH ls)

⊢ ∀f x ls.
    ALL_DISTINCT ls ⇒
    (MEM x (ZIP (ls,MAP f ls)) ⇔ MEM (FST x) ls ∧ SND x = f (FST x))

⊢ ∀x l. ALL_DISTINCT (SNOC x l) ⇔ ¬MEM x l ∧ ALL_DISTINCT l

⊢ ∀ls x y. ALL_DISTINCT (x::y::ls) ⇔ ALL_DISTINCT (y::x::ls)

⊢ ∀ls n. ALL_DISTINCT ls ⇒ ALL_DISTINCT (TAKE n ls)

⊢ ∀ls. ALL_DISTINCT ls ⇒ ∀k e. MEM e (TAKE k ls) ∧ MEM e (DROP k ls) ⇒ F

⊢ (∀P. EVERY P [] ⇔ T) ∧ ∀P h t. EVERY P (h::t) ⇔ P h ∧ EVERY P t

⊢ ∀P l1 l2. EVERY P (l1 ⧺ l2) ⇔ EVERY P l1 ∧ EVERY P l2

⊢ ∀P l m. EVERY P l ⇒ EVERY P (DROP m l)

⊢ ∀P l m. EVERY P l ⇒ EVERY P (BUTLASTN m l)

⊢ ∀P Q l. EVERY (λx. P x ∧ Q x) l ⇔ EVERY P l ∧ EVERY Q l

⊢ ∀P l m. EVERY P l ⇒ EVERY P (TAKE m l)

⊢ ∀P l. EVERY P l ⇔ FOLDL (λl' x. l' ∧ P x) T l

⊢ ∀P l. EVERY P l ⇔ FOLDL $/\ T (MAP P l)

⊢ ∀P l. EVERY P l ⇔ FOLDR (λx l'. P x ∧ l') T l

⊢ ∀P l. EVERY P l ⇔ FOLDR $/\ T (MAP P l)

⊢ ∀P l m. EVERY P l ⇒ EVERY P (LASTN m l)

⊢ ∀P f l. EVERY P (MAP f l) ⇔ EVERY (P ∘ f) l

⊢ ∀f n x. EVERY f (REPLICATE n x) ⇔ n = 0 ∨ f x

⊢ ∀P l. EVERY P (REVERSE l) ⇔ EVERY P l

⊢ ∀P l. EVERY P l ⇒ ∀m k. m + k ≤ LENGTH l ⇒ EVERY P (SEG m k l)

⊢ ∀P x l. EVERY P (SNOC x l) ⇔ EVERY P l ∧ P x

⊢ ∀l. AND_EL l ⇔ FOLDL $/\ T l

⊢ ∀l. AND_EL l ⇔ FOLDR $/\ T l

⊢ (∀l. [] ⧺ l = l) ∧ ∀l1 l2 h. h::l1 ⧺ l2 = h::(l1 ⧺ l2)

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

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

⊢ ∀l1 h l2 l3. l1 ⧺ h::l2 ⧺ l3 = l1 ⧺ h::(l2 ⧺ l3)

⊢ ∀m n l. m + n = LENGTH l ⇒ BUTLASTN m l ⧺ DROP n l = l

⊢ ∀m n l. m + n = LENGTH l ⇒ BUTLASTN m l ⧺ DROP n l = l

⊢ ∀n l. n ≤ LENGTH l ⇒ BUTLASTN n l ⧺ LASTN n l = l

⊢ ∀l. l ≠ [] ⇒ FRONT l ⧺ [LAST l] = l

⊢ ∀l1 l2 m1 m2.
    l1 ⧺ l2 = m1 ⧺ m2 ∧ LENGTH l1 = LENGTH m1 ⇔ l1 = m1 ∧ l2 = m2

⊢ ∀n l. TAKE n l ⧺ DROP n l = l

⊢ ∀m n l. m + n = LENGTH l ⇒ TAKE n l ⧺ LASTN m l = l

⊢ ∀l1 l2. l1 ⧺ l2 = FOLDL (λl' x. SNOC x l') l1 l2

⊢ ∀l1 l2. l1 ⧺ l2 = FOLDR CONS l2 l1

⊢ ∀l1 l1'.
    LENGTH l1 = LENGTH l1' ⇒
    ∀l2 l2'.
      LENGTH l2 = LENGTH l2' ⇒ (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2')

⊢ (∀l. l ⧺ [] = l) ∧ ∀l. [] ⧺ l = l

⊢ ∀l1 x l2. l1 ⧺ SNOC x l2 = SNOC x (l1 ⧺ l2)

⊢ ∀l1 x l2. SNOC x l1 ⧺ l2 = l1 ⧺ x::l2

⊢ ∀m n l. m + n = LENGTH l ⇒ TAKE n l ⧺ LASTN m l = l

⊢ ASSOC $++

⊢ ∀f. ASSOC f ⇒
      ∀e. RIGHT_ID f e ⇒
          ∀l. FOLDL f e (FLAT l) = FOLDL f e (MAP (FOLDL f e) l)

⊢ ∀f. ASSOC f ⇒
      ∀e. LEFT_ID f e ⇒
          ∀l. FOLDR f e (FLAT l) = FOLDR f e (MAP (FOLDR f e) l)

⊢ (∀l. DROP 0 l = l) ∧ ∀n x l. DROP (SUC n) (x::l) = DROP n l

⊢ ∀n l1. n ≤ LENGTH l1 ⇒ ∀l2. DROP n (l1 ⧺ l2) = DROP n l1 ⧺ l2

⊢ ∀l1 n. LENGTH l1 ≤ n ⇒ ∀l2. DROP n (l1 ⧺ l2) = DROP (n − LENGTH l1) l2

⊢ ∀n m l. n + m ≤ LENGTH l ⇒ DROP n (DROP m l) = DROP (n + m) l

⊢ ∀n l. n < LENGTH l ⇒ DROP n l = l❲n❳::DROP (SUC n) l

⊢ ∀n l. n ≤ LENGTH l ⇒ DROP n l = LASTN (LENGTH l − n) l

⊢ ∀l1 l2. DROP (LENGTH l1) (l1 ⧺ l2) = l2

⊢ ∀l. DROP (LENGTH l) l = []

⊢ ∀n l. n ≤ LENGTH l ⇒ DROP n (REVERSE l) = REVERSE (BUTLASTN n l)

⊢ ∀n l. n ≤ LENGTH l ⇒ DROP n l = SEG (LENGTH l − n) n l

⊢ ∀n l. n ≤ LENGTH l ⇒ ∀x. DROP n (SNOC x l) = SNOC x (DROP n l)

⊢ ∀x l. FRONT (SNOC x l) = l

⊢ (∀l. BUTLASTN 0 l = l) ∧
  ∀n x l. BUTLASTN (SUC n) (SNOC x l) = BUTLASTN n l

⊢ ∀l. BUTLASTN 1 l = FRONT l

⊢ ∀l2 n.
    LENGTH l2 ≤ n ⇒ ∀l1. BUTLASTN n (l1 ⧺ l2) = BUTLASTN (n − LENGTH l2) l1

⊢ ∀n l1 l2. n ≤ LENGTH l2 ⇒ BUTLASTN n (l1 ⧺ l2) = l1 ⧺ BUTLASTN n l2

⊢ ∀n l. n < LENGTH l ⇒ BUTLASTN n (FRONT l) = FRONT (BUTLASTN n l)

⊢ ∀m n l. n + m ≤ LENGTH l ⇒ BUTLASTN n (BUTLASTN m l) = BUTLASTN (n + m) l

⊢ ∀n l. n ≤ LENGTH l ⇒ ∀x. BUTLASTN n (x::l) = x::BUTLASTN n l

⊢ ∀n l. n ≤ LENGTH l ⇒ BUTLASTN n l = TAKE (LENGTH l − n) l

⊢ ∀n l. n < LENGTH l ⇒ BUTLASTN n (FRONT l) = FRONT (BUTLASTN n l)

⊢ ∀m n l.
    m ≤ n ∧ n ≤ LENGTH l ⇒
    BUTLASTN m (LASTN n l) = LASTN (n − m) (BUTLASTN m l)

⊢ ∀n l. n ≤ LENGTH l ⇒ BUTLASTN n (LASTN n l) = []

⊢ ∀l2 l1. BUTLASTN (LENGTH l2) (l1 ⧺ l2) = l1

⊢ ∀l x. BUTLASTN (LENGTH l) (x::l) = [x]

⊢ ∀l. BUTLASTN (LENGTH l) l = []

⊢ ∀n l. n ≤ LENGTH l ⇒ ∀f. BUTLASTN n (MAP f l) = MAP f (BUTLASTN n l)

⊢ ∀n l. n ≤ LENGTH l ⇒ BUTLASTN n (REVERSE l) = REVERSE (DROP n l)

⊢ ∀n l. n ≤ LENGTH l ⇒ BUTLASTN n l = SEG (LENGTH l − n) 0 l

⊢ ∀n l. n < LENGTH l ⇒ BUTLASTN (SUC n) l = BUTLASTN n (FRONT l)

⊢ ∀n l. n < LENGTH l ⇒ BUTLASTN (SUC n) l = BUTLASTN n (FRONT l)

⊢ ∀n l. n ≤ LENGTH l ⇒ BUTLASTN n l = TAKE (LENGTH l − n) l

⊢ ∀n l. BUTLASTN n l = TAKE (LENGTH l − n) l

⊢ ∀n l.
    BUTLASTN n l =
    (let
       m = LENGTH l
     in
       if n ≤ m then TAKE (m − n) l
       else FAIL BUTLASTN $var$(longer than list) n l)

⊢ (∀x. FRONT [x] = []) ∧ ∀x y z. FRONT (x::y::z) = x::FRONT (y::z)

⊢ ∀f. COMM f ⇒ ASSOC f ⇒ ∀e l. FOLDL f e (REVERSE l) = FOLDL f e l

⊢ ∀f. COMM f ⇒ ASSOC f ⇒ ∀e l. FOLDR f e (REVERSE l) = FOLDR f e l

⊢ ∀f. COMM f ⇒ ∀e'. MONOID f e' ⇒ ∀e l. FOLDL f e l = f e (FOLDL f e' l)

⊢ ∀f. COMM f ⇒ ∀e'. MONOID f e' ⇒ ∀e l. FOLDR f e l = f e (FOLDR f e' l)

⊢ ∀l. ¬NULL l ⇒ HD l::TL l = l

⊢ ∀a0 a1 a0' a1'. a0::a1 = a0'::a1' ⇔ a0 = a0' ∧ a1 = a1'

⊢ ∀x l. x::l = [x] ⧺ l

⊢ ∀n m.
    COUNT_LIST (n + m) = COUNT_LIST n ⧺ MAP (λn'. n' + n) (COUNT_LIST m)

⊢ (∀l. COUNT_LIST_AUX 0 l = l) ∧
  (∀n l.
     COUNT_LIST_AUX <..num comp'n..> l =
     COUNT_LIST_AUX (<..num comp'n..> − 1) (<..num comp'n..> − 1::l)) ∧
  ∀n l.
    COUNT_LIST_AUX <..num comp'n..> l =
    COUNT_LIST_AUX <..num comp'n..> (<..num comp'n..> ::l)

⊢ ∀n. set (COUNT_LIST n) = count n

⊢ ∀n. COUNT_LIST n = GENLIST I n

⊢ COUNT_LIST 0 = [] ∧ ∀n. COUNT_LIST (SUC n) = SNOC n (COUNT_LIST n)

⊢ ∀n. COUNT_LIST n = COUNT_LIST_AUX n []

⊢ ∀a L L'.
    DELETE_ELEMENT a (L ⧺ L') = DELETE_ELEMENT a L ⧺ DELETE_ELEMENT a L'

⊢ ∀e L. DELETE_ELEMENT e L = FILTER (λy. e ≠ y) L

⊢ ∀l x. ALL_DISTINCT l ∧ set l = {x} ⇔ l = [x]

⊢ (∀l. DROP 0 l = l) ∧ ∀n x l. DROP (SUC n) (x::l) = DROP n l

⊢ ∀h t. DROP 1 (h::t) = t

⊢ ∀x y. x ≠ [] ⇒ DROP 1 (x ⧺ y) = DROP 1 x ⧺ y

⊢ ∀n l1 l2. DROP n (l1 ⧺ l2) = DROP n l1 ⧺ DROP (n − LENGTH l1) l2

⊢ ∀n l1. n ≤ LENGTH l1 ⇒ ∀l2. DROP n (l1 ⧺ l2) = DROP n l1 ⧺ l2

⊢ ∀l1 n. LENGTH l1 ≤ n ⇒ ∀l2. DROP n (l1 ⧺ l2) = DROP (n − LENGTH l1) l2

⊢ ∀k x. k < LENGTH x ⇒ DROP k x = x❲k❳::DROP (SUC k) x

⊢ ∀n l. n < LENGTH l ⇒ DROP n l = l❲n❳::DROP (SUC n) l

⊢ ∀n m l. n + m ≤ LENGTH l ⇒ DROP n (DROP m l) = DROP (n + m) l

⊢ ∀n m l. DROP n (DROP m l) = DROP (n + m) l

⊢ ∀ls n. n < LENGTH ls ⇒ DROP n ls = ls❲n❳::DROP (n + 1) ls

⊢ ∀n l. DROP n l = FUNPOW TL n l

⊢ ∀ls n. n < LENGTH ls ⇒ ∃u. DROP n ls = [ls❲n❳] ⧺ u

⊢ ∀n l. n ≤ LENGTH l ⇒ DROP n l = LASTN (LENGTH l − n) l

⊢ ∀l1 l2. DROP (LENGTH l1) (l1 ⧺ l2) = l2

⊢ ∀l. DROP (LENGTH l) l = []

⊢ ∀l m. m = LENGTH l ⇒ DROP m l = []

⊢ ∀l n. 0 < n ∧ n ≤ LENGTH l ⇒ DROP (n − 1) l = LAST (TAKE n l)::DROP n l

⊢ DROP n (REPLICATE m a) = REPLICATE (m − n) a

⊢ ∀n l. n ≤ LENGTH l ⇒ DROP n (REVERSE l) = REVERSE (BUTLASTN n l)

⊢ ∀n l. n ≤ LENGTH l ⇒ DROP n l = SEG (LENGTH l − n) n l

⊢ ∀n l. n ≤ LENGTH l ⇒ ∀x. DROP n (SNOC x l) = SNOC x (DROP n l)

⊢ ∀n x. DROP (SUC n) x = DROP 1 (DROP n x)

⊢ ∀ls n. DROP n (TAKE n ls) = []

⊢ (∀l. l❲0❳ = HD l) ∧ ∀l n. l❲SUC n❳ = (TL l)❲n❳

⊢ ∀l x. ELL 0 (SNOC x l) = x

⊢ ∀l2 n. LENGTH l2 ≤ n ⇒ ∀l1. ELL n (l1 ⧺ l2) = ELL (n − LENGTH l2) l1

⊢ ∀n l2. n < LENGTH l2 ⇒ ∀l1. ELL n (l1 ⧺ l2) = ELL n l2

⊢ ∀n l. n < LENGTH l ⇒ ∀x. ELL n (x::l) = ELL n l

⊢ ∀n l. n < LENGTH l ⇒ ELL n l = l❲PRE (LENGTH l − n)❳

⊢ ∀n l. n < LENGTH l ⇒ MEM (ELL n l) l

⊢ ∀l. ¬NULL l ⇒ ELL 0 l = LAST l

⊢ ∀l1 l2. ¬NULL l1 ⇒ ELL (LENGTH l2) (l1 ⧺ l2) = LAST l1

⊢ ∀l x. ELL (LENGTH l) (x::l) = x

⊢ ∀l x. ELL (LENGTH l) (SNOC x l) = if NULL l then x else HD l

⊢ ∀n l f. n < LENGTH l ⇒ ELL n (MAP f l) = f (ELL n l)

⊢ ∀n l. n < LENGTH l ⇒ MEM (ELL n l) l

⊢ ∀l. l ≠ [] ⇒ ELL (PRE (LENGTH l)) l = HD l

⊢ ∀n l. n < LENGTH l ⇒ ELL n (REVERSE l) = ELL (PRE (LENGTH l − n)) l

⊢ ∀n l. n < LENGTH l ⇒ ELL n (REVERSE l) = l❲n❳

⊢ ∀n l. n < LENGTH l ⇒ ELL n l = HD (SEG 1 (PRE (LENGTH l − n)) l)

⊢ ∀n. 0 < n ⇒ ∀x l. ELL n (SNOC x l) = ELL (PRE n) l

⊢ ∀n x l. ELL (SUC n) (SNOC x l) = ELL n l

⊢ (∀l. ELL 0 l = LAST l) ∧
  (∀n l. ELL <..num comp'n..> l = ELL (<..num comp'n..> − 1) (FRONT l)) ∧
  ∀n l. ELL <..num comp'n..> l = ELL <..num comp'n..> (FRONT l)

⊢ ∀n l1 l2.
    (l1 ⧺ l2)❲n❳ = if n < LENGTH l1 then l1❲n❳ else l2❲n − LENGTH l1❳

⊢ ∀n l1 l2. n < LENGTH l1 ⇒ (l1 ⧺ l2)❲n❳ = l1❲n❳

⊢ ∀l1 n. LENGTH l1 ≤ n ⇒ ∀l2. (l1 ⧺ l2)❲n❳ = l2❲n − LENGTH l1❳

⊢ ∀m n l. m + n < LENGTH l ⇒ (DROP n l)❲m❳ = l❲m + n❳

⊢ ∀n. 0 < n ⇒ ∀x l. (x::l)❲n❳ = l❲PRE n❳

⊢ ∀m n. m < n ⇒ (COUNT_LIST n)❲m❳ = m

⊢ ∀m n l. m + n < LENGTH l ⇒ (DROP n l)❲m❳ = l❲m + n❳

⊢ ∀n l. n < LENGTH l ⇒ l❲n❳ = ELL (PRE (LENGTH l − n)) l

⊢ ∀n x l. x < n ⇒ (TAKE n l)❲x❳ = l❲x❳

⊢ ∀l n. n < LENGTH (FRONT l) ∧ ¬NULL l ⇒ (FRONT l)❲n❳ = l❲n❳

⊢ ∀f n x. x < n ⇒ (GENLIST f n)❲x❳ = f x

⊢ ∀n l. n < LENGTH l ⇒ MEM l❲n❳ l

⊢ ∀l2 l1. ¬NULL l2 ⇒ (l1 ⧺ l2)❲LENGTH l1❳ = HD l2

⊢ ∀ls h t. (ls ⧺ h::t)❲LENGTH ls❳ = h

⊢ ∀ls h k t. (ls ⧺ h::k::t)❲LENGTH ls + 1❳ = k

⊢ ¬NULL l2 ∧ n = LENGTH l1 ⇒ (l1 ⧺ l2)❲n❳ = HD l2

⊢ ∀l x. (SNOC x l)❲LENGTH l❳ = x

⊢ ∀n l. n < LENGTH l ⇒ ∀f. (MAP f l)❲n❳ = f l❲n❳

⊢ ∀n l. n < LENGTH l ⇒ MEM l❲n❳ l

⊢ ∀l. l ≠ [] ⇒ l❲PRE (LENGTH l)❳ = LAST l

⊢ ∀n1 n2 x. n1 < n2 ⇒ (REPLICATE n2 x)❲n1❳ = x

⊢ ∀n l. n < LENGTH l ⇒ (REVERSE l)❲n❳ = l❲PRE (LENGTH l − n)❳

⊢ ∀n l. n < LENGTH l ⇒ (REVERSE l)❲n❳ = ELL n l

⊢ ∀n l. n < LENGTH l ⇒ l❲n❳ = HD (SEG 1 n l)

⊢ ∀n l. n < LENGTH l ⇒ ∀x. (SNOC x l)❲n❳ = l❲n❳

⊢ ∀ls j. j < LENGTH ls ⇒ ∃l1 l2. ls = l1 ⧺ ls❲j❳::l2

⊢ ∀ls j k.
    j < k ∧ k < LENGTH ls ⇒ ∃l1 l2 l3. ls = l1 ⧺ ls❲j❳::l2 ⧺ ls❲k❳::l3

⊢ ∀h t n. 0 ≠ n ⇒ t❲n − 1❳ = (h::t)❲n❳

⊢ ∀n x l. x < n ⇒ (TAKE n l)❲x❳ = l❲x❳

⊢ ∀k ls n.
    n < LENGTH (chunks k ls) ∧ 0 < k ∧ ¬NULL ls ⇒
    (chunks k ls)❲n❳ = TAKE k (DROP (n * k) ls)

⊢ ∀h1 h2. h1 = h2 ⇒ ∀l1 l2. l1 = l2 ⇒ h1::l1 = h2::l2

⊢ LIST_REL R l1 l2 ∧ LIST_REL R l3 l4 ⇔
  LIST_REL R (l1 ⧺ l3) (l2 ⧺ l4) ∧ LENGTH l1 = LENGTH l2 ∧
  LENGTH l3 = LENGTH l4

⊢ LIST_REL R l1 l2 ∧ LIST_REL R l3 l4 ⇒ LIST_REL R (l1 ⧺ l3) (l2 ⧺ l4)

⊢ ∀R l1 l2 n. LIST_REL R l1 l2 ⇒ LIST_REL R (DROP n l1) (DROP n l2)

⊢ ∀l1 l2. LIST_REL R l1 (REVERSE l2) ⇔ LIST_REL R (REVERSE l1) l2

⊢ ∀P xs ys n. LIST_REL P xs ys ⇒ LIST_REL P (TAKE n xs) (TAKE n ys)

⊢ ∀P l m. EVERY P l ⇒ EVERY P (BUTLASTN m l)

⊢ ∀e L P. P e ∧ EVERY P (DELETE_ELEMENT e L) ⇒ EVERY P L

⊢ ∀P l m. EVERY P l ⇒ EVERY P (DROP m l)

⊢ ∀P l. EVERY P l ⇔ FOLDL (λl' x. l' ∧ P x) T l

⊢ ∀P l. EVERY P l ⇔ FOLDL $/\ T (MAP P l)

⊢ ∀P l. EVERY P l ⇔ FOLDR (λx l'. P x ∧ l') T l

⊢ ∀P l. EVERY P l ⇔ FOLDR $/\ T (MAP P l)

⊢ ∀n. EVERY P (GENLIST f n) ⇔ ∀i. i < n ⇒ P (f i)

⊢ ∀P l m. EVERY P l ⇒ EVERY P (LASTN m l)

⊢ ∀f n x. EVERY f (REPLICATE n x) ⇔ n = 0 ∨ f x

⊢ ∀P l. EVERY P (REVERSE l) ⇔ EVERY P l

⊢ ∀P l. EVERY P l ⇒ ∀m k. m + k ≤ LENGTH l ⇒ EVERY P (SEG m k l)

⊢ ∀P l m. EVERY P l ⇒ EVERY P (TAKE m l)

⊢ ∀l m P. EXISTS P (BUTLASTN m l) ⇒ EXISTS P l

⊢ ∀P Q l. (EXISTS (λx. P x ∨ Q x) l ⇔ EXISTS P l) ∨ EXISTS Q l

⊢ ∀l m P. EXISTS P (DROP m l) ⇒ EXISTS P l

⊢ ∀P l. EXISTS P l ⇔ FOLDL (λl' x. l' ∨ P x) F l

⊢ ∀P l. EXISTS P l ⇔ FOLDL $\/ F (MAP P l)

⊢ ∀P l. EXISTS P l ⇔ FOLDR (λx l'. P x ∨ l') F l

⊢ ∀P l. EXISTS P l ⇔ FOLDR $\/ F (MAP P l)

⊢ ∀n. EXISTS P (GENLIST f n) ⇔ ∃i. i < n ∧ P (f i)

⊢ ∀l m P. EXISTS P (LASTN m l) ⇒ EXISTS P l

⊢ ∀P l. EXISTS P (REVERSE l) ⇔ EXISTS P l

⊢ ∀m k l. m + k ≤ LENGTH l ⇒ ∀P. EXISTS P (SEG m k l) ⇒ EXISTS P l

⊢ ∀l m P. EXISTS P (TAKE m l) ⇒ EXISTS P l

⊢ ∀f g.
    FCOMM f g ⇒
    ∀e. RIGHT_ID g e ⇒
        ∀l1 l2. FOLDL f e (l1 ⧺ l2) = g (FOLDL f e l1) (FOLDL f e l2)

⊢ ∀f g.
    FCOMM f g ⇒
    ∀e. RIGHT_ID g e ⇒
        ∀l. FOLDL f e (FLAT l) = FOLDL g e (MAP (FOLDL f e) l)

⊢ ∀g f.
    FCOMM g f ⇒
    ∀e. LEFT_ID g e ⇒
        ∀l1 l2. FOLDR f e (l1 ⧺ l2) = g (FOLDR f e l1) (FOLDR f e l2)

⊢ ∀g f.
    FCOMM g f ⇒
    ∀e. LEFT_ID g e ⇒
        ∀l. FOLDR f e (FLAT l) = FOLDR g e (MAP (FOLDR f e) l)

⊢ (∀P. FILTER P [] = []) ∧
  ∀P h t. FILTER P (h::t) = if P h then h::FILTER P t else FILTER P t

⊢ ∀P L M. FILTER P (L ⧺ M) = FILTER P L ⧺ FILTER P M

⊢ ∀f1 f2 l. FILTER f1 (FILTER f2 l) = FILTER f2 (FILTER f1 l)

⊢ ∀P ls l1 l2 x j.
    (let
       fs = FILTER P ls
     in
       ALL_DISTINCT ls ∧ ls = l1 ⧺ x::l2 ∧ j < LENGTH fs ⇒
       (x = fs❲j❳ ⇔ P x ∧ j = LENGTH (FILTER P l1)))

⊢ ∀P ls l1 l2 x.
    (let
       fs = FILTER P ls
     in
       ls = l1 ⧺ x::l2 ∧ P x ⇒ x = fs❲LENGTH (FILTER P l1)❳)

⊢ ∀P ls l1 l2 l3 x y.
    (let
       fs = FILTER P ls;
       j = LENGTH (FILTER P l1)
     in
       ls = l1 ⧺ x::l2 ⧺ y::l3 ∧ P x ∧ P y ∧ FILTER P l2 = [] ⇒
       x = fs❲j❳ ∧ y = fs❲j + 1❳)

⊢ ∀P ls l1 l2 l3 x y.
    (let
       fs = FILTER P ls;
       j = LENGTH (FILTER P l1)
     in
       ALL_DISTINCT ls ∧ ls = l1 ⧺ x::l2 ⧺ y::l3 ∧ P x ∧ P y ⇒
       (x = fs❲j❳ ∧ y = fs❲j + 1❳ ⇔ FILTER P l2 = []))

⊢ ∀P1 P2 l. FILTER P1 l = FILTER P2 l ⇔ ∀x. MEM x l ⇒ (P1 x ⇔ P2 x)

⊢ ∀P Q l. FILTER P (FILTER Q l) = FILTER (λx. P x ∧ Q x) l

⊢ ∀P l. FILTER P (FLAT l) = FLAT (MAP (FILTER P) l)

⊢ ∀P l. FILTER P l = FOLDL (λl' x. if P x then SNOC x l' else l') [] l

⊢ ∀P l. FILTER P l = FOLDR (λx l'. if P x then x::l' else l') [] l

⊢ ∀P ls l1 l2 x.
    ls = l1 ⧺ x::l2 ∧ P x ∧ FILTER P l1 = [] ⇒ x = HD (FILTER P ls)

⊢ ∀P ls l1 l2 x.
    ALL_DISTINCT ls ∧ ls = l1 ⧺ x::l2 ∧ P x ⇒
    (x = HD (FILTER P ls) ⇔ FILTER P l1 = [])

⊢ ∀f l. FILTER f (FILTER f l) = FILTER f l

⊢ ∀P ls l1 l2 x.
    ls = l1 ⧺ x::l2 ∧ P x ∧ FILTER P l2 = [] ⇒ x = LAST (FILTER P ls)

⊢ ∀P ls l1 l2 x.
    ALL_DISTINCT ls ∧ ls = l1 ⧺ x::l2 ∧ P x ⇒
    (x = LAST (FILTER P ls) ⇔ FILTER P l2 = [])

⊢ ∀f1 f2 l. FILTER f1 (MAP f2 l) = MAP f2 (FILTER (f1 ∘ f2) l)

⊢ ∀P ls. MONO_DEC ls ⇒ MONO_DEC (FILTER P ls)

⊢ ∀P ls. MONO_INC ls ⇒ MONO_INC (FILTER P ls)

⊢ ∀l P. FILTER P (REVERSE l) = REVERSE (FILTER P l)

⊢ ∀P x l.
    FILTER P (SNOC x l) = if P x then SNOC x (FILTER P l) else FILTER P l

⊢ ∀P ls. FILTER P ls ≤ ls

⊢ s ≠ ∅ ⇒ FINITE (common_prefixes s)

⊢ FINITE {a | a ≼ b}

⊢ (∀l. TAKE 0 l = []) ∧ ∀n x l. TAKE (SUC n) (x::l) = x::TAKE n l

⊢ ∀n l1. n ≤ LENGTH l1 ⇒ ∀l2. TAKE n (l1 ⧺ l2) = TAKE n l1

⊢ ∀l1 n.
    LENGTH l1 ≤ n ⇒ ∀l2. TAKE n (l1 ⧺ l2) = l1 ⧺ TAKE (n − LENGTH l1) l2

⊢ ∀n l. n ≤ LENGTH l ⇒ TAKE n l = BUTLASTN (LENGTH l − n) l

⊢ ∀m l. m ≤ LENGTH l ⇒ ∀n. n ≤ m ⇒ TAKE n (TAKE m l) = TAKE n l

⊢ ∀l1 l2. TAKE (LENGTH l1) (l1 ⧺ l2) = l1

⊢ ∀l. TAKE (LENGTH l) l = l

⊢ ∀n l. n ≤ LENGTH l ⇒ TAKE n (REVERSE l) = REVERSE (LASTN n l)

⊢ ∀n l. n ≤ LENGTH l ⇒ TAKE n l = SEG n 0 l

⊢ ∀n l. n ≤ LENGTH l ⇒ ∀x. TAKE n (SNOC x l) = TAKE n l

⊢ FLAT [] = [] ∧ ∀h t. FLAT (h::t) = h ⧺ FLAT t

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

⊢ ∀l. FLAT (FLAT l) = FLAT (MAP FLAT l)

⊢ ∀l. FLAT l = FOLDL $++ [] l

⊢ ∀l. FLAT l = FOLDR $++ [] l

⊢ ∀l. FLAT (REVERSE l) = REVERSE (FLAT (MAP REVERSE l))

⊢ ∀x l. FLAT (SNOC x l) = FLAT l ⧺ x

⊢ FLAT (chunks n ls) = ls

⊢ (∀f e. FOLDL f e [] = e) ∧ ∀f e x l. FOLDL f e (x::l) = FOLDL f (f e x) l

⊢ ∀f e l1 l2. FOLDL f e (l1 ⧺ l2) = FOLDL f (FOLDL f e l1) l2

⊢ ∀P f1 f2 l e.
    P e ∧ (∀x a. MEM x l ∧ P a ⇒ f1 a x = f2 a x ∧ P (f2 a x)) ⇒
    FOLDL f1 e l = FOLDL f2 e l ∧ P (FOLDL f2 e l)

⊢ ∀f e P l.
    FOLDL f e (FILTER P l) = FOLDL (λx y. if P y then f x y else x) e l

⊢ ∀f e l. FOLDL f e l = FOLDR (λx y. f y x) e (REVERSE l)

⊢ ∀f e g l. FOLDL f e (MAP g l) = FOLDL (λx y. f x (g y)) e l

⊢ ∀f e g l. FOLDL f e (MAP g l) = FOLDL (λx y. f x (g y)) e l

⊢ ∀f e l. FOLDL f e (REVERSE l) = FOLDR (λx y. f y x) e l

⊢ ∀f e x. FOLDL f e [x] = f e x

⊢ ∀f e x l. FOLDL f e (SNOC x l) = f (FOLDL f e l) x

⊢ ∀l. FOLDL (λxs x. SNOC x xs) [] l = l

⊢ (∀f e. FOLDR f e [] = e) ∧ ∀f e x l. FOLDR f e (x::l) = f x (FOLDR f e l)

⊢ ∀f e l1 l2. FOLDR f e (l1 ⧺ l2) = FOLDR f (FOLDR f e l2) l1

⊢ ∀l. FOLDR CONS [] l = l

⊢ ∀f e P l.
    FOLDR f e (FILTER P l) = FOLDR (λx y. if P x then f x y else y) e l

⊢ ∀f. (∀a b c. f a (f b c) = f b (f a c)) ⇒
      ∀e P l. FOLDR f e (FILTER P (REVERSE l)) = FOLDR f e (FILTER P l)

⊢ ∀f e. MONOID f e ⇒ ∀l. FOLDR f e l = FOLDL f e l

⊢ ∀f e l. FOLDR f e l = FOLDL (λx y. f y x) e (REVERSE l)

⊢ ∀f e g l. FOLDR f e (MAP g l) = FOLDR (λx y. f (g x) y) e l

⊢ ∀f. (∀a b c. f a (f b c) = f b (f a c)) ⇒
      ∀e g l. FOLDR f e (MAP g (REVERSE l)) = FOLDR f e (MAP g l)

⊢ ∀f e l. FOLDR f e (REVERSE l) = FOLDL (λx y. f y x) e l

⊢ ∀f e x. FOLDR f e [x] = f x e

⊢ ∀f e x l. FOLDR f e (SNOC x l) = FOLDR f (f x e) l

⊢ ∀l1 l2 e. FRONT (l1 ⧺ e::l2) = l1 ⧺ FRONT (e::l2)

⊢ ∀l1 l2. l2 ≠ [] ⇒ FRONT (l1 ⧺ l2) = l1 ⧺ FRONT l2

⊢ ∀ls. ls ≠ [] ⇒ FRONT ls = TAKE (LENGTH ls − 1) ls

⊢ ∀l n. l ≠ [] ∧ n < LENGTH (FRONT l) ⇒ (FRONT l)❲n❳ = l❲n❳

⊢ ∀l. LENGTH l = 1 ⇒ FRONT l = []

⊢ ∀l. l ≠ [] ⇒ LENGTH (FRONT l) = PRE (LENGTH l)

⊢ ∀l. 1 < LENGTH l ⇒ FRONT l ≠ []

⊢ ∀x. FRONT [x] = []

⊢ FUNPOW TL n [] = []

⊢ (∀f. GENLIST f 0 = []) ∧
  ∀f n. GENLIST f (SUC n) = SNOC (f n) (GENLIST f n)

⊢ ∀f a b. GENLIST f (a + b) = GENLIST f b ⧺ GENLIST (λt. f (t + b)) a

⊢ GENLIST f (SUC n) = f 0::GENLIST (f ∘ SUC) n

⊢ ∀n f g. GENLIST f n = GENLIST g n ⇔ ∀x. x < n ⇒ f x = g x

⊢ ∀e n m. GENLIST (K e) (n + m) = GENLIST (K e) m ⧺ GENLIST (K e) n

⊢ ∀a b c. GENLIST (K c) a ⧺ GENLIST (K c) b = GENLIST (K c) (a + b)

⊢ ∀c n. GENLIST (K c) n ⧺ [c] = [c] ⧺ GENLIST (K c) n

⊢ ∀e n. GENLIST (K e) (SUC n) = e::GENLIST (K e) n

⊢ ∀f e n. (∀k. k < n ⇒ f k = e) ⇒ GENLIST f n = GENLIST (K e) n

⊢ ∀x c n. 0 < n ⇒ (MEM x (GENLIST (K c) n) ⇔ x = c)

⊢ ∀f e n.
    (∀k. 0 < k ∧ k ≤ n ⇒ f k = e) ⇒ GENLIST (f ∘ SUC) n = GENLIST (K e) n

⊢ ∀c n. 0 < n ⇒ set (GENLIST (K c) n) = {c}

⊢ ∀h t. HD (h::t) = h

⊢ ∀h t ls. HD (h::t ⧺ ls) = h

⊢ ∀l1 l2. l1 ≠ [] ⇒ HD (l1 ⧺ l2) = HD l1

⊢ HD (GENLIST f (SUC n)) = f 0

⊢ ∀ls. ls ≠ [] ⇒ MEM (HD ls) ls

⊢ (∀x. MEM x [] ⇔ F) ∧ ∀x h t. MEM x (h::t) ⇔ x = h ∨ MEM x t

⊢ ∀e l1 l2. MEM e (l1 ⧺ l2) ⇔ MEM e l1 ∨ MEM e l2

⊢ ∀l m x. MEM x (DROP m l) ⇒ MEM x l

⊢ ∀l m x. MEM x (BUTLASTN m l) ⇒ MEM x l

⊢ ∀x l. MEM x l ⇔ EXISTS ($= x) l

⊢ ∀P L x. MEM x (FILTER P L) ⇔ P x ∧ MEM x L

⊢ ∀l m x. MEM x (TAKE m l) ⇒ MEM x l

⊢ ∀y l. MEM y l ⇔ FOLDL (λl' x. l' ∨ y = x) F l

⊢ ∀x l. MEM x l ⇔ FOLDL $\/ F (MAP ($= x) l)

⊢ ∀y l. MEM y l ⇔ FOLDR (λx l'. y = x ∨ l') F l

⊢ ∀x l. MEM x l ⇔ FOLDR $\/ F (MAP ($= x) l)

⊢ ∀m l x. MEM x (LASTN m l) ⇒ MEM x l

⊢ ∀n x y. MEM y (REPLICATE n x) ⇔ x = y ∧ 0 < n

⊢ ∀l x. MEM x (REVERSE l) ⇔ MEM x l

⊢ ∀n m l. n + m ≤ LENGTH l ⇒ ∀x. MEM x (SEG n m l) ⇒ MEM x l

⊢ ∀y x l. MEM y (SNOC x l) ⇔ y = x ∨ MEM y l

⊢ ∀x l. MEM x l ⇔ EXISTS ($= x) l

⊢ (∀l. [] ≼ l ⇔ T) ∧ (∀x l. x::l ≼ [] ⇔ F) ∧
  ∀x1 l1 x2 l2. x2::l2 ≼ x1::l1 ⇔ x1 = x2 ∧ l2 ≼ l1

⊢ ∀l l1. l1 ≼ l ∧ ALL_DISTINCT l ⇒ ALL_DISTINCT l1

⊢ ∀x y. x ≼ y ∧ y ≼ x ⇒ x = y

⊢ ∀l1 l2. l2 ≼ l1 ⇔ ∃l. l1 = l2 ⧺ l

⊢ ∀a b c. a ⧺ b ≼ c ⇒ a ≼ c

⊢ ∀a b c. a ≼ b ⧺ c ⇒ a ≼ b ∨ b ≼ a

⊢ ∀c a. a ≼ a ⧺ c

⊢ ∀a b c. a ⧺ b ≼ a ⧺ c ⇔ b ≼ c

⊢ ∀x y. FRONT (x::y) ≼ x::y

⊢ ∀l. l ≠ [] ⇒ FRONT l ≼ l

⊢ ∀l1 l2 l. l1 ≼ l ∧ l2 ≼ l ⇒ (l1 = l2 ⇔ LENGTH l1 = LENGTH l2)

⊢ ∀l l1. l1 ≼ l ⇔ ∃n. n ≤ LENGTH l ∧ l1 = TAKE n l

⊢ ∀l l1. l1 ≼ l ⇔ ∃n. l1 = TAKE n l

⊢ ∀l l1. l ≠ [] ⇒ (l1 ≼ l ⇔ l = l1 ∨ l1 ≼ FRONT l)

⊢ ∀l1 l2. l1 ≠ [] ∧ l2 ≠ [] ∧ l1 ≼ l2 ⇒ FRONT l1 ≼ FRONT l2

⊢ ∀f m n. GENLIST f m ≼ GENLIST f n ⇔ m ≤ n

⊢ ∀l l1. l1 ≼ l ⇒ l1 = TAKE (LENGTH l1) l

⊢ ∀l1 l2. l2 ≼ l1 ⇒ IS_SUBLIST l1 l2

⊢ ∀x y. x ≼ y ⇒ LENGTH x ≤ LENGTH y

⊢ ∀x y. x ≼ y ∧ LENGTH x = LENGTH y ⇔ x = y

⊢ ∀l l1 e. l1 ≼ l ∧ MEM e l1 ⇒ MEM e l

⊢ ∀x. [] ≼ x ∧ (x ≼ [] ⇔ x = [])

⊢ ∀P l. PREFIX P l ≼ l

⊢ ∀x. x ≼ x

⊢ ∀l1 l2. REVERSE l2 ≼ REVERSE l1 ⇔ IS_SUFFIX l1 l2

⊢ l ≼ SNOC x l

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

⊢ ∀l1 l2. IS_SUBLIST l1 l2 ⇔ ∃l l'. l1 = l ⧺ (l2 ⧺ l')

⊢ ∀l1 l2. IS_SUBLIST (REVERSE l1) (REVERSE l2) ⇔ IS_SUBLIST l1 l2

⊢ ∀l l1. IS_SUFFIX l l1 ∧ ALL_DISTINCT l ⇒ ALL_DISTINCT l1

⊢ ∀l1 l2. IS_SUFFIX l1 l2 ⇔ ∃l. l1 = l ⧺ l2

⊢ ∀l1 l2 l. IS_SUFFIX l2 l ⇒ IS_SUFFIX (l1 ⧺ l2) l

⊢ ∀l1 l2 a. IS_SUFFIX l1 l2 ⇒ IS_SUFFIX (a::l1) l2

⊢ ∀s h t. IS_SUFFIX s (h::t) ⇒ IS_SUFFIX s t

⊢ ∀l l1. IS_SUFFIX l l1 ⇔ ∃n. n ≤ LENGTH l ∧ l1 = DROP n l

⊢ ∀l l1. IS_SUFFIX l l1 ⇔ ∃n. l1 = DROP n l

⊢ ∀l l1. IS_SUFFIX l l1 ⇒ l1 = DROP (LENGTH l − LENGTH l1) l

⊢ ∀l l1. IS_SUFFIX l l1 ⇒ l1 = LASTN (LENGTH l1) l

⊢ ∀l1 l2. IS_SUFFIX l1 l2 ⇒ IS_SUBLIST l1 l2

⊢ ∀l. IS_SUFFIX l l

⊢ ∀l2 l1. IS_SUFFIX (REVERSE l1) (REVERSE l2) ⇔ l2 ≼ l1

⊢ ∀l1 l2 l3. IS_SUFFIX l1 l2 ∧ IS_SUFFIX l2 l3 ⇒ IS_SUFFIX l1 l3

⊢ ∀l1 l2. IS_SUFFIX l1 l2 ⇔ REVERSE l2 ≼ REVERSE l1

⊢ IS_SUFFIX ls (dropWhile P ls)

⊢ ∀f s b. FINITE s ⇒ ITSET f s b = FOLDR f b (REVERSE (SET_TO_LIST s))

⊢ ∀x l. LAST (SNOC x l) = x

⊢ (∀l. LASTN 0 l = []) ∧
  ∀n x l. LASTN (SUC n) (SNOC x l) = SNOC x (LASTN n l)

⊢ ∀l. l ≠ [] ⇒ LASTN 1 l = [LAST l]

⊢ ∀l2 n.
    LENGTH l2 ≤ n ⇒ ∀l1. LASTN n (l1 ⧺ l2) = LASTN (n − LENGTH l2) l1 ⧺ l2

⊢ ∀n l2. n ≤ LENGTH l2 ⇒ ∀l1. LASTN n (l1 ⧺ l2) = LASTN n l2

⊢ ∀n l. n ≤ LENGTH l ⇒ LASTN n l = DROP (LENGTH l − n) l

⊢ ∀n m l.
    n + m ≤ LENGTH l ⇒
    LASTN n (BUTLASTN m l) = BUTLASTN m (LASTN (n + m) l)

⊢ ∀n l. n ≤ LENGTH l ⇒ ∀x. LASTN n (x::l) = LASTN n l

⊢ ∀n l. n ≤ LENGTH l ⇒ LASTN n l = DROP (LENGTH l − n) l

⊢ ∀n l. LASTN n l = DROP (LENGTH l − n) l

⊢ ∀l n m. m ≤ LENGTH l ⇒ n ≤ m ⇒ LASTN n (LASTN m l) = LASTN n l

⊢ ∀l2 l1. LASTN (LENGTH l2) (l1 ⧺ l2) = l2

⊢ ∀l. LASTN (LENGTH l) l = l

⊢ ∀n l. n ≤ LENGTH l ⇒ ∀f. LASTN n (MAP f l) = MAP f (LASTN n l)

⊢ ∀n l. n ≤ LENGTH l ⇒ LASTN n (REVERSE l) = REVERSE (TAKE n l)

⊢ ∀n l. n ≤ LENGTH l ⇒ LASTN n l = SEG n (LENGTH l − n) l

⊢ ∀n l.
    LASTN n l =
    (let
       m = LENGTH l
     in
       if n ≤ m then DROP (m − n) l
       else FAIL LASTN $var$(longer than list) n l)

⊢ ∀h l1 l2. LAST (l1 ⧺ h::l2) = LAST (h::l2)

⊢ ∀l1 l2. l2 ≠ [] ⇒ LAST (l1 ⧺ l2) = LAST l2

⊢ (∀x. LAST [x] = x) ∧ ∀x y z. LAST (x::y::z) = LAST (y::z)

⊢ ∀h t. t ≠ [] ⇒ LAST t = (h::t)❲LENGTH t❳

⊢ ∀h t. ¬MEM h t ∧ LAST (h::t) = h ⇔ t = []

⊢ ∀n l. n ≤ LENGTH l ⇒ 0 < n ⇒ LAST (LASTN n l) = LAST l

⊢ ∀ls. ls ≠ [] ⇒ MEM (LAST ls) ls

⊢ ∀l n. 0 < n ∧ n ≤ LENGTH l ⇒ LAST (TAKE n l) = l❲PRE n❳

⊢ LENGTH [] = 0 ∧ ∀h t. LENGTH (h::t) = SUC (LENGTH t)

⊢ ∀l1 l2. LENGTH (l1 ⧺ l2) = LENGTH l1 + LENGTH l2

⊢ ∀n l. LENGTH (DROP n l) = LENGTH l − n

⊢ ∀l. l ≠ [] ⇒ LENGTH (FRONT l) = PRE (LENGTH l)

⊢ ∀n l. n ≤ LENGTH l ⇒ LENGTH (BUTLASTN n l) = LENGTH l − n

⊢ ∀l n. LENGTH l = SUC n ⇔ ∃h l'. LENGTH l' = n ∧ l = h::l'

⊢ ∀n. LENGTH (COUNT_LIST n) = n

⊢ ∀e L. MEM e L ⇒ LENGTH (DELETE_ELEMENT e L) < LENGTH L

⊢ ∀e L. LENGTH (DELETE_ELEMENT e L) ≤ LENGTH L

⊢ ∀P. (∀l. LENGTH l = 0 ⇒ P l) ⇔ P []

⊢ ∀P l. LENGTH (FILTER P l) ≤ LENGTH l

⊢ ∀P ls. EXISTS ($¬ ∘ P) ls ⇒ LENGTH (FILTER P ls) < LENGTH ls

⊢ ∀n l. n ≤ LENGTH l ⇒ LENGTH (TAKE n l) = n

⊢ ∀l. LENGTH (FLAT l) = SUM (MAP LENGTH l)

⊢ ∀n. LENGTH (FLAT (REPLICATE n ls)) = n * LENGTH ls

⊢ ∀l. LENGTH l = FOLDL (λl' x. SUC l') 0 l

⊢ ∀l. LENGTH l = FOLDR (λx l'. SUC l') 0 l

⊢ ∀l. l ≠ [] ⇒ LENGTH (FRONT l) = PRE (LENGTH l)

⊢ ∀f n. LENGTH (GENLIST f n) = n

⊢ ∀n l. n ≤ LENGTH l ⇒ LENGTH (LASTN n l) = n

⊢ ∀l f. LENGTH (MAP f l) = LENGTH l

⊢ ∀l. LENGTH l = 0 ⇔ l = []

⊢ ∀l. 0 < LENGTH l ⇔ ¬NULL l

⊢ ∀n x. LENGTH (REPLICATE n x) = n

⊢ ∀l. LENGTH (REVERSE l) = LENGTH l

⊢ ∀f e l. LENGTH (SCANL f e l) = SUC (LENGTH l)

⊢ ∀f e l. LENGTH (SCANR f e l) = SUC (LENGTH l)

⊢ ∀n k l. n + k ≤ LENGTH l ⇒ LENGTH (SEG n k l) = n

⊢ ∀x. LENGTH [x] = 1

⊢ ∀x l. LENGTH (SNOC x l) = SUC (LENGTH l)

⊢ ∀n l. LENGTH (TAKE n l) ≤ LENGTH l

⊢ ∀ls. ls ≠ [] ⇒ LENGTH (TL ls) < LENGTH ls

⊢ ∀l. LENGTH (UNZIP_FST l) = LENGTH l

⊢ ∀l. LENGTH (UNZIP_SND l) = LENGTH l

⊢ ∀l1 l2.
    LENGTH l1 = LENGTH l2 ⇒
    LENGTH (ZIP (l1,l2)) = LENGTH l1 ∧ LENGTH (ZIP (l1,l2)) = LENGTH l2

⊢ ∀n ls.
    0 < n ∧ ¬NULL ls ⇒
    LENGTH (chunks n ls) =
    LENGTH ls DIV n + bool_to_bit (¬divides n (LENGTH ls))

⊢ LENGTH (dropWhile P ls) = LENGTH ls ⇔ dropWhile P ls = ls

⊢ ∀ls. LIST_ELEM_COUNT x ls = CARD {n | n < LENGTH ls ∧ ls❲n❳ = x}

⊢ ∀e l. LIST_ELEM_COUNT e l > 0 ⇔ MEM e l

⊢ (∀e. LIST_ELEM_COUNT e [] = 0) ∧
  (∀e l1 l2.
     LIST_ELEM_COUNT e (l1 ⧺ l2) =
     LIST_ELEM_COUNT e l1 + LIST_ELEM_COUNT e l2) ∧
  (∀e h l. h = e ⇒ LIST_ELEM_COUNT e (h::l) = SUC (LIST_ELEM_COUNT e l)) ∧
  ∀e h l. h ≠ e ⇒ LIST_ELEM_COUNT e (h::l) = LIST_ELEM_COUNT e l

⊢ ∀p q. p ≠ [] ∧ q ≠ [] ⇒ (p = q ⇔ HD p = HD q ∧ TL p = TL q)

⊢ ∀ls. 0 < LENGTH ls ⇔ ls = HD ls::TL ls

⊢ ∀l1 l2. l1 ≠ l2 ⇒ ∀h1 h2. h1::l1 ≠ h2::l2

⊢ LIST_REL R (l1 ⧺ [x1]) (l2 ⧺ [x2]) ⇔ LIST_REL R l1 l2 ∧ R x1 x2

⊢ ∀R l1 l2 n. LIST_REL R l1 l2 ⇒ LIST_REL R (DROP n l1) (DROP n l2)

⊢ LIST_REL P (GENLIST f l) (GENLIST g l) ⇔ ∀i. i < l ⇒ P (f i) (g i)

⊢ LIST_REL P (REPLICATE n x) (REPLICATE n y) ⇔ 0 < n ⇒ P x y

⊢ ∀l1 l2. LIST_REL R l1 (REVERSE l2) ⇔ LIST_REL R (REVERSE l1) l2

⊢ LIST_REL R (REVERSE l1) (REVERSE l2) ⇔ LIST_REL R l1 l2

⊢ ∀P xs ys n. LIST_REL P xs ys ⇒ LIST_REL P (TAKE n xs) (TAKE n ys)

⊢ ∀x y. [x] = [y] ⇔ x = y

⊢ ∀x ls. set ls = {x} ⇔ ls ≠ [] ∧ EVERY ($= x) ls

⊢ ∀l l1. l1 ≼ l ⇒ set l1 ⊆ set l

⊢ ∀ls. ls ≠ [] ⇒ (SING (set ls) ⇔ ∃c. ls = GENLIST (K c) (LENGTH ls))

⊢ ∀l l1. IS_SUFFIX l l1 ⇒ set l1 ⊆ set l

⊢ ∀l1 l2 n x. n < LENGTH l1 ⇒ (l1 ⧺ l2)❲n ↦ x❳ = l1❲n ↦ x❳ ⧺ l2

⊢ ∀l1 l2 n x. LENGTH l1 ≤ n ⇒ (l1 ⧺ l2)❲n ↦ x❳ = l1 ⧺ l2❲n − LENGTH l1 ↦ x❳

⊢ (∀f. MAP f [] = []) ∧ ∀f h t. MAP f (h::t) = f h::MAP f t

⊢ (∀f. MAP2 f [] [] = []) ∧
  ∀f h1 t1 h2 t2. MAP2 f (h1::t1) (h2::t2) = f h1 h2::MAP2 f t1 t2

⊢ ∀ls f g1 g2.
    MAP2 f (MAP g1 ls) (MAP g2 ls) = MAP (λx. f (g1 x) (g2 x)) ls

⊢ ∀l1 l2.
    LENGTH l1 = LENGTH l2 ⇒
    ∀f. MAP2 f l1 l2 = MAP (UNCURRY f) (ZIP (l1,l2))

⊢ ∀f l1 l2. MAP f (l1 ⧺ l2) = MAP f l1 ⧺ MAP f l2

⊢ MAP f (COUNT_LIST n) = GENLIST f n

⊢ ∀f1 f2 l. MAP f1 l = MAP f2 l ⇔ ∀e. MEM e l ⇒ f1 e = f2 e

⊢ ∀f P l. (∀x. P (f x) ⇔ P x) ⇒ MAP f (FILTER P l) = FILTER P (MAP f l)

⊢ ∀f l. MAP f (FLAT l) = FLAT (MAP (MAP f) l)

⊢ ∀f l. MAP f l = FOLDL (λl' x. SNOC (f x) l') [] l

⊢ ∀f l. MAP f l = FOLDR (λx l'. f x::l') [] l

⊢ MAP (λ(x,y,z). x) funs = MAP FST funs

⊢ ∀f g n. MAP f (GENLIST g n) = GENLIST (f ∘ g) n

⊢ ∀ls f. ls ≠ [] ⇒ HD (MAP f ls) = f (HD ls)

⊢ ∀f g l. MAP f (MAP g l) = MAP (f ∘ g) l

⊢ ∀f l. MAP f (REVERSE l) = REVERSE (MAP f l)

⊢ ∀f x. MAP f [x] = [f x]

⊢ MAP SND (FILTER (λ(x,y). y ≠ z) ls) = FILTER (λy. z ≠ y) (MAP SND ls)

⊢ ∀f x l. MAP f (SNOC x l) = SNOC (f x) (MAP f l)

⊢ ∀f p q. p ≤ q ⇒ MAP f p ≤ MAP f q

⊢ ∀f g. MAP (f ∘ g) = MAP f ∘ MAP g

⊢ ∀l1 l2. MAX_LIST (l1 ⧺ l2) = MAX (MAX_LIST l1) (MAX_LIST l2)

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

⊢ ∀h t. MAX_LIST (h::t) = MAX h (MAX_LIST t)

⊢ ∀l. MAX_LIST l = 0 ⇔ EVERY (λx. x = 0) l

⊢ ∀h t. MAX_LIST t ≤ MAX_LIST (h::t)

⊢ ∀l1 l2. l1 ≼ l2 ⇒ MAX_LIST l1 ≤ MAX_LIST l2

⊢ ∀f g. (∀x. f x ≤ g x) ⇒ ∀ls. MAX_LIST (MAP f ls) ≤ MAX_LIST (MAP g ls)

⊢ ∀l. l ≠ [] ⇒ MEM (MAX_LIST l) l

⊢ ∀ls. ls ≠ [] ∧ MONO_DEC ls ⇒ MAX_LIST ls = HD ls

⊢ ∀ls. ls ≠ [] ∧ MONO_INC ls ⇒ MAX_LIST ls = LAST ls

⊢ MAX_LIST [] = 0

⊢ ∀l x. MEM x l ⇒ x ≤ MAX_LIST l

⊢ ∀x. MAX_LIST [x] = x

⊢ ∀l. l ≠ [] ⇒ ∀x. MEM x l ∧ (∀y. MEM y l ⇒ y ≤ x) ⇒ x = MAX_LIST l

⊢ ∀l1 x l2 h. MEM h (l1 ⧺ [x] ⧺ l2) ⇔ MEM h (x::(l1 ⧺ l2))

⊢ ∀l m x. MEM x (BUTLASTN m l) ⇒ MEM x l

⊢ ∀m n. MEM m (COUNT_LIST n) ⇔ m < n

⊢ ∀l m x. MEM x (DROP m l) ⇒ MEM x l

⊢ ∀x l. MEM x l ⇔ EXISTS ($= x) l

⊢ ∀y l. MEM y l ⇔ FOLDL (λl' x. l' ∨ y = x) F l

⊢ ∀x l. MEM x l ⇔ FOLDL $\/ F (MAP ($= x) l)

⊢ ∀y l. MEM y l ⇔ FOLDR (λx l'. y = x ∨ l') F l

⊢ ∀x l. MEM x l ⇔ FOLDR $\/ F (MAP ($= x) l)

⊢ ∀l e y. MEM y (FRONT (e::l)) ⇒ MEM y (e::l)

⊢ ∀ls. ls ≠ [] ∧ ALL_DISTINCT ls ⇒ ¬MEM (LAST ls) (FRONT ls)

⊢ ∀l y. l ≠ [] ∧ MEM y (FRONT l) ⇒ MEM y l

⊢ ∀e l. MEM (LAST (e::l)) (e::l)

⊢ ∀m l x. MEM x (LASTN m l) ⇒ MEM x l

⊢ ∀e l h. MEM e l ∧ e ≠ LAST (h::l) ⇒ MEM e (FRONT (h::l))

⊢ ∀e l. l ≠ [] ⇒ MEM (LAST l) l

⊢ ∀n x y. MEM y (REPLICATE n x) ⇔ x = y ∧ 0 < n

⊢ ∀n m l. n + m ≤ LENGTH l ⇒ ∀x. MEM x (SEG n m l) ⇒ MEM x l

⊢ (∀a c. d ≠ a ⧺ [b] ⧺ c) ⇔ ¬MEM b d

⊢ ∀l. ALL_DISTINCT l ⇒
      ∀x. MEM x l ⇔ ∃p1 p2. l = p1 ⧺ [x] ⧺ p2 ∧ ¬MEM x p1 ∧ ¬MEM x p2

⊢ ∀ls.
    ALL_DISTINCT ls ⇒
    ∀x. MEM x ls ⇔
        ∃k. k < LENGTH ls ∧ x = ls❲k❳ ∧
            ls = TAKE k ls ⧺ x::DROP (k + 1) ls ∧ ¬MEM x (TAKE k ls) ∧
            ¬MEM x (DROP (k + 1) ls)

⊢ ∀ls x.
    MEM x ls ⇔
    ∃k. k < LENGTH ls ∧ x = ls❲k❳ ∧ ls = TAKE k ls ⧺ x::DROP (k + 1) ls ∧
        ¬MEM x (TAKE k ls)

⊢ ∀ls x.
    MEM x ls ⇔
    ∃k. k < LENGTH ls ∧ x = ls❲k❳ ∧ ls = TAKE k ls ⧺ x::DROP (k + 1) ls ∧
        ¬MEM x (DROP (k + 1) ls)

⊢ ∀l m x. MEM x (TAKE m l) ⇒ MEM x l

⊢ ∀h t. t ≠ [] ⇒ MIN_LIST (h::t) = MIN h (MIN_LIST t)

⊢ ∀h t. t ≠ [] ⇒ MIN_LIST (h::t) ≤ MIN_LIST t

⊢ ∀l. l ≠ [] ⇒ MIN_LIST l ≤ MAX_LIST l

⊢ ∀f g. (∀x. f x ≤ g x) ⇒ ∀ls. MIN_LIST (MAP f ls) ≤ MIN_LIST (MAP g ls)

⊢ ∀l. l ≠ [] ⇒ MEM (MIN_LIST l) l

⊢ ∀ls. ls ≠ [] ∧ MONO_DEC ls ⇒ MIN_LIST ls = LAST ls

⊢ ∀ls. ls ≠ [] ∧ MONO_INC ls ⇒ MIN_LIST ls = HD ls

⊢ ∀l. l ≠ [] ⇒ ∀x. MEM x l ⇒ MIN_LIST l ≤ x

⊢ ∀x. MIN_LIST [x] = x

⊢ ∀l. l ≠ [] ⇒ ∀x. MEM x l ∧ (∀y. MEM y l ⇒ x ≤ y) ⇒ x = MIN_LIST l

⊢ MONOID $++ []

⊢ ∀l1 l2.
    SING (set l1) ∧ SING (set l2) ⇒
    (l1 = l2 ⇔ LENGTH l1 = LENGTH l2 ∧ set l1 = set l2)

⊢ ∀c ls. ls ≠ [] ∧ EVERY ($= c) ls ⇒ SING (set ls)

⊢ ∀h t. MONO_DEC (h::t) ⇒ MONO_DEC t

⊢ ∀h t x. MONO_DEC (h::t) ∧ MEM x t ⇒ x ≤ h

⊢ MONO_DEC []

⊢ ∀h t. MONO_INC (h::t) ⇒ MONO_INC t

⊢ ∀h t x. MONO_INC (h::t) ∧ MEM x t ⇒ h ≤ x

⊢ MONO_INC []

⊢ [] ∈ common_prefixes s

⊢ ∀ls. ls = [] ⇔ ∀x. ¬MEM x ls

⊢ ∀l. ¬SING (set (h::t)) ⇒ ∃h'. MEM h' t ∧ h' ≠ h

⊢ ∀P l. ¬EVERY P l ⇔ EXISTS ($¬ ∘ P) l

⊢ ∀a1 a0. a0::a1 ≠ []

⊢ ∀h1 h2. h1 ≠ h2 ⇒ ∀l1 l2. h1::l1 ≠ h2::l2

⊢ ∀e L. ¬MEM e (DELETE_ELEMENT e L)

⊢ ∀a1 a0. [] ≠ a0::a1

⊢ ∀x l. [] ≠ SNOC x l

⊢ ∀x l. ¬NULL (SNOC x l)

⊢ ∀x l. SNOC x l ≠ []

⊢ ∀P l. ¬EXISTS P l ⇔ EVERY ($¬ ∘ P) l

⊢ NULL [] ∧ ∀h t. ¬NULL (h::t)

⊢ (NULL [] ⇔ T) ∧ ∀h t. NULL (h::t) ⇔ F

⊢ ∀l. NULL l ⇔ l = []

⊢ ∀l. NULL l ⇔ FOLDL (λx l'. F) T l

⊢ ∀l. NULL l ⇔ FOLDR (λx l'. F) T l

⊢ ∀l. OR_EL l ⇔ FOLDL $\/ F l

⊢ ∀l. OR_EL l ⇔ FOLDR $\/ F l

⊢ (∀P. PREFIX P [] = []) ∧
  ∀P x l. PREFIX P (x::l) = if P x then x::PREFIX P l else []

⊢ ∀P l. PREFIX P l = FOLDR (λx l'. if P x then x::l' else []) [] l

⊢ REPLICATE n a ⧺ REPLICATE m a = REPLICATE (n + m) a

⊢ REPLICATE n x = y::r ⇔ y = x ∧ ∃m. n = SUC m ∧ r = REPLICATE m x

⊢ ∀n x. REPLICATE n x = GENLIST (K x) n

⊢ REPLICATE x y = [] ⇔ x = 0

⊢ (∀x. REPLICATE 0 x = []) ∧
  (∀n x.
     REPLICATE <..num comp'n..> x = x::REPLICATE (<..num comp'n..> − 1) x) ∧
  ∀n x. REPLICATE <..num comp'n..> x = x::REPLICATE <..num comp'n..> x

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

⊢ ∀ls n.
    n ≤ LENGTH ls ⇒
    REVERSE (DROP n ls) = REVERSE (LASTN (LENGTH ls − n) ls)

⊢ REVERSE l = [] ⇔ l = []

⊢ ∀l. REVERSE (FLAT l) = FLAT (REVERSE (MAP REVERSE l))

⊢ ∀l. REVERSE l = FOLDL (λl' x. x::l') [] l

⊢ ∀l. REVERSE l = FOLDR SNOC [] l

⊢ ∀ls. ls ≠ [] ⇒ HD (REVERSE ls) = LAST ls

⊢ ∀n x. REVERSE (REPLICATE n x) = REPLICATE n x

⊢ ∀l. REVERSE (REVERSE l) = l

⊢ ∀x. REVERSE [x] = [x]

⊢ ∀x l. REVERSE (SNOC x l) = x::REVERSE l

⊢ ∀ls. ls ≠ [] ⇒ TL (REVERSE ls) = REVERSE (FRONT ls)

⊢ ∀l1 l2.
    LENGTH l1 = LENGTH l2 ⇒
    REVERSE (ZIP (l1,l2)) = ZIP (REVERSE l1,REVERSE l2)

⊢ ∀n l. n < LENGTH l ⇒ SEG 1 n l = [l❲n❳]

⊢ ∀m l x. m ≤ LENGTH l ⇒ SEG m 0 (SNOC x l) = SEG m 0 l

⊢ ∀m l1 n l2.
    m < LENGTH l1 ∧ LENGTH l1 ≤ n + m ∧ n + m ≤ LENGTH l1 + LENGTH l2 ⇒
    SEG n m (l1 ⧺ l2) =
    SEG (LENGTH l1 − m) m l1 ⧺ SEG (n + m − LENGTH l1) 0 l2

⊢ ∀n m l1. n + m ≤ LENGTH l1 ⇒ ∀l2. SEG n m (l1 ⧺ l2) = SEG n m l1

⊢ ∀l1 m n l2.
    LENGTH l1 ≤ m ∧ n ≤ LENGTH l2 ⇒
    SEG n m (l1 ⧺ l2) = SEG n (m − LENGTH l1) l2

⊢ ∀j n h t. 0 < j ∧ n + j ≤ LENGTH t + 1 ⇒ SEG n j (h::t) = SEG n (j − 1) t

⊢ ∀n m l.
    n + m ≤ LENGTH l ⇒
    SEG n m l = LASTN n (BUTLASTN (LENGTH l − (n + m)) l)

⊢ ∀l. SEG (LENGTH l) 0 l = l

⊢ ∀l x. SEG 1 (LENGTH l) (SNOC x l) = [x]

⊢ ∀n m l.
    n + m ≤ LENGTH l ⇒
    SEG n m (REVERSE l) = REVERSE (SEG n (LENGTH l − (n + m)) l)

⊢ ∀n1 m1 n2 m2 l.
    n1 + m1 ≤ LENGTH l ∧ n2 + m2 ≤ n1 ⇒
    SEG n2 m2 (SEG n1 m1 l) = SEG n2 (m1 + m2) l

⊢ ∀n m l. n + m ≤ LENGTH l ⇒ ∀x. SEG n m (SNOC x l) = SEG n m l

⊢ ∀m n l x. SEG m (SUC n) (x::l) = SEG m n l

⊢ ∀n i l. i + n < LENGTH l ⇒ SEG (SUC n) i l = l❲i❳::SEG n (i + 1) l

⊢ ∀n m l. n + m ≤ LENGTH l ⇒ SEG n m l = TAKE n (DROP m l)

⊢ (∀k l. SEG 0 k l = []) ∧
  (∀m x l.
     SEG <..num comp'n..> 0 (x::l) = x::SEG (<..num comp'n..> − 1) 0 l) ∧
  (∀m x l. SEG <..num comp'n..> 0 (x::l) = x::SEG <..num comp'n..> 0 l) ∧
  (∀m k x l.
     SEG <..num comp'n..> <..num comp'n..> (x::l) =
     SEG <..num comp'n..> (<..num comp'n..> − 1) l) ∧
  (∀m k x l.
     SEG <..num comp'n..> <..num comp'n..> (x::l) =
     SEG <..num comp'n..> (<..num comp'n..> − 1) l) ∧
  (∀m k x l.
     SEG <..num comp'n..> <..num comp'n..> (x::l) =
     SEG <..num comp'n..> <..num comp'n..> l) ∧
  ∀m k x l.
    SEG <..num comp'n..> <..num comp'n..> (x::l) =
    SEG <..num comp'n..> <..num comp'n..> l

⊢ ∀l. LENGTH l = 1 ⇒ SING (set l)

⊢ (∀x. SNOC x [] = [x]) ∧ ∀x x' l. SNOC x (x'::l) = x'::SNOC x l

⊢ ∀x y a b. SNOC x y = SNOC a b ⇔ x = a ∧ y = b

⊢ l ≠ SNOC x l ∧ SNOC x l ≠ l

⊢ ∀x l. SNOC x l = l ⧺ [x]

⊢ ∀e f. ∃fn. fn [] = e ∧ ∀x l. fn (SNOC x l) = f x l (fn l)

⊢ ∀ll. ll = [] ∨ ∃x l. ll = SNOC x l

⊢ ∀n l. n < LENGTH l ⇒ SNOC l❲n❳ (TAKE n l) = TAKE (SUC n) l

⊢ ∀n l. n < LENGTH l ⇒ SNOC l❲n❳ (TAKE n l) = TAKE (SUC n) l

⊢ ∀x1 l1 x2 l2. SNOC x1 l1 = SNOC x2 l2 ⇒ LENGTH l1 = LENGTH l2

⊢ ∀x l. SNOC x l = FOLDR CONS [x] l

⊢ ∀P. P [] ∧ (∀l. P l ⇒ ∀x. P (SNOC x l)) ⇒ ∀l. P l

⊢ ∀l x n. LASTN (SUC n) (SNOC x l) = SNOC x (LASTN n l)

⊢ ∀l. l ≠ [] ⇒ l = SNOC (LAST l) (FRONT l)

⊢ ∀n x. SNOC x (REPLICATE n x) = REPLICATE (SUC n) x

⊢ ∀x l. SNOC x l = REVERSE (x::REVERSE l)

⊢ (∀P. EXISTS P [] ⇔ F) ∧ ∀P h t. EXISTS P (h::t) ⇔ P h ∨ EXISTS P t

⊢ ∀P l1 l2. EXISTS P (l1 ⧺ l2) ⇔ EXISTS P l1 ∨ EXISTS P l2

⊢ ∀l m P. EXISTS P (DROP m l) ⇒ EXISTS P l

⊢ ∀l m P. EXISTS P (BUTLASTN m l) ⇒ EXISTS P l

⊢ ∀P Q l. (EXISTS (λx. P x ∨ Q x) l ⇔ EXISTS P l) ∨ EXISTS Q l

⊢ ∀l m P. EXISTS P (TAKE m l) ⇒ EXISTS P l

⊢ ∀P l. EXISTS P l ⇔ FOLDL (λl' x. l' ∨ P x) F l

⊢ ∀P l. EXISTS P l ⇔ FOLDL $\/ F (MAP P l)

⊢ ∀P l. EXISTS P l ⇔ FOLDR (λx l'. P x ∨ l') F l

⊢ ∀P l. EXISTS P l ⇔ FOLDR $\/ F (MAP P l)

⊢ ∀l m P. EXISTS P (LASTN m l) ⇒ EXISTS P l

⊢ ∀P f l. EXISTS P (MAP f l) ⇔ EXISTS (λx. P (f x)) l

⊢ ∀P l. EXISTS P (REVERSE l) ⇔ EXISTS P l

⊢ ∀m k l. m + k ≤ LENGTH l ⇒ ∀P. EXISTS P (SEG m k l) ⇒ EXISTS P l

⊢ ∀P x l. EXISTS P (SNOC x l) ⇔ P x ∨ EXISTS P l

⊢ ∀l1 l2.
    SPLITP P (l1 ⧺ l2) =
    if EXISTS P l1 then (FST (SPLITP P l1),SND (SPLITP P l1) ⧺ l2)
    else (l1 ⧺ FST (SPLITP P l2),SND (SPLITP P l2))

⊢ ∀P l. EVERY (λx. ¬P x) l ⇒ SPLITP P l = (l,[])

⊢ ∀P ls l r. SPLITP P ls = (l,r) ⇒ EVERY ($¬ ∘ P) l ∧ (¬NULL r ⇒ P (HD r))

⊢ ∀ls l r. SPLITP P ls = (l,r) ⇒ ls = l ⧺ r

⊢ ∀l. LENGTH (FST (SPLITP P l)) + LENGTH (SND (SPLITP P l)) = LENGTH l

⊢ ∀ls r. SPLITP P ls = ([],r) ⇒ r = ls

⊢ ∀ls r. SPLITP P ls = (r,[]) ⇔ r = ls ∧ EVERY ($¬ ∘ P) ls

⊢ SPLITP = SPLITP_TAILREC []

⊢ SPLITP P = splitAtPki (K P) $,

⊢ SUM [] = 0 ∧ ∀h t. SUM (h::t) = h + SUM t

⊢ ∀l1 l2. SUM (l1 ⧺ l2) = SUM l1 + SUM l2

⊢ ∀l. SUM (FLAT l) = SUM (MAP SUM l)

⊢ ∀l. SUM l = FOLDL $+ 0 l

⊢ ∀l. SUM l = FOLDR $+ 0 l

⊢ (∀m. m < n ⇒ g m = ∑ (λx. f (x + k * m)) (count k)) ⇒
  ∑ f (count (k * n)) = ∑ g (count n)

⊢ ∑ f (count n) = SUM (GENLIST f n)

⊢ ∀n k. SUM (REPLICATE n k) = n * k

⊢ ∀l. SUM (REVERSE l) = SUM l

⊢ ∀x l. SUM (SNOC x l) = SUM l + x

⊢ ∀p q. p ≤ q ⇒ SUM p ≤ SUM q

⊢ ∀ls. ls ≠ [] ⇒ TL ls = DROP 1 ls

⊢ (∀l. TAKE 0 l = []) ∧ ∀n x l. TAKE (SUC n) (x::l) = x::TAKE n l

⊢ ∀x y. x ≠ [] ⇒ TAKE 1 (x ⧺ y) = TAKE 1 x

⊢ ∀n l1 l2. TAKE n (l1 ⧺ l2) = TAKE n l1 ⧺ TAKE (n − LENGTH l1) l2

⊢ ∀n l1. n ≤ LENGTH l1 ⇒ ∀l2. TAKE n (l1 ⧺ l2) = TAKE n l1

⊢ ∀l1 n.
    LENGTH l1 ≤ n ⇒ ∀l2. TAKE n (l1 ⧺ l2) = l1 ⧺ TAKE (n − LENGTH l1) l2

⊢ ∀n l. n ≤ LENGTH l ⇒ TAKE n l = BUTLASTN (LENGTH l − n) l

⊢ ∀n l. n < LENGTH l ⇒ TAKE n l ⧺ [l❲n❳] ⧺ DROP (SUC n) l = l

⊢ ∀ls m n. TAKE m (DROP n ls) = DROP n (TAKE (n + m) ls)

⊢ ∀ls n. n < LENGTH ls ⇒ TAKE (n + 1) ls = SNOC ls❲n❳ (TAKE n ls)

⊢ ∀l n. l ≠ [] ∧ n < LENGTH l ⇒ TAKE n (FRONT l) = TAKE n l

⊢ ∀l1 l2. TAKE (LENGTH l1) (l1 ⧺ l2) = l1

⊢ ∀l1 l2 x k. TAKE (LENGTH l1) (l1 ⧺ l2)❲LENGTH l1 + k ↦ x❳ = l1

⊢ ∀ls. ls ≠ [] ⇒ TAKE (PRE (LENGTH ls)) ls = FRONT ls

⊢ ∀n l. n ≤ LENGTH l ⇒ TAKE n (REVERSE l) = REVERSE (LASTN n l)

⊢ ∀n l. n ≤ LENGTH l ⇒ TAKE n l = SEG n 0 l

⊢ ∀n i l. i + n ≤ LENGTH l ⇒ TAKE i l ⧺ SEG n i l ⧺ DROP (i + n) l = l

⊢ ∀n l. n ≤ LENGTH l ⇒ ∀x. TAKE n (SNOC x l) = TAKE n l

⊢ ∀n x. TAKE (SUC n) x = TAKE n x ⧺ TAKE 1 (DROP n x)

⊢ ∀k x. k < LENGTH x ⇒ TAKE (SUC k) x = SNOC x❲k❳ (TAKE k x)

⊢ ∀m l. m ≤ LENGTH l ⇒ ∀n. n ≤ m ⇒ TAKE n (TAKE m l) = TAKE n l

⊢ ∀m l n. n ≤ m ⇒ TAKE n (TAKE m l) = TAKE n l

⊢ ∀h t. TL (h::t) = t

⊢ ∀ls n. n < LENGTH ls ⇒ TL (DROP n ls) = DROP n (TL ls)

⊢ ∀f n. TL (GENLIST f (SUC n)) = GENLIST (f ∘ SUC) n

⊢ ∀x l. TL (SNOC x l) = if NULL l then [] else SNOC x (TL l)

⊢ ∀e L. UNIQUE e L ⇔ LIST_ELEM_COUNT e L = 1

⊢ UNZIP [] = ([],[]) ∧
  ∀x l. UNZIP (x::l) = (FST x::FST (UNZIP l),SND x::SND (UNZIP l))

⊢ ∀x l.
    UNZIP (SNOC x l) =
    (SNOC (FST x) (FST (UNZIP l)),SNOC (SND x) (SND (UNZIP l)))

⊢ ∀l1 l2. LENGTH l1 = LENGTH l2 ⇒ UNZIP (ZIP (l1,l2)) = (l1,l2)

⊢ ZIP ([],[]) = [] ∧
  ∀x1 l1 x2 l2. ZIP (x1::l1,x2::l2) = (x1,x2)::ZIP (l1,l2)

⊢ ∀a b c d.
    LENGTH a = LENGTH b ∧ LENGTH c = LENGTH d ⇒
    ZIP (a,b) ⧺ ZIP (c,d) = ZIP (a ⧺ c,b ⧺ d)

⊢ n = LENGTH l1 ⇒
  ZIP (l1,COUNT_LIST n) = GENLIST (λn. (l1❲n❳,n)) (LENGTH l1)

⊢ ∀n a b.
    n ≤ LENGTH a ∧ LENGTH a = LENGTH b ⇒
    ZIP (TAKE n a,TAKE n b) = TAKE n (ZIP (a,b))

⊢ ∀n a b.
    n ≤ LENGTH a ∧ LENGTH a ≤ LENGTH b ⇒
    ZIP (TAKE n a,TAKE n b) = TAKE n (ZIP (a,TAKE (LENGTH a) b))

⊢ ∀l f n. LENGTH l = n ⇒ ZIP (l,GENLIST f n) = GENLIST (λx. (l❲x❳,f x)) n

⊢ ∀ls f g. ZIP (MAP f ls,MAP g ls) = MAP (λx. (f x,g x)) ls

⊢ ∀l1 l2.
    LENGTH l1 = LENGTH l2 ⇒
    ∀x1 x2. ZIP (SNOC x1 l1,SNOC x2 l2) = SNOC (x1,x2) (ZIP (l1,l2))

⊢ ∀n a b.
    n ≤ LENGTH a ∧ LENGTH a = LENGTH b ⇒
    ZIP (TAKE n a,TAKE n b) = TAKE n (ZIP (a,b))

⊢ ∀n a b.
    n ≤ LENGTH a ∧ LENGTH a ≤ LENGTH b ⇒
    ZIP (TAKE n a,TAKE n b) = TAKE n (ZIP (a,TAKE (LENGTH a) b))

⊢ ∀l. ZIP (UNZIP l) = l

⊢ ∀n. ALL_DISTINCT (COUNT_LIST n)

⊢ ∀ls. ALL_DISTINCT ls ⇒ INJ (λj. ls❲j❳) (count (LENGTH ls)) 𝕌(:α)

⊢ chunks 0 ls = [ls]

⊢ ∀n ls. chunks n (MAP f ls) = MAP (MAP f) (chunks n ls)

⊢ chunks n [] = [[]]

⊢ ∀n ls m.
    divides n m ∧ 0 < m ⇒
    chunks n (TAKE m ls) = TAKE (m DIV n) (chunks n ls)

⊢ ∀n ls l2.
    LENGTH ls = LENGTH l2 ⇒
    chunks n (ZIP (ls,l2)) = MAP ZIP (ZIP (chunks n ls,chunks n l2))

⊢ ∀n l1 l2.
    0 < n ∧ divides n (LENGTH l1) ∧ ¬NULL l1 ∧ ¬NULL l2 ⇒
    chunks n (l1 ⧺ l2) = chunks n l1 ⧺ chunks n l2

⊢ ∀n ls.
    chunks n ls =
    if LENGTH ls ≤ n ∨ n = 0 then [ls] else TAKE n ls::chunks n (DROP n ls)

⊢ ∀P. (∀n ls. (¬(LENGTH ls ≤ n ∨ n = 0) ⇒ P n (DROP n ls)) ⇒ P n ls) ⇒
      ∀v v1. P v v1

⊢ chunks (LENGTH ls) ls = [ls]

⊢ ∀n ls. chunks n ls ≠ []

⊢ ∀n ls acc.
    chunks_tr_aux n ls acc =
    if LENGTH ls ≤ SUC n then REVERSE (ls::acc)
    else chunks_tr_aux n (DROP (SUC n) ls) (TAKE (SUC n) ls::acc)

⊢ ∀P. (∀n ls acc.
         (¬(LENGTH ls ≤ SUC n) ⇒
          P n (DROP (SUC n) ls) (TAKE (SUC n) ls::acc)) ⇒
         P n ls acc) ⇒
      ∀v v1 v2. P v v1 v2

⊢ ∀n ls acc. chunks_tr_aux n ls acc = REVERSE acc ⧺ chunks (SUC n) ls

⊢ chunks_tr = chunks

⊢ common_prefixes s = BIGINTER (IMAGE (λl. {p | p ≼ l}) s)

⊢ common_prefixes ({x; y} ∪ rest) = common_prefixes ({lcp2 x y} ∪ rest)

⊢ [] ∈ s ⇒ common_prefixes s = {[]}

⊢ common_prefixes s ≠ ∅

⊢ common_prefixes {[]; x} = {[]} ∧ common_prefixes {x; []} = {[]} ∧
  common_prefixes {a::xs; b::ys} =
  [] INSERT if a = b then IMAGE (CONS a) (common_prefixes {xs; ys}) else ∅

⊢ ∀n. n ≠ 0 ⇒ COUNT_LIST n = 0::MAP SUC (COUNT_LIST (n − 1))

⊢ ∀n ls.
    ls ≠ [] ∧ divides n (LENGTH ls) ⇒ EVERY ($= n ∘ LENGTH) (chunks n ls)

⊢ ∀n f m. n < m ⇒ (MAP f (COUNT_LIST m))❲n❳ = f n

⊢ ∀P n. EVERY P (COUNT_LIST n) ⇔ ∀m. m < n ⇒ P m

⊢ ∀n l1 l2. l1 ≼ l2 ∧ n < LENGTH l1 ∧ n < LENGTH l2 ⇒ l1❲n❳ = l2❲n❳

⊢ lcp2 (lcp2 x y) z = lcp2 x (lcp2 y z)

⊢ lcp2 x y = [] ⇔ x = [] ∨ y = [] ∨ HD x ≠ HD y

⊢ p ≼ x ∧ p ≼ y ⇒ p ≼ lcp2 x y

⊢ lcp2 x y ≼ x ∧ lcp2 x y ≼ y

⊢ lcp2 xs ys =
  case xs of
    [] => []
  | x::xs =>
    case ys of [] => [] | y::ys => if x = y then x::lcp2 xs ys else []

⊢ lcp (x::xs) = if NULL xs then x else lcp2 x (lcp xs)

⊢ lcp (x::y::xs) = lcp (lcp2 x y::xs)

⊢ ∀ls. lcp ls = [] ⇔ ls = [] ∨ ∃x y. MEM x ls ∧ MEM y ls ∧ lcp2 x y = []

⊢ lcp [] = []

⊢ lcp ls = case ls of [] => [] | [x] => x | x::y::xs => lcp (lcp2 x y::xs)

⊢ lcp [x] = x

⊢ ∀ls.
    (∀x. MEM x ls ⇒ lcp ls ≼ x) ∧
    (ls ≠ [] ⇒ ∀p. (∀x. MEM x ls ⇒ p ≼ x) ⇒ p ≼ lcp ls)

⊢ ∀f l1 l2 n.
    n ≤ LENGTH l1 ∧ LIST_REL f l1 l2 ⇒
    LIST_REL f (BUTLASTN n l1) (BUTLASTN n l2)

⊢ ∀f l1 l2 n.
    n ≤ LENGTH l1 ∧ LIST_REL f l1 l2 ⇒ LIST_REL f (LASTN n l1) (LASTN n l2)

⊢ ∀ls. set ls = IMAGE (λj. ls❲j❳) (count (LENGTH ls))

⊢ longest_prefix ∅ = []

⊢ longest_prefix ({x; y} ∪ rest) = longest_prefix ({lcp2 x y} ∪ rest)

⊢ [] ∈ s ⇒ longest_prefix s = []

⊢ longest_prefix {[]; ys} = [] ∧ longest_prefix {xs; []} = [] ∧
  longest_prefix {x::xs; y::ys} =
  if x = y then x::longest_prefix {xs; ys} else []

⊢ longest_prefix {s} = s

⊢ s ≠ ∅ ∧ is_measure_maximal LENGTH (common_prefixes s) x ∧
  is_measure_maximal LENGTH (common_prefixes s) y ⇒
  x = y

⊢ ∀f n x. MAP f (REPLICATE n x) = REPLICATE n (f x)

⊢ nub (GENLIST f n) =
  MAP f (FILTER (λi. ∀j. i < j ∧ j < n ⇒ f i ≠ f j) (COUNT_LIST n))

⊢ ∀l l1 l2. l1 ≼ l ∧ l2 ≼ l ⇒ l1 ≼ l2 ∨ l2 ≼ l1

⊢ ∀ls n. set ls = count n ⇒ ∀j. j < LENGTH ls ⇒ ls❲j❳ < n

⊢ ∀p q. p ≤ q ∧ ALL_DISTINCT q ⇒ ALL_DISTINCT p

⊢ ∀ls sl. sl ≤ ls ∧ MONO_DEC ls ⇒ MONO_DEC sl

⊢ ∀ls sl. sl ≤ ls ∧ MONO_INC ls ⇒ MONO_INC sl

⊢ ∀p q. p ≤ q ∧ q ≤ p ⇒ p = q

⊢ ∀h t q. h::t ≤ q ⇔ ∃x y. q = x ⧺ h::y ∧ t ≤ y

⊢ ∀p q h. p ≤ q ⇒ p ⧺ [h] ≤ q ⧺ [h]

⊢ ∀p q h. p ≤ q ⇔ p ⧺ [h] ≤ q ⧺ [h]

⊢ ∀p q x. p ≤ q ⇒ p ≤ x ⧺ q

⊢ ∀p q h. p ⧺ [h] ≤ q ⧺ [h] ⇒ p ≤ q

⊢ ∀a b c d. a ≤ b ∧ c ≤ d ⇒ a ⧺ c ≤ b ⧺ d

⊢ ∀p q. p ≤ q ⧺ p

⊢ ∀p q x. x ⧺ p ≤ q ⇒ p ≤ q

⊢ ∀p q. p ≤ p ⧺ q

⊢ ∀h p q. p ≤ q ⇔ h::p ≤ h::q

⊢ ∀h. (∀p q. h::p ≤ q ⇒ p ≤ q) ⇔ ∀p q. p ≤ q ⇒ p ≤ h::q

⊢ ∀h p q. p ≤ q ⇒ p ≤ h::q

⊢ ∀h p q. h::p ≤ q ⇒ p ≤ q

⊢ (∀x. [] ≤ x ⇔ T) ∧ (∀t1 h1. h1::t1 ≤ [] ⇔ F) ∧
  ∀t2 t1 h2 h1. h1::t1 ≤ h2::t2 ⇔ h1 = h2 ∧ t1 ≤ t2 ∨ h1 ≠ h2 ∧ h1::t1 ≤ t2

⊢ ∀ls n. DROP n ls ≤ ls

⊢ ∀l ls. l ≤ ls ⇒ ∀P. EVERY P ls ⇒ EVERY P l

⊢ ∀ls. ls ≠ [] ⇒ FRONT ls ≤ ls

⊢ ∀ls. ls ≠ [] ⇒ [HD ls] ≤ ls

⊢ ∀P. (∀x. P [] x) ∧ (∀h1 t1. P (h1::t1) []) ∧
      (∀h1 t1 h2 t2. P t1 t2 ∧ P (h1::t1) t2 ⇒ P (h1::t1) (h2::t2)) ⇒
      ∀v v1. P v v1

⊢ ∀P. (∀y. P [] y) ∧ (∀h x y. P x y ∧ x ≤ y ⇒ P (h::x) (h::y)) ∧
      (∀h x y. P x y ∧ x ≤ y ⇒ P x (h::y)) ⇒
      ∀x y. x ≤ y ⇒ P x y

⊢ ∀ls. ls ≠ [] ⇒ [LAST ls] ≤ ls

⊢ ∀p q. p ≤ q ⇒ LENGTH p ≤ LENGTH q

⊢ ∀p q x. p ≤ q ∧ MEM x p ⇒ MEM x q

⊢ ∀ls x. MEM x ls ⇒ [x] ≤ ls

⊢ ∀p. [] ≤ p

⊢ ∀p. p ≤ [] ⇔ p = []

⊢ ∀ls sl x.
    sl ≤ ls ∧ MEM x sl ⇒
    ∃l1 l2 l3 l4.
      ls = l1 ⧺ [x] ⧺ l2 ∧ sl = l3 ⧺ [x] ⧺ l4 ∧ l3 ≤ l1 ∧ l4 ≤ l2

⊢ ∀x p q. p ≤ q ⇔ x ⧺ p ≤ x ⧺ q

⊢ ∀p q. p ⧺ q ≤ q ⇒ p = []

⊢ ∀p. p ≤ p

⊢ ∀h p q. p ≤ q ⇒ SNOC h p ≤ SNOC h q

⊢ ∀ls sl. sl ≤ ls ⇒ set sl ⊆ set ls

⊢ ∀x p q. p ≤ q ⇔ p ⧺ x ≤ q ⧺ x

⊢ ∀ls. ls ≠ [] ⇒ TL ls ≤ ls

⊢ ∀ls n. TAKE n ls ≤ ls

⊢ ∀p q r. p ≤ q ∧ q ≤ r ⇒ p ≤ r

⊢ ∑ (λm. ∑ (f m) (count a)) (count b) =
  ∑ (λm. f (m DIV a) (m MOD a)) (count (a * b))

⊢ ∀n m l. m ≤ n ⇒ TAKE m l ⧺ TAKE (n − m) (DROP m l) = TAKE n l

⊢ s ≠ ∅ ∧ p1 ∈ common_prefixes s ∧ p2 ∈ common_prefixes s ⇒
  p1 ≼ p2 ∨ p2 ≼ p1