Theory Encode

⊢ ∀a b. biprefix a b ⇔ b ≼ a ∨ a ≼ b

⊢ ∀m p.
    collision_free m p ⇔
    ∀x y. p x ∧ p y ∧ x MOD 2 ** m = y MOD 2 ** m ⇒ x = y

⊢ (∀e l. encode_blist 0 e l = []) ∧
  ∀m e l. encode_blist (SUC m) e l = e (HD l) ⧺ encode_blist m e (TL l)

⊢ (∀n. encode_bnum 0 n = []) ∧
  ∀m n. encode_bnum (SUC m) n = ¬EVEN n::encode_bnum m (n DIV 2)

⊢ ∀x. encode_bool x = [x]

⊢ (∀xb. encode_list xb [] = [F]) ∧
  ∀xb x xs. encode_list xb (x::xs) = T::(xb x ⧺ encode_list xb xs)

⊢ encode_num =
  WFREC
    (@R. WF R ∧ (∀n. n ≠ 0 ∧ EVEN n ⇒ R ((n − 2) DIV 2) n) ∧
         ∀n. n ≠ 0 ∧ ¬EVEN n ⇒ R ((n − 1) DIV 2) n)
    (λencode_num a.
         I
           (if a = 0 then [T; T]
            else if EVEN a then F::encode_num ((a − 2) DIV 2)
            else T::F::encode_num ((a − 1) DIV 2)))

⊢ (∀xb. encode_option xb NONE = [F]) ∧
  ∀xb x. encode_option xb (SOME x) = T::xb x

⊢ ∀xb yb x y. encode_prod xb yb (x,y) = xb x ⧺ yb y

⊢ (∀xb yb x. encode_sum xb yb (INL x) = T::xb x) ∧
  ∀xb yb y. encode_sum xb yb (INR y) = F::yb y

⊢ ∀v0. encode_unit v0 = []

⊢ ∀m p x. lift_blist m p x ⇔ EVERY p x ∧ LENGTH x = m

⊢ ∀p x. lift_option p x ⇔ case x of NONE => T | SOME y => p y

⊢ ∀p1 p2 x. lift_prod p1 p2 x ⇔ p1 (FST x) ∧ p2 (SND x)

