Theory numposrep

⊢ (∀m a. BOOLIFY 0 m a = a) ∧
  ∀n m a. BOOLIFY (SUC n) m a = BOOLIFY n (DIV2 m) (ODD m::a)

⊢ numposrep$l2n2 = l2n 2

⊢ (∀b. l2n b [] = 0) ∧ ∀b h t. l2n b (h::t) = h MOD b + b * l2n b t

⊢ num_from_bin_list = l2n 2 ∘ REVERSE

⊢ num_from_dec_list = l2n 10 ∘ REVERSE

⊢ num_from_hex_list = l2n 16 ∘ REVERSE

⊢ num_from_oct_list = l2n 8 ∘ REVERSE

⊢ num_to_bin_list = REVERSE ∘ n2l 2

⊢ num_to_dec_list = REVERSE ∘ n2l 10

⊢ num_to_hex_list = REVERSE ∘ n2l 16

⊢ num_to_oct_list = REVERSE ∘ n2l 8

⊢ LENGTH l1 = LENGTH l2 ⇒
  BITWISE (LENGTH l1) op (l2n 2 l1) (l2n 2 l2) =
  l2n 2 (MAP2 (λx y. bool_to_bit (op (ODD x) (ODD y))) l1 l2)

⊢ ∀x l. EVERY ($> 2) l ⇒ (BIT x (l2n 2 l) ⇔ x < LENGTH l ∧ l❲x❳ = 1)

⊢ ∀x l.
    EVERY ($> 2) l ∧ x < LENGTH l ⇒
    (BIT x (num_from_bin_list l) ⇔ (REVERSE l)❲x❳ = 1)

⊢ (∀m a. BOOLIFY 0 m a = a) ∧
  (∀n m a.
     BOOLIFY <..num comp'n..> m a =
     BOOLIFY (<..num comp'n..> − 1) (DIV2 m) (ODD m::a)) ∧
  ∀n m a.
    BOOLIFY <..num comp'n..> m a =
    BOOLIFY <..num comp'n..> (DIV2 m) (ODD m::a)

⊢ ∀b x n. 1 < b ∧ x < LENGTH (n2l b n) ⇒ (n2l b n)❲x❳ = n DIV b ** x MOD b

⊢ ∀x n.
    x < LENGTH (num_to_bin_list n) ⇒
    (REVERSE (num_to_bin_list n))❲x❳ = BITV n x

⊢ ∀b l.
    1 < b ∧ EVERY ($> b) l ∧ l2n b l ≠ 0 ⇒ SUC (LOG b (l2n b l)) ≤ LENGTH l

⊢ ∀b n. 1 < b ⇒ LENGTH (n2l b n) = if n = 0 then 1 else SUC (LOG b n)

⊢ ∀b. 1 < b ⇒
      ∀l. l ≠ [] ∧ 0 < LAST l ∧ EVERY ($> b) l ⇒
          LOG b (l2n b l) = PRE (LENGTH l)

⊢ ∀b l.
    1 < b ∧ EXISTS (λy. 0 ≠ y) l ∧ EVERY ($> b) l ⇒
    LOG b (l2n b l) = PRE (LENGTH (dropWhile ($= 0) (REVERSE l)))

⊢ ∀b l1 l2.
    1 < b ∧ EVERY ($> b) l1 ∧ EVERY ($> b) l2 ⇒
    (l2n b (l1 ⧺ [1]) = l2n b (l2 ⧺ [1]) ⇔ l1 = l2)

⊢ ∀ls.
    EVERY ($> 2) ls ⇒
    l2n 2 (MAP (λx. 1 − x) ls) = 2 ** LENGTH ls − SUC (l2n 2 ls)

⊢ (∀t. l2n 2 (0::t) = <..num comp'n..> ) ∧
  (∀t. l2n 2 (1::t) = <..num comp'n..> ) ∧ numposrep$l2n2 [] = ZERO ∧
  (∀t. numposrep$l2n2 (0::t) = <..num comp'n..> ) ∧
  ∀t. numposrep$l2n2 (1::t) = <..num comp'n..>

⊢ ∀b l1 l2. l2n b (l1 ⧺ l2) = l2n b l1 + b ** LENGTH l1 * l2n b l2

⊢ ∀b l x.
    1 < b ∧ EVERY ($> b) l ∧ x < LENGTH l ⇒ l2n b l DIV b ** x MOD b = l❲x❳

⊢ 0 < b ⇒ l2n b (PAD_RIGHT 0 h ls) = l2n b ls

⊢ ∀b ls. 0 < b ⇒ l2n b (SNOC 0 ls) = l2n b ls

⊢ ∀b ls. 0 < b ⇒ l2n b (REVERSE (dropWhile ($= 0) (REVERSE ls))) = l2n b ls

⊢ ∀b. 0 < b ⇒ ∀l. l2n b l = 0 ⇔ EVERY ($= 0 ∘ flip $MOD b) l

⊢ ∀l b. 0 < b ⇒ l2n b l < b ** LENGTH l

⊢ 0 < b ⇒
  ∀ls. l2n b ls = b ** LENGTH ls − 1 ⇔ EVERY ($= (b − 1) ∘ flip $MOD b) ls

⊢ ∀b n. 1 < b ⇒ l2n b (n2l b n) = n

⊢ (∀p. l2n (2 ** p) [] = 0) ∧
  ∀p h t.
    l2n (2 ** p) (h::t) = MOD_2EXP p h + TIMES_2EXP p (l2n (2 ** p) t)

⊢ n2lA A f 10 n =
  if n < 10 then f n::A else n2lA (f (n MOD 10)::A) f 10 (n DIV 10)

⊢ ∀n f b A.
    n2lA A f b n =
    if n < b ∨ b < 2 then f (n MOD b)::A
    else n2lA (f (n MOD b)::A) f b (n DIV b)

⊢ ∀P. (∀A f b n.
         (¬(n < b ∨ b < 2) ⇒ P (f (n MOD b)::A) f b (n DIV b)) ⇒ P A f b n) ⇒
      ∀v v1 v2 v3. P v v1 v2 v3

⊢ ∀A n. n2lA A f b n = MAP f (REVERSE (n2l b n)) ⧺ A

⊢ ∀b n. 0 < b ⇒ EVERY ($> b) (n2l b n)

⊢ ∀n b.
    n2l b n = if n < b ∨ b < 2 then [n MOD b] else n MOD b::n2l b (n DIV b)

⊢ ∀P. (∀b n. (¬(n < b ∨ b < 2) ⇒ P b (n DIV b)) ⇒ P b n) ⇒ ∀v v1. P v v1

⊢ ∀b l.
    1 < b ∧ EVERY ($> b) l ⇒
    n2l b (l2n b l) =
    if l2n b l = 0 then [0] else TAKE (SUC (LOG b (l2n b l))) l

⊢ n2l b n = REVERSE (n2lA [] I b n)

⊢ ∀p n.
    0 < p ⇒
    n2l (2 ** p) n =
    (let
       (q,r) = DIVMOD_2EXP p n
     in
       if q = 0 then [r] else r::n2l (2 ** p) q)

⊢ num_from_bin_list ∘ num_to_bin_list = I

⊢ num_from_dec_list ∘ num_to_dec_list = I

⊢ num_from_hex_list ∘ num_to_hex_list = I

⊢ num_from_oct_list ∘ num_to_oct_list = I