|- ∀x y. FST (x,y) = x

|- ∀x y. SND (x,y) = y

|- ∀f x y. CURRY f x y = f (x,y)

|- ∀f v. UNCURRY f v = f (FST v) (SND v)

|- ∀f g. f o g = (λx. f (g x))

|- ∀x. I x = x

|- combin$C = (λf x y. f y x)

|- K = (λx y. x)

|- S = (λf g x. f x (g x))

|- ∀a b. a =+ b = (λf c. if a = c then b else f c)

|- W = (λf x. f x x)

|- ∀x. THE (SOME x) = x

|- (∀x. IS_NONE (SOME x) ⇔ F) ∧ (IS_NONE NONE ⇔ T)

|- (∀x. IS_SOME (SOME x) ⇔ T) ∧ (IS_SOME NONE ⇔ F)

|- (∀f x. OPTION_MAP f (SOME x) = SOME (f x)) ∧
   ∀f. OPTION_MAP f NONE = NONE

|- ∀f x y.
     OPTION_MAP2 f x y =
     if IS_SOME x ∧ IS_SOME y then SOME (f (THE x) (THE y)) else NONE

|- (∀x. ISL (INL x)) ∧ ∀y. ¬ISL (INR y)

|- (∀x. ISR (INR x)) ∧ ∀y. ¬ISR (INL y)

|- ∀x. OUTL (INL x) = x

|- ∀x. OUTR (INR x) = x

|- (∀f g a. (f ++ g) (INL a) = INL (f a)) ∧
   ∀f g b. (f ++ g) (INR b) = INR (g b)

|- (∀n. LENGTH_AUX [] n = n) ∧
   ∀x xs n. LENGTH_AUX (x::xs) n = LENGTH_AUX xs (n + 1)

|- LENGTH xs = LENGTH_AUX xs 0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

|- (∀P l1 l2. PART P [] l1 l2 = (l1,l2)) ∧
   ∀P h rst l1 l2.
     PART P (h::rst) l1 l2 =
     if P h then PART P rst (h::l1) l2 else PART P rst l1 (h::l2)

|- ∀P l. PARTITION P l = PART P l [] []

|- (QSORT ord [] = []) ∧
   (QSORT ord (h::t) =
    (let (l1,l2) = PARTITION (λy. ord y h) t
     in
       QSORT ord l1 ++ [h] ++ QSORT ord l2))

|- ∀n m k.
     EXP_AUX m n k = if n = 0 then k else EXP_AUX m (n − 1) (m * k)

|- m ** n = EXP_AUX m n 1

|- ∀m n. MIN m n = if m < n then m else n

|- ∀m n. MAX m n = if m < n then n else m

|- ∀x. EVEN x ⇔ (x MOD 2 = 0)

|- ∀n. ODD n ⇔ 0 < n MOD 2

|- (∀f x. FUNPOW f 0 x = x) ∧
   ∀f n x. FUNPOW f (SUC n) x = FUNPOW f n (f x)

|- ∀x n. MOD_2EXP x n = n MOD 2 ** x

|- ∀x n. DIV_2EXP x n = n DIV 2 ** x

|- PRE n = n − 1

|- ∀n m. ABS_DIFF n m = if n < m then m − n else n − m

|- ∀n. DIV2 n = n DIV 2

|- ("" < "" ⇔ F) ∧ (∀v3 v2. STRING v2 v3 < "" ⇔ F) ∧
   (∀s c. "" < STRING c s ⇔ T) ∧
   ∀s2 s1 c2 c1.
     STRING c1 s1 < STRING c2 s2 ⇔ c1 < c2 ∨ (c1 = c2) ∧ s1 < s2

|- ∀s1 s2. s1 ≤ s2 ⇔ (s1 = s2) ∨ s1 < s2

|- ∀s1 s2. s1 > s2 ⇔ s2 < s1

|- ∀s1 s2. s1 ≥ s2 ⇔ s2 ≤ s1

|- ∀h l n. BITS h l n = n MOD 2 ** SUC h DIV 2 ** l

|- ∀b n. BIT b n ⇔ ((n DIV 2 ** b) MOD 2 = 1)

|- ∀b n. SBIT b n = if b then 2 ** n else 0

|- BRANCHING_BIT p0 p1 =
   if (ODD p0 ⇔ EVEN p1) ∨ (p0 = p1) then
     0
   else
     SUC (BRANCHING_BIT (DIV2 p0) (DIV2 p1))

|- (∀k. <{}> ' k = NONE) ∧
   (∀k j d. Leaf j d ' k = if k = j then SOME d else NONE) ∧
   ∀r p m l k. Branch p m l r ' k = (if BIT m k then l else r) ' k

|- ∀n a b. MOD_2EXP_EQ n a b ⇔ (MOD_2EXP n a = MOD_2EXP n b)

|- ∀p0 t0 p1 t1.
     JOIN (p0,t0,p1,t1) =
     (let m = BRANCHING_BIT p0 p1
      in
        if BIT m p0 then
          Branch (MOD_2EXP m p0) m t0 t1
        else
          Branch (MOD_2EXP m p0) m t1 t0)

|- (∀k e. <{}> |+ (k,e) = Leaf k e) ∧
   (∀k j e d.
      Leaf j d |+ (k,e) =
      if j = k then Leaf k e else JOIN (k,Leaf k e,j,Leaf j d)) ∧
   ∀r p m l k e.
     Branch p m l r |+ (k,e) =
     if MOD_2EXP_EQ m k p then
       if BIT m k then
         Branch p m (l |+ (k,e)) r
       else
         Branch p m l (r |+ (k,e))
     else
       JOIN (k,Leaf k e,p,Branch p m l r)

|- (BRANCH (p,m,<{}>,<{}>) = <{}>) ∧
   (BRANCH (p,m,<{}>,Leaf v24 v25) = Leaf v24 v25) ∧
   (BRANCH (p,m,<{}>,Branch v26 v27 v28 v29) = Branch v26 v27 v28 v29) ∧
   (BRANCH (p,m,Leaf v6 v7,<{}>) = Leaf v6 v7) ∧
   (BRANCH (p,m,Branch v8 v9 v10 v11,<{}>) = Branch v8 v9 v10 v11) ∧
   (BRANCH (p,m,Leaf v12 v13,Leaf v42 v43) =
    Branch p m (Leaf v12 v13) (Leaf v42 v43)) ∧
   (BRANCH (p,m,Leaf v12 v13,Branch v44 v45 v46 v47) =
    Branch p m (Leaf v12 v13) (Branch v44 v45 v46 v47)) ∧
   (BRANCH (p,m,Branch v14 v15 v16 v17,Leaf v54 v55) =
    Branch p m (Branch v14 v15 v16 v17) (Leaf v54 v55)) ∧
   (BRANCH (p,m,Branch v14 v15 v16 v17,Branch v56 v57 v58 v59) =
    Branch p m (Branch v14 v15 v16 v17) (Branch v56 v57 v58 v59))

|- (∀k. <{}> \\ k = <{}>) ∧
   (∀j d k. Leaf j d \\ k = if j = k then <{}> else Leaf j d) ∧
   ∀p m l r k.
     Branch p m l r \\ k =
     if MOD_2EXP_EQ m k p then
       if BIT m k then BRANCH (p,m,l \\ k,r) else BRANCH (p,m,l,r \\ k)
     else
       Branch p m l r