Theory "rich_list"

Signature

Definitions

UNZIP_SND_DEF

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

UNZIP_FST_DEF

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

TL_T_def

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

SUFFIX_DEF

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

SPLITR_def

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

SPLITP_AUX_def

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

SPLITP

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

SPLITL_def

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

SEG

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

SCANR

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

SCANL

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

REPLICATE

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

PREFIX_DEF

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

OR_EL_DEF

⊢ OR_EL = EXISTS I

longest_prefix_def

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

LIST_ELEM_COUNT_DEF

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

LASTN_def

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

IS_SUFFIX

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

IS_SUBLIST

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

ELL

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

COUNT_LIST_def

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

COUNT_LIST_AUX_def

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

common_prefixes_def

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

BUTLASTN_def

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

AND_EL_DEF

⊢ AND_EL = EVERY I

Theorems

ZIP_TAKE_LEQ

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

ZIP_TAKE

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

ZIP_SNOC

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

ZIP_COUNT_LIST

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

ZIP_APPEND

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

UNZIP_SNOC

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

UNIQUE_LIST_ELEM_COUNT

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

two_common_prefixes

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

TL_SNOC

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

TAKE_TAKE_T

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

TAKE_TAKE

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

TAKE_SNOC

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

TAKE_SEG_DROP

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

TAKE_SEG

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

TAKE_REVERSE

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

TAKE_PRE_LENGTH

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

TAKE_LENGTH_APPEND

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

TAKE_EL_SNOC

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

take_drop_partition

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

TAKE_BUTLASTN

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

TAKE_APPEND2

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

TAKE_APPEND1

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

TAKE_APPEND

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

TAKE

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

SUM_REVERSE

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

SUM_REPLICATE

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

SUM_FOLDR

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

SUM_FOLDL

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

SUM_FLAT

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

SPLITP_splitAtPki

⊢ SPLITP P = splitAtPki (K P) $,

SPLITP_NIL_SND_EVERY

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

SPLITP_NIL_FST_IMP

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

SPLITP_LENGTH

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

SPLITP_JOIN

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

SPLITP_IMP

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

SPLITP_EVERY

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

SPLITP_compute

⊢ SPLITP = SPLITP_AUX []

SPLITP_APPEND

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

SNOC_REVERSE_CONS

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

SNOC_REPLICATE

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

SNOC_FOLDR

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

SNOC_EQ_LENGTH_EQ

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

SNOC_EL_TAKE

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

SEG_TAKE_DROP

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

SEG_SUC_EL

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

SEG_SUC_CONS

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

SEG_SNOC

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

SEG_SEG

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

SEG_REVERSE

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

SEG_LENGTH_SNOC

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

SEG_LENGTH_ID

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

SEG_LASTN_BUTLASTN

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

SEG_CONS

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

SEG_compute

⊢ (∀k l. SEG 0 k l = []) ∧
  (∀m x l. SEG (NUMERAL (BIT1 m)) 0 (x::l) = x::SEG (NUMERAL (BIT1 m) − 1) 0 l) ∧
  (∀m x l. SEG (NUMERAL (BIT2 m)) 0 (x::l) = x::SEG (NUMERAL (BIT1 m)) 0 l) ∧
  (∀m k x l.
       SEG (NUMERAL (BIT1 m)) (NUMERAL (BIT1 k)) (x::l) =
       SEG (NUMERAL (BIT1 m)) (NUMERAL (BIT1 k) − 1) l) ∧
  (∀m k x l.
       SEG (NUMERAL (BIT2 m)) (NUMERAL (BIT1 k)) (x::l) =
       SEG (NUMERAL (BIT2 m)) (NUMERAL (BIT1 k) − 1) l) ∧
  (∀m k x l.
       SEG (NUMERAL (BIT1 m)) (NUMERAL (BIT2 k)) (x::l) =
       SEG (NUMERAL (BIT1 m)) (NUMERAL (BIT1 k)) l) ∧
  ∀m k x l.
      SEG (NUMERAL (BIT2 m)) (NUMERAL (BIT2 k)) (x::l) =
      SEG (NUMERAL (BIT2 m)) (NUMERAL (BIT1 k)) l

SEG_APPEND2

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

SEG_APPEND1

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

SEG_APPEND

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

SEG_0_SNOC

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

SEG1

⊢ ∀n l. n < LENGTH l ⇒ (SEG 1 n l = [EL n l])

REVERSE_ZIP

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

REVERSE_REPLICATE

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

REVERSE_FOLDR

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

REVERSE_FOLDL

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

REVERSE_FLAT

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

REVERSE_DROP

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

REPLICATE_NIL

⊢ (REPLICATE x y = []) ⇔ (x = 0)

REPLICATE_GENLIST

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

REPLICATE_compute

