Package hol-string: HOL string theories

Information

namehol-string
version1.0
descriptionHOL string theories
authorHOL developers <hol-developers@lists.sourceforge.net>
licenseMIT
checksumf17086fdeef36a8441fe738fcfbd94a050e20031
requiresbase
hol-base
showData.Bool
Data.List
Data.Option
Data.Pair
Function
HOL4
Number.Natural
Relation

Files

Defined Type Operator

Defined Constants

Theorems

string.EXPLODE (string.IMPLODE cs) = cs

string.IMPLODE (string.EXPLODE s) = s

string_num.n2s (string_num.s2n s) = s

ASCIInumbers.num_from_bin_string ASCIInumbers.num_to_bin_string = id

ASCIInumbers.num_from_dec_string ASCIInumbers.num_to_dec_string = id

ASCIInumbers.num_from_hex_string ASCIInumbers.num_to_hex_string = id

ASCIInumbers.num_from_oct_string ASCIInumbers.num_to_oct_string = id

c. string.char_size c = 0

s. ¬string.string_lt s s

ASCIInumbers.num_to_bin_string =
  ASCIInumbers.n2s (arithmetic.BIT2 0) ASCIInumbers.HEX

ASCIInumbers.num_from_bin_string =
  ASCIInumbers.s2n (arithmetic.BIT2 0) ASCIInumbers.UNHEX

length s = length (string.EXPLODE s)

string.TOCHAR (c :: []) = c

a. string.CHR (string.ORD a) = a

n. string_num.s2n (string_num.n2s n) = n

n.
    ASCIInumbers.num_from_dec_string (ASCIInumbers.num_to_dec_string n) = n

c. n. c = string.CHR n

%%genvar%%1436. s. %%genvar%%1436 = string_num.s2n s

%%genvar%%1433. n. %%genvar%%1433 = string_num.n2s n

%%genvar%%1503. s. %%genvar%%1503 = string.EXPLODE s

%%genvar%%1507. cs. %%genvar%%1507 = string.IMPLODE cs

s1 @ s2 = s1 @ s2

c. string.STR c = c :: []

ASCIInumbers.num_to_dec_string =
  ASCIInumbers.n2s (arithmetic.BIT2 (arithmetic.BIT2 1)) ASCIInumbers.HEX

ASCIInumbers.num_to_oct_string =
  ASCIInumbers.n2s (arithmetic.BIT2 3) ASCIInumbers.HEX

ASCIInumbers.num_from_dec_string =
  ASCIInumbers.s2n (arithmetic.BIT2 (arithmetic.BIT2 1)) ASCIInumbers.UNHEX

ASCIInumbers.num_from_oct_string =
  ASCIInumbers.s2n (arithmetic.BIT2 3) ASCIInumbers.UNHEX

clist. string.IMPLODE clist = list.FOLDR (::) [] clist

ASCIInumbers.num_to_hex_string =
  ASCIInumbers.n2s (arithmetic.BIT2 7) ASCIInumbers.HEX

ASCIInumbers.num_from_hex_string =
  ASCIInumbers.s2n (arithmetic.BIT2 7) ASCIInumbers.UNHEX

string.EXPLODE s = s string.IMPLODE s = s

string_num.s2n x = string_num.s2n y x = y

string.EXPLODE s1 = string.EXPLODE s2 s1 = s2

string.IMPLODE cs1 = string.IMPLODE cs2 cs1 = cs2

string_num.n2s x = string_num.n2s y x = y

c. string.isAlpha c string.isLower c string.isUpper c

c. string.isAlphaNum c string.isAlpha c string.isDigit c

c. string.isDigit c ASCIInumbers.HEX (ASCIInumbers.UNHEX c) = c

l. length l = 0 l = []

s1 s2. string.string_ge s1 s2 string.string_le s2 s1

s1 s2. string.string_gt s1 s2 string.string_lt s2 s1

c. string.isGraph c string.isPrint c ¬string.isSpace c

c. string.isPunct c string.isGraph c ¬string.isAlphaNum c

c.
    string.isHexDigit c
    ASCIInumbers.HEX (ASCIInumbers.UNHEX c) = string.toUpper c

s n. string.SUB (s, n) = list.EL n s

s t. ¬(string.string_lt s t string.string_lt t s)

x x1. string.string_lt x x1 string.string_lt_tupled (x, x1)

x x1. string.FIELDS x x1 = string.FIELDS_tupled (x, x1)

x x1. string.TOKENS x x1 = string.TOKENS_tupled (x, x1)

f s. string.TRANSLATE f s = concat (map f s)

a a'. a = a' string.ORD a = string.ORD a'

a b. string.char_ge a b string.ORD a string.ORD b

a b. string.char_gt a b string.ORD a > string.ORD b

a b. string.char_le a b string.ORD a string.ORD b

a b. string.char_lt a b string.ORD a < string.ORD b

a a'. string.ORD a = string.ORD a' a = a'

n m.
    ASCIInumbers.num_to_dec_string n = ASCIInumbers.num_to_dec_string m
    n = m

s1 s2. s1 @ s2 = list.FOLDR (::) s2 (string.EXPLODE s1)

ASCIInumbers.s2n b f s =
  numposrep.l2n b (map f (reverse (string.EXPLODE s)))

ASCIInumbers.n2s b f n =
  string.IMPLODE (reverse (map f (numposrep.n2l b n)))

l1 l2. length (l1 @ l2) = length l1 + length l2

c. string.ORD c < arithmetic.BIT2 127

s1 s2. list.isPREFIX s1 s2 s3. s2 = s1 @ s3

s1 s2. string.string_le s1 s2 s1 = s2 string.string_lt s1 s2

s t. s = t string.string_lt s t string.string_lt t s

n. n < arithmetic.BIT2 7 ASCIInumbers.UNHEX (ASCIInumbers.HEX n) = n

rep. bool.TYPE_DEFINITION (λn. n < arithmetic.BIT2 127) rep

c. string.isAscii c string.ORD c 127

b f s. ASCIInumbers.s2n b f s = numposrep.l2n b (map f (reverse s))

b f n. ASCIInumbers.n2s b f n = reverse (map f (numposrep.n2l b n))

s i n. string.SUBSTRING (s, i, n) = rich_list.SEG n i s

l1 l2 l3. l1 @ l2 @ l3 = (l1 @ l2) @ l3

s1 s2 s3.
    string.string_lt s1 s2 string.string_lt s2 s3
    string.string_lt s1 s3

s c. ¬(c :: s = s) ¬(s = c :: s)

l1 l2. l1 @ l2 = [] l1 = [] l2 = []

s.
    string.EXPLODE s =
    option.option_CASE (string.DEST_STRING s) []
      (λv. pair.pair_CASE v (λc t. c :: string.EXPLODE t))

length [] = 0 h t. length (h :: t) = suc (length t)

string.EXPLODE [] = []
  c s. string.EXPLODE (c :: s) = c :: string.EXPLODE s

string.IMPLODE [] = []
  c cs. string.IMPLODE (c :: cs) = c :: string.IMPLODE cs

