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)

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0'.
           ∀ $var$('word_ptree').
             (∀a0'.
                (∃a0 a1.
                   a0' =
                   (λa0 a1. ind_type$CONSTR 0 (a0,a1) (λn. ind_type$BOTTOM))
                     a0 a1) ⇒
                $var$('word_ptree') a0') ⇒
             $var$('word_ptree') a0') rep

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

⊢ ∀f f1 a0 a1.
    word_ptree_size f 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')

⊢ ∀f. ∃fn. ∀a0 a1. fn (Word_ptree a0 a1) = f a0 a1

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

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