Theory "list"

Signature

Definitions

ZIP_def

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

UNZIP

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

UNIQUE_DEF

⊢ ∀e L. UNIQUE e L ⇔ ∃L1 L2. (L1 ++ [e] ++ L2 = L) ∧ ¬MEM e L1 ∧ ¬MEM e L2

TL_DEF

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

TAKE_def

⊢ (∀n. TAKE n [] = []) ∧
  ∀n x xs. TAKE n (x::xs) = if n = 0 then [] else x::TAKE (n − 1) xs

SUM_ACC_DEF

⊢ (∀acc. SUM_ACC [] acc = acc) ∧
  ∀h t acc. SUM_ACC (h::t) acc = SUM_ACC t (h + acc)

SUM

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

splitAtPki_def

⊢ (∀P k. splitAtPki P k [] = k [] []) ∧
  ∀P k h t.
      splitAtPki P k (h::t) =
      if P 0 h then k [] (h::t) else splitAtPki (P ∘ SUC) (λp s. k (h::p) s) t

SNOC

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

SHORTLEX_def

⊢ (∀R l2. SHORTLEX R [] l2 ⇔ l2 ≠ []) ∧
  ∀R h1 t1 l2.
      SHORTLEX R (h1::t1) l2 ⇔
      case l2 of
        [] => F
      | h2::t2 =>
        if LENGTH t1 < LENGTH t2 then T
        else if LENGTH t1 = LENGTH t2 then
          if R h1 h2 then T else if h1 = h2 then SHORTLEX R t1 t2 else F
        else F

SET_TO_LIST_primitive_def

⊢ SET_TO_LIST =
  WFREC (@R. WF R ∧ ∀s. FINITE s ∧ s ≠ ∅ ⇒ R (REST s) s)
    (λSET_TO_LIST a.
         I
           (if FINITE a then
              if a = ∅ then [] else CHOICE a::SET_TO_LIST (REST a)
            else ARB))

REVERSE_DEF

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

REV_DEF

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

PAD_RIGHT

⊢ ∀c n s. PAD_RIGHT c n s = s ++ GENLIST (K c) (n − LENGTH s)

PAD_LEFT

⊢ ∀c n s. PAD_LEFT c n s = GENLIST (K c) (n − LENGTH s) ++ s

OPT_MMAP_def

⊢ (∀f. OPT_MMAP f [] = SOME []) ∧
  ∀f h0 t0.
      OPT_MMAP f (h0::t0) =
      OPTION_BIND (f h0) (λh. OPTION_BIND (OPT_MMAP f t0) (λt. SOME (h::t)))

oHD_def

⊢ ∀l. oHD l = case l of [] => NONE | h::v1 => SOME h

oEL_def

⊢ (∀n. oEL n [] = NONE) ∧
  ∀n x xs. oEL n (x::xs) = if n = 0 then SOME x else oEL (n − 1) xs

NULL_DEF

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

nub_def

⊢ (nub [] = []) ∧ ∀x l. nub (x::l) = if MEM x l then nub l else x::nub l

MAP

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

LUPDATE_def

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

LRC_def

⊢ (∀R x y. LRC R [] x y ⇔ (x = y)) ∧
  ∀R h t x y. LRC R (h::t) x y ⇔ (x = h) ∧ ∃z. R x z ∧ LRC R t z y

LLEX_def

⊢ (∀R l2. LLEX R [] l2 ⇔ l2 ≠ []) ∧
  ∀R h1 t1 l2.
      LLEX R (h1::t1) l2 ⇔
      case l2 of
        [] => F
      | h2::t2 => if R h1 h2 then T else if h1 = h2 then LLEX R t1 t2 else F

list_TY_DEF

