Theory lbtree

⊢ Lf = lbtree_abs Lfrep

⊢ Lfrep = (λl. NONE)

⊢ ∀a t1 t2.
    Nd a t1 t2 = lbtree_abs (Ndrep a (lbtree_rep t1) (lbtree_rep t2))

⊢ ∀a t1 t2.
    Ndrep a t1 t2 =
    (λl. case l of [] => SOME a | T::xs => t1 xs | F::xs => t2 xs)

⊢ bf_flatten [] = [||] ∧ (∀ts. bf_flatten (Lf::ts) = bf_flatten ts) ∧
  ∀a t1 t2 ts. bf_flatten (Nd a t1 t2::ts) = a:::bf_flatten (ts ⧺ [t1; t2])

⊢ ∀t. is_lbtree t ⇔
      ∃P. (∀t. P t ⇒ t = Lfrep ∨ ∃a t1 t2. P t1 ∧ P t2 ∧ t = Ndrep a t1 t2) ∧
          P t

⊢ ∀f l n d.
    lbtree$is_mmindex f l n d ⇔
    n < LENGTH l ∧ f l❲n❳ = SOME d ∧
    ∀i. i < LENGTH l ⇒
        f l❲i❳ = NONE ∨ ∃d'. f l❲i❳ = SOME d' ∧ d ≤ d' ∧ (i < n ⇒ d < d')

⊢ ∃rep. TYPE_DEFINITION is_lbtree rep

⊢ (∀a. lbtree_abs (lbtree_rep a) = a) ∧
  ∀r. is_lbtree r ⇔ lbtree_rep (lbtree_abs r) = r

⊢ ∀e f t.
    lbtree_case e f t =
    if t = Lf then e
    else
      f (@a. ∃t1 t2. t = Nd a t1 t2) (@t1. ∃a t2. t = Nd a t1 t2)
        (@t2. ∃a t1. t = Nd a t1 t2)

⊢ ∀f. map f Lf = Lf ∧
      ∀a t1 t2. map f (Nd a t1 t2) = Nd (f a) (map f t1) (map f t2)

⊢ ∀x t.
    lbtree$mindepth x t =
    if mem x t then SOME (LEAST n. lbtree$depth x t n) else NONE

⊢ (∀g x. path_follow g x [] = OPTION_MAP FST (g x)) ∧
  ∀g x h t.
    path_follow g x (h::t) =
    case g x of
      NONE => NONE
    | SOME (a,y,z) => path_follow g (if h then y else z) t

⊢ ∀l. EXISTS P l ⇒ ∃l1 x l2. l = l1 ⧺ x::l2 ∧ EVERY ($¬ ∘ P) l1 ∧ P x

⊢ Lf ≠ Nd a t1 t2

⊢ Nd a1 t1 u1 = Nd a2 t2 u2 ⇔ a1 = a2 ∧ t1 = t2 ∧ u1 = u2

⊢ ∀l1. EVERY ($= Lf) l1 ⇒ bf_flatten (l1 ⧺ l2) = bf_flatten l2

⊢ ∀l. bf_flatten l = [||] ⇔ EVERY ($= Lf) l

⊢ ∀a0 a1 a2.
    lbtree$depth a0 a1 a2 ⇔
    (∃t1 t2. a1 = Nd a0 t1 t2 ∧ a2 = 0) ∨
    (∃m a t1 t2. a1 = Nd a t1 t2 ∧ a2 = SUC m ∧ lbtree$depth a0 t1 m) ∨
    ∃m a t1 t2. a1 = Nd a t1 t2 ∧ a2 = SUC m ∧ lbtree$depth a0 t2 m

