Theory alist_tree

⊢ ∀n xs ys. count_append n xs ys = xs ⧺ ys

⊢ ∀frame_l frame_r R k x al al'.
    is_insert frame_l frame_r R k x al al' ⇔
    irreflexive R ∧ transitive R ⇒
    SORTED R (MAP FST al) ⇒
    ALOOKUP al' = ALOOKUP ((k,x)::al) ∧
    (frame_l ⇒ al ≠ [] ∧ FST (HD al') = FST (HD al)) ∧
    (frame_r ⇒ al ≠ [] ∧ FST (LAST al') = FST (LAST al)) ∧
    SORTED R (MAP FST al')

⊢ ∀fl fr R al x r.
    is_lookup fl fr R al x r ⇔
    ∀xs ys.
      fl ∨ xs = [] ⇒
      fr ∨ ys = [] ⇒
      irreflexive R ∧ transitive R ⇒
      SORTED R (MAP FST (xs ⧺ al ⧺ ys)) ⇒
      ALOOKUP (xs ⧺ al ⧺ ys) x = r

⊢ ∀f g. option_choice_f f g = (λx. OPTION_CHOICE (f x) (g x))

⊢ ∀R al f.
    sorted_alist_repr R al f ⇔
    SORTED R (MAP FST al) ∧ irreflexive R ∧ transitive R ∧ f = ALOOKUP al

⊢ P ∨ Q ⇔ ¬P ⇒ Q

⊢ HD (xs ⧺ ys) = if xs = [] then HD ys else HD xs

⊢ xs ≠ [] ⇒ HD (MAP f xs) = f (HD xs)

⊢ xs ≠ [] ⇒ MEM (HD xs) xs

⊢ LAST (xs ⧺ ys) = if ys = [] then LAST xs else LAST ys

⊢ sorted_alist_repr R al f ∧
  sorted_alist_repr R al' (option_choice_f (ALOOKUP al) g) ⇒
  sorted_alist_repr R al' (option_choice_f f g)

⊢ ∀al.
    irreflexive R ∧ transitive R ⇒
    SORTED R (MAP FST al) ⇒
    sorted_alist_repr R al (ALOOKUP al)

⊢ ALOOKUP (xs ⧺ ys) = option_choice_f (ALOOKUP xs) (ALOOKUP ys)

⊢ option_choice_f (ALOOKUP []) f = f ∧ option_choice_f f (ALOOKUP []) = f

⊢ ALOOKUP (x::y::zs) = option_choice_f (ALOOKUP [x]) (ALOOKUP (y::zs)) ∧
  option_choice_f (ALOOKUP []) g = g

⊢ count_append i xs (count_append j ys zs) =
  count_append ARB (count_append ARB xs ys) zs

⊢ count_append i (count_append j xs ys) zs =
  count_append ARB xs (count_append ARB ys zs)

⊢ HD (count_append i (count_append j xs ys) zs) =
  HD (count_append 0 xs (count_append 0 ys zs)) ∧
  HD (count_append i (x::xs) ys) = x ∧ HD (count_append i [] ys) = HD ys ∧
  LAST (count_append i xs (count_append j ys zs)) =
  LAST (count_append 0 (count_append 0 xs ys) zs) ∧
  LAST (count_append i xs (y::ys)) = LAST (y::ys) ∧
  LAST (count_append i xs []) = LAST xs ∧ HD (x::xs) = x ∧
  LAST (x::y::zs) = LAST (y::zs) ∧ LAST [x] = x ∧
  (count_append i (count_append j xs ys) zs = [] ⇔
   count_append 0 xs (count_append 0 ys zs) = []) ∧
  (count_append i [] ys = [] ⇔ ys = []) ∧
  (count_append i (x::xs) ys = [] ⇔ F) ∧ (x::xs = [] ⇔ F)

⊢ (λx. NONE) = ALOOKUP []

⊢ is_insert fl fr R k x al al' ⇒
  fl ⇒
  SORTED R (MAP FST al) ⇒
  irreflexive R ∧ transitive R ⇒
  k = FST (HD al) ∨ R (HD (MAP FST al)) k

⊢ is_insert T fr R k x r r' ⇒
  SORTED R (MAP FST (l ⧺ r)) ⇒
  irreflexive R ∧ transitive R ⇒
  ¬MEM k (MAP FST l)

⊢ ∀R n k x.
    l ≠ [] ⇒
    R (FST (LAST l)) k ⇒
    r ≠ [] ⇒
    R k (FST (HD r)) ⇒
    is_insert T T R k x (count_append n l r)
      (count_append ARB l (count_append ARB [(k,x)] r))

⊢ (fl ⇒ l ≠ []) ⇒
  (l ≠ [] ⇒ R (FST (LAST l)) k) ⇒
  (fr ⇒ r ≠ []) ⇒
  (r ≠ [] ⇒ R k (FST (HD r))) ⇒
  is_insert fl fr R k x (count_append n l r)
    (count_append ARB l (count_append ARB [(k,x)] r))

⊢ ∀R k x xs.
    xs ≠ [] ⇒
    R k (FST (HD xs)) ⇒
    is_insert F T R k x xs (count_append ARB [(k,x)] xs)

⊢ ∀R k x xs.
    xs ≠ [] ⇒
    R (FST (LAST xs)) k ⇒
    is_insert T F R k x xs (count_append ARB xs [(k,x)])

⊢ ∀n. is_insert fl T R k x l l' ⇒
      is_insert fl T R k x (count_append n l r) (count_append ARB l' r)

⊢ ∀R k x v. FST v = k ⇒ is_insert T T R k x [v] [(k,x)]

⊢ ∀n. is_insert T fr R k x r r' ⇒
      is_insert T fr R k x (count_append n l r) (count_append ARB l r')

⊢ ∀R k x. is_insert F F R k x [] [(k,x)]

⊢ ∀R n l r k.
    l ≠ [] ⇒
    R (FST (LAST l)) k ⇒
    r ≠ [] ⇒
    R k (FST (HD r)) ⇒
    is_lookup T T R (count_append n l r) k NONE

⊢ ∀R k al. al = [] ⇒ is_lookup F F R al k NONE

⊢ ∀R k k' v. R k k' ⇒ is_lookup F T R [(k',v)] k NONE

⊢ ∀R k k' v. R k' k ⇒ is_lookup T F R [(k',v)] k NONE

⊢ ∀R k k' v. k' = k ⇒ is_lookup T T R [(k',v)] k (SOME v)

⊢ ∀n. is_lookup fl T R l x res ⇒
      is_lookup fl T R (count_append n l r) x res

⊢ ∀n. is_lookup T fr R r x res ⇒
      is_lookup T fr R (count_append n l r) x res

⊢ sorted_alist_repr R al f ∧ is_lookup fl fr R al x r ⇒ f x = r

⊢ option_choice_f (option_choice_f f g) h =
  option_choice_f f (option_choice_f g h)

⊢ sorted_alist_repr R al f ∧ is_insert fl fr R k x al al' ⇒
  sorted_alist_repr R al' (option_choice_f (ALOOKUP [(k,x)]) f)

⊢ ∀j. count_append i xs ys = count_append j xs ys

⊢ ∀k. SORTED R (MAP FST l ⧺ MAP FST r) ⇒
      (l ≠ [] ⇒ R (FST (LAST l)) k) ⇒
      (r ≠ [] ⇒ R k (FST (HD r))) ⇒
      SORTED R (MAP FST l ⧺ k::MAP FST r)