Theory patricia_casts

⊢ $|++ = FOLDL $|+

⊢ $|++ = FOLDL $|+

⊢ ∀t w d. t |+ (w,d) = t |+ (string_to_num w,d)

⊢ ∀t w d. t |+ (w,d) = SOME_PTREE (THE_PTREE t |+ (w2n w,d))

⊢ ∀t. DEPTHw t = DEPTH (THE_PTREE t)

⊢ ∀P t. EVERY_LEAFw P t ⇔ EVERY_LEAF (λk d. P (n2w k) d) (THE_PTREE t)

⊢ ∀P t. EXISTS_LEAFw P t ⇔ EXISTS_LEAF (λk d. P (n2w k) d) (THE_PTREE t)

⊢ ∀t w. FINDs t w = THE (t ' w)

⊢ ∀t w. FINDw t w = THE (t ' w)

⊢ ∀w t. w INSERT_PTREEs t = string_to_num w INSERT_PTREE t

⊢ ∀w t. w INSERT_PTREEw t = SOME_PTREE (w2n w INSERT_PTREE THE_PTREE t)

⊢ ∀w t. w IN_PTREEs t ⇔ string_to_num w IN_PTREE t

⊢ ∀w t. w IN_PTREEw t ⇔ w2n w IN_PTREE THE_PTREE t

⊢ ∀t. KEYSs t = QSORT string_lt (TRAVERSEs t)

⊢ ∀t. KEYSw t = QSORT $<+ (TRAVERSEw t)

⊢ ∀t w. t ' w = t ' (string_to_num w)

⊢ ∀t w. t ' w = THE_PTREE t ' (w2n w)

⊢ ∀t s. t |++ s = t |++ IMAGE string_to_num s

⊢ ∀t s. t |++ s = SOME_PTREE (THE_PTREE t |++ IMAGE w2n s)

⊢ ∀t w. t \\ w = t \\ string_to_num w

⊢ ∀t w. t \\ w = SOME_PTREE (THE_PTREE t \\ w2n w)

⊢ ∀t. SIZEw t = SIZE (THE_PTREE t)

⊢ ∀c s. SKIP1 (STRING c s) = s

⊢ ∀t. SOME_PTREE t = Word_ptree (K ()) t

⊢ ∀t. STRINGSET_OF_PTREE t = LIST_TO_SET (TRAVERSEs t)

⊢ ∀a t. THE_PTREE (Word_ptree a t) = t

⊢ ∀f t. TRANSFORMw f t = SOME_PTREE (TRANSFORM f (THE_PTREE t))

⊢ ∀t. TRAVERSEs t = MAP num_to_string (TRAVERSE t)

⊢ ∀t. TRAVERSEw t = MAP n2w (TRAVERSE (THE_PTREE t))

⊢ ∀t1 t2.
    t1 UNION_PTREEw t2 = SOME_PTREE (THE_PTREE t1 UNION_PTREE THE_PTREE t2)

⊢ ∀t. WORDSET_OF_PTREE t = LIST_TO_SET (TRAVERSEw t)

⊢ +{}+ = SOME_PTREE -{}-

⊢ ∀n. num_to_string n = SKIP1 (n2s 256 CHR n)

⊢ ∀s. string_to_num s = s2n 256 ORD (STRING #"\^A" s)

⊢ ∀f. word_ptreeMAP f = word_ptree_ABS ∘ (I ## ptreeMAP f) ∘ word_ptree_REP

⊢ word_ptreeREL =
  (λR x y.
     ∃z. (∀p. p ∈ word_ptreeSET z ⇒ R (FST p) (SND p)) ∧
         (word_ptreeMAP FST z = x) ∧ (word_ptreeMAP SND z = y))

⊢ word_ptreeSET =
  S ($UNION ∘ BIMG (K ∅) ∘ setFST) (BIMG (BIMG $= ∘ ptreeSET) ∘ setSND) ∘
  word_ptree_REP

⊢ (∀a. word_ptree_ABS (word_ptree_REP a) = a) ∧
  ∀r. (λx. T) r ⇔ (word_ptree_REP (word_ptree_ABS r) = r)

⊢ word_ptree_CONS = word_ptree_ABS

⊢ ∃rep. TYPE_DEFINITION (λx. T) rep

⊢ ∀a0 a1 f. word_ptree_CASE (Word_ptree a0 a1) f = f a0 a1

⊢ ∀f0 f1 a0 a1.
    word_ptree_size f0 f1 (Word_ptree a0 a1) = 1 + ptree_size f1 a1

⊢ ∀w v t. t |+ (w,v) = t |+ (w,())

⊢ ∀w v t. t |+ (w,v) = t |+ (w,())

⊢ ∀l. EVERY ($> 256) (MAP ORD l)

⊢ ∀n. (n = 1) ∨ 256 ≤ n ∧ (n DIV 256 ** LOG 256 n = 1) ⇔
      n ∈ IMAGE string_to_num 𝕌(:string)

⊢ ∀f l1 l2.
    (∀x y. (f x = f y) ⇔ (x = y)) ⇒ ((MAP f l1 = MAP f l2) ⇔ (l1 = l2))

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

⊢ ∀t. THE_PTREE (SOME_PTREE t) = t

⊢ DATATYPE (word_ptree Word_ptree)

⊢ ∀s. num_to_string (string_to_num s) = s

⊢ ∀s t. (string_to_num s = string_to_num t) ⇔ (s = t)

⊢ ∀n. n ∈ IMAGE string_to_num 𝕌(:string) ⇒
      (string_to_num (num_to_string n) = n)

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

⊢ ∀f0. ∃h. ∀a0 a1. h (Word_ptree a0 a1) = f0 a0 a1

⊢ ∀f g x.
    (∀a. a ∈ word_ptreeSET x ⇒ (f a = g a)) ⇒
    (word_ptreeMAP f x = word_ptreeMAP g x)

⊢ word_ptreeMAP I = I

⊢ ∀f x. word_ptreeSET (word_ptreeMAP f x) = IMAGE f (word_ptreeSET x)

⊢ word_ptreeMAP g ∘ word_ptreeMAP f = word_ptreeMAP (g ∘ f)

⊢ ∀x. cardleq (word_ptreeSET x) 𝕌(:num)

⊢ ∀M M' f.
    (M = M') ∧ (∀a0 a1. (M' = Word_ptree a0 a1) ⇒ (f a0 a1 = f' a0 a1)) ⇒
    (word_ptree_CASE M f = word_ptree_CASE M' f')

⊢ (word_ptree_CASE x f = v) ⇔ ∃f' p. (x = Word_ptree f' p) ∧ (f f' p = v)

⊢ ∀P. (∀f p. P (Word_ptree f p)) ⇒ ∀w. P w

⊢ ∀a. a ∈
      word_ptreeSET
        ((λa.
            word_ptree_ABS
              ((λa. (ARB,(λa2. ptree_CONS (INR (INL (ARB,a2)))) a)) a)) a)

⊢ ∀ww. ∃f p. ww = Word_ptree f p

⊢ ∀a. word_ptreeSET
        ((λa.
            word_ptree_ABS
              ((λa. (ARB,(λa. ptree_CONS ((K ∘ INL) ARB ARB)) ARB)) a)) a) ⊆
      ∅