string.DEST_STRING [] = none
  c rst. string.DEST_STRING (c :: rst) = some (c, rst)

(string.EXPLODE s = [] s = []) ([] = string.EXPLODE s s = [])

(string.IMPLODE l = [] l = []) ([] = string.IMPLODE l l = [])

n m s.
    s @ ASCIInumbers.num_to_dec_string n =
    s @ ASCIInumbers.num_to_dec_string m n = m

s.
    ASCIInumbers.fromDecString s =
    if ¬(s = []) all string.isDigit s then
      some (ASCIInumbers.num_from_dec_string s)
    else none

s.
    ASCIInumbers.fromHexString s =
    if ¬(s = []) all string.isHexDigit s then
      some (ASCIInumbers.num_from_hex_string s)
    else none

string.TOCHAR =
  relation.WFREC (select R. wellFounded R)
    (λTOCHAR a.
       list.list_CASE a bool.ARB
         (λc v1. list.list_CASE v1 (id c) (λv2 v3. bool.ARB)))

c.
    string.toLower c =
    if string.isUpper c then string.CHR (string.ORD c + arithmetic.BIT2 15)
    else c

c.
    string.toUpper c =
    if string.isLower c then
      string.CHR (arithmetic.- (string.ORD c) (arithmetic.BIT2 15))
    else c

r. r < arithmetic.BIT2 127 string.ORD (string.CHR r) = r

r. r < arithmetic.BIT2 127 string.ORD (string.CHR r) = r

a. r. a = string.CHR r r < arithmetic.BIT2 127

r. r < arithmetic.BIT2 127 a. r = string.ORD a

s s1. (s = s @ s1 s1 = []) (s = s1 @ s s1 = [])

P. (n. n < arithmetic.BIT2 127 P (string.CHR n)) c. P c

[] @ s = s s @ [] = s (c :: s1) @ s2 = c :: s1 @ s2

(l. [] @ l = l) l1 l2 h. (h :: l1) @ l2 = h :: l1 @ l2

c.
    string.isDigit c
    arithmetic.BIT2 (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
    string.ORD c
    string.ORD c
    bit1 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))))

n.
    string.ORD (string.CHR n) =
    if n < arithmetic.BIT2 127 then n
    else combin.FAIL string.ORD > 255 (string.CHR n)

s.
    (string.DEST_STRING s = none s = [])
    (string.DEST_STRING s = some (c, t) s = c :: t)

x n.
    x < length (ASCIInumbers.num_to_bin_string n)
    string.SUB (ASCIInumbers.num_to_bin_string n, x) =
    ASCIInumbers.HEX
      (bit.BITV n
         (prim_rec.PRE
            (arithmetic.- (length (ASCIInumbers.num_to_bin_string n)) x)))

c.
    string.isCntrl c
    string.ORD c < arithmetic.BIT2 15 127 string.ORD c

c.
    string.isLower c
    bit1 (arithmetic.BIT2 (bit1 (bit1 (bit1 (arithmetic.BIT2 0)))))
    string.ORD c
    string.ORD c
    arithmetic.BIT2
      (arithmetic.BIT2
         (bit1 (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0)))))

c.
    string.isPrint c
    arithmetic.BIT2 15 string.ORD c string.ORD c < 127

c.
    string.isUpper c
    bit1 (arithmetic.BIT2 15) string.ORD c
    string.ORD c
    arithmetic.BIT2
      (arithmetic.BIT2 (bit1 (arithmetic.BIT2 (arithmetic.BIT2 1))))

P. (c. P (c :: [])) P [] (v6 v4 v5. P (v6 :: v4 :: v5)) s. P s

(a. string.CHR (string.ORD a) = a)
  r.
    (let n r in n < arithmetic.BIT2 127) string.ORD (string.CHR r) = r

c.
    string.isSpace c
    string.ORD c = arithmetic.BIT2 15
    bit1 (arithmetic.BIT2 1) string.ORD c
    string.ORD c bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))

string_num.s2n [] = 0
  c s.
    string_num.s2n (c :: s) =
    string_num.s2n s * arithmetic.BIT2 127 + string.ORD c + 1

string.EXTRACT (s, i, none) =
  string.SUBSTRING (s, i, arithmetic.- (length s) i)
  string.EXTRACT (s, i, some n) = string.SUBSTRING (s, i, n)

c s l.
    (c :: s = string.IMPLODE l l = c :: string.EXPLODE s)
    (string.IMPLODE l = c :: s l = c :: string.EXPLODE s)

s h t.
    (h :: t = string.EXPLODE s s = h :: string.IMPLODE t)
    (string.EXPLODE s = h :: t s = h :: string.IMPLODE t)

c2n n2c b n.
    1 < b (x. x < b c2n (n2c x) = x)
    ASCIInumbers.s2n b c2n (ASCIInumbers.n2s b n2c n) = n

(l1 l2 l3. l1 @ l2 = l1 @ l3 l2 = l3)
  l1 l2 l3. l2 @ l1 = l3 @ l1 l2 = l3

x s.
    all ((>) (arithmetic.BIT2 0) ASCIInumbers.UNHEX) s x < length s
    (bit.BIT x (ASCIInumbers.num_from_bin_string s)
     ASCIInumbers.UNHEX
       (string.SUB (s, prim_rec.PRE (arithmetic.- (length s) x))) = 1)

string.EXTRACT =
  relation.WFREC (select R. wellFounded R)
    (λEXTRACT a.
       pair.pair_CASE a
         (λs v1.
            pair.pair_CASE v1
              (λi v3.
                 option.option_CASE v3
                   (id
                      (string.SUBSTRING (s, i, arithmetic.- (length s) i)))
                   (λn. id (string.SUBSTRING (s, i, n))))))

s1 s2.
    list.isPREFIX s1 s2
    pair.pair_CASE (string.DEST_STRING s1, string.DEST_STRING s2)
      (λv v1.
         option.option_CASE v
           (λv2.
              option.option_CASE v1
                (λv3.
                   pair.pair_CASE v3
                     (λc2 t2.
                        pair.pair_CASE v2
                          (λc1 t1. c1 = c2 list.isPREFIX t1 t2)))))

P.
    (s i. P (s, i, none)) (s i n. P (s, i, some n))
    v v1 v2. P (v, v1, v2)

r r'.
    r < arithmetic.BIT2 127 r' < arithmetic.BIT2 127
    (string.CHR r = string.CHR r' r = r')

s.
    ASCIInumbers.fromBinString s =
    if ¬(s = [])
       all
         (λc.
            c =
            string.CHR
              (arithmetic.BIT2 (bit1 (bit1 (bit1 (arithmetic.BIT2 0)))))
            c =
            string.CHR
              (bit1 (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))))) s
    then some (ASCIInumbers.num_from_bin_string s)
    else none

(P. string.TOKENS P [] = [])
  t h P.
    string.TOKENS P (h :: t) =
    bool.LET
      (pair.UNCURRY
         (λl r.
            if null l then string.TOKENS P (tail r)
            else l :: string.TOKENS P r)) (rich_list.SPLITP P (h :: t))