⊢ (∀x. REPLICATE 0 x = []) ∧
  (∀n x.
       REPLICATE (NUMERAL (BIT1 n)) x = x::REPLICATE (NUMERAL (BIT1 n) − 1) x) ∧
  ∀n x. REPLICATE (NUMERAL (BIT2 n)) x = x::REPLICATE (NUMERAL (BIT1 n)) x

REPLICATE_APPEND

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

prefixes_is_prefix_total

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

PREFIX_FOLDR

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

PREFIX

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

OR_EL_FOLDR

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

OR_EL_FOLDL

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

NULL_FOLDR

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

NULL_FOLDL

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

NOT_SNOC_NIL

⊢ ∀x l. SNOC x l ≠ []

NOT_NULL_SNOC

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

NOT_NIL_SNOC

⊢ ∀x l. [] ≠ SNOC x l

NIL_IN_common_prefixes

⊢ [] ∈ common_prefixes s

MONOID_APPEND_NIL

⊢ MONOID $++ []

MEM_TAKE_IMP

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

MEM_TAKE

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

MEM_SING_APPEND

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

MEM_SEG

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

MEM_REPLICATE

⊢ ∀n. 0 < n ⇒ ∀x. MEM x (REPLICATE n x)

MEM_LASTN

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

MEM_LAST_FRONT

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

MEM_LAST

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

MEM_FRONT

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

MEM_FOLDR_MAP

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

MEM_FOLDR

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

MEM_FOLDL_MAP

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

MEM_FOLDL

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

MEM_EXISTS

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

MEM_DROP_IMP

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

MEM_COUNT_LIST

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

MEM_BUTLASTN

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

MAP_SND_FILTER_NEQ

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

MAP_REVERSE

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

map_replicate

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

MAP_FST_funs

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

MAP_FOLDR

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

MAP_FOLDL

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

MAP_FLAT

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

MAP_FILTER

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

MAP_COUNT_LIST

⊢ MAP f (COUNT_LIST n) = GENLIST f n

LUPDATE_APPEND2

⊢ ∀l1 l2 n x.
      LENGTH l1 ≤ n ⇒
      (LUPDATE x n (l1 ++ l2) = l1 ++ LUPDATE x (n − LENGTH l1) l2)

LUPDATE_APPEND1

⊢ ∀l1 l2 n x. n < LENGTH l1 ⇒ (LUPDATE x n (l1 ++ l2) = LUPDATE x n l1 ++ l2)

longest_prefix_UNIQUE

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

longest_prefix_SING

⊢ longest_prefix {s} = s

longest_prefix_PAIR

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

longest_prefix_NIL

⊢ [] ∈ s ⇒ (longest_prefix s = [])

longest_prefix_EMPTY

⊢ longest_prefix ∅ = []

LIST_TO_SET_EQ_SING

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

LIST_REL_REVERSE_EQ

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

LIST_REL_REPLICATE_same

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

list_rel_lastn

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

LIST_REL_GENLIST

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

list_rel_butlastn

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

LIST_REL_APPEND_SING

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

LIST_ELEM_COUNT_THM

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

LIST_ELEM_COUNT_MEM

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

LIST_ELEM_COUNT_CARD_EL

⊢ ∀ls. LIST_ELEM_COUNT x ls = CARD {n | n < LENGTH ls ∧ (EL n ls = x)}

LENGTH_UNZIP_SND

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

LENGTH_UNZIP_FST

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

LENGTH_SEG

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

LENGTH_SCANR

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

LENGTH_SCANL

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

LENGTH_REPLICATE

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

LENGTH_NOT_NULL

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

LENGTH_LASTN

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

LENGTH_FRONT

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

LENGTH_FOLDR

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

LENGTH_FOLDL

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

LENGTH_FLAT_REPLICATE

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

LENGTH_FLAT

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

LENGTH_FILTER_LESS

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

LENGTH_FILTER_LEQ

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

LENGTH_COUNT_LIST

⊢ ∀n. LENGTH (COUNT_LIST n) = n

LENGTH_BUTLASTN

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

LASTN_SEG

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

LASTN_REVERSE

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

LASTN_MAP

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

LASTN_LENGTH_ID

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

LASTN_LENGTH_APPEND

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

LASTN_LASTN

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

LASTN_DROP

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

LASTN_CONS

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

LASTN_compute

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

LASTN_BUTLASTN

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

LASTN_APPEND2

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

LASTN_APPEND1

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

LASTN_1

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

LASTN

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

LAST_LASTN_LAST

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

IS_SUFFIX_TRANS

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

IS_SUFFIX_REVERSE

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

IS_SUFFIX_REFL

⊢ ∀l. IS_SUFFIX l l

IS_SUFFIX_IS_SUBLIST

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

IS_SUFFIX_CONS2_E

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

