Theory "patricia"

Parents words sorting

Signature

Type	Arity
ptree	1
Constant	Type
ADD	:α ptree -> num # α -> α ptree
ADD_LIST	:α ptree -> (num # α) list -> α ptree
BRANCH	:num # num # α ptree # α ptree -> α ptree
BRANCHING_BIT	:num -> num -> num
Branch	:num -> num -> α ptree -> α ptree -> α ptree
DEPTH	:α ptree -> num
EVERY_LEAF	:(num -> α -> bool) -> α ptree -> bool
EXISTS_LEAF	:(num -> α -> bool) -> α ptree -> bool
Empty	:α ptree
FIND	:α ptree -> num -> α
INSERT_PTREE	:num -> unit ptree -> unit ptree
IN_PTREE	:num -> unit ptree -> bool
IS_EMPTY	:α ptree -> bool
IS_PTREE	:α ptree -> bool
JOIN	:num # α ptree # num # α ptree -> α ptree
KEYS	:α ptree -> num list
Leaf	:num -> α -> α ptree
NUMSET_OF_PTREE	:unit ptree -> num -> bool
PEEK	:α ptree -> num -> α option
PTREE_OF_NUMSET	:unit ptree -> (num -> bool) -> unit ptree
REMOVE	:α ptree -> num -> α ptree
SIZE	:α ptree -> num
TRANSFORM	:(β -> α) -> β ptree -> α ptree
TRAVERSE	:α ptree -> num list
TRAVERSE_AUX	:α ptree -> num list -> num list
UNION_PTREE	:unit ptree -> unit ptree -> unit ptree
ptree_CASE	:α ptree -> β -> (num -> α -> β) -> (num -> num -> α ptree -> α ptree -> β) -> β
ptree_size	:(α -> num) -> α ptree -> num

Definitions

UNION_PTREE_def

⊢ ∀t1 t2. t1 UNION_PTREE t2 = t1 |++ NUMSET_OF_PTREE t2

TRAVERSE_def

⊢ (TRAVERSE -{}- = []) ∧ (∀j d. TRAVERSE (Leaf j d) = [j]) ∧
  ∀p m l r. TRAVERSE (Branch p m l r) = TRAVERSE l ++ TRAVERSE r

TRAVERSE_AUX_def

⊢ (∀a. TRAVERSE_AUX -{}- a = a) ∧ (∀k d a. TRAVERSE_AUX (Leaf k d) a = k::a) ∧
  ∀p m l r a.
      TRAVERSE_AUX (Branch p m l r) a = TRAVERSE_AUX l (TRAVERSE_AUX r a)

TRANSFORM_def

⊢ (∀f. TRANSFORM f -{}- = -{}-) ∧
  (∀f j d. TRANSFORM f (Leaf j d) = Leaf j (f d)) ∧
  ∀f p m l r.
      TRANSFORM f (Branch p m l r) =
      Branch p m (TRANSFORM f l) (TRANSFORM f r)

SIZE_def

⊢ ∀t. SIZE t = LENGTH (TRAVERSE t)

REMOVE_def

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

ptree_TY_DEF

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

ptree_size_def

⊢ (∀f. ptree_size f -{}- = 0) ∧
  (∀f a0 a1. ptree_size f (Leaf a0 a1) = 1 + (a0 + f a1)) ∧
  ∀f a0 a1 a2 a3.
      ptree_size f (Branch a0 a1 a2 a3) =
      1 + (a0 + (a1 + (ptree_size f a2 + ptree_size f a3)))

PTREE_OF_NUMSET_def

⊢ ∀t s. t |++ s = FOLDL (combin$C $INSERT_PTREE) t (SET_TO_LIST s)

ptree_case_def

⊢ (∀v f f1. ptree_CASE -{}- v f f1 = v) ∧
  (∀a0 a1 v f f1. ptree_CASE (Leaf a0 a1) v f f1 = f a0 a1) ∧
  ∀a0 a1 a2 a3 v f f1. ptree_CASE (Branch a0 a1 a2 a3) v f f1 = f1 a0 a1 a2 a3

NUMSET_OF_PTREE_def

⊢ ∀t. NUMSET_OF_PTREE t = LIST_TO_SET (TRAVERSE t)

KEYS_def

⊢ ∀t. KEYS t = QSORT $< (TRAVERSE t)

JOIN_def

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

IS_PTREE_def

⊢ (IS_PTREE -{}- ⇔ T) ∧ (∀k d. IS_PTREE (Leaf k d) ⇔ T) ∧
  ∀p m l r.
      IS_PTREE (Branch p m l r) ⇔
      p < 2 ** m ∧ IS_PTREE l ∧ IS_PTREE r ∧ l ≠ -{}- ∧ r ≠ -{}- ∧
      EVERY_LEAF (λk d. MOD_2EXP_EQ m k p ∧ BIT m k) l ∧
      EVERY_LEAF (λk d. MOD_2EXP_EQ m k p ∧ ¬BIT m k) r

IS_EMPTY_primitive_def

⊢ IS_EMPTY =
  WFREC (@R. WF R)
    (λIS_EMPTY a.
         case a of
           -{}- => I T
         | Leaf v6 v7 => I F
         | Branch v8 v9 v10 v11 => I F)

INSERT_PTREE_def

⊢ ∀n t. n INSERT_PTREE t = t |+ (n,())

IN_PTREE_def

⊢ ∀n t. n IN_PTREE t ⇔ IS_SOME (t ' n)

FIND_def

⊢ ∀t k. FIND t k = THE (t ' k)

EXISTS_LEAF_def

⊢ (∀P. EXISTS_LEAF P -{}- ⇔ F) ∧ (∀P j d. EXISTS_LEAF P (Leaf j d) ⇔ P j d) ∧
  ∀P p m l r.
      EXISTS_LEAF P (Branch p m l r) ⇔ EXISTS_LEAF P l ∨ EXISTS_LEAF P r

EVERY_LEAF_def

⊢ (∀P. EVERY_LEAF P -{}- ⇔ T) ∧ (∀P j d. EVERY_LEAF P (Leaf j d) ⇔ P j d) ∧
  ∀P p m l r. EVERY_LEAF P (Branch p m l r) ⇔ EVERY_LEAF P l ∧ EVERY_LEAF P r

DEPTH_def

⊢ (DEPTH -{}- = 0) ∧ (∀j d. DEPTH (Leaf j d) = 1) ∧
  ∀p m l r. DEPTH (Branch p m l r) = 1 + MAX (DEPTH l) (DEPTH r)

BRANCH_primitive_def

⊢ BRANCH =
  WFREC (@R. WF R)
    (λBRANCH a.
         case a of
           (p,m,-{}-,t) => I t
         | (p,m,Leaf v18 v19,-{}-) => I (Leaf v18 v19)
         | (p,m,Leaf v18 v19,Leaf v30 v31) =>
           I (Branch p m (Leaf v18 v19) (Leaf v30 v31))
         | (p,m,Leaf v18 v19,Branch v32 v33 v34 v35) =>
           I (Branch p m (Leaf v18 v19) (Branch v32 v33 v34 v35))
         | (p,m,Branch v20 v21 v22 v23,-{}-) => I (Branch v20 v21 v22 v23)
         | (p,m,Branch v20 v21 v22 v23,Leaf v42 v43) =>
           I (Branch p m (Branch v20 v21 v22 v23) (Leaf v42 v43))
         | (p,m,Branch v20 v21 v22 v23,Branch v44 v45 v46 v47) =>
           I (Branch p m (Branch v20 v21 v22 v23) (Branch v44 v45 v46 v47)))

ADD_LIST_def

⊢ $|++ = FOLDL $|+

Theorems

UNION_PTREE_IS_PTREE

⊢ ∀t1 t2. IS_PTREE t1 ∧ IS_PTREE t2 ⇒ IS_PTREE (t1 UNION_PTREE t2)

UNION_PTREE_EMPTY

⊢ (∀t. t UNION_PTREE -{}- = t) ∧ ∀t. IS_PTREE t ⇒ (-{}- UNION_PTREE t = t)

UNION_PTREE_COMM_EMPTY

⊢ ∀t. IS_PTREE t ⇒ (-{}- UNION_PTREE t = t UNION_PTREE -{}-)

UNION_PTREE_COMM

⊢ ∀t1 t2. IS_PTREE t1 ∧ IS_PTREE t2 ⇒ (t1 UNION_PTREE t2 = t2 UNION_PTREE t1)

UNION_PTREE_ASSOC

⊢ ∀t1 t2 t3.
      IS_PTREE t1 ∧ IS_PTREE t2 ∧ IS_PTREE t3 ⇒
      (t1 UNION_PTREE (t2 UNION_PTREE t3) = t1 UNION_PTREE t2 UNION_PTREE t3)

TRAVERSE_TRANSFORM

⊢ ∀f t. TRAVERSE (TRANSFORM f t) = TRAVERSE t

TRAVERSE_AUX

⊢ ∀t. TRAVERSE t = TRAVERSE_AUX t []

TRANSFORM_IS_PTREE

⊢ ∀f t. IS_PTREE t ⇒ IS_PTREE (TRANSFORM f t)

TRANSFORM_EMPTY

⊢ ∀f t. (TRANSFORM f t = -{}-) ⇔ (t = -{}-)

TRANSFORM_BRANCH

⊢ ∀f p m l r.
      TRANSFORM f (BRANCH (p,m,l,r)) =
      BRANCH (p,m,TRANSFORM f l,TRANSFORM f r)

SIZE_REMOVE

⊢ ∀t k.
      IS_PTREE t ⇒
      (SIZE (t \\ k) = if MEM k (TRAVERSE t) then SIZE t − 1 else SIZE t)

SIZE_PTREE_OF_NUMSET_EMPTY

⊢ ∀s. FINITE s ⇒ (SIZE (-{}- |++ s) = CARD s)

SIZE_PTREE_OF_NUMSET

⊢ ∀t s.
      FINITE s ⇒
      IS_PTREE t ∧ ALL_DISTINCT (TRAVERSE t ++ SET_TO_LIST s) ⇒
      (SIZE (t |++ s) = SIZE t + CARD s)

SIZE_ADD

⊢ ∀t k d.
      IS_PTREE t ⇒
      (SIZE (t |+ (k,d)) = if MEM k (TRAVERSE t) then SIZE t else SIZE t + 1)

SIZE

⊢ (SIZE -{}- = 0) ∧ (∀k d. SIZE (Leaf k d) = 1) ∧
  ∀p m l r. SIZE (Branch p m l r) = SIZE l + SIZE r

REMOVE_TRANSFORM

⊢ ∀f t k. TRANSFORM f (t \\ k) = TRANSFORM f t \\ k

REMOVE_REMOVE

⊢ ∀t k. IS_PTREE t ⇒ (t \\ k \\ k = t \\ k)

REMOVE_IS_PTREE

⊢ ∀t k. IS_PTREE t ⇒ IS_PTREE (t \\ k)

REMOVE_ADD_EQ

⊢ ∀t k d. t |+ (k,d) \\ k = t \\ k

REMOVE_ADD

⊢ ∀t k d j.
      IS_PTREE t ⇒
      (t |+ (k,d) \\ j = if k = j then t \\ j else t \\ j |+ (k,d))

QSORT_MEM_EQ

⊢ ∀l2 l1 R. (QSORT R l1 = QSORT R l2) ⇒ ∀x. MEM x l1 ⇔ MEM x l2

PTREE_TRAVERSE_EQ

⊢ ∀t1 t2.
      IS_PTREE t1 ∧ IS_PTREE t2 ⇒
      ((∀k. MEM k (TRAVERSE t1) ⇔ MEM k (TRAVERSE t2)) ⇔
       (TRAVERSE t1 = TRAVERSE t2))

PTREE_OF_NUMSET_UNION

⊢ ∀t s1 s2.
      IS_PTREE t ∧ FINITE s1 ∧ FINITE s2 ⇒ (t |++ (s1 ∪ s2) = t |++ s1 |++ s2)

PTREE_OF_NUMSET_NUMSET_OF_PTREE

⊢ ∀t s. IS_PTREE t ∧ FINITE s ⇒ (-{}- |++ (NUMSET_OF_PTREE t ∪ s) = t |++ s)

PTREE_OF_NUMSET_IS_PTREE_EMPTY

⊢ ∀s. IS_PTREE (-{}- |++ s)

PTREE_OF_NUMSET_IS_PTREE

⊢ ∀t s. IS_PTREE t ⇒ IS_PTREE (t |++ s)

PTREE_OF_NUMSET_INSERT_EMPTY

⊢ ∀s x. FINITE s ⇒ (-{}- |++ (x INSERT s) = x INSERT_PTREE -{}- |++ s)

PTREE_OF_NUMSET_INSERT

⊢ ∀t s x.
      IS_PTREE t ∧ FINITE s ⇒ (t |++ (x INSERT s) = x INSERT_PTREE t |++ s)

PTREE_OF_NUMSET_EMPTY

⊢ ∀t. t |++ ∅ = t

PTREE_OF_NUMSET_DELETE

⊢ ∀s x. FINITE s ⇒ (-{}- |++ (s DELETE x) = (-{}- |++ s) \\ x)

ptree_nchotomy

⊢ ∀pp. (pp = -{}-) ∨ (∃n a. pp = Leaf n a) ∨ ∃n0 n p p0. pp = Branch n0 n p p0

ptree_induction

⊢ ∀P.
      P -{}- ∧ (∀n a. P (Leaf n a)) ∧
      (∀p p0. P p ∧ P p0 ⇒ ∀n n0. P (Branch n0 n p p0)) ⇒
      ∀p. P p

PTREE_EXTENSION

⊢ ∀t1 t2.
      IS_PTREE t1 ∧ IS_PTREE t2 ⇒
      ((t1 = t2) ⇔ ∀x. x IN_PTREE t1 ⇔ x IN_PTREE t2)

PTREE_EQ

⊢ ∀t1 t2. IS_PTREE t1 ∧ IS_PTREE t2 ⇒ ((∀k. t1 ' k = t2 ' k) ⇔ (t1 = t2))

ptree_distinct

⊢ (∀a1 a0. -{}- ≠ Leaf a0 a1) ∧ (∀a3 a2 a1 a0. -{}- ≠ Branch a0 a1 a2 a3) ∧
  ∀a3 a2 a1' a1 a0' a0. Leaf a0 a1 ≠ Branch a0' a1' a2 a3

ptree_case_eq

⊢ (ptree_CASE x v f f1 = v') ⇔
  (x = -{}-) ∧ (v = v') ∨ (∃n a. (x = Leaf n a) ∧ (f n a = v')) ∨
  ∃n0 n p p0. (x = Branch n0 n p p0) ∧ (f1 n0 n p p0 = v')

ptree_case_cong

⊢ ∀M M' v f f1.
      (M = M') ∧ ((M' = -{}-) ⇒ (v = v')) ∧
      (∀a0 a1. (M' = Leaf a0 a1) ⇒ (f a0 a1 = f' a0 a1)) ∧
      (∀a0 a1 a2 a3.
           (M' = Branch a0 a1 a2 a3) ⇒ (f1 a0 a1 a2 a3 = f1' a0 a1 a2 a3)) ⇒
      (ptree_CASE M v f f1 = ptree_CASE M' v' f' f1')

ptree_Axiom

⊢ ∀f0 f1 f2.
      ∃fn.
          (fn -{}- = f0) ∧ (∀a0 a1. fn (Leaf a0 a1) = f1 a0 a1) ∧
          ∀a0 a1 a2 a3.
              fn (Branch a0 a1 a2 a3) = f2 a0 a1 a2 a3 (fn a2) (fn a3)

ptree_11

⊢ (∀a0 a1 a0' a1'. (Leaf a0 a1 = Leaf a0' a1') ⇔ (a0 = a0') ∧ (a1 = a1')) ∧
  ∀a0 a1 a2 a3 a0' a1' a2' a3'.
      (Branch a0 a1 a2 a3 = Branch a0' a1' a2' a3') ⇔
      (a0 = a0') ∧ (a1 = a1') ∧ (a2 = a2') ∧ (a3 = a3')

PERM_REMOVE

⊢ ∀t k.
      IS_PTREE t ∧ MEM k (TRAVERSE t) ⇒
      PERM (TRAVERSE (t \\ k)) (FILTER (λx. x ≠ k) (TRAVERSE t))

PERM_NOT_REMOVE

⊢ ∀t k. IS_PTREE t ∧ ¬MEM k (TRAVERSE t) ⇒ (TRAVERSE (t \\ k) = TRAVERSE t)

PERM_NOT_ADD

⊢ ∀t k d.
      IS_PTREE t ∧ MEM k (TRAVERSE t) ⇒ (TRAVERSE (t |+ (k,d)) = TRAVERSE t)

PERM_INSERT_PTREE

⊢ ∀t s.
      FINITE s ⇒
      IS_PTREE t ⇒
      PERM (TRAVERSE (FOLDL (combin$C $INSERT_PTREE) t (SET_TO_LIST s)))
        (SET_TO_LIST (NUMSET_OF_PTREE t ∪ s))

PERM_DELETE_PTREE

⊢ ∀t k.
      IS_PTREE t ∧ MEM k (TRAVERSE t) ⇒
      PERM (TRAVERSE (t \\ k)) (FILTER (λx. x ≠ k) (TRAVERSE t))

PERM_ADD

⊢ ∀t k d.
      IS_PTREE t ∧ ¬MEM k (TRAVERSE t) ⇒
      PERM (TRAVERSE (t |+ (k,d))) (k::TRAVERSE t)

PEEK_TRANSFORM

⊢ ∀f t k.
      TRANSFORM f t ' k = case t ' k of NONE => NONE | SOME x => SOME (f x)

PEEK_REMOVE

⊢ ∀t k j. IS_PTREE t ⇒ ((t \\ k) ' j = if k = j then NONE else t ' j)

PEEK_NONE

⊢ ∀P t k. (∀d. ¬P k d) ∧ EVERY_LEAF P t ⇒ (t ' k = NONE)

PEEK_INSERT_PTREE

⊢ ∀t k j.
      IS_PTREE t ⇒ ((k INSERT_PTREE t) ' j = if k = j then SOME () else t ' j)

PEEK_ind

⊢ ∀P.
      (∀k. P -{}- k) ∧ (∀j d k. P (Leaf j d) k) ∧
      (∀p m l r k. P (if BIT m k then l else r) k ⇒ P (Branch p m l r) k) ⇒
      ∀v v1. P v v1

PEEK_def

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

PEEK_ADD

⊢ ∀t k d j. IS_PTREE t ⇒ ((t |+ (k,d)) ' j = if k = j then SOME d else t ' j)

NUMSET_OF_PTREE_PTREE_OF_NUMSET_EMPTY

⊢ ∀s. FINITE s ⇒ (NUMSET_OF_PTREE (-{}- |++ s) = s)

NUMSET_OF_PTREE_PTREE_OF_NUMSET

⊢ ∀t s.
      IS_PTREE t ∧ FINITE s ⇒
      (NUMSET_OF_PTREE (t |++ s) = NUMSET_OF_PTREE t ∪ s)

NUMSET_OF_PTREE_EMPTY

⊢ NUMSET_OF_PTREE -{}- = ∅

NOT_KEY_LEFT_AND_RIGHT

⊢ ∀p m l r k j.
      IS_PTREE (Branch p m l r) ∧ IS_SOME (l ' k) ∧ IS_SOME (r ' j) ⇒ k ≠ j

NOT_ADD_EMPTY

⊢ ∀t k d. t |+ (k,d) ≠ -{}-

MONO_EVERY_LEAF

⊢ ∀P Q t. (∀k d. P k d ⇒ Q k d) ∧ EVERY_LEAF P t ⇒ EVERY_LEAF Q t

MEM_TRAVERSE_PEEK

⊢ ∀t k. IS_PTREE t ⇒ (MEM k (TRAVERSE t) ⇔ IS_SOME (t ' k))

MEM_TRAVERSE_INSERT_PTREE

⊢ ∀t x h.
      IS_PTREE t ⇒
      (MEM x (TRAVERSE (h INSERT_PTREE t)) ⇔
       (x = h) ∨ x ≠ h ∧ MEM x (TRAVERSE t))

MEM_TRAVERSE

⊢ ∀t k. IS_PTREE t ⇒ (MEM k (TRAVERSE t) ⇔ k ∈ NUMSET_OF_PTREE t)

MEM_ALL_DISTINCT_IMP_PERM

⊢ ∀l1 l2.
      ALL_DISTINCT l1 ∧ ALL_DISTINCT l2 ∧ (∀x. MEM x l1 ⇔ MEM x l2) ⇒
      PERM l1 l2

KEYS_PEEK

⊢ ∀t1 t2.
      IS_PTREE t1 ∧ IS_PTREE t2 ⇒
      ((KEYS t1 = KEYS t2) ⇔ (TRAVERSE t1 = TRAVERSE t2))

IS_PTREE_PEEK

⊢ (∀k. ¬IS_SOME (-{}- ' k)) ∧ (∀k j b. IS_SOME (Leaf j b ' k) ⇔ (j = k)) ∧
  ∀p m l r.
      IS_PTREE (Branch p m l r) ⇒
      (∃k. BIT m k ∧ IS_SOME (l ' k)) ∧ (∃k. ¬BIT m k ∧ IS_SOME (r ' k)) ∧
      ∀k n.
          ¬MOD_2EXP_EQ m k p ∨ n < m ∧ (BIT n p ⇎ BIT n k) ⇒
          ¬IS_SOME (l ' k) ∧ ¬IS_SOME (r ' k)

IS_PTREE_BRANCH

⊢ ∀p m l r.
      p < 2 ** m ∧ ¬((l = -{}-) ∧ (r = -{}-)) ∧
      EVERY_LEAF (λk d. MOD_2EXP_EQ m k p ∧ BIT m k) l ∧
      EVERY_LEAF (λk d. MOD_2EXP_EQ m k p ∧ ¬BIT m k) r ∧ IS_PTREE l ∧
      IS_PTREE r ⇒
      IS_PTREE (BRANCH (p,m,l,r))

IS_EMPTY_ind

⊢ ∀P.
      P -{}- ∧ (∀v v1. P (Leaf v v1)) ∧ (∀v2 v3 v4 v5. P (Branch v2 v3 v4 v5)) ⇒
      ∀v. P v

IS_EMPTY_def

⊢ (IS_EMPTY -{}- ⇔ T) ∧ (IS_EMPTY (Leaf v v1) ⇔ F) ∧
  (IS_EMPTY (Branch v2 v3 v4 v5) ⇔ F)

INSERT_PTREE_IS_PTREE

⊢ ∀t x. IS_PTREE t ⇒ IS_PTREE (x INSERT_PTREE t)

IN_PTREE_UNION_PTREE

⊢ ∀t1 t2 n.
      IS_PTREE t1 ∧ IS_PTREE t2 ⇒
      (n IN_PTREE t1 UNION_PTREE t2 ⇔ n IN_PTREE t1 ∨ n IN_PTREE t2)

IN_PTREE_REMOVE

⊢ ∀t m n. IS_PTREE t ⇒ (n IN_PTREE t \\ m ⇔ n ≠ m ∧ n IN_PTREE t)

IN_PTREE_OF_NUMSET_EMPTY

⊢ ∀s n. FINITE s ⇒ (n ∈ s ⇔ n IN_PTREE -{}- |++ s)

IN_PTREE_OF_NUMSET

⊢ ∀t s n. IS_PTREE t ∧ FINITE s ⇒ (n IN_PTREE t |++ s ⇔ n IN_PTREE t ∨ n ∈ s)

IN_PTREE_INSERT_PTREE

⊢ ∀t m n. IS_PTREE t ⇒ (n IN_PTREE m INSERT_PTREE t ⇔ (m = n) ∨ n IN_PTREE t)

IN_PTREE_EMPTY

⊢ ∀n. ¬(n IN_PTREE -{}-)

IN_NUMSET_OF_PTREE

⊢ ∀t n. IS_PTREE t ⇒ (n ∈ NUMSET_OF_PTREE t ⇔ n IN_PTREE t)

FINITE_NUMSET_OF_PTREE

⊢ ∀t. FINITE (NUMSET_OF_PTREE t)

FILTER_NONE

⊢ ∀P l. (∀n. n < LENGTH l ⇒ P (EL n l)) ⇒ (FILTER P l = l)

FILTER_ALL

⊢ ∀P l. (∀n. n < LENGTH l ⇒ ¬P (EL n l)) ⇔ (FILTER P l = [])

EVERY_LEAF_TRANSFORM

⊢ ∀P Q f t.
      (∀k d. P k d ⇒ Q k (f d)) ∧ EVERY_LEAF P t ⇒
      EVERY_LEAF Q (TRANSFORM f t)

EVERY_LEAF_REMOVE

⊢ ∀P t k. EVERY_LEAF P t ⇒ EVERY_LEAF P (t \\ k)

EVERY_LEAF_PEEK

⊢ ∀P t k. EVERY_LEAF P t ∧ IS_SOME (t ' k) ⇒ P k (THE (t ' k))

EVERY_LEAF_BRANCH

⊢ ∀P p m l r.
      EVERY_LEAF P (BRANCH (p,m,l,r)) ⇔ EVERY_LEAF P l ∧ EVERY_LEAF P r

EVERY_LEAF_ADD

⊢ ∀P t k d. P k d ∧ EVERY_LEAF P t ⇒ EVERY_LEAF P (t |+ (k,d))

EMPTY_IS_PTREE

⊢ IS_PTREE -{}-

DELETE_UNION

⊢ ∀x s1 s2. s1 ∪ s2 DELETE x = s1 DELETE x ∪ (s2 DELETE x)

datatype_ptree

⊢ DATATYPE (ptree -{}- Leaf Branch)

CARD_NUMSET_OF_PTREE

⊢ ∀t. IS_PTREE t ⇒ (CARD (NUMSET_OF_PTREE t) = SIZE t)

CARD_LIST_TO_SET

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

BRANCHING_BIT_ZERO

⊢ ∀a b. (BRANCHING_BIT a b = 0) ⇔ (ODD a ⇔ EVEN b) ∨ (a = b)

BRANCHING_BIT_SYM

⊢ ∀a b. BRANCHING_BIT a b = BRANCHING_BIT b a

BRANCHING_BIT_ind

⊢ ∀P.
      (∀p0 p1.
           (¬((ODD p0 ⇔ EVEN p1) ∨ (p0 = p1)) ⇒ P (DIV2 p0) (DIV2 p1)) ⇒
           P p0 p1) ⇒
      ∀v v1. P v v1

BRANCHING_BIT_def

⊢ ∀p1 p0.
      BRANCHING_BIT p0 p1 =
      if (ODD p0 ⇔ EVEN p1) ∨ (p0 = p1) then 0
      else SUC (BRANCHING_BIT (DIV2 p0) (DIV2 p1))

BRANCHING_BIT

⊢ ∀a b. a ≠ b ⇒ (BIT (BRANCHING_BIT a b) a ⇎ BIT (BRANCHING_BIT a b) b)

BRANCH_ind

⊢ ∀P.
      (∀p m t. P (p,m,-{}-,t)) ∧ (∀p m v6 v7. P (p,m,Leaf v6 v7,-{}-)) ∧
      (∀p m v8 v9 v10 v11. P (p,m,Branch v8 v9 v10 v11,-{}-)) ∧
      (∀p m v12 v13 v24 v25. P (p,m,Leaf v12 v13,Leaf v24 v25)) ∧
      (∀p m v12 v13 v26 v27 v28 v29.
           P (p,m,Leaf v12 v13,Branch v26 v27 v28 v29)) ∧
      (∀p m v14 v15 v16 v17 v36 v37.
           P (p,m,Branch v14 v15 v16 v17,Leaf v36 v37)) ∧
      (∀p m v14 v15 v16 v17 v38 v39 v40 v41.
           P (p,m,Branch v14 v15 v16 v17,Branch v38 v39 v40 v41)) ⇒
      ∀v v1 v2 v3. P (v,v1,v2,v3)

BRANCH_def

⊢ (BRANCH (p,m,-{}-,t) = t) ∧ (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 v24 v25) =
   Branch p m (Leaf v12 v13) (Leaf v24 v25)) ∧
  (BRANCH (p,m,Leaf v12 v13,Branch v26 v27 v28 v29) =
   Branch p m (Leaf v12 v13) (Branch v26 v27 v28 v29)) ∧
  (BRANCH (p,m,Branch v14 v15 v16 v17,Leaf v36 v37) =
   Branch p m (Branch v14 v15 v16 v17) (Leaf v36 v37)) ∧
  (BRANCH (p,m,Branch v14 v15 v16 v17,Branch v38 v39 v40 v41) =
   Branch p m (Branch v14 v15 v16 v17) (Branch v38 v39 v40 v41))

BRANCH

⊢ ∀p m l r.
      BRANCH (p,m,l,r) =
      if l = -{}- then r else if r = -{}- then l else Branch p m l r

ALL_DISTINCT_TRAVERSE

⊢ ∀t. IS_PTREE t ⇒ ALL_DISTINCT (TRAVERSE t)

ADD_TRANSFORM

⊢ ∀f t k d. TRANSFORM f (t |+ (k,d)) = TRANSFORM f t |+ (k,f d)

ADD_LIST_TO_EMPTY_IS_PTREE

⊢ ∀l. IS_PTREE (-{}- |++ l)

ADD_LIST_IS_PTREE

⊢ ∀t l. IS_PTREE t ⇒ IS_PTREE (t |++ l)

ADD_IS_PTREE

⊢ ∀t x. IS_PTREE t ⇒ IS_PTREE (t |+ x)

ADD_INSERT

⊢ ∀v t n. t |+ (n,v) = n INSERT_PTREE t

ADD_ind

⊢ ∀P.
      (∀k e. P -{}- (k,e)) ∧ (∀j d k e. P (Leaf j d) (k,e)) ∧
      (∀p m l r k e.
           (MOD_2EXP_EQ m k p ∧ ¬BIT m k ⇒ P r (k,e)) ∧
           (MOD_2EXP_EQ m k p ∧ BIT m k ⇒ P l (k,e)) ⇒
           P (Branch p m l r) (k,e)) ⇒
      ∀v v1 v2. P v (v1,v2)

ADD_def

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

ADD_ADD_SYM

⊢ ∀t k j d e. IS_PTREE t ∧ k ≠ j ⇒ (t |+ (k,d) |+ (j,e) = t |+ (j,e) |+ (k,d))

ADD_ADD

⊢ ∀t k d e. t |+ (k,d) |+ (k,e) = t |+ (k,e)