P.
    (s1 s2.
       (c t1 t2.
          string.DEST_STRING s1 = some (c, t1)
          string.DEST_STRING s2 = some (c, t2) P t1 t2) P s1 s2)
    v v1. P v v1

P.
    (s. P s []) (c s. P [] (c :: s))
    (c1 s1 c2 s2. P s1 s2 P (c1 :: s1) (c2 :: s2)) v v1. P v v1

(s. string.string_lt s [] )
  (s c. string.string_lt [] (c :: s) )
  s2 s1 c2 c1.
    string.string_lt (c1 :: s1) (c2 :: s2)
    string.char_lt c1 c2 c1 = c2 string.string_lt s1 s2

(P. string.FIELDS P [] = [] :: [])
  t h P.
    string.FIELDS P (h :: t) =
    bool.LET
      (pair.UNCURRY
         (λl r.
            if null l then [] :: string.FIELDS P (tail r)
            else if null r then l :: []
            else l :: string.FIELDS P (tail r)))
      (rich_list.SPLITP P (h :: t))

c2n n2c b s.
    1 < b all ((>) b c2n) s
    ASCIInumbers.n2s b n2c (ASCIInumbers.s2n b c2n s) =
    if ASCIInumbers.s2n b c2n s = 0 then n2c 0 :: []
    else
      map (n2c c2n)
        (rich_list.LASTN (suc (logroot.LOG b (ASCIInumbers.s2n b c2n s)))
           s)

string.string_lt_tupled =
  relation.WFREC
    (select R.
       wellFounded R c2 c1 s2 s1. R (s1, s2) (c1 :: s1, c2 :: s2))
    (λstring_lt_tupled a.
       pair.pair_CASE a
         (λs v1.
            list.list_CASE v1 (id )
              (λc s'.
                 list.list_CASE s (id )
                   (λc1 s1.
                      id
                        (string.char_lt c1 c
                         c1 = c string_lt_tupled (s1, s'))))))

n.
    string_num.n2s n =
    if n = 0 then []
    else
      bool.LET
        (λr0.
           bool.LET
             (λr.
                bool.LET (λs0. string.CHR (arithmetic.- r 1) :: s0)
                  (string_num.n2s
                     (arithmetic.- n r div arithmetic.BIT2 127)))
             (if r0 = 0 then arithmetic.BIT2 127 else r0))
        (n mod arithmetic.BIT2 127)

P.
    (n.
       (r0 r.
          ¬(n = 0) r0 = n mod arithmetic.BIT2 127
          r = (if r0 = 0 then arithmetic.BIT2 127 else r0)
          P (arithmetic.- n r div arithmetic.BIT2 127)) P n) n. P n

P'.
    (P. P' P [])
    (P h t.
       (l r.
          (l, r) = rich_list.SPLITP P (h :: t) null l P' P (tail r))
       (l r. (l, r) = rich_list.SPLITP P (h :: t) ¬null l P' P r)
       P' P (h :: t)) v v1. P' v v1

c.
    string.isHexDigit c
    arithmetic.BIT2 (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))
    string.ORD c
    string.ORD c
    bit1 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))))
    bit1 (arithmetic.BIT2 (bit1 (bit1 (bit1 (arithmetic.BIT2 0)))))
    string.ORD c
    string.ORD c
    arithmetic.BIT2
      (arithmetic.BIT2
         (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))))
    bit1 (arithmetic.BIT2 15) string.ORD c
    string.ORD c arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 7))

P'.
    (P. P' P [])
    (P h t.
       (l r.
          (l, r) = rich_list.SPLITP P (h :: t) null l P' P (tail r))
       (l r.
          (l, r) = rich_list.SPLITP P (h :: t) ¬null l ¬null r
          P' P (tail r)) P' P (h :: t)) v v1. P' v v1

P.
    P 0 P 1 P (arithmetic.BIT2 0) P 3 P (arithmetic.BIT2 1)
    P (bit1 (arithmetic.BIT2 0))
    P (arithmetic.BIT2 (arithmetic.BIT2 0)) P 7 P (arithmetic.BIT2 3)
    P (bit1 (arithmetic.BIT2 1))
    P (arithmetic.BIT2 (arithmetic.BIT2 1))
    P (bit1 (bit1 (arithmetic.BIT2 0)))
    P (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))
    P (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)))
    P (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0))) P 15
    (v18. P v18) v18. P v18

string.TOKENS_tupled =
  relation.WFREC
    (select R.
       wellFounded R
       (t h P l r.
          (l, r) = rich_list.SPLITP P (h :: t) null l
          R (P, tail r) (P, h :: t))
       t h P l r.
         (l, r) = rich_list.SPLITP P (h :: t) ¬null l
         R (P, r) (P, h :: t))
    (λTOKENS_tupled a.
       pair.pair_CASE a
         (λP v1.
            list.list_CASE v1 (id [])
              (λh t.
                 id
                   (bool.LET
                      (pair.UNCURRY
                         (λl r.
                            if null l then TOKENS_tupled (P, tail r)
                            else l :: TOKENS_tupled (P, r)))
                      (rich_list.SPLITP P (h :: t))))))

string.FIELDS_tupled =
  relation.WFREC
    (select R.
       wellFounded R
       (t h P l r.
          (l, r) = rich_list.SPLITP P (h :: t) null l
          R (P, tail r) (P, h :: t))
       t h P l r.
         (l, r) = rich_list.SPLITP P (h :: t) ¬null l ¬null r
         R (P, tail r) (P, h :: t))
    (λFIELDS_tupled a.
       pair.pair_CASE a
         (λP v1.
            list.list_CASE v1 (id ([] :: []))
              (λh t.
                 id
                   (bool.LET
                      (pair.UNCURRY
                         (λl r.
                            if null l then [] :: FIELDS_tupled (P, tail r)
                            else if null r then l :: []
                            else l :: FIELDS_tupled (P, tail r)))
                      (rich_list.SPLITP P (h :: t))))))

string_num.n2s =
  relation.WFREC
    (select R.
       wellFounded R
       n r0 r.
         ¬(n = 0) r0 = n mod arithmetic.BIT2 127
         r = (if r0 = 0 then arithmetic.BIT2 127 else r0)
         R (arithmetic.- n r div arithmetic.BIT2 127) n)
    (λn2s n.
       id
         (if n = 0 then []
          else
            bool.LET
              (λr0.
                 bool.LET
                   (λr.
                      bool.LET (λs0. string.CHR (arithmetic.- r 1) :: s0)
                        (n2s (arithmetic.- n r div arithmetic.BIT2 127)))
                   (if r0 = 0 then arithmetic.BIT2 127 else r0))
              (n mod arithmetic.BIT2 127)))