IS_SUFFIX_CONS

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

IS_SUFFIX_compute

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

IS_SUFFIX_APPEND

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

IS_SUBLIST_REVERSE

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

IS_SUBLIST_APPEND

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

IS_PREFIX_TRANS

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

IS_PREFIX_SNOC

⊢ ∀x y z. z ≼ SNOC x y ⇔ z ≼ y ∨ (z = SNOC x y)

IS_PREFIX_REVERSE

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

IS_PREFIX_REFL

⊢ ∀x. x ≼ x

IS_PREFIX_PREFIX

⊢ ∀P l. PREFIX P l ≼ l

IS_PREFIX_NIL

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

IS_PREFIX_LENGTH_ANTI

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

IS_PREFIX_LENGTH

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

IS_PREFIX_IS_SUBLIST

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

is_prefix_el

⊢ ∀n l1 l2. l1 ≼ l2 ∧ n < LENGTH l1 ∧ n < LENGTH l2 ⇒ (EL n l1 = EL n l2)

IS_PREFIX_BUTLAST

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

IS_PREFIX_APPENDS

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

IS_PREFIX_APPEND3

⊢ ∀c a. a ≼ a ++ c

IS_PREFIX_APPEND2

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

IS_PREFIX_APPEND1

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

IS_PREFIX_APPEND

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

IS_PREFIX_ANTISYM

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

IS_PREFIX

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

FRONT_APPEND

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

FOLDR_SNOC

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

FOLDR_SINGLE

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

FOLDR_REVERSE

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

FOLDR_MAP_REVERSE

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

FOLDR_MAP

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

FOLDR_FOLDL_REVERSE

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

FOLDR_FOLDL

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

FOLDR_FILTER_REVERSE

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

FOLDR_FILTER

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

FOLDR_CONS_NIL

⊢ ∀l. FOLDR CONS [] l = l

FOLDR_APPEND

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

FOLDL_SNOC_NIL

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

FOLDL_SINGLE

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

FOLDL_REVERSE

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

FOLDL_MAP2

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

FOLDL_MAP

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

FOLDL_FOLDR_REVERSE

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

FOLDL_FILTER

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

FOLDL_APPEND

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

FLAT_SNOC

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

FLAT_REVERSE

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

FLAT_FOLDR

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

FLAT_FOLDL

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

FLAT_FLAT

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

FINITE_prefix

⊢ FINITE {a | a ≼ b}

FINITE_common_prefixes

⊢ s ≠ ∅ ⇒ FINITE (common_prefixes s)

FILTER_SNOC

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

FILTER_MAP

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

FILTER_IDEM

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

FILTER_FOLDR

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

FILTER_FOLDL

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

FILTER_FLAT

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

FILTER_FILTER

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

FILTER_EQ

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

FILTER_COMM

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

FCOMM_FOLDR_FLAT

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

FCOMM_FOLDR_APPEND

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

FCOMM_FOLDL_FLAT

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

FCOMM_FOLDL_APPEND

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

EXISTS_TAKE_IMP

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

EXISTS_TAKE

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

EXISTS_SEG

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

EXISTS_REVERSE

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

EXISTS_LASTN

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

EXISTS_FOLDR_MAP

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

EXISTS_FOLDR

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

EXISTS_FOLDL_MAP

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

EXISTS_FOLDL

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

EXISTS_DROP_IMP

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

EXISTS_DROP

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

EXISTS_DISJ

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

EXISTS_BUTLASTN

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

EVERY_TAKE

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

EVERY_SEG

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

EVERY_REVERSE

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

EVERY_REPLICATE

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

EVERY_LASTN

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

EVERY_FOLDR_MAP

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

EVERY_FOLDR

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

EVERY_FOLDL_MAP

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

EVERY_FOLDL

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

EVERY_DROP

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

every_count_list

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

EVERY_BUTLASTN

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

EVERY2_TAKE

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

EVERY2_REVERSE1

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

EVERY2_DROP

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

EVERY2_APPEND_suff

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

EVERY2_APPEND

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

ELL_SUC_SNOC

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

ELL_SNOC

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

ELL_SEG

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

ELL_REVERSE_EL

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

ELL_REVERSE

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

ELL_PRE_LENGTH

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

ELL_MEM

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

ELL_MAP

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

ELL_LENGTH_SNOC

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

ELL_LENGTH_CONS

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

ELL_LENGTH_APPEND

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

ELL_LAST

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

ELL_EL

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

ELL_CONS

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

ELL_compute

⊢ (∀l. ELL 0 l = LAST l) ∧
  (∀n l. ELL (NUMERAL (BIT1 n)) l = ELL (NUMERAL (BIT1 n) − 1) (FRONT l)) ∧
  ∀n l. ELL (NUMERAL (BIT2 n)) l = ELL (NUMERAL (BIT1 n)) (FRONT l)