⊢ ∀depth'.
    (∀x t1 t2. depth' x (Nd x t1 t2) 0) ∧
    (∀m x a t1 t2. depth' x t1 m ⇒ depth' x (Nd a t1 t2) (SUC m)) ∧
    (∀m x a t1 t2. depth' x t2 m ⇒ depth' x (Nd a t1 t2) (SUC m)) ⇒
    ∀a0 a1 a2. lbtree$depth a0 a1 a2 ⇒ depth' a0 a1 a2

⊢ ∀x t n. lbtree$depth x t n ⇒ mem x t

⊢ (∀x t1 t2. lbtree$depth x (Nd x t1 t2) 0) ∧
  (∀m x a t1 t2. lbtree$depth x t1 m ⇒ lbtree$depth x (Nd a t1 t2) (SUC m)) ∧
  ∀m x a t1 t2. lbtree$depth x t2 m ⇒ lbtree$depth x (Nd a t1 t2) (SUC m)

⊢ ∀depth'.
    (∀x t1 t2. depth' x (Nd x t1 t2) 0) ∧
    (∀m x a t1 t2.
       lbtree$depth x t1 m ∧ depth' x t1 m ⇒ depth' x (Nd a t1 t2) (SUC m)) ∧
    (∀m x a t1 t2.
       lbtree$depth x t2 m ∧ depth' x t2 m ⇒ depth' x (Nd a t1 t2) (SUC m)) ⇒
    ∀a0 a1 a2. lbtree$depth a0 a1 a2 ⇒ depth' a0 a1 a2

⊢ exists ($= x) (bf_flatten tlist) ⇒ EXISTS (mem x) tlist

⊢ ∀a0.
    finite a0 ⇔ a0 = Lf ∨ ∃a t1 t2. a0 = Nd a t1 t2 ∧ finite t1 ∧ finite t2

⊢ ∀finite'.
    finite' Lf ∧ (∀a t1 t2. finite' t1 ∧ finite' t2 ⇒ finite' (Nd a t1 t2)) ⇒
    ∀a0. finite a0 ⇒ finite' a0

⊢ finite (map f t) ⇔ finite t

⊢ finite Lf ∧ ∀a t1 t2. finite t1 ∧ finite t2 ⇒ finite (Nd a t1 t2)

⊢ ∀finite'.
    finite' Lf ∧
    (∀a t1 t2.
       finite t1 ∧ finite' t1 ∧ finite t2 ∧ finite' t2 ⇒
       finite' (Nd a t1 t2)) ⇒
    ∀a0. finite a0 ⇒ finite' a0

⊢ (finite Lf ⇔ T) ∧ (finite (Nd a t1 t2) ⇔ finite t1 ∧ finite t2)

⊢ ∀t u.
    t = u ⇔
    ∃R. R t u ∧
        ∀t u.
          R t u ⇒
          t = Lf ∧ u = Lf ∨
          ∃a t1 u1 t2 u2.
            R t1 u1 ∧ R t2 u2 ∧ t = Nd a t1 t2 ∧ u = Nd a u1 u2

⊢ lbtree_case e f Lf = e ∧ lbtree_case e f (Nd a t1 t2) = f a t1 t2

⊢ ∀t. t = Lf ∨ ∃a t1 t2. t = Nd a t1 t2

⊢ ∀t u.
    t = u ⇔
    ∃R. R t u ∧
        ∀t u.
          R t u ⇒
          t = u ∨
          ∃a t1 u1 t2 u2.
            R t1 u1 ∧ R t2 u2 ∧ t = Nd a t1 t2 ∧ u = Nd a u1 u2

⊢ ∀f. ∃!g. ∀x.
    g x = case f x of NONE => Lf | SOME (b,y,z) => Nd b (g y) (g z)

⊢ (map f t = Lf ⇔ t = Lf) ∧ (Lf = map f t ⇔ t = Lf)

⊢ map f t = Nd a t1 t2 ⇔
  ∃a' t1' t2'.
    t = Nd a' t1' t2' ∧ a = f a' ∧ t1 = map f t1' ∧ t2 = map f t2'

⊢ exists ($= x) (bf_flatten tlist) ⇔ EXISTS (mem x) tlist

⊢ ∀a0 a1.
    mem a0 a1 ⇔
    (∃t1 t2. a1 = Nd a0 t1 t2) ∨ (∃b t1 t2. a1 = Nd b t1 t2 ∧ mem a0 t1) ∨
    ∃b t1 t2. a1 = Nd b t1 t2 ∧ mem a0 t2

⊢ ∀x t. mem x t ⇒ ∃n. lbtree$depth x t n

⊢ ∀mem'.
    (∀a t1 t2. mem' a (Nd a t1 t2)) ∧
    (∀a b t1 t2. mem' a t1 ⇒ mem' a (Nd b t1 t2)) ∧
    (∀a b t1 t2. mem' a t2 ⇒ mem' a (Nd b t1 t2)) ⇒
    ∀a0 a1. mem a0 a1 ⇒ mem' a0 a1

⊢ ∀x t. mem x t ⇒ ∃n. lbtree$mindepth x t = SOME n

⊢ (∀a t1 t2. mem a (Nd a t1 t2)) ∧
  (∀a b t1 t2. mem a t1 ⇒ mem a (Nd b t1 t2)) ∧
  ∀a b t1 t2. mem a t2 ⇒ mem a (Nd b t1 t2)

⊢ ∀mem'.
    (∀a t1 t2. mem' a (Nd a t1 t2)) ∧
    (∀a b t1 t2. mem a t1 ∧ mem' a t1 ⇒ mem' a (Nd b t1 t2)) ∧
    (∀a b t1 t2. mem a t2 ∧ mem' a t2 ⇒ mem' a (Nd b t1 t2)) ⇒
    ∀a0 a1. mem a0 a1 ⇒ mem' a0 a1

⊢ (mem a Lf ⇔ F) ∧ (mem a (Nd b t1 t2) ⇔ a = b ∨ mem a t1 ∨ mem a t2)

⊢ lbtree$mindepth x t = SOME n ⇒ lbtree$depth x t n

⊢ lbtree$mindepth x Lf = NONE ∧
  lbtree$mindepth x (Nd a t1 t2) =
  if x = a then SOME 0
  else
    OPTION_MAP SUC
      (lbtree$optmin (lbtree$mindepth x t1) (lbtree$mindepth x t2))

⊢ EXISTS (λe. ∃n. f e = SOME n) l ⇒ ∃i m. lbtree$is_mmindex f l i m

⊢ lbtree$is_mmindex f l i m ⇒
  ∀j n. lbtree$is_mmindex f l j n ⇔ j = i ∧ n = m

⊢ lbtree$optmin NONE NONE = NONE ∧ lbtree$optmin (SOME x) NONE = SOME x ∧
  lbtree$optmin NONE (SOME y) = SOME y ∧
  lbtree$optmin (SOME x) (SOME y) = SOME (MIN x y)

⊢ ∀P. P NONE NONE ∧ (∀x. P (SOME x) NONE) ∧ (∀y. P NONE (SOME y)) ∧
      (∀x y. P (SOME x) (SOME y)) ⇒
      ∀v v1. P v v1