ASCIInumbers.HEX 0 =
  string.CHR (arithmetic.BIT2 (bit1 (bit1 (bit1 (arithmetic.BIT2 0)))))
  ASCIInumbers.HEX 1 =
  string.CHR (bit1 (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))))
  ASCIInumbers.HEX (arithmetic.BIT2 0) =
  string.CHR
    (arithmetic.BIT2 (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))))
  ASCIInumbers.HEX 3 =
  string.CHR (bit1 (bit1 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))))
  ASCIInumbers.HEX (arithmetic.BIT2 1) =
  string.CHR
    (arithmetic.BIT2 (bit1 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))))
  ASCIInumbers.HEX (bit1 (arithmetic.BIT2 0)) =
  string.CHR
    (bit1 (arithmetic.BIT2 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))))
  ASCIInumbers.HEX (arithmetic.BIT2 (arithmetic.BIT2 0)) =
  string.CHR
    (arithmetic.BIT2
       (arithmetic.BIT2 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))))
  ASCIInumbers.HEX 7 =
  string.CHR (bit1 (bit1 (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)))))
  ASCIInumbers.HEX (arithmetic.BIT2 3) =
  string.CHR
    (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)))))
  ASCIInumbers.HEX (bit1 (arithmetic.BIT2 1)) =
  string.CHR
    (bit1 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)))))
  ASCIInumbers.HEX (arithmetic.BIT2 (arithmetic.BIT2 1)) =
  string.CHR (bit1 (arithmetic.BIT2 15))
  ASCIInumbers.HEX (bit1 (bit1 (arithmetic.BIT2 0))) =
  string.CHR (arithmetic.BIT2 (arithmetic.BIT2 15))
  ASCIInumbers.HEX (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))) =
  string.CHR (bit1 (bit1 (arithmetic.BIT2 7)))
  ASCIInumbers.HEX (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))) =
  string.CHR (arithmetic.BIT2 (bit1 (arithmetic.BIT2 7)))
  ASCIInumbers.HEX
    (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0))) =
  string.CHR (bit1 (arithmetic.BIT2 (arithmetic.BIT2 7)))
  ASCIInumbers.HEX 15 =
  string.CHR (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 7)))

P.
    P
      (string.CHR
         (arithmetic.BIT2 (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))))
    P
      (string.CHR
         (bit1 (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))))
    P
      (string.CHR
         (arithmetic.BIT2
            (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))))
    P
      (string.CHR
         (bit1 (bit1 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))))))
    P
      (string.CHR
         (arithmetic.BIT2
            (bit1 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))))))
    P
      (string.CHR
         (bit1
            (arithmetic.BIT2
               (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))))))
    P
      (string.CHR
         (arithmetic.BIT2
            (arithmetic.BIT2
               (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))))))
    P
      (string.CHR
         (bit1 (bit1 (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))))))
    P
      (string.CHR
         (arithmetic.BIT2
            (bit1 (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))))))
    P
      (string.CHR
         (bit1
            (arithmetic.BIT2
               (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))))))
    P
      (string.CHR
         (bit1
            (arithmetic.BIT2 (bit1 (bit1 (bit1 (arithmetic.BIT2 0)))))))
    P
      (string.CHR
         (arithmetic.BIT2
            (arithmetic.BIT2 (bit1 (bit1 (bit1 (arithmetic.BIT2 0)))))))
    P
      (string.CHR
         (bit1
            (bit1 (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))))))
    P
      (string.CHR
         (arithmetic.BIT2
            (bit1 (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))))))
    P
      (string.CHR
         (bit1
            (arithmetic.BIT2
               (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))))))
    P
      (string.CHR
         (arithmetic.BIT2
            (arithmetic.BIT2
               (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))))))
    P (string.CHR (bit1 (arithmetic.BIT2 15)))
    P (string.CHR (arithmetic.BIT2 (arithmetic.BIT2 15)))
    P (string.CHR (bit1 (bit1 (arithmetic.BIT2 7))))
    P (string.CHR (arithmetic.BIT2 (bit1 (arithmetic.BIT2 7))))
    P (string.CHR (bit1 (arithmetic.BIT2 (arithmetic.BIT2 7))))
    P
      (string.CHR
         (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 7))))
    (v24. P v24) v24. P v24

ASCIInumbers.HEX =
  relation.WFREC (select R. wellFounded R)
    (λHEX a.
       bool.literal_case
         (λv.
            if v = 0 then
              id
                (string.CHR
                   (arithmetic.BIT2
                      (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))))
            else if v = 1 then
              id
                (string.CHR
                   (bit1
                      (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))))
            else if v = arithmetic.BIT2 0 then
              id
                (string.CHR
                   (arithmetic.BIT2
                      (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))))
            else if v = 3 then
              id
                (string.CHR
                   (bit1
                      (bit1 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))))))
            else if v = arithmetic.BIT2 1 then
              id
                (string.CHR
                   (arithmetic.BIT2
                      (bit1 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))))))
            else if v = bit1 (arithmetic.BIT2 0) then
              id
                (string.CHR
                   (bit1
                      (arithmetic.BIT2
                         (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))))))
            else if v = arithmetic.BIT2 (arithmetic.BIT2 0) then
              id
                (string.CHR
                   (arithmetic.BIT2
                      (arithmetic.BIT2
                         (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))))))
            else if v = 7 then
              id
                (string.CHR
                   (bit1
                      (bit1 (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))))))
            else if v = arithmetic.BIT2 3 then
              id
                (string.CHR
                   (arithmetic.BIT2
                      (bit1 (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))))))
            else if v = bit1 (arithmetic.BIT2 1) then
              id
                (string.CHR
                   (bit1
                      (arithmetic.BIT2
                         (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))))))
            else if v = arithmetic.BIT2 (arithmetic.BIT2 1) then
              id (string.CHR (bit1 (arithmetic.BIT2 15)))
            else if v = bit1 (bit1 (arithmetic.BIT2 0)) then
              id (string.CHR (arithmetic.BIT2 (arithmetic.BIT2 15)))
            else if v = arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)) then
              id (string.CHR (bit1 (bit1 (arithmetic.BIT2 7))))
            else if v = bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)) then
              id (string.CHR (arithmetic.BIT2 (bit1 (arithmetic.BIT2 7))))
            else if v =
                    arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0))
            then
              id (string.CHR (bit1 (arithmetic.BIT2 (arithmetic.BIT2 7))))
            else if v = 15 then
              id
                (string.CHR
                   (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 7))))
            else bool.ARB) a)