ELL_APPEND2

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

ELL_APPEND1

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

ELL_0_SNOC

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

EL_SEG

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

EL_REVERSE_ELL

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

EL_REPLICATE

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

EL_PRE_LENGTH

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

EL_MEM

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

el_map_count

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

EL_LENGTH_APPEND_rwt

⊢ ¬NULL l2 ∧ (n = LENGTH l1) ⇒ (EL n (l1 ++ l2) = HD l2)

EL_LENGTH_APPEND

⊢ ∀l2 l1. ¬NULL l2 ⇒ (EL (LENGTH l1) (l1 ++ l2) = HD l2)

EL_FRONT

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

EL_ELL

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

EL_COUNT_LIST

⊢ ∀m n. m < n ⇒ (EL m (COUNT_LIST n) = m)

EL_CONS

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

EL_APPEND2

⊢ ∀l1 n. LENGTH l1 ≤ n ⇒ ∀l2. EL n (l1 ++ l2) = EL (n − LENGTH l1) l2

EL_APPEND1

⊢ ∀n l1 l2. n < LENGTH l1 ⇒ (EL n (l1 ++ l2) = EL n l1)

DROP_SNOC

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

DROP_SEG

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

DROP_REVERSE

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

DROP_REPLICATE

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

DROP_LENGTH_NIL_rwt

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

DROP_LENGTH_NIL

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

DROP_LENGTH_APPEND

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

DROP_LASTN

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

DROP_FUNPOW_TL

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

DROP_EL_CONS

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

DROP_DROP_T

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

DROP_DROP

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

DROP_CONS_EL

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

DROP_APPEND2

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

DROP_APPEND1

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

DROP_APPEND

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

DROP

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

count_list_sub1

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

COUNT_LIST_SNOC

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

COUNT_LIST_GENLIST

⊢ ∀n. COUNT_LIST n = GENLIST I n

COUNT_LIST_COUNT

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

COUNT_LIST_compute

⊢ ∀n. COUNT_LIST n = COUNT_LIST_AUX n []

COUNT_LIST_AUX_compute

⊢ (∀l. COUNT_LIST_AUX 0 l = l) ∧
  (∀n l.
       COUNT_LIST_AUX (NUMERAL (BIT1 n)) l =
       COUNT_LIST_AUX (NUMERAL (BIT1 n) − 1) (NUMERAL (BIT1 n) − 1::l)) ∧
  ∀n l.
      COUNT_LIST_AUX (NUMERAL (BIT2 n)) l =
      COUNT_LIST_AUX (NUMERAL (BIT1 n)) (NUMERAL (BIT1 n)::l)

COUNT_LIST_ADD

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

CONS_APPEND

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

common_prefixes_PAIR

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

common_prefixes_NONEMPTY

⊢ common_prefixes s ≠ ∅

common_prefixes_NIL

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

common_prefixes_BIGINTER

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

COMM_MONOID_FOLDR

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

COMM_MONOID_FOLDL

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

COMM_ASSOC_FOLDR_REVERSE

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

COMM_ASSOC_FOLDL_REVERSE

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

BUTLASTN_TAKE

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

BUTLASTN_SUC_FRONT

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

BUTLASTN_SEG

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

BUTLASTN_REVERSE

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

BUTLASTN_MAP

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

BUTLASTN_LENGTH_NIL

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

BUTLASTN_LENGTH_CONS

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

BUTLASTN_LENGTH_APPEND

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

BUTLASTN_LASTN_NIL

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

BUTLASTN_LASTN

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

BUTLASTN_FRONT

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

BUTLASTN_CONS

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

BUTLASTN_compute

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

BUTLASTN_BUTLASTN

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

BUTLASTN_APPEND2

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

BUTLASTN_APPEND1

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

BUTLASTN_1

⊢ ∀l. l ≠ [] ⇒ (BUTLASTN 1 l = FRONT l)

BUTLASTN

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

ASSOC_FOLDR_FLAT

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

ASSOC_FOLDL_FLAT

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

ASSOC_APPEND

⊢ ASSOC $++

APPEND_TAKE_LASTN

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

APPEND_SNOC1

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

APPEND_NIL

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

APPEND_FOLDR

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

APPEND_FOLDL

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

APPEND_BUTLASTN_LASTN

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

APPEND_BUTLASTN_DROP

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

APPEND_ASSOC_CONS

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

AND_EL_FOLDR

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

AND_EL_FOLDL

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

ALL_EL_MAP

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

ALL_DISTINCT_MEM_ZIP_MAP

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

ALL_DISTINCT_DROP

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

all_distinct_count_list

⊢ ∀n. ALL_DISTINCT (COUNT_LIST n)