⊢ ∀p1 p2 x. lift_sum p1 p2 x ⇔ case x of INL x1 => p1 x1 | INR x2 => p2 x2

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0'.
           ∀ $var$('tree') $var$('@temp@ind_typeEncode0list').
             (∀a0'.
                (∃a0 a1.
                   a0' =
                   (λa0 a1.
                        ind_type$CONSTR 0 a0
                          (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) a0 a1 ∧
                   $var$('@temp@ind_typeEncode0list') a1) ⇒
                $var$('tree') a0') ∧
             (∀a1'.
                a1' = ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ∨
                (∃a0 a1.
                   a1' =
                   (λa0 a1.
                        ind_type$CONSTR (SUC (SUC 0)) ARB
                          (ind_type$FCONS a0
                             (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))) a0
                     a1 ∧ $var$('tree') a0 ∧
                   $var$('@temp@ind_typeEncode0list') a1) ⇒
                $var$('@temp@ind_typeEncode0list') a1') ⇒
             $var$('tree') a0') rep

⊢ ∀a0 a1 f. tree_CASE (Node a0 a1) f = f a0 a1

⊢ (∀f a0 a1. tree_size f (Node a0 a1) = 1 + (f a0 + tree1_size f a1)) ∧
  (∀f. tree1_size f [] = 0) ∧
  ∀f a0 a1. tree1_size f (a0::a1) = 1 + (tree_size f a0 + tree1_size f a1)

⊢ ∀p e. wf_encoder p e ⇔ ∀x y. p x ∧ p y ∧ e y ≼ e x ⇒ x = y

⊢ ∀m p. wf_pred_bnum m p ⇔ wf_pred p ∧ ∀x. p x ⇒ x < 2 ** m

⊢ ∀p. wf_pred p ⇔ ∃x. p x

⊢ ∀a b c d. biprefix (a ⧺ b) (c ⧺ d) ⇒ biprefix a c

⊢ ∀a b c. biprefix (a ⧺ b) (a ⧺ c) ⇔ biprefix b c

⊢ ∀a b c d. biprefix (a::b) (c::d) ⇔ a = c ∧ biprefix b d

⊢ ∀x. biprefix x x

⊢ ∀x y. biprefix x y ⇒ biprefix y x

⊢ DATATYPE (tree Node)

⊢ (∀e l. encode_blist 0 e l = []) ∧
  (∀m e l.
     encode_blist (NUMERAL (BIT1 m)) e l =
     e (HD l) ⧺ encode_blist (NUMERAL (BIT1 m) − 1) e (TL l)) ∧
  ∀m e l.
    encode_blist (NUMERAL (BIT2 m)) e l =
    e (HD l) ⧺ encode_blist (NUMERAL (BIT1 m)) e (TL l)

⊢ (∀n. encode_bnum 0 n = []) ∧
  (∀m n.
     encode_bnum (NUMERAL (BIT1 m)) n =
     ¬EVEN n::encode_bnum (NUMERAL (BIT1 m) − 1) (n DIV 2)) ∧
  ∀m n.
    encode_bnum (NUMERAL (BIT2 m)) n =
    ¬EVEN n::encode_bnum (NUMERAL (BIT1 m)) (n DIV 2)

⊢ ∀m x y.
    x < 2 ** m ∧ y < 2 ** m ∧ encode_bnum m x = encode_bnum m y ⇒ x = y

⊢ ∀m n. LENGTH (encode_bnum m n) = m

⊢ ∀l1 l2 f1 f2.
    l1 = l2 ∧ (∀x. MEM x l2 ⇒ f1 x = f2 x) ⇒
    encode_list f1 l1 = encode_list f2 l2

⊢ ∀n. encode_num n =
      if n = 0 then [T; T]
      else if EVEN n then F::encode_num ((n − 2) DIV 2)
      else T::F::encode_num ((n − 1) DIV 2)

⊢ ∀P. (∀n. (n ≠ 0 ∧ EVEN n ⇒ P ((n − 2) DIV 2)) ∧
           (n ≠ 0 ∧ ¬EVEN n ⇒ P ((n − 1) DIV 2)) ⇒
           P n) ⇒
      ∀v. P v

⊢ ∀xb yb p. encode_prod xb yb p = xb (FST p) ⧺ yb (SND p)

⊢ ∀ts e a. encode_tree e (Node a ts) = e a ⧺ encode_list (encode_tree e) ts

⊢ ∀P. (∀e a ts. (∀a'. MEM a' ts ⇒ P e a') ⇒ P e (Node a ts)) ⇒
      ∀v v1. P v v1

⊢ ∀n p h t. lift_blist (SUC n) p (h::t) ⇔ p h ∧ lift_blist n p t

⊢ ∀ts p a. lift_tree p (Node a ts) ⇔ p a ∧ EVERY (lift_tree p) ts

⊢ ∀P. (∀p a ts. (∀a'. MEM a' ts ⇒ P p a') ⇒ P p (Node a ts)) ⇒
      ∀v v1. P v v1

⊢ ∀a0 a1 a0' a1'. Node a0 a1 = Node a0' a1' ⇔ a0 = a0' ∧ a1 = a1'

⊢ ∀f0 f1 f2. ∃fn0 fn1.
    (∀a0 a1. fn0 (Node a0 a1) = f0 a0 a1 (fn1 a1)) ∧ fn1 [] = f1 ∧
    ∀a0 a1. fn1 (a0::a1) = f2 a0 a1 (fn0 a0) (fn1 a1)

⊢ ∀M M' f.
    M = M' ∧ (∀a0 a1. M' = Node a0 a1 ⇒ f a0 a1 = f' a0 a1) ⇒
    tree_CASE M f = tree_CASE M' f'

⊢ tree_CASE x f = v ⇔ ∃a l. x = Node a l ∧ f a l = v

⊢ ∀p. (∀a ts. (∀t. MEM t ts ⇒ p t) ⇒ p (Node a ts)) ⇒ ∀t. p t

⊢ ∀P0 P1.
    (∀l. P1 l ⇒ ∀a. P0 (Node a l)) ∧ P1 [] ∧
    (∀t l. P0 t ∧ P1 l ⇒ P1 (t::l)) ⇒
    (∀t. P0 t) ∧ ∀l. P1 l

⊢ ∀tt. ∃a l. tt = Node a l

⊢ ∀m p e. wf_encoder p e ⇒ wf_encoder (lift_blist m p) (encode_blist m e)

⊢ ∀m p. wf_pred_bnum m p ⇒ wf_encoder p (encode_bnum m)

⊢ ∀m p. wf_encoder p (encode_bnum m) ⇔ collision_free m p

⊢ ∀p. wf_encoder p encode_bool

⊢ ∀p e. wf_encoder p e ⇒ wf_encoder (EVERY p) (encode_list e)

⊢ ∀p. wf_encoder p encode_num

⊢ ∀p e. wf_encoder p e ⇒ wf_encoder (lift_option p) (encode_option e)

⊢ ∀p1 p2 e1 e2.
    wf_encoder p1 e1 ∧ wf_encoder p2 e2 ⇒
    wf_encoder (lift_prod p1 p2) (encode_prod e1 e2)

⊢ ∀p1 p2 e1 e2.
    wf_encoder p1 e1 ∧ wf_encoder p2 e2 ⇒
    wf_encoder (lift_sum p1 p2) (encode_sum e1 e2)

⊢ ∀p e. wf_encoder p e ⇒ wf_encoder (lift_tree p) (encode_tree e)

⊢ ∀p. wf_encoder p encode_unit

⊢ wf_encoder p e ⇔ ∀x y. p x ∧ p y ∧ biprefix (e x) (e y) ⇒ x = y

⊢ ∀p e f. wf_encoder p e ∧ (∀x. p x ⇒ e x = f x) ⇒ wf_encoder p f

⊢ ∀p e. wf_encoder (K T) e ⇒ wf_encoder p e

⊢ ∀m p. wf_pred_bnum m p ⇒ collision_free m p

⊢ ∀m. wf_pred_bnum m (λx. x < 2 ** m)