Theory string_num

⊢ ∀n. n2nsum n = if ODD n then INL (n DIV 2) else INR (n DIV 2)

⊢ n2s =
  WFREC
    (@R. WF R ∧
         ∀n r0 r.
           n ≠ 0 ∧ r0 = n MOD 256 ∧ r = (if r0 = 0 then 256 else r0) ⇒
           R ((n − r) DIV 256) n)
    (λn2s a.
         I
           (if a = 0 then ""
            else
              (let
                 r0 = a MOD 256;
                 r = if r0 = 0 then 256 else r0;
                 s0 = n2s ((a − r) DIV 256)
               in
                 STRING (CHR (r − 1)) s0)))

⊢ (∀n. nsum2n (INL n) = 2 * n + 1) ∧ ∀n. nsum2n (INR n) = 2 * n

⊢ s2n "" = 0 ∧ ∀c s. s2n (STRING c s) = s2n s * 256 + ORD c + 1

⊢ ∀s. s2ssum s = SUM_MAP n2s n2s (n2nsum (s2n s))

⊢ ∀sm. ssum2s sm = n2s (nsum2n (SUM_MAP s2n s2n sm))

⊢ n2nsum (nsum2n ns) = ns

⊢ n2s x = n2s y ⇔ x = y

⊢ ∀n. n2s n =
      if n = 0 then ""
      else
        (let
           r0 = n MOD 256;
           r = if r0 = 0 then 256 else r0;
           s0 = n2s ((n − r) DIV 256)
         in
           STRING (CHR (r − 1)) s0)

⊢ ∀P. (∀n. (∀r0 r.
              n ≠ 0 ∧ r0 = n MOD 256 ∧ r = (if r0 = 0 then 256 else r0) ⇒
              P ((n − r) DIV 256)) ⇒
           P n) ⇒
      ∀v. P v

⊢ ∀s. ∃n. s = n2s n

⊢ n2s (s2n s) = s

⊢ nsum2n (n2nsum n) = n

⊢ s2n x = s2n y ⇔ x = y

⊢ ∀n. s2n (n2s n) = n

⊢ ∀n. ∃s. n = s2n s

⊢ s2ssum (ssum2s sm) = sm

⊢ ssum2s (s2ssum s) = s