ASCIInumbers.UNHEX
    (string.CHR
       (arithmetic.BIT2 (bit1 (bit1 (bit1 (arithmetic.BIT2 0)))))) = 0
  ASCIInumbers.UNHEX
    (string.CHR
       (bit1 (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))))) = 1
  ASCIInumbers.UNHEX
    (string.CHR
       (arithmetic.BIT2
          (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))))) =
  arithmetic.BIT2 0
  ASCIInumbers.UNHEX
    (string.CHR
       (bit1 (bit1 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))))) = 3
  ASCIInumbers.UNHEX
    (string.CHR
       (arithmetic.BIT2
          (bit1 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))))) =
  arithmetic.BIT2 1
  ASCIInumbers.UNHEX
    (string.CHR
       (bit1
          (arithmetic.BIT2
             (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))))) =
  bit1 (arithmetic.BIT2 0)
  ASCIInumbers.UNHEX
    (string.CHR
       (arithmetic.BIT2
          (arithmetic.BIT2
             (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))))) =
  arithmetic.BIT2 (arithmetic.BIT2 0)
  ASCIInumbers.UNHEX
    (string.CHR
       (bit1 (bit1 (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)))))) = 7
  ASCIInumbers.UNHEX
    (string.CHR
       (arithmetic.BIT2
          (bit1 (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)))))) =
  arithmetic.BIT2 3
  ASCIInumbers.UNHEX
    (string.CHR
       (bit1
          (arithmetic.BIT2
             (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)))))) =
  bit1 (arithmetic.BIT2 1)
  ASCIInumbers.UNHEX
    (string.CHR
       (bit1 (arithmetic.BIT2 (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))))) =
  arithmetic.BIT2 (arithmetic.BIT2 1)
  ASCIInumbers.UNHEX
    (string.CHR
       (arithmetic.BIT2
          (arithmetic.BIT2 (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))))) =
  bit1 (bit1 (arithmetic.BIT2 0))
  ASCIInumbers.UNHEX
    (string.CHR
       (bit1 (bit1 (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))))) =
  arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))
  ASCIInumbers.UNHEX
    (string.CHR
       (arithmetic.BIT2
          (bit1 (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))))) =
  bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))
  ASCIInumbers.UNHEX
    (string.CHR
       (bit1
          (arithmetic.BIT2
             (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))))) =
  arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0))
  ASCIInumbers.UNHEX
    (string.CHR
       (arithmetic.BIT2
          (arithmetic.BIT2
             (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0))))))) = 15
  ASCIInumbers.UNHEX (string.CHR (bit1 (arithmetic.BIT2 15))) =
  arithmetic.BIT2 (arithmetic.BIT2 1)
  ASCIInumbers.UNHEX (string.CHR (arithmetic.BIT2 (arithmetic.BIT2 15))) =
  bit1 (bit1 (arithmetic.BIT2 0))
  ASCIInumbers.UNHEX (string.CHR (bit1 (bit1 (arithmetic.BIT2 7)))) =
  arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))
  ASCIInumbers.UNHEX
    (string.CHR (arithmetic.BIT2 (bit1 (arithmetic.BIT2 7)))) =
  bit1 (arithmetic.BIT2 (arithmetic.BIT2 0))
  ASCIInumbers.UNHEX
    (string.CHR (bit1 (arithmetic.BIT2 (arithmetic.BIT2 7)))) =
  arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0))
  ASCIInumbers.UNHEX
    (string.CHR (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 7)))) =
  15

ASCIInumbers.UNHEX =
  relation.WFREC (select R. wellFounded R)
    (λUNHEX a.
       bool.literal_case
         (λv.
            if v =
               string.CHR
                 (arithmetic.BIT2 (bit1 (bit1 (bit1 (arithmetic.BIT2 0)))))
            then id 0
            else if v =
                    string.CHR
                      (bit1
                         (arithmetic.BIT2
                            (bit1 (bit1 (arithmetic.BIT2 0)))))
            then id 1
            else if v =
                    string.CHR
                      (arithmetic.BIT2
                         (arithmetic.BIT2
                            (bit1 (bit1 (arithmetic.BIT2 0)))))
            then id (arithmetic.BIT2 0)
            else if v =
                    string.CHR
                      (bit1
                         (bit1
                            (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))))
            then id 3
            else if v =
                    string.CHR
                      (arithmetic.BIT2
                         (bit1
                            (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))))
            then id (arithmetic.BIT2 1)
            else if v =
                    string.CHR
                      (bit1
                         (arithmetic.BIT2
                            (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))))
            then id (bit1 (arithmetic.BIT2 0))
            else if v =
                    string.CHR
                      (arithmetic.BIT2
                         (arithmetic.BIT2
                            (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))))
            then id (arithmetic.BIT2 (arithmetic.BIT2 0))
            else if v =
                    string.CHR
                      (bit1
                         (bit1
                            (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)))))
            then id 7
            else if v =
                    string.CHR
                      (arithmetic.BIT2
                         (bit1
                            (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)))))
            then id (arithmetic.BIT2 3)
            else if v =
                    string.CHR
                      (bit1
                         (arithmetic.BIT2
                            (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)))))
            then id (bit1 (arithmetic.BIT2 1))
            else if v =
                    string.CHR
                      (bit1
                         (arithmetic.BIT2
                            (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))))
            then id (arithmetic.BIT2 (arithmetic.BIT2 1))
            else if v =
                    string.CHR
                      (arithmetic.BIT2
                         (arithmetic.BIT2
                            (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))))
            then id (bit1 (bit1 (arithmetic.BIT2 0)))
            else if v =
                    string.CHR
                      (bit1
                         (bit1
                            (arithmetic.BIT2
                               (bit1 (bit1 (arithmetic.BIT2 0))))))
            then id (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))
            else if v =
                    string.CHR
                      (arithmetic.BIT2
                         (bit1
                            (arithmetic.BIT2
                               (bit1 (bit1 (arithmetic.BIT2 0))))))
            then id (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)))
            else if v =
                    string.CHR
                      (bit1
                         (arithmetic.BIT2
                            (arithmetic.BIT2
                               (bit1 (bit1 (arithmetic.BIT2 0))))))
            then id (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0)))
            else if v =
                    string.CHR
                      (arithmetic.BIT2
                         (arithmetic.BIT2
                            (arithmetic.BIT2
                               (bit1 (bit1 (arithmetic.BIT2 0))))))
            then id 15
            else if v = string.CHR (bit1 (arithmetic.BIT2 15)) then
              id (arithmetic.BIT2 (arithmetic.BIT2 1))
            else if v = string.CHR (arithmetic.BIT2 (arithmetic.BIT2 15))
            then id (bit1 (bit1 (arithmetic.BIT2 0)))
            else if v = string.CHR (bit1 (bit1 (arithmetic.BIT2 7))) then
              id (arithmetic.BIT2 (bit1 (arithmetic.BIT2 0)))
            else if v =
                    string.CHR (arithmetic.BIT2 (bit1 (arithmetic.BIT2 7)))
            then id (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)))
            else if v =
                    string.CHR (bit1 (arithmetic.BIT2 (arithmetic.BIT2 7)))
            then id (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0)))
            else if v =
                    string.CHR
                      (arithmetic.BIT2
                         (arithmetic.BIT2 (arithmetic.BIT2 7)))
            then id 15
            else bool.ARB) a)

External Type Operators

External Constants

Assumptions

wellFounded empty

wellFounded (<)

prim_rec.measure = relation.inv_image (<)

x. x = x

t. t

n. 0 n

m. m m

m. wellFounded (prim_rec.measure m)

bool.LET = λf x. f x

combin.FAIL x y = x

arithmetic.DIV2 (bit1 x) = x

¬¬p p

x. id x = x

t. t ¬t

x. marker.Abbrev x x

n. ¬(n < 0)

n. ¬(n < n)

(¬) = λt. t

() = λP. P ((select) P)

a. x. x = a

t. (x. t) t

t. (x. t) t

t. (λx. t x) = t

() = λP. P = λx.

¬(p q) p

x. ¬(none = some x)

x. x = x

c. arithmetic.- c c = 0

n. n + 0 = n

l. reverse (reverse l) = l

l. l @ [] = l

¬(p q) ¬q

¬(p q) ¬p

¬(p q) ¬q

A. A ¬A

t. ¬t t

t. (t ) ¬t

l. null l l = []

l. length (reverse l) = length l

n m. arithmetic.- n m n

() = λp q. p q p

t. t t

t. (t ) (t )

m. prim_rec.PRE m = arithmetic.- m 1

n. suc n = 1 + n

n. n 0 n = 0

a. arithmetic.- (suc a) a = 1

x. (fst x, snd x) = x

x y. fst (x, y) = x

x y. snd (x, y) = y

h t. tail (h :: t) = t

a1 a0. ¬([] = a0 :: a1)

f x. bool.literal_case f x = f x

P x. P x P ((select) P)

f (λx. g x) = λx. f (g x)

flip (λx. f x) y = λx. f x y

pair.pair_CASE (x, y) f = f x y

l. length l = 0 l = []

x. q r. x = (q, r)

x y. x = y y = x

A B. A B B A

m n. m > n n < m

m n. m * n = n * m

m n. m + n = n + m

a c. arithmetic.- (a + c) c = a

l f. length (map f l) = length l

R f. wellFounded R wellFounded (relation.inv_image R f)

P (bool.LET f v) = bool.LET (P f) v

bool.LET f v x = bool.LET (flip f x) v

(¬A ) (A )

Combinator.s f (λx. g x) = λx. f x (g x)

n. 0 < n 0 mod n = 0

f g. f g = λx. f (g x)

A B. A B ¬A B

m n. m < n suc m n

n b. bit.BITV n b = bit.BITS b b n

m n. ¬(m < n) n m

opt. opt = none x. opt = some x

P l. all P (reverse l) all P l

() = λp q. (λf. f p q) = λf. f

P. ¬(x. P x) x. ¬P x

P. ¬(x. P x) x. ¬P x

() = λP. q. (x. P x q) q

x y. some x = some y x = y

m n. 0 < n m mod n < n

n k. k < n k mod n = k

m n. ¬(m n) suc n m

m n. suc m < suc n m < n

n m. suc n suc m n m

l1 l2. reverse l1 = reverse l2 l1 = l2

f l. map f (reverse l) = reverse (map f l)

reverse l = e :: [] l = e :: []

m. arithmetic.- 0 m = 0 arithmetic.- m 0 = m

f g x. (f g) x = f (g x)

f x y. flip f x y = f y x

b n. 0 < b all ((>) b) (numposrep.n2l b n)

l1 l2. length (l1 @ l2) = length l1 + length l2

R f. relation.inv_image R f = λx y. R (f x) (f y)

l. l = [] h t. l = h :: t

f g. f = g x. f x = g x

f v. (x. x = v f x) f v

P a. (x. x = a P x) P a

f x y. pair.UNCURRY f (x, y) = f x y

() = λt1 t2. t. (t1 t) (t2 t) t

t1 t2. (t1 t2) (t1 t2) (t2 t1)

t1 t2. (t1 t2) (t2 t1) (t1 t2)

m n. m = n m n n m

b n. bit.BIT b n bit.BITS b b n = 1

n q. 0 < n q * n div n = q

bool.LET f v () (Combinator.s (() (marker.Abbrev flip (=) v)) f)

(p ¬q) (p q) (¬q ¬p)

¬(¬A B) A ¬B

P Q. (x. P Q x) P x. Q x

Q P. (x. P x Q) (x. P x) Q

P Q. (x. P Q x) P x. Q x

P Q. P (x. Q x) x. P Q x

P Q. P (x. Q x) x. P Q x

m n. m < suc n m = n m < n

b n. 1 < b numposrep.l2n b (numposrep.n2l b n) = n

P Q. (x. P x Q) (x. P x) Q

P Q. (x. P x) Q x. P x Q

P Q. (x. P x) Q x. P x Q

¬(A B) (A ) ¬B

t1 t2 t3. t1 t2 t3 (t1 t2) t3

t1 t2 t3. t1 t2 t3 t1 t2 t3

A B C. A B C (A B) C

m n p. m * (n * p) = m * n * p

m n p. m + (n + p) = m + n + p

m n p. arithmetic.- (arithmetic.- m n) p = arithmetic.- m (n + p)

m n p. m + n m + p n p

m n p. m < n n < p m < p

m n p. m n n < p m < p

m n p. m n n p m p

n. 1 n = 1 n 1 = n

l1 l2 l3. l1 @ l2 @ l3 = (l1 @ l2) @ l3

f g l. map f (map g l) = map (f g) l

P. (x. y. P x y) f. x. P x (f x)

t1 t2. (if then t1 else t2) = t1 (if then t1 else t2) = t2

t1 t2. (t1 t2) t1 t2 ¬t1 ¬t2

n m. arithmetic.- n m = if m < n then numeral.iSUB n m else 0

m n. 0 < n (m = prim_rec.PRE n suc m = n)

m n. m * n = 0 m = 0 n = 0

m n. m + n = 0 m = 0 n = 0

P f l. all P (map f l) all (λx. P (f x)) l

length [] = 0 h t. length (h :: t) = suc (length t)

(t. ¬¬t t) (¬ ) (¬ )

m n. ¬(m = n) suc m n suc n m

n d. 0 < n 1 < d n div d < n

n l.
    n length l list.TAKE n (reverse l) = reverse (rich_list.LASTN n l)

P Q R. P Q R (P Q) (P R)

A B C. B C A (B A) (C A)

m n p. m n suc p * m suc p * n

m n p. p * (m + n) = p * m + p * n

m n p. arithmetic.- m n * p = arithmetic.- (m * p) (n * p)

n. 0 < n n div n = 1 n mod n = 0

b f g x. (if b then f else g) x = if b then f x else g x

f b x y. f (if b then x else y) = if b then f x else f y

f R y z. R y z relation.RESTRICT f R z y = f y

P. (n. (m. m < n P m) P n) n. P n

P Q. (x. P x Q x) (x. P x) x. Q x

P Q. (x. P x Q x) (x. P x) x. Q x

P Q. (x. P x Q x) l. all P l all Q l

P. P [] (t. P t h. P (h :: t)) l. P l

m n p. arithmetic.- m n < p m < n + p 0 < p

n x y. 0 < n x y x div n y div n

n l. n < length l f. list.EL n (map f l) = f (list.EL n l)

n. 0 < n q r. (q * n + r) mod n = r mod n

map f l = x :: [] x0. l = x0 :: [] x = f x0

n l.
    n < length l
    list.EL n (reverse l) =
    list.EL (prim_rec.PRE (arithmetic.- (length l) n)) l

x y a b. (x, y) = (a, b) x = a y = b

a0 a1 a0' a1'. a0 :: a1 = a0' :: a1' a0 = a0' a1 = a1'

n.
    numeral.iDUB (bit1 n) = arithmetic.BIT2 (numeral.iDUB n)
    numeral.iDUB (arithmetic.BIT2 n) = arithmetic.BIT2 (bit1 n)
    numeral.iDUB 0 = 0

l f. (map f l = [] l = []) ([] = map f l l = [])

(p q r) (p q) (p ¬r) (¬q r ¬p)

(p q r) (p ¬q) (p ¬r) (q r ¬p)

f0 f1. fn. fn [] = f0 a0 a1. fn (a0 :: a1) = f1 a0 a1 (fn a1)

R. wellFounded R P. (x. (y. R y x P y) P x) x. P x

(v f. option.option_CASE none v f = v)
  x v f. option.option_CASE (some x) v f = f x

x x' y y'. (x x') (x' (y y')) (x y x' y')

n k q. (r. k = q * n + r r < n) k div n = q

n k r. (q. k = q * n + r r < n) k mod n = r

b n.
    1 < b
    length (numposrep.n2l b n) = if n = 0 then 1 else suc (logroot.LOG b n)

(p q r) (p ¬q ¬r) (q ¬p) (r ¬p)

suc 0 = 1 (n. suc (bit1 n) = arithmetic.BIT2 n)
  n. suc (arithmetic.BIT2 n) = bit1 (suc n)

(l. [] @ l = l) l1 l2 h. (h :: l1) @ l2 = h :: l1 @ l2

h l n.
    bit.BITS h l n =
    n div arithmetic.BIT2 0 l mod
    arithmetic.BIT2 0 arithmetic.- (suc h) l

m n p. arithmetic.- m n = p m = n + p m n p 0

P (arithmetic.- a b) d. (b = a + d P 0) (a = b + d P d)

A B. (¬(A B) ¬A ¬B) (¬(A B) ¬A ¬B)

n. 0 < n k. k = (k div n) * n + k mod n k mod n < n

M R f.
    f = relation.WFREC R M wellFounded R
    x. f x = M (relation.RESTRICT f R x) x

(f. map f [] = []) f h t. map f (h :: t) = f h :: map f t

(P. all P [] ) P h t. all P (h :: t) P h all P t

n.
    even 0 even (arithmetic.BIT2 n) ¬even (bit1 n) ¬odd 0
    ¬odd (arithmetic.BIT2 n) odd (bit1 n)

bool.TYPE_DEFINITION =
  λP rep.
    (x' x''. rep x' = rep x'' x' = x'') x. P x x'. x = rep x'

(v f. list.list_CASE [] v f = v)
  a0 a1 v f. list.list_CASE (a0 :: a1) v f = f a0 a1

t. (( t) t) ((t ) t) (( t) ¬t) ((t ) ¬t)

P.
    (rep. bool.TYPE_DEFINITION P rep)
    rep abs. (a. abs (rep a) = a) r. P r rep (abs r) = r

(b. numposrep.l2n b [] = 0)
  b h t. numposrep.l2n b (h :: t) = h mod b + b * numposrep.l2n b t

(f. list.list_size f [] = 0)
  f a0 a1. list.list_size f (a0 :: a1) = 1 + (f a0 + list.list_size f a1)

f g M N. M = N (x. x = N f x = g x) bool.LET f M = bool.LET g N

b l.
    1 < b all ((>) b) l ¬(numposrep.l2n b l = 0)
    suc (logroot.LOG b (numposrep.l2n b l)) length l

(list.isPREFIX [] l ) (list.isPREFIX (h :: t) [] )
  (list.isPREFIX (h1 :: t1) (h2 :: t2) h1 = h2 list.isPREFIX t1 t2)

numeral.texp_help 0 acc = arithmetic.BIT2 acc
  numeral.texp_help (bit1 n) acc =
  numeral.texp_help (prim_rec.PRE (bit1 n)) (bit1 acc)
  numeral.texp_help (arithmetic.BIT2 n) acc =
  numeral.texp_help (bit1 n) (bit1 acc)

(l. list.isPREFIX [] l )
  h t l.
    list.isPREFIX (h :: t) l
    list.list_CASE l (λh' t'. h = h' list.isPREFIX t t')

(f e. list.FOLDR f e [] = e)
  f e x l. list.FOLDR f e (x :: l) = f x (list.FOLDR f e l)

b x n.
    1 < b x < length (numposrep.n2l b n)
    list.EL x (numposrep.n2l b n) = n div b x mod b

numeral.exactlog 0 = 0 (n. numeral.exactlog (bit1 n) = 0)
  n.
    numeral.exactlog (arithmetic.BIT2 n) =
    bool.LET (λx. if x = 0 then 0 else bit1 x) (numeral.onecount n 0)

(x. numeral.onecount 0 x = x)
  (n x. numeral.onecount (bit1 n) x = numeral.onecount n (suc x))
  n x. numeral.onecount (arithmetic.BIT2 n) x = 0

n b.
    numposrep.n2l b n =
    if n < b b < arithmetic.BIT2 0 then n mod b :: []
    else n mod b :: numposrep.n2l b (n div b)

t. ( t t) (t t) ( t ) (t ) (t t t)

t. ( t ) (t ) ( t t) (t t) (t t t)

0 + m = m m + 0 = m suc m + n = suc (m + n) m + suc n = suc (m + n)

(n. list.TAKE n [] = [])
  n x xs.
    list.TAKE n (x :: xs) =
    if n = 0 then [] else x :: list.TAKE (arithmetic.- n 1) xs

t. ( t t) (t ) ( t ) (t t ) (t ¬t)

(l1 l2 l3. l1 @ l2 = l1 @ l3 l2 = l3)
  l1 l2 l3. l2 @ l1 = l3 @ l1 l2 = l3

b l x.
    1 < b all ((>) b) l x < length l
    numposrep.l2n b l div b x mod b = list.EL x l

(l1 l2. [] = l1 @ l2 l1 = [] l2 = [])
  l1 l2. l1 @ l2 = [] l1 = [] l2 = []

P Q x x' y y'.
    (P Q) (Q x = x') (¬Q y = y')
    (if P then x else y) = if Q then x' else y'

(p q r) (p q r) (p ¬r ¬q) (q ¬r ¬p) (r ¬q ¬p)

b l.
    1 < b all ((>) b) l
    numposrep.n2l b (numposrep.l2n b l) =
    if numposrep.l2n b l = 0 then 0 :: []
    else list.TAKE (suc (logroot.LOG b (numposrep.l2n b l))) l

f g.
    (n. g (suc n) = f n (suc n))
    (n. g (bit1 n) = f (arithmetic.- (bit1 n) 1) (bit1 n))
    n. g (arithmetic.BIT2 n) = f (bit1 n) (arithmetic.BIT2 n)

(P. rich_list.SPLITP P [] = ([], []))
  P x l.
    rich_list.SPLITP P (x :: l) =
    if P x then ([], x :: l)
    else (x :: fst (rich_list.SPLITP P l), snd (rich_list.SPLITP P l))

n m.
    0 * n = 0 n * 0 = 0
    bit1 n * m = numeral.iZ (numeral.iDUB (n * m) + m)
    arithmetic.BIT2 n * m = numeral.iDUB (numeral.iZ (n * m + m))

prim_rec.PRE 0 = 0 prim_rec.PRE 1 = 0
  (n.
     prim_rec.PRE (bit1 (bit1 n)) =
     arithmetic.BIT2 (prim_rec.PRE (bit1 n)))
  (n.
     prim_rec.PRE (bit1 (arithmetic.BIT2 n)) = arithmetic.BIT2 (bit1 n))
  n. prim_rec.PRE (arithmetic.BIT2 n) = bit1 n

(p if q then r else s)
  (p q ¬s) (p ¬r ¬q) (p ¬r ¬s) (¬q r ¬p)
  (q s ¬p)

m n.
    0 * m = 0 m * 0 = 0 1 * m = m m * 1 = m suc m * n = m * n + n
    m * suc n = m + m * n

n m.
    (0 n ) (bit1 n 0 ) (arithmetic.BIT2 n 0 )
    (bit1 n bit1 m n m) (bit1 n arithmetic.BIT2 m n m)
    (arithmetic.BIT2 n bit1 m ¬(m n))
    (arithmetic.BIT2 n arithmetic.BIT2 m n m)

n m.
    (0 < bit1 n ) (0 < arithmetic.BIT2 n ) (n < 0 )
    (bit1 n < bit1 m n < m)
    (arithmetic.BIT2 n < arithmetic.BIT2 m n < m)
    (bit1 n < arithmetic.BIT2 m ¬(m < n))
    (arithmetic.BIT2 n < bit1 m n < m)

n m.
    (0 = bit1 n ) (bit1 n = 0 ) (0 = arithmetic.BIT2 n )
    (arithmetic.BIT2 n = 0 ) (bit1 n = arithmetic.BIT2 m )
    (arithmetic.BIT2 n = bit1 m ) (bit1 n = bit1 m n = m)
    (arithmetic.BIT2 n = arithmetic.BIT2 m n = m)

0 * n = 0 n * 0 = 0
  bit1 x * bit1 y = numeral.internal_mult (bit1 x) (bit1 y)
  bit1 x * arithmetic.BIT2 y =
  bool.LET
    (λn.
       if odd n then
         numeral.texp_help (arithmetic.DIV2 n) (prim_rec.PRE (bit1 x))
       else numeral.internal_mult (bit1 x) (arithmetic.BIT2 y))
    (numeral.exactlog (arithmetic.BIT2 y))
  arithmetic.BIT2 x * bit1 y =
  bool.LET
    (λm.
       if odd m then
         numeral.texp_help (arithmetic.DIV2 m) (prim_rec.PRE (bit1 y))
       else numeral.internal_mult (arithmetic.BIT2 x) (bit1 y))
    (numeral.exactlog (arithmetic.BIT2 x))
  arithmetic.BIT2 x * arithmetic.BIT2 y =
  bool.LET
    (λm.
       bool.LET
         (λn.
            if odd m then
              numeral.texp_help (arithmetic.DIV2 m)
                (prim_rec.PRE (arithmetic.BIT2 y))
            else if odd n then
              numeral.texp_help (arithmetic.DIV2 n)
                (prim_rec.PRE (arithmetic.BIT2 x))
            else
              numeral.internal_mult (arithmetic.BIT2 x)
                (arithmetic.BIT2 y))
         (numeral.exactlog (arithmetic.BIT2 y)))
    (numeral.exactlog (arithmetic.BIT2 x))

b n m.
    numeral.iSUB b 0 x = 0 numeral.iSUB n 0 = n
    numeral.iSUB (bit1 n) 0 = numeral.iDUB n
    numeral.iSUB (bit1 n) (bit1 m) = numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (bit1 n) (bit1 m) = bit1 (numeral.iSUB n m)
    numeral.iSUB (bit1 n) (arithmetic.BIT2 m) =
    bit1 (numeral.iSUB n m)
    numeral.iSUB (bit1 n) (arithmetic.BIT2 m) =
    numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) 0 = bit1 n
    numeral.iSUB (arithmetic.BIT2 n) (bit1 m) =
    bit1 (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) (bit1 m) =
    numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) (arithmetic.BIT2 m) =
    numeral.iDUB (numeral.iSUB n m)
    numeral.iSUB (arithmetic.BIT2 n) (arithmetic.BIT2 m) =
    bit1 (numeral.iSUB n m)

n m.
    numeral.iZ (0 + n) = n numeral.iZ (n + 0) = n
    numeral.iZ (bit1 n + bit1 m) = arithmetic.BIT2 (numeral.iZ (n + m))
    numeral.iZ (bit1 n + arithmetic.BIT2 m) = bit1 (suc (n + m))
    numeral.iZ (arithmetic.BIT2 n + bit1 m) = bit1 (suc (n + m))
    numeral.iZ (arithmetic.BIT2 n + arithmetic.BIT2 m) =
    arithmetic.BIT2 (suc (n + m)) suc (0 + n) = suc n
    suc (n + 0) = suc n suc (bit1 n + bit1 m) = bit1 (suc (n + m))
    suc (bit1 n + arithmetic.BIT2 m) = arithmetic.BIT2 (suc (n + m))
    suc (arithmetic.BIT2 n + bit1 m) = arithmetic.BIT2 (suc (n + m))
    suc (arithmetic.BIT2 n + arithmetic.BIT2 m) =
    bit1 (numeral.iiSUC (n + m))
    numeral.iiSUC (0 + n) = numeral.iiSUC n
    numeral.iiSUC (n + 0) = numeral.iiSUC n
    numeral.iiSUC (bit1 n + bit1 m) = arithmetic.BIT2 (suc (n + m))
    numeral.iiSUC (bit1 n + arithmetic.BIT2 m) =
    bit1 (numeral.iiSUC (n + m))
    numeral.iiSUC (arithmetic.BIT2 n + bit1 m) =
    bit1 (numeral.iiSUC (n + m))
    numeral.iiSUC (arithmetic.BIT2 n + arithmetic.BIT2 m) =
    arithmetic.BIT2 (numeral.iiSUC (n + m))

(n. 0 + n = n) (n. n + 0 = n) (n m. n + m = numeral.iZ (n + m))
  (n. 0 * n = 0) (n. n * 0 = 0) (n m. n * m = n * m)
  (n. arithmetic.- 0 n = 0) (n. arithmetic.- n 0 = n)
  (n m. arithmetic.- n m = arithmetic.- n m) (n. 0 bit1 n = 0)
  (n. 0 arithmetic.BIT2 n = 0) (n. n 0 = 1)
  (n m. n m = n m) suc 0 = 1 (n. suc n = suc n)
  prim_rec.PRE 0 = 0 (n. prim_rec.PRE n = prim_rec.PRE n)
  (n. n = 0 n = 0) (n. 0 = n n = 0) (n m. n = m n = m)
  (n. n < 0 ) (n. 0 < n 0 < n) (n m. n < m n < m)
  (n. 0 > n ) (n. n > 0 0 < n) (n m. n > m m < n)
  (n. 0 n ) (n. n 0 n 0) (n m. n m n m)
  (n. n 0 ) (n. 0 n n = 0) (n m. n m m n)
  (n. odd n odd n) (n. even n even n) ¬odd 0 even 0