⊢ ∃rep.
      TYPE_DEFINITION
        (λa0'.
             ∀ $var$('list').
                 (∀a0'.
                      (a0' = ind_type$CONSTR 0 ARB (λn. ind_type$BOTTOM)) ∨
                      (∃a0 a1.
                           (a0' =
                            (λa0 a1.
                                 ind_type$CONSTR (SUC 0) a0
                                   (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
                              a0 a1) ∧ $var$('list') a1) ⇒
                      $var$('list') a0') ⇒
                 $var$('list') a0') rep

LIST_TO_SET_DEF

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

list_size_def

⊢ (∀f. list_size f [] = 0) ∧
  ∀f a0 a1. list_size f (a0::a1) = 1 + (f a0 + list_size f a1)

LIST_LIFT2_def

⊢ ∀f xs ys. LIST_LIFT2 f xs ys = MAP f xs <*> ys

LIST_IGNORE_BIND_def

⊢ ∀m1 m2. LIST_IGNORE_BIND m1 m2 = LIST_BIND m1 (K m2)

LIST_GUARD_def

⊢ ∀b. LIST_GUARD b = if b then [()] else []

list_case_def

⊢ (∀v f. list_CASE [] v f = v) ∧ ∀a0 a1 v f. list_CASE (a0::a1) v f = f a0 a1

LIST_BIND_def

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

LIST_APPLY_def

⊢ ∀fs xs. fs <*> xs = LIST_BIND fs (combin$C MAP xs)

LENGTH

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

LEN_DEF

⊢ (∀n. LEN [] n = n) ∧ ∀h t n. LEN (h::t) n = LEN t (n + 1)

LAST_DEF

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

isPREFIX

⊢ (∀l. [] ≼ l ⇔ T) ∧
  ∀h t l. h::t ≼ l ⇔ case l of [] => F | h'::t' => (h = h') ∧ t ≼ t'

INDEX_OF_def

⊢ ∀x. INDEX_OF x = OPTION_MAP FST ∘ INDEX_FIND 0 ($= x)

INDEX_FIND_def

⊢ (∀i P. INDEX_FIND i P [] = NONE) ∧
  ∀i P h t.
      INDEX_FIND i P (h::t) =
      if P h then SOME (i,h) else INDEX_FIND (SUC i) P t

HD

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

GENLIST_AUX

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

GENLIST

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

FRONT_DEF

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

FOLDR

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

FOLDL

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

FLAT

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

FIND_def

⊢ ∀P. FIND P = OPTION_MAP SND ∘ INDEX_FIND 0 P

FILTER

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

EXISTS_DEF

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

EVERYi_def

⊢ (∀P. EVERYi P [] ⇔ T) ∧ ∀P h t. EVERYi P (h::t) ⇔ P 0 h ∧ EVERYi (P ∘ SUC) t

EVERY_DEF

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

EL

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

dropWhile_def

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

DROP_def

⊢ (∀n. DROP n [] = []) ∧
  ∀n x xs. DROP n (x::xs) = if n = 0 then x::xs else DROP (n − 1) xs

APPEND

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

ALL_DISTINCT

⊢ (ALL_DISTINCT [] ⇔ T) ∧
  ∀h t. ALL_DISTINCT (h::t) ⇔ ¬MEM h t ∧ ALL_DISTINCT t

Theorems

ZIP_UNZIP

⊢ ∀l. ZIP (UNZIP l) = l

ZIP_MAP

⊢ ∀l1 l2 f1 f2.
      (LENGTH l1 = LENGTH l2) ⇒
      (ZIP (MAP f1 l1,l2) = MAP (λp. (f1 (FST p),SND p)) (ZIP (l1,l2))) ∧
      (ZIP (l1,MAP f2 l2) = MAP (λp. (FST p,f2 (SND p))) (ZIP (l1,l2)))

ZIP_GENLIST

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

ZIP_EQ_NIL

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

ZIP_DROP

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

ZIP

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

WF_SHORTLEX_same_lengths

⊢ WF R ⇒
  ∀l s.
      (∀d. d ∈ s ⇒ (LENGTH d = l)) ∧ (∃a. a ∈ s) ⇒
      ∃b. b ∈ s ∧ ∀c. SHORTLEX R c b ⇒ c ∉ s

WF_SHORTLEX

⊢ WF R ⇒ WF (SHORTLEX R)

WF_LIST_PRED

⊢ WF (λL1 L2. ∃h. L2 = h::L1)

UNZIP_ZIP

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

UNZIP_THM

⊢ (UNZIP [] = ([],[])) ∧
  (UNZIP ((x,y)::t) = (let (L1,L2) = UNZIP t in (x::L1,y::L2)))

UNZIP_MAP

⊢ ∀L. UNZIP L = (MAP FST L,MAP SND L)

UNIQUE_LENGTH_FILTER

⊢ ∀e L. UNIQUE e L ⇔ (LENGTH (FILTER ($= e) L) = 1)

UNIQUE_FILTER

⊢ ∀e L. UNIQUE e L ⇔ (FILTER ($= e) L = [e])

UNION_APPEND

⊢ ∀l1 l2. LIST_TO_SET l1 ∪ LIST_TO_SET l2 = LIST_TO_SET (l1 ++ l2)

TL_GENLIST

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

TL

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

TAKE_TAKE_MIN

⊢ ∀m n. TAKE n (TAKE m l) = TAKE (MIN n m) l

TAKE_SUM

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

TAKE_splitAtPki

⊢ TAKE n l = splitAtPki (K ∘ $= n) K l

TAKE_nil

⊢ ∀n. TAKE n [] = []

TAKE_LENGTH_TOO_LONG

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

TAKE_LENGTH_ID_rwt

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

TAKE_LENGTH_ID

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

TAKE_GENLIST

⊢ TAKE n (GENLIST f m) = GENLIST f (MIN n m)

TAKE_EQ_NIL

⊢ (TAKE n l = []) ⇔ (n = 0) ∨ (l = [])

TAKE_DROP

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

TAKE_cons

⊢ 0 < n ⇒ (TAKE n (x::xs) = x::TAKE (n − 1) xs)

TAKE_compute

⊢ (∀l. TAKE 0 l = []) ∧ (∀n. TAKE (NUMERAL (BIT1 n)) [] = []) ∧
  (∀n. TAKE (NUMERAL (BIT2 n)) [] = []) ∧
  (∀n h t. TAKE (NUMERAL (BIT1 n)) (h::t) = h::TAKE (NUMERAL (BIT1 n) − 1) t) ∧
  ∀n h t. TAKE (NUMERAL (BIT2 n)) (h::t) = h::TAKE (NUMERAL (BIT1 n)) t

TAKE_APPEND2

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

TAKE_APPEND1

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

TAKE_0

⊢ TAKE 0 l = []

TAKE1_DROP

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

TAKE1

⊢ ∀l. l ≠ [] ⇒ (TAKE 1 l = [EL 0 l])

SWAP_REVERSE_SYM

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

SWAP_REVERSE

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

SUM_SUM_ACC

⊢ ∀L. SUM L = SUM_ACC L 0

SUM_SNOC

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

SUM_MAP_PLUS_ZIP

⊢ ∀ls1 ls2.
      (LENGTH ls1 = LENGTH ls2) ∧ (∀x y. f (x,y) = g x + h y) ⇒
      (SUM (MAP f (ZIP (ls1,ls2))) = SUM (MAP g ls1) + SUM (MAP h ls2))

SUM_MAP_PLUS

⊢ ∀f g ls. SUM (MAP (λx. f x + g x) ls) = SUM (MAP f ls) + SUM (MAP g ls)

SUM_MAP_MEM_bound

⊢ ∀f x ls. MEM x ls ⇒ f x ≤ SUM (MAP f ls)

SUM_MAP_FOLDL

⊢ ∀ls. SUM (MAP f ls) = FOLDL (λa e. a + f e) 0 ls

SUM_IMAGE_LIST_TO_SET_upper_bound

⊢ ∀ls. ∑ f (LIST_TO_SET ls) ≤ SUM (MAP f ls)

SUM_IMAGE_eq_SUM_MAP_SET_TO_LIST

⊢ FINITE s ⇒ (∑ f s = SUM (MAP f (SET_TO_LIST s)))

SUM_eq_0

⊢ ∀ls. (SUM ls = 0) ⇔ ∀x. MEM x ls ⇒ (x = 0)

SUM_APPEND

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

SUM_ACC_SUM_LEM

⊢ ∀L n. SUM_ACC L n = SUM L + n

splitAtPki_RAND

⊢ f (splitAtPki P k l) = splitAtPki P ($o f ∘ k) l

splitAtPki_MAP

⊢ splitAtPki P k (MAP f l) =
  splitAtPki (combin$C ($o ∘ P) f) (combin$C ($o ∘ k ∘ MAP f) (MAP f)) l

splitAtPki_EQN

⊢ splitAtPki P k l =
  case OLEAST i. i < LENGTH l ∧ P i (EL i l) of
    NONE => k l []
  | SOME i => k (TAKE i l) (DROP i l)

splitAtPki_change_predicate

⊢ (∀i. i < LENGTH l ⇒ (P1 i (EL i l) ⇔ P2 i (EL i l))) ⇒
  (splitAtPki P1 k l = splitAtPki P2 k l)

splitAtPki_APPEND

⊢ ∀l1 l2 P k.
      EVERYi (λi. $~ ∘ P i) l1 ∧ (0 < LENGTH l2 ⇒ P (LENGTH l1) (HD l2)) ⇒
      (splitAtPki P k (l1 ++ l2) = k l1 l2)

SNOC_INDUCT

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

SNOC_CASES

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

SNOC_Axiom

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

SNOC_APPEND

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

SNOC_11

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

SINGL_SINGL_APPLY

⊢ [f] <*> [x] = [f x]

SINGL_LIST_APPLY_R

⊢ LIST_BIND l (λx. [x]) = l

SINGL_LIST_APPLY_L

⊢ LIST_BIND [x] f = f x

SINGL_APPLY_PERMUTE

⊢ fs <*> [x] = [(λf. f x)] <*> fs

SINGL_APPLY_MAP

⊢ [f] <*> l = MAP f l

SING_HD

⊢ (([HD xs] = xs) ⇔ (LENGTH xs = 1)) ∧ ((xs = [HD xs]) ⇔ (LENGTH xs = 1))

SHORTLEX_transitive

⊢ transitive R ⇒ transitive (SHORTLEX R)

SHORTLEX_total

⊢ total (RC R) ⇒ total (RC (SHORTLEX R))

SHORTLEX_THM

⊢ (¬SHORTLEX R [] [] ∧ ¬SHORTLEX R (h1::t1) []) ∧ SHORTLEX R [] (h2::t2) ∧
  (SHORTLEX R (h1::t1) (h2::t2) ⇔
   LENGTH t1 < LENGTH t2 ∨
   (LENGTH t1 = LENGTH t2) ∧ (R h1 h2 ∨ (h1 = h2) ∧ SHORTLEX R t1 t2))

SHORTLEX_NIL2

⊢ ¬SHORTLEX R l []

SHORTLEX_MONO

⊢ (∀x y. R1 x y ⇒ R2 x y) ⇒ SHORTLEX R1 x y ⇒ SHORTLEX R2 x y

SHORTLEX_LENGTH_LE

⊢ ∀l1 l2. SHORTLEX R l1 l2 ⇒ LENGTH l1 ≤ LENGTH l2

SET_TO_LIST_THM

⊢ FINITE s ⇒
  (SET_TO_LIST s = if s = ∅ then [] else CHOICE s::SET_TO_LIST (REST s))

SET_TO_LIST_SING

⊢ SET_TO_LIST {x} = [x]

SET_TO_LIST_INV

⊢ ∀s. FINITE s ⇒ (LIST_TO_SET (SET_TO_LIST s) = s)

SET_TO_LIST_IND

⊢ ∀P. (∀s. (FINITE s ∧ s ≠ ∅ ⇒ P (REST s)) ⇒ P s) ⇒ ∀v. P v

SET_TO_LIST_IN_MEM

⊢ ∀s. FINITE s ⇒ ∀x. x ∈ s ⇔ MEM x (SET_TO_LIST s)

SET_TO_LIST_EMPTY

⊢ SET_TO_LIST ∅ = []

SET_TO_LIST_CARD

⊢ ∀s. FINITE s ⇒ (LENGTH (SET_TO_LIST s) = CARD s)

REVERSE_SNOC_DEF

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

REVERSE_SNOC

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

REVERSE_REVERSE

⊢ ∀l. REVERSE (REVERSE l) = l

REVERSE_REV

⊢ ∀L. REVERSE L = REV L []

REVERSE_o_REVERSE

⊢ REVERSE ∘ REVERSE ∘ f = f

REVERSE_GENLIST

⊢ REVERSE (GENLIST f n) = GENLIST (λm. f (PRE n − m)) n

REVERSE_EQ_SING

⊢ (REVERSE l = [e]) ⇔ (l = [e])

REVERSE_EQ_NIL

⊢ (REVERSE l = []) ⇔ (l = [])

REVERSE_APPEND

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

REVERSE_11

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

REV_REVERSE_LEM

⊢ ∀L1 L2. REV L1 L2 = REVERSE L1 ++ L2

OPT_MMAP_cong

⊢ ∀f1 f2 x1 x2.
      (x1 = x2) ∧ (∀a. MEM a x2 ⇒ (f1 a = f2 a)) ⇒
      (OPT_MMAP f1 x1 = OPT_MMAP f2 x2)

oHD_thm

⊢ (oHD [] = NONE) ∧ (oHD (h::t) = SOME h)

oEL_THM

⊢ ∀xs n. oEL n xs = if n < LENGTH xs then SOME (EL n xs) else NONE

oEL_TAKE_E

⊢ (oEL n (TAKE m xs) = SOME x) ⇒ (oEL n xs = SOME x)

oEL_LUPDATE

⊢ ∀xs i n x.
      oEL n (LUPDATE x i xs) =
      if i ≠ n then oEL n xs else if i < LENGTH xs then SOME x else NONE

oEL_EQ_EL

⊢ ∀xs n y. (oEL n xs = SOME y) ⇔ n < LENGTH xs ∧ (y = EL n xs)

oEL_DROP

⊢ oEL n (DROP m xs) = oEL (m + n) xs

NULL_LENGTH

⊢ ∀l. NULL l ⇔ (LENGTH l = 0)

NULL_GENLIST

⊢ ∀n f. NULL (GENLIST f n) ⇔ (n = 0)

NULL_FILTER

⊢ ∀P ls. NULL (FILTER P ls) ⇔ ∀x. MEM x ls ⇒ ¬P x

NULL_EQ

⊢ ∀l. NULL l ⇔ (l = [])

NULL_APPEND

⊢ NULL (l1 ++ l2) ⇔ NULL l1 ∧ NULL l2

NULL

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

nub_set

⊢ ∀l. LIST_TO_SET (nub l) = LIST_TO_SET l

nub_append

⊢ ∀l1 l2. nub (l1 ++ l2) = nub (FILTER (λx. ¬MEM x l2) l1) ++ nub l2

NRC_LRC

⊢ NRC R n x y ⇔ ∃ls. LRC R ls x y ∧ (LENGTH ls = n)

NOT_NULL_MEM

⊢ ∀l. ¬NULL l ⇔ ∃e. MEM e l

NOT_NIL_EQ_LENGTH_NOT_0

⊢ x ≠ [] ⇔ 0 < LENGTH x

NOT_NIL_CONS

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

NOT_EXISTS

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

NOT_EVERY

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

NOT_EQ_LIST

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

NOT_CONS_NIL

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

MONO_EXISTS

⊢ (∀x. P x ⇒ Q x) ⇒ EXISTS P l ⇒ EXISTS Q l

MONO_EVERY

⊢ (∀x. P x ⇒ Q x) ⇒ EVERY P l ⇒ EVERY Q l

MEM_ZIP_MEM_MAP

⊢ (LENGTH (FST ps) = LENGTH (SND ps)) ∧ MEM p (ZIP ps) ⇒
  MEM (FST p) (FST ps) ∧ MEM (SND p) (SND ps)

MEM_ZIP

⊢ ∀l1 l2 p.
      (LENGTH l1 = LENGTH l2) ⇒
      (MEM p (ZIP (l1,l2)) ⇔ ∃n. n < LENGTH l1 ∧ (p = (EL n l1,EL n l2)))

MEM_SPLIT_APPEND_last

⊢ MEM e l ⇔ ∃pfx sfx. (l = pfx ++ [e] ++ sfx) ∧ ¬MEM e sfx

MEM_SPLIT_APPEND_first

⊢ MEM e l ⇔ ∃pfx sfx. (l = pfx ++ [e] ++ sfx) ∧ ¬MEM e pfx

MEM_SPLIT

⊢ ∀x l. MEM x l ⇔ ∃l1 l2. l = l1 ++ x::l2

MEM_SNOC

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

MEM_SET_TO_LIST

⊢ ∀s. FINITE s ⇒ ∀x. MEM x (SET_TO_LIST s) ⇔ x ∈ s

MEM_REVERSE

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

MEM_MAP

⊢ ∀l f x. MEM x (MAP f l) ⇔ ∃y. (x = f y) ∧ MEM y l

MEM_LUPDATE_E

⊢ ∀l x y i. MEM x (LUPDATE y i l) ⇒ (x = y) ∨ MEM x l

MEM_LUPDATE

⊢ ∀l x y i.
      MEM x (LUPDATE y i l) ⇔
      i < LENGTH l ∧ (x = y) ∨ ∃j. j < LENGTH l ∧ i ≠ j ∧ (EL j l = x)

MEM_GENLIST

⊢ MEM x (GENLIST f n) ⇔ ∃m. m < n ∧ (x = f m)

MEM_FLAT

⊢ ∀x L. MEM x (FLAT L) ⇔ ∃l. MEM l L ∧ MEM x l

MEM_FILTER

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

mem_exists_set

⊢ ∀x y l. MEM (x,y) l ⇒ ∃z. (x = FST z) ∧ MEM z l

MEM_EL

⊢ ∀l x. MEM x l ⇔ ∃n. n < LENGTH l ∧ (x = EL n l)

MEM_dropWhile_IMP

⊢ ∀P ls x. MEM x (dropWhile P ls) ⇒ MEM x ls

MEM_DROP

⊢ ∀x ls n. MEM x (DROP n ls) ⇔ ∃m. m + n < LENGTH ls ∧ (x = EL (m + n) ls)

MEM_APPEND_lemma

⊢ ∀a b c d x.
      (a ++ [x] ++ b = c ++ [x] ++ d) ∧ ¬MEM x b ∧ ¬MEM x a ⇒
      (a = c) ∧ (b = d)

MEM_APPEND

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

MEM

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

MAP_ZIP_SAME

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

MAP_ZIP

⊢ (LENGTH l1 = LENGTH l2) ⇒
  (MAP FST (ZIP (l1,l2)) = l1) ∧ (MAP SND (ZIP (l1,l2)) = l2) ∧
  (MAP (f ∘ FST) (ZIP (l1,l2)) = MAP f l1) ∧
  (MAP (g ∘ SND) (ZIP (l1,l2)) = MAP g l2)

MAP_TL

⊢ ∀l f. ¬NULL l ⇒ (MAP f (TL l) = TL (MAP f l))

MAP_TAKE

⊢ ∀f n l. MAP f (TAKE n l) = TAKE n (MAP f l)

MAP_SNOC

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

MAP_o

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

MAP_MAP_o

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

MAP_LIST_BIND

⊢ MAP f (LIST_BIND l g) = LIST_BIND l (MAP f ∘ g)

MAP_ID

⊢ (MAP (λx. x) l = l) ∧ (MAP I l = l)

MAP_GENLIST

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

MAP_FRONT

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

MAP_FLAT

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

MAP_EQ_SING

⊢ (MAP f l = [x]) ⇔ ∃x0. (l = [x0]) ∧ (x = f x0)

MAP_EQ_NIL

⊢ ∀l f. ((MAP f l = []) ⇔ (l = [])) ∧ (([] = MAP f l) ⇔ (l = []))

MAP_EQ_f

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

MAP_EQ_EVERY2

⊢ ∀f1 f2 l1 l2.
      (MAP f1 l1 = MAP f2 l2) ⇔
      (LENGTH l1 = LENGTH l2) ∧ LIST_REL (λx y. f1 x = f2 y) l1 l2

MAP_EQ_CONS

⊢ (MAP f l = h::t) ⇔ ∃x0 t0. (l = x0::t0) ∧ (h = f x0) ∧ (t = MAP f t0)

MAP_EQ_APPEND

⊢ (MAP f l = l1 ++ l2) ⇔
  ∃l10 l20. (l = l10 ++ l20) ∧ (l1 = MAP f l10) ∧ (l2 = MAP f l20)

MAP_DROP

⊢ ∀l i. MAP f (DROP i l) = DROP i (MAP f l)

MAP_CONG

⊢ ∀l1 l2 f f'.
      (l1 = l2) ∧ (∀x. MEM x l2 ⇒ (f x = f' x)) ⇒ (MAP f l1 = MAP f' l2)

MAP_APPEND_MAP_EQ

⊢ ∀xs ys.
      (MAP f1 xs ++ MAP g1 ys = MAP f2 xs ++ MAP g2 ys) ⇔
      (MAP f1 xs = MAP f2 xs) ∧ (MAP g1 ys = MAP g2 ys)

MAP_APPEND

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

MAP2_ZIP

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

MAP2_NIL

⊢ MAP2 f x [] = []

MAP2_MAP

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

MAP2_ind

⊢ ∀P.
      (∀f h1 t1 h2 t2. P f t1 t2 ⇒ P f (h1::t1) (h2::t2)) ∧ (∀f y. P f [] y) ∧
      (∀f v4 v5. P f (v4::v5) []) ⇒
      ∀v v1 v2. P v v1 v2

MAP2_DEF

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

MAP2_CONG

⊢ ∀l1 l1' l2 l2' f f'.
      (l1 = l1') ∧ (l2 = l2') ∧
      (∀x y. MEM x l1' ∧ MEM y l2' ⇒ (f x y = f' x y)) ⇒
      (MAP2 f l1 l2 = MAP2 f' l1' l2')

MAP2_APPEND

⊢ ∀xs ys xs1 ys1 f.
      (LENGTH xs = LENGTH xs1) ⇒
      (MAP2 f (xs ++ ys) (xs1 ++ ys1) = MAP2 f xs xs1 ++ MAP2 f ys ys1)

MAP2

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

LUPDATE_SOME_MAP

⊢ ∀xs n f h.
      LUPDATE (SOME (f h)) n (MAP (OPTION_MAP f) xs) =
      MAP (OPTION_MAP f) (LUPDATE (SOME h) n xs)

LUPDATE_SNOC

⊢ ∀ys k x y.
      LUPDATE x k (SNOC y ys) =
      if k = LENGTH ys then SNOC x ys else SNOC y (LUPDATE x k ys)

LUPDATE_SEM

⊢ (∀e n l. LENGTH (LUPDATE e n l) = LENGTH l) ∧
  ∀e n l p.
      p < LENGTH l ⇒ (EL p (LUPDATE e n l) = if p = n then e else EL p l)

LUPDATE_SAME

⊢ ∀n ls. n < LENGTH ls ⇒ (LUPDATE (EL n ls) n ls = ls)

LUPDATE_NIL

⊢ ∀xs n x. (LUPDATE x n xs = []) ⇔ (xs = [])

LUPDATE_MAP

⊢ ∀x n l f. MAP f (LUPDATE x n l) = LUPDATE (f x) n (MAP f l)

LUPDATE_LENGTH

⊢ ∀xs x y ys. LUPDATE x (LENGTH xs) (xs ++ y::ys) = xs ++ x::ys

LUPDATE_compute

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

lupdate_append2

⊢ ∀v l1 x l2 l3. LUPDATE v (LENGTH l1) (l1 ++ [x] ++ l2) = l1 ++ [v] ++ l2

lupdate_append

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

LRC_MEM_right

⊢ LRC R (h::t) x y ∧ MEM e t ⇒ ∃z p. R z e ∧ LRC R p x z

LRC_MEM

⊢ LRC R ls x y ∧ MEM e ls ⇒ ∃z t. R e z ∧ LRC R t z y

LLEX_transitive

⊢ transitive R ⇒ transitive (LLEX R)

LLEX_total

⊢ total (RC R) ⇒ total (RC (LLEX R))

LLEX_THM

⊢ (¬LLEX R [] [] ∧ ¬LLEX R (h1::t1) []) ∧ LLEX R [] (h2::t2) ∧
  (LLEX R (h1::t1) (h2::t2) ⇔ R h1 h2 ∨ (h1 = h2) ∧ LLEX R t1 t2)

LLEX_not_WF

⊢ (∃a b. R a b) ⇒ ¬WF (LLEX R)

LLEX_NIL2

⊢ ¬LLEX R l []

LLEX_MONO

⊢ (∀x y. R1 x y ⇒ R2 x y) ⇒ LLEX R1 x y ⇒ LLEX R2 x y

LLEX_EL_THM

⊢ ∀R l1 l2.
      LLEX R l1 l2 ⇔
      ∃n.
          n ≤ LENGTH l1 ∧ n < LENGTH l2 ∧ (TAKE n l1 = TAKE n l2) ∧
          (n < LENGTH l1 ⇒ R (EL n l1) (EL n l2))

LLEX_CONG

⊢ ∀R l1 l2 R' l1' l2'.
      (l1 = l1') ∧ (l2 = l2') ∧
      (∀a b. MEM a l1' ∧ MEM b l2' ⇒ (R a b ⇔ R' a b)) ⇒
      (LLEX R l1 l2 ⇔ LLEX R' l1' l2')

LIST_TO_SET_THM

⊢ (LIST_TO_SET [] = ∅) ∧ (LIST_TO_SET (h::t) = h INSERT LIST_TO_SET t)

LIST_TO_SET_SNOC

⊢ LIST_TO_SET (SNOC x ls) = x INSERT LIST_TO_SET ls

LIST_TO_SET_REVERSE

⊢ ∀ls. LIST_TO_SET (REVERSE ls) = LIST_TO_SET ls

LIST_TO_SET_MAP

⊢ ∀f l. LIST_TO_SET (MAP f l) = IMAGE f (LIST_TO_SET l)

LIST_TO_SET_GENLIST

⊢ ∀f n. LIST_TO_SET (GENLIST f n) = IMAGE f (count n)

LIST_TO_SET_FLAT

⊢ ∀ls. LIST_TO_SET (FLAT ls) = BIGUNION (LIST_TO_SET (MAP LIST_TO_SET ls))

LIST_TO_SET_FILTER

⊢ LIST_TO_SET (FILTER P l) = {x | P x} ∩ LIST_TO_SET l

LIST_TO_SET_EQ_EMPTY

⊢ ((LIST_TO_SET l = ∅) ⇔ (l = [])) ∧ ((∅ = LIST_TO_SET l) ⇔ (l = []))

list_to_set_diff

⊢ ∀l1 l2.
      LIST_TO_SET l2 DIFF LIST_TO_SET l1 =
      LIST_TO_SET (FILTER (λx. ¬MEM x l1) l2)

LIST_TO_SET_APPEND

⊢ ∀l1 l2. LIST_TO_SET (l1 ++ l2) = LIST_TO_SET l1 ∪ LIST_TO_SET l2

LIST_TO_SET

⊢ (LIST_TO_SET [] = ∅) ∧ (LIST_TO_SET (h::t) = h INSERT LIST_TO_SET t)

list_size_cong

⊢ ∀M N f f'.
      (M = N) ∧ (∀x. MEM x N ⇒ (f x = f' x)) ⇒
      (list_size f M = list_size f' N)

LIST_REL_trans

⊢ ∀l1 l2 l3.
      (∀n.
           n < LENGTH l1 ∧ R (EL n l1) (EL n l2) ∧ R (EL n l2) (EL n l3) ⇒
           R (EL n l1) (EL n l3)) ∧ LIST_REL R l1 l2 ∧ LIST_REL R l2 l3 ⇒
      LIST_REL R l1 l3

LIST_REL_strongind

⊢ ∀R LIST_REL'.
      LIST_REL' [] [] ∧
      (∀h1 h2 t1 t2.
           R h1 h2 ∧ LIST_REL R t1 t2 ∧ LIST_REL' t1 t2 ⇒
           LIST_REL' (h1::t1) (h2::t2)) ⇒
      ∀a0 a1. LIST_REL R a0 a1 ⇒ LIST_REL' a0 a1

LIST_REL_SPLIT2

⊢ ∀xs1 zs.
      LIST_REL P zs (xs1 ++ xs2) ⇔
      ∃ys1 ys2. (zs = ys1 ++ ys2) ∧ LIST_REL P ys1 xs1 ∧ LIST_REL P ys2 xs2

LIST_REL_SPLIT1

⊢ ∀xs1 zs.
      LIST_REL P (xs1 ++ xs2) zs ⇔
      ∃ys1 ys2. (zs = ys1 ++ ys2) ∧ LIST_REL P xs1 ys1 ∧ LIST_REL P xs2 ys2

LIST_REL_SNOC

⊢ (LIST_REL R (SNOC x xs) yys ⇔
   ∃y ys. (yys = SNOC y ys) ∧ LIST_REL R xs ys ∧ R x y) ∧
  (LIST_REL R xxs (SNOC y ys) ⇔
   ∃x xs. (xxs = SNOC x xs) ∧ LIST_REL R xs ys ∧ R x y)

LIST_REL_rules

⊢ ∀R.
      LIST_REL R [] [] ∧
      ∀h1 h2 t1 t2. R h1 h2 ∧ LIST_REL R t1 t2 ⇒ LIST_REL R (h1::t1) (h2::t2)

LIST_REL_O

⊢ ∀R1 R2. LIST_REL (R1 ∘ᵣ R2) = LIST_REL R1 ∘ᵣ LIST_REL R2

LIST_REL_NIL

⊢ (LIST_REL R [] y ⇔ (y = [])) ∧ (LIST_REL R x [] ⇔ (x = []))

LIST_REL_mono

⊢ (∀x y. R1 x y ⇒ R2 x y) ⇒ LIST_REL R1 l1 l2 ⇒ LIST_REL R2 l1 l2

LIST_REL_MEM_IMP

⊢ ∀xs ys P x. LIST_REL P xs ys ∧ MEM x xs ⇒ ∃y. MEM y ys ∧ P x y

LIST_REL_MAP_inv_image

⊢ LIST_REL R (MAP f l1) (MAP f l2) ⇔ LIST_REL (inv_image R f) l1 l2

LIST_REL_MAP2

⊢ LIST_REL (λa b. R a b) l1 (MAP f l2) ⇔ LIST_REL (λa b. R a (f b)) l1 l2

LIST_REL_MAP1

⊢ LIST_REL R (MAP f l1) l2 ⇔ LIST_REL (R ∘ f) l1 l2

LIST_REL_LENGTH

⊢ ∀x y. LIST_REL R x y ⇒ (LENGTH x = LENGTH y)

LIST_REL_ind

⊢ ∀R LIST_REL'.
      LIST_REL' [] [] ∧
      (∀h1 h2 t1 t2. R h1 h2 ∧ LIST_REL' t1 t2 ⇒ LIST_REL' (h1::t1) (h2::t2)) ⇒
      ∀a0 a1. LIST_REL R a0 a1 ⇒ LIST_REL' a0 a1

LIST_REL_EVERY_ZIP

⊢ ∀R l1 l2.
      LIST_REL R l1 l2 ⇔
      (LENGTH l1 = LENGTH l2) ∧ EVERY (UNCURRY R) (ZIP (l1,l2))

LIST_REL_eq

⊢ LIST_REL $= = $=

LIST_REL_EL_EQN

⊢ ∀R l1 l2.
      LIST_REL R l1 l2 ⇔
      (LENGTH l1 = LENGTH l2) ∧ ∀n. n < LENGTH l1 ⇒ R (EL n l1) (EL n l2)

LIST_REL_def

⊢ (LIST_REL R [] [] ⇔ T) ∧ (LIST_REL R (a::as) [] ⇔ F) ∧
  (LIST_REL R [] (b::bs) ⇔ F) ∧
  (LIST_REL R (a::as) (b::bs) ⇔ R a b ∧ LIST_REL R as bs)

LIST_REL_CONS2

⊢ LIST_REL R xs (h::t) ⇔ ∃h' t'. (xs = h'::t') ∧ R h' h ∧ LIST_REL R t' t

LIST_REL_CONS1

⊢ LIST_REL R (h::t) xs ⇔ ∃h' t'. (xs = h'::t') ∧ R h h' ∧ LIST_REL R t t'

LIST_REL_CONJ

⊢ LIST_REL (λa b. P a b ∧ Q a b) l1 l2 ⇔
  LIST_REL (λa b. P a b) l1 l2 ∧ LIST_REL (λa b. Q a b) l1 l2

LIST_REL_cases

⊢ ∀R a0 a1.
      LIST_REL R a0 a1 ⇔
      (a0 = []) ∧ (a1 = []) ∨
      ∃h1 h2 t1 t2. (a0 = h1::t1) ∧ (a1 = h2::t2) ∧ R h1 h2 ∧ LIST_REL R t1 t2

LIST_REL_APPEND_suff

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

LIST_REL_APPEND_IMP

⊢ ∀xs ys xs1 ys1.
      LIST_REL P (xs ++ xs1) (ys ++ ys1) ∧ (LENGTH xs = LENGTH ys) ⇒
      LIST_REL P xs ys ∧ LIST_REL P xs1 ys1

LIST_REL_APPEND_EQ

⊢ (LENGTH x1 = LENGTH x2) ⇒
  (LIST_REL R (x1 ++ y1) (x2 ++ y2) ⇔ LIST_REL R x1 x2 ∧ LIST_REL R y1 y2)

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

LIST_NOT_EQ

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

list_nchotomy

⊢ ∀l. (l = []) ∨ ∃h t. l = h::t

list_induction

⊢ ∀P. P [] ∧ (∀t. P t ⇒ ∀h. P (h::t)) ⇒ ∀l. P l

list_INDUCT0

⊢ ∀P. P [] ∧ (∀l. P l ⇒ ∀a. P (a::l)) ⇒ ∀l. P l

list_INDUCT

⊢ ∀P. P [] ∧ (∀t. P t ⇒ ∀h. P (h::t)) ⇒ ∀l. P l

LIST_EQ_REWRITE

⊢ ∀l1 l2.
      (l1 = l2) ⇔
      (LENGTH l1 = LENGTH l2) ∧ ∀x. x < LENGTH l1 ⇒ (EL x l1 = EL x l2)

LIST_EQ_MAP_PAIR

⊢ ∀l1 l2. (MAP FST l1 = MAP FST l2) ∧ (MAP SND l1 = MAP SND l2) ⇒ (l1 = l2)

LIST_EQ

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

list_distinct

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

list_CASES

⊢ ∀l. (l = []) ∨ ∃h t. l = h::t

list_case_eq

⊢ (list_CASE x v f = v') ⇔
  (x = []) ∧ (v = v') ∨ ∃a l. (x = a::l) ∧ (f a l = v')

list_case_cong

⊢ ∀M M' v f.
      (M = M') ∧ ((M' = []) ⇒ (v = v')) ∧
      (∀a0 a1. (M' = a0::a1) ⇒ (f a0 a1 = f' a0 a1)) ⇒
      (list_CASE M v f = list_CASE M' v' f')

list_case_compute

⊢ ∀l. list_CASE l b f = if NULL l then b else f (HD l) (TL l)

LIST_BIND_THM

⊢ (LIST_BIND [] f = []) ∧ (LIST_BIND (h::t) f = f h ++ LIST_BIND t f)

LIST_BIND_MAP

⊢ LIST_BIND (MAP f l) g = LIST_BIND l (g ∘ f)

LIST_BIND_LIST_BIND

⊢ LIST_BIND (LIST_BIND l g) f = LIST_BIND l (combin$C LIST_BIND f ∘ g)

LIST_BIND_ID

⊢ (LIST_BIND l (λx. x) = FLAT l) ∧ (LIST_BIND l I = FLAT l)

LIST_BIND_APPEND

⊢ LIST_BIND (l1 ++ l2) f = LIST_BIND l1 f ++ LIST_BIND l2 f

list_Axiom_old

⊢ ∀x f. ∃!fn1. (fn1 [] = x) ∧ ∀h t. fn1 (h::t) = f (fn1 t) h t

list_Axiom

⊢ ∀f0 f1. ∃fn. (fn [] = f0) ∧ ∀a0 a1. fn (a0::a1) = f1 a0 a1 (fn a1)

LIST_APPLY_o

⊢ [$o] <*> fs <*> gs <*> xs = fs <*> (gs <*> xs)

list_11

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

LENGTH_ZIP_MIN

⊢ ∀xs ys. LENGTH (ZIP (xs,ys)) = MIN (LENGTH xs) (LENGTH ys)

LENGTH_ZIP

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

LENGTH_UNZIP

⊢ ∀pl.
      (LENGTH (FST (UNZIP pl)) = LENGTH pl) ∧
      (LENGTH (SND (UNZIP pl)) = LENGTH pl)

LENGTH_TL

⊢ ∀l. 0 < LENGTH l ⇒ (LENGTH (TL l) = LENGTH l − 1)

LENGTH_TAKE_EQ

⊢ LENGTH (TAKE n xs) = if n ≤ LENGTH xs then n else LENGTH xs

LENGTH_TAKE

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

LENGTH_SNOC

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

LENGTH_REVERSE

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

LENGTH_o_REVERSE

⊢ (LENGTH ∘ REVERSE = LENGTH) ∧ (LENGTH ∘ REVERSE ∘ f = LENGTH ∘ f)

length_nub_append

⊢ ∀l1 l2.
      LENGTH (nub (l1 ++ l2)) =
      LENGTH (nub l1) + LENGTH (nub (FILTER (λx. ¬MEM x l1) l2))

LENGTH_NIL_SYM

⊢ (0 = LENGTH l) ⇔ (l = [])

LENGTH_NIL

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

LENGTH_MAP2

⊢ ∀xs ys. LENGTH (MAP2 f xs ys) = MIN (LENGTH xs) (LENGTH ys)

LENGTH_MAP

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

LENGTH_LUPDATE

⊢ ∀x n ys. LENGTH (LUPDATE x n ys) = LENGTH ys

LENGTH_LT_SHORTLEX

⊢ ∀l1 l2. LENGTH l1 < LENGTH l2 ⇒ SHORTLEX R l1 l2

LENGTH_LEN

⊢ ∀L. LENGTH L = LEN L 0

LENGTH_GENLIST

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

LENGTH_FRONT_CONS

⊢ ∀x xs. LENGTH (FRONT (x::xs)) = LENGTH xs

LENGTH_FILTER_LEQ_MONO

⊢ ∀P Q. (∀x. P x ⇒ Q x) ⇒ ∀ls. LENGTH (FILTER P ls) ≤ LENGTH (FILTER Q ls)

LENGTH_EQ_SUM

⊢ ∀l n1 n2.
      (LENGTH l = n1 + n2) ⇔
      ∃l1 l2. (LENGTH l1 = n1) ∧ (LENGTH l2 = n2) ∧ (l = l1 ++ l2)

LENGTH_EQ_NUM_compute

⊢ (∀l. (LENGTH l = 0) ⇔ (l = [])) ∧
  (∀l n.
       (LENGTH l = NUMERAL (BIT1 n)) ⇔
       ∃h l'. (LENGTH l' = NUMERAL (BIT1 n) − 1) ∧ (l = h::l')) ∧
  (∀l n.
       (LENGTH l = NUMERAL (BIT2 n)) ⇔
       ∃h l'. (LENGTH l' = NUMERAL (BIT1 n)) ∧ (l = h::l')) ∧
  ∀l n1 n2.
      (LENGTH l = n1 + n2) ⇔
      ∃l1 l2. (LENGTH l1 = n1) ∧ (LENGTH l2 = n2) ∧ (l = l1 ++ l2)

LENGTH_EQ_NUM

⊢ (∀l. (LENGTH l = 0) ⇔ (l = [])) ∧
  (∀l n. (LENGTH l = SUC n) ⇔ ∃h l'. (LENGTH l' = n) ∧ (l = h::l')) ∧
  ∀l n1 n2.
      (LENGTH l = n1 + n2) ⇔
      ∃l1 l2. (LENGTH l1 = n1) ∧ (LENGTH l2 = n2) ∧ (l = l1 ++ l2)

LENGTH_EQ_NIL

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

LENGTH_EQ_CONS

⊢ ∀P n.
      (∀l. (LENGTH l = SUC n) ⇒ P l) ⇔
      ∀l. (LENGTH l = n) ⇒ (λl. ∀x. P (x::l)) l

LENGTH_dropWhile_LESS_EQ

⊢ ∀P ls. LENGTH (dropWhile P ls) ≤ LENGTH ls

LENGTH_DROP

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

LENGTH_CONS

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

LENGTH_APPEND

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

LEN_LENGTH_LEM

⊢ ∀L n. LEN L n = LENGTH L + n

lazy_list_case_compute

⊢ list_CASE = (λl b f. if NULL l then b else f (HD l) (TL l))

LAST_SNOC

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

LAST_REVERSE

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

LAST_MAP

⊢ ∀l f. l ≠ [] ⇒ (LAST (MAP f l) = f (LAST l))

LAST_EL

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

last_drop

⊢ ∀l n. n < LENGTH l ⇒ (LAST (DROP n l) = LAST l)

LAST_CONS_cond

⊢ LAST (h::t) = if t = [] then h else LAST t

LAST_CONS

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

LAST_compute

⊢ (∀x. LAST [x] = x) ∧ ∀h1 h2 t. LAST (h1::h2::t) = LAST (h2::t)

LAST_APPEND_CONS

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

ITSET_eq_FOLDL_SET_TO_LIST

⊢ ∀s. FINITE s ⇒ ∀f a. ITSET f s a = FOLDL (combin$C f) a (SET_TO_LIST s)

isPREFIX_THM

⊢ ([] ≼ l ⇔ T) ∧ (h::t ≼ [] ⇔ F) ∧ (h1::t1 ≼ h2::t2 ⇔ (h1 = h2) ∧ t1 ≼ t2)

isPREFIX_NILR

⊢ x ≼ [] ⇔ (x = [])

isPREFIX_CONSR

⊢ x ≼ y::ys ⇔ (x = []) ∨ ∃xs. (x = y::xs) ∧ xs ≼ ys

INJ_MAP_EQ_IFF

⊢ ∀f l1 l2.
      INJ f (LIST_TO_SET l1 ∪ LIST_TO_SET l2) 𝕌(:β) ⇒
      ((MAP f l1 = MAP f l2) ⇔ (l1 = l2))

INJ_MAP_EQ

⊢ ∀f l1 l2.
      INJ f (LIST_TO_SET l1 ∪ LIST_TO_SET l2) 𝕌(:β) ∧ (MAP f l1 = MAP f l2) ⇒
      (l1 = l2)

INFINITE_LIST_UNIV

⊢ INFINITE 𝕌(:α list)

IMP_EVERY_LUPDATE

⊢ ∀xs h i. P h ∧ EVERY P xs ⇒ EVERY P (LUPDATE h i xs)

IMAGE_EL_count_LENGTH

⊢ ∀f ls.
      IMAGE (λn. f (EL n ls)) (count (LENGTH ls)) = IMAGE f (LIST_TO_SET ls)

HD_REVERSE

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

HD_GENLIST_COR

⊢ ∀n f. 0 < n ⇒ (HD (GENLIST f n) = f 0)

HD_GENLIST

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

HD_dropWhile

⊢ ∀P ls. EXISTS ($~ ∘ P) ls ⇒ ¬P (HD (dropWhile P ls))

HD_DROP

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

GENLIST_PLUS_APPEND

⊢ GENLIST ($+ a) n1 ++ GENLIST ($+ (n1 + a)) n2 = GENLIST ($+ a) (n1 + n2)

GENLIST_NUMERALS

⊢ (GENLIST f 0 = []) ∧ (GENLIST f (NUMERAL n) = GENLIST_AUX f (NUMERAL n) [])

GENLIST_ID

⊢ ∀x. GENLIST (λi. EL i x) (LENGTH x) = x

GENLIST_GENLIST_AUX

⊢ ∀n. GENLIST f n = GENLIST_AUX f n []

GENLIST_FUN_EQ

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

GENLIST_EL_MAP

⊢ ∀f ls. GENLIST (λn. f (EL n ls)) (LENGTH ls) = MAP f ls

GENLIST_EL

⊢ ∀ls f n.
      (n = LENGTH ls) ∧ (∀i. i < n ⇒ (f i = EL i ls)) ⇒ (GENLIST f n = ls)

GENLIST_CONS

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

GENLIST_AUX_compute

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

GENLIST_APPEND

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

FRONT_SNOC

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

FRONT_CONS_EQ_NIL

⊢ (∀x xs. (FRONT (x::xs) = []) ⇔ (xs = [])) ∧
  (∀x xs. ([] = FRONT (x::xs)) ⇔ (xs = [])) ∧
  ∀x xs. NULL (FRONT (x::xs)) ⇔ NULL xs

FRONT_CONS

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

FORALL_LIST

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

FOLDR_CONS

⊢ ∀f ls a. FOLDR (λx y. f x::y) a ls = MAP f ls ++ a

FOLDR_CONG

⊢ ∀l l' b b' f f'.
      (l = l') ∧ (b = b') ∧ (∀x a. MEM x l' ⇒ (f x a = f' x a)) ⇒
      (FOLDR f b l = FOLDR f' b' l')

FOLDL_ZIP_SAME

⊢ ∀ls f e. FOLDL f e (ZIP (ls,ls)) = FOLDL (λx y. f x (y,y)) e ls

FOLDL_UNION_BIGUNION_paired

⊢ ∀f ls s.
      FOLDL (λs (x,y). s ∪ f x y) s ls =
      s ∪ BIGUNION (IMAGE (UNCURRY f) (LIST_TO_SET ls))

FOLDL_UNION_BIGUNION

⊢ ∀f ls s.
      FOLDL (λs x. s ∪ f x) s ls = s ∪ BIGUNION (IMAGE f (LIST_TO_SET ls))

FOLDL_SNOC

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

FOLDL_EQ_FOLDR

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

FOLDL_CONG

⊢ ∀l l' b b' f f'.
      (l = l') ∧ (b = b') ∧ (∀x a. MEM x l' ⇒ (f a x = f' a x)) ⇒
      (FOLDL f b l = FOLDL f' b' l')

FOLDL2_ind

⊢ ∀P.
      (∀f a b bs c cs. P f (f a b c) bs cs ⇒ P f a (b::bs) (c::cs)) ∧
      (∀f a cs. P f a [] cs) ∧ (∀f a v6 v7. P f a (v6::v7) []) ⇒
      ∀v v1 v2 v3. P v v1 v2 v3

FOLDL2_FOLDL

⊢ ∀l1 l2.
      (LENGTH l1 = LENGTH l2) ⇒
      ∀f a. FOLDL2 f a l1 l2 = FOLDL (λa. UNCURRY (f a)) a (ZIP (l1,l2))

FOLDL2_def

⊢ (∀f cs c bs b a. FOLDL2 f a (b::bs) (c::cs) = FOLDL2 f (f a b c) bs cs) ∧
  (∀f cs a. FOLDL2 f a [] cs = a) ∧ ∀v7 v6 f a. FOLDL2 f a (v6::v7) [] = a

FOLDL2_cong

⊢ ∀l1 l1' l2 l2' a a' f f'.
      (l1 = l1') ∧ (l2 = l2') ∧ (a = a') ∧
      (∀z b c. MEM b l1' ∧ MEM c l2' ⇒ (f z b c = f' z b c)) ⇒
      (FOLDL2 f a l1 l2 = FOLDL2 f' a' l1' l2')

FLAT_EQ_NIL

⊢ ∀ls. (FLAT ls = []) ⇔ EVERY ($= []) ls

FLAT_compute

⊢ (FLAT [] = []) ∧ (FLAT ([]::t) = FLAT t) ∧
  (FLAT ((h::t1)::t2) = h::FLAT (t1::t2))

FLAT_APPEND

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

FINITE_LIST_TO_SET

⊢ ∀l. FINITE (LIST_TO_SET l)

FILTER_T

⊢ ∀xs. FILTER (λx. T) xs = xs

FILTER_REVERSE

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

FILTER_NEQ_NIL

⊢ ∀P l. FILTER P l ≠ [] ⇔ ∃x. MEM x l ∧ P x

FILTER_NEQ_ID

⊢ ∀P l. FILTER P l ≠ l ⇔ ∃x. MEM x l ∧ ¬P x

FILTER_F

⊢ ∀xs. FILTER (λx. F) xs = []

FILTER_EQ_NIL

⊢ ∀P l. (FILTER P l = []) ⇔ EVERY (λx. ¬P x) l

FILTER_EQ_ID

⊢ ∀P l. (FILTER P l = l) ⇔ EVERY P l

FILTER_EQ_CONS

⊢ ∀P l h lr.
      (FILTER P l = h::lr) ⇔
      ∃l1 l2.
          (l = l1 ++ [h] ++ l2) ∧ (FILTER P l1 = []) ∧ (FILTER P l2 = lr) ∧
          P h

FILTER_EQ_APPEND

⊢ ∀P l l1 l2.
      (FILTER P l = l1 ++ l2) ⇔
      ∃l3 l4. (l = l3 ++ l4) ∧ (FILTER P l3 = l1) ∧ (FILTER P l4 = l2)

FILTER_COND_REWRITE

⊢ (FILTER P [] = []) ∧ (∀h. P h ⇒ (FILTER P (h::l) = h::FILTER P l)) ∧
  ∀h. ¬P h ⇒ (FILTER P (h::l) = FILTER P l)

FILTER_APPEND_DISTRIB

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

FILTER_ALL_DISTINCT

⊢ ∀P l. ALL_DISTINCT l ⇒ ALL_DISTINCT (FILTER P l)

EXISTS_SNOC

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

EXISTS_SIMP

⊢ ∀c l. EXISTS (λx. c) l ⇔ l ≠ [] ∧ c

EXISTS_NOT_EVERY

⊢ ∀P l. EXISTS P l ⇔ ¬EVERY (λx. ¬P x) l

EXISTS_MEM

⊢ ∀P l. EXISTS P l ⇔ ∃e. MEM e l ∧ P e

EXISTS_MAP

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

exists_list_GENLIST

⊢ (∃ls. P ls) ⇔ ∃n f. P (GENLIST f n)

EXISTS_LIST_EQ_MAP

⊢ ∀ls f. EVERY (λx. ∃y. x = f y) ls ⇒ ∃l. ls = MAP f l

EXISTS_LIST

⊢ (∃l. P l) ⇔ P [] ∨ ∃h t. P (h::t)

EXISTS_GENLIST

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

EXISTS_CONG

⊢ ∀l1 l2 P P'.
      (l1 = l2) ∧ (∀x. MEM x l2 ⇒ (P x ⇔ P' x)) ⇒ (EXISTS P l1 ⇔ EXISTS P' l2)

EXISTS_APPEND

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

every_zip_snd

⊢ ∀l1 l2 P.
      (LENGTH l1 = LENGTH l2) ⇒
      (EVERY (λx. P (SND x)) (ZIP (l1,l2)) ⇔ EVERY P l2)

every_zip_fst

⊢ ∀l1 l2 P.
      (LENGTH l1 = LENGTH l2) ⇒
      (EVERY (λx. P (FST x)) (ZIP (l1,l2)) ⇔ EVERY P l1)

EVERY_SNOC

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

EVERY_SIMP

⊢ ∀c l. EVERY (λx. c) l ⇔ (l = []) ∨ c

EVERY_NOT_EXISTS

⊢ ∀P l. EVERY P l ⇔ ¬EXISTS (λx. ¬P x) l

EVERY_MONOTONIC

⊢ ∀P Q. (∀x. P x ⇒ Q x) ⇒ ∀l. EVERY P l ⇒ EVERY Q l

EVERY_MEM_MONO

⊢ ∀P Q l. (∀x. MEM x l ∧ P x ⇒ Q x) ∧ EVERY P l ⇒ EVERY Q l

EVERY_MEM

⊢ ∀P l. EVERY P l ⇔ ∀e. MEM e l ⇒ P e

EVERY_MAP

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

EVERY_GENLIST

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

EVERY_FLAT

⊢ EVERY P (FLAT ls) ⇔ EVERY (EVERY P) ls

EVERY_FILTER_IMP

⊢ ∀P1 P2 l. EVERY P1 l ⇒ EVERY P1 (FILTER P2 l)

EVERY_FILTER

⊢ ∀P1 P2 l. EVERY P1 (FILTER P2 l) ⇔ EVERY (λx. P2 x ⇒ P1 x) l

EVERY_EL

⊢ ∀l P. EVERY P l ⇔ ∀n. n < LENGTH l ⇒ P (EL n l)

EVERY_CONJ

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

EVERY_CONG

⊢ ∀l1 l2 P P'.
      (l1 = l2) ∧ (∀x. MEM x l2 ⇒ (P x ⇔ P' x)) ⇒ (EVERY P l1 ⇔ EVERY P' l2)

EVERY_APPEND

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

EVERY2_trans

⊢ (∀x y z. R x y ∧ R y z ⇒ R x z) ⇒
  ∀x y z. LIST_REL R x y ∧ LIST_REL R y z ⇒ LIST_REL R x z

EVERY2_THM

⊢ (∀P ys. LIST_REL P [] ys ⇔ (ys = [])) ∧
  (∀P yys x xs.
       LIST_REL P (x::xs) yys ⇔
       ∃y ys. (yys = y::ys) ∧ P x y ∧ LIST_REL P xs ys) ∧
  (∀P xs. LIST_REL P xs [] ⇔ (xs = [])) ∧
  ∀P xxs y ys.
      LIST_REL P xxs (y::ys) ⇔ ∃x xs. (xxs = x::xs) ∧ P x y ∧ LIST_REL P xs ys

EVERY2_sym

⊢ (∀x y. R1 x y ⇒ R2 y x) ⇒ ∀x y. LIST_REL R1 x y ⇒ LIST_REL R2 y x

EVERY2_REVERSE

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

EVERY2_refl

⊢ (∀x. MEM x ls ⇒ R x x) ⇒ LIST_REL R ls ls

EVERY2_mono

⊢ (∀x y. R1 x y ⇒ R2 x y) ⇒ LIST_REL R1 l1 l2 ⇒ LIST_REL R2 l1 l2

EVERY2_MEM_MONO

⊢ ∀P Q l1 l2.
      (∀x. MEM x (ZIP (l1,l2)) ∧ UNCURRY P x ⇒ UNCURRY Q x) ∧ LIST_REL P l1 l2 ⇒
      LIST_REL Q l1 l2

EVERY2_MAP

⊢ (LIST_REL P (MAP f l1) l2 ⇔ LIST_REL (λx y. P (f x) y) l1 l2) ∧
  (LIST_REL Q l1 (MAP g l2) ⇔ LIST_REL (λx y. Q x (g y)) l1 l2)

EVERY2_LUPDATE_same

⊢ ∀P l1 l2 v1 v2 n.
      P v1 v2 ∧ LIST_REL P l1 l2 ⇒
      LIST_REL P (LUPDATE v1 n l1) (LUPDATE v2 n l2)

EVERY2_LENGTH

⊢ ∀P l1 l2. LIST_REL P l1 l2 ⇒ (LENGTH l1 = LENGTH l2)

EVERY2_EVERY

⊢ ∀l1 l2 f.
      LIST_REL f l1 l2 ⇔
      (LENGTH l1 = LENGTH l2) ∧ EVERY (UNCURRY f) (ZIP (l1,l2))

EVERY2_cong

⊢ ∀l1 l1' l2 l2' P P'.
      (l1 = l1') ∧ (l2 = l2') ∧
      (∀x y. MEM x l1' ∧ MEM y l2' ⇒ (P x y ⇔ P' x y)) ⇒
      (LIST_REL P l1 l2 ⇔ LIST_REL P' l1' l2')

EQ_LIST

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

EL_ZIP

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

EL_TAKE

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

EL_SNOC

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

EL_simp_restricted

⊢ (EL (NUMERAL (BIT1 n)) (l::ls) = EL (PRE (NUMERAL (BIT1 n))) ls) ∧
  (EL (NUMERAL (BIT2 n)) (l::ls) = EL (NUMERAL (BIT1 n)) ls)

EL_simp

⊢ (EL (NUMERAL (BIT1 n)) l = EL (PRE (NUMERAL (BIT1 n))) (TL l)) ∧
  (EL (NUMERAL (BIT2 n)) l = EL (NUMERAL (BIT1 n)) (TL l))

EL_REVERSE

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

EL_restricted

⊢ (EL 0 = HD) ∧ (EL (SUC n) (l::ls) = EL n ls)

EL_MAP2

⊢ ∀ts tt n.
      n < MIN (LENGTH ts) (LENGTH tt) ⇒
      (EL n (MAP2 f ts tt) = f (EL n ts) (EL n tt))

EL_MAP

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

EL_LUPDATE

⊢ ∀ys x i k.
      EL i (LUPDATE x k ys) = if (i = k) ∧ k < LENGTH ys then x else EL i ys

EL_LENGTH_SNOC

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

EL_LENGTH_dropWhile_REVERSE

⊢ ∀P ls k. LENGTH (dropWhile P (REVERSE ls)) ≤ k ∧ k < LENGTH ls ⇒ P (EL k ls)

EL_GENLIST

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

EL_DROP

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

EL_compute

⊢ ∀n. EL n l = if n = 0 then HD l else EL (PRE n) (TL l)

EL_APPEND_EQN

⊢ ∀l1 l2 n.
      EL n (l1 ++ l2) =
      if n < LENGTH l1 then EL n l1 else EL (n − LENGTH l1) l2

el_append3

⊢ ∀l1 x l2. EL (LENGTH l1) (l1 ++ [x] ++ l2) = x

EL_ALL_DISTINCT_EL_EQ

⊢ ∀l.
      ALL_DISTINCT l ⇔
      ∀n1 n2.
          n1 < LENGTH l ∧ n2 < LENGTH l ⇒ ((EL n1 l = EL n2 l) ⇔ (n1 = n2))

dropWhile_splitAtPki

⊢ ∀P. dropWhile P = splitAtPki (combin$C (K ∘ $~ ∘ P)) (K I)

dropWhile_eq_nil

⊢ ∀P ls. (dropWhile P ls = []) ⇔ EVERY P ls

dropWhile_APPEND_EXISTS

⊢ ∀P l1 l2.
      EXISTS ($~ ∘ P) l1 ⇒ (dropWhile P (l1 ++ l2) = dropWhile P l1 ++ l2)

dropWhile_APPEND_EVERY

⊢ ∀P l1 l2. EVERY P l1 ⇒ (dropWhile P (l1 ++ l2) = dropWhile P l2)

DROP_splitAtPki

⊢ DROP n l = splitAtPki (K ∘ $= n) (K I) l

DROP_nil

⊢ ∀n. DROP n [] = []

DROP_NIL

⊢ ∀ls n. (DROP n ls = []) ⇔ n ≥ LENGTH ls

DROP_LENGTH_TOO_LONG

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

DROP_GENLIST

⊢ DROP n (GENLIST f m) = GENLIST (f ∘ $+ n) (m − n)

DROP_cons

⊢ 0 < n ⇒ (DROP n (x::xs) = DROP (n − 1) xs)

DROP_compute

⊢ (∀l. DROP 0 l = l) ∧ (∀n. DROP (NUMERAL (BIT1 n)) [] = []) ∧
  (∀n. DROP (NUMERAL (BIT2 n)) [] = []) ∧
  (∀n h t. DROP (NUMERAL (BIT1 n)) (h::t) = DROP (NUMERAL (BIT1 n) − 1) t) ∧
  ∀n h t. DROP (NUMERAL (BIT2 n)) (h::t) = DROP (NUMERAL (BIT1 n)) t

DROP_0

⊢ DROP 0 l = l

DISJOINT_GENLIST_PLUS

⊢ DISJOINT x (LIST_TO_SET (GENLIST ($+ n) (a + b))) ⇒
  DISJOINT x (LIST_TO_SET (GENLIST ($+ n) a)) ∧
  DISJOINT x (LIST_TO_SET (GENLIST ($+ (n + a)) b))

datatype_list

⊢ DATATYPE (list [] CONS)

CONS_ACYCLIC

⊢ ∀l x. l ≠ x::l ∧ x::l ≠ l

CONS_11

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

CONS

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

CARD_LIST_TO_SET_ALL_DISTINCT

⊢ ∀ls. (CARD (LIST_TO_SET ls) = LENGTH ls) ⇒ ALL_DISTINCT ls

CARD_LIST_TO_SET

⊢ CARD (LIST_TO_SET ls) ≤ LENGTH ls

BIGUNION_IMAGE_set_SUBSET

⊢ BIGUNION (IMAGE f (LIST_TO_SET ls)) ⊆ s ⇔ ∀x. MEM x ls ⇒ f x ⊆ s

APPEND_SNOC

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

APPEND_NIL

⊢ ∀l. l ++ [] = l

APPEND_LENGTH_EQ

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

APPEND_FRONT_LAST

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

APPEND_EQ_SING

⊢ (l1 ++ l2 = [e]) ⇔ (l1 = [e]) ∧ (l2 = []) ∨ (l1 = []) ∧ (l2 = [e])

APPEND_EQ_SELF

⊢ (∀l1 l2. (l1 ++ l2 = l1) ⇔ (l2 = [])) ∧
  (∀l1 l2. (l1 ++ l2 = l2) ⇔ (l1 = [])) ∧
  (∀l1 l2. (l1 = l1 ++ l2) ⇔ (l2 = [])) ∧ ∀l1 l2. (l2 = l1 ++ l2) ⇔ (l1 = [])

APPEND_eq_NIL

⊢ (∀l1 l2. ([] = l1 ++ l2) ⇔ (l1 = []) ∧ (l2 = [])) ∧
  ∀l1 l2. (l1 ++ l2 = []) ⇔ (l1 = []) ∧ (l2 = [])

APPEND_EQ_CONS

⊢ (l1 ++ l2 = h::t) ⇔
  (l1 = []) ∧ (l2 = h::t) ∨ ∃lt. (l1 = h::lt) ∧ (t = lt ++ l2)

APPEND_EQ_APPEND_MID

⊢ (l1 ++ [e] ++ l2 = m1 ++ m2) ⇔
  (∃l. (m1 = l1 ++ [e] ++ l) ∧ (l2 = l ++ m2)) ∨
  ∃l. (l1 = m1 ++ l) ∧ (m2 = l ++ [e] ++ l2)

APPEND_EQ_APPEND

⊢ (l1 ++ l2 = m1 ++ m2) ⇔
  (∃l. (l1 = m1 ++ l) ∧ (m2 = l ++ l2)) ∨ ∃l. (m1 = l1 ++ l) ∧ (l2 = l ++ m2)

APPEND_ASSOC

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

APPEND_11_LENGTH

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

APPEND_11

⊢ (∀l1 l2 l3. (l1 ++ l2 = l1 ++ l3) ⇔ (l2 = l3)) ∧
  ∀l1 l2 l3. (l2 ++ l1 = l3 ++ l1) ⇔ (l2 = l3)

ALL_DISTINCT_ZIP_SWAP

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

ALL_DISTINCT_ZIP

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

ALL_DISTINCT_SNOC

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

ALL_DISTINCT_SING

⊢ ∀x. ALL_DISTINCT [x]

ALL_DISTINCT_SET_TO_LIST

⊢ ∀s. FINITE s ⇒ ALL_DISTINCT (SET_TO_LIST s)

ALL_DISTINCT_REVERSE

⊢ ∀l. ALL_DISTINCT (REVERSE l) ⇔ ALL_DISTINCT l

all_distinct_nub

⊢ ∀l. ALL_DISTINCT (nub l)

ALL_DISTINCT_MAP_INJ

⊢ ∀ls f.
      (∀x y. MEM x ls ∧ MEM y ls ∧ (f x = f y) ⇒ (x = y)) ∧ ALL_DISTINCT ls ⇒
      ALL_DISTINCT (MAP f ls)

ALL_DISTINCT_MAP

⊢ ∀f ls. ALL_DISTINCT (MAP f ls) ⇒ ALL_DISTINCT ls

ALL_DISTINCT_GENLIST

⊢ ALL_DISTINCT (GENLIST f n) ⇔
  ∀m1 m2. m1 < n ∧ m2 < n ∧ (f m1 = f m2) ⇒ (m1 = m2)

ALL_DISTINCT_FLAT_REVERSE

⊢ ∀xs. ALL_DISTINCT (FLAT (REVERSE xs)) ⇔ ALL_DISTINCT (FLAT xs)

ALL_DISTINCT_FILTER_EL_IMP

⊢ ∀P l n1 n2.
      ALL_DISTINCT (FILTER P l) ∧ n1 < LENGTH l ∧ n2 < LENGTH l ∧
      P (EL n1 l) ∧ (EL n1 l = EL n2 l) ⇒
      (n1 = n2)

ALL_DISTINCT_FILTER

⊢ ∀l. ALL_DISTINCT l ⇔ ∀x. MEM x l ⇒ (FILTER ($= x) l = [x])

ALL_DISTINCT_EL_IMP

⊢ ∀l n1 n2.
      ALL_DISTINCT l ∧ n1 < LENGTH l ∧ n2 < LENGTH l ⇒
      ((EL n1 l = EL n2 l) ⇔ (n1 = n2))

ALL_DISTINCT_DROP

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

ALL_DISTINCT_CARD_LIST_TO_SET

⊢ ∀ls. ALL_DISTINCT ls ⇒ (CARD (LIST_TO_SET ls) = LENGTH ls)

ALL_DISTINCT_APPEND

⊢ ∀l1 l2.
      ALL_DISTINCT (l1 ++ l2) ⇔
      ALL_DISTINCT l1 ∧ ALL_DISTINCT l2 ∧ ∀e. MEM e l1 ⇒ ¬MEM e l2