Package hol-string: HOL string theories
Information
| name | hol-string |
| version | 1.0 |
| description | HOL string theories |
| author | HOL developers <hol-developers@lists.sourceforge.net> |
| license | MIT |
| checksum | f17086fdeef36a8441fe738fcfbd94a050e20031 |
| requires | base hol-base |
| show | Data.Bool Data.List Data.Option Data.Pair Function HOL4 Number.Natural Relation |
Files
- Package tarball hol-string-1.0.tgz
- Theory source file hol-string.thy (included in the package tarball)
Defined Type Operator
- HOL4
- string
- string.char
- string
Defined Constants
- HOL4
- string
- string.char_ge
- string.char_gt
- string.char_le
- string.char_lt
- string.char_size
- string.isAlpha
- string.isAlphaNum
- string.isAscii
- string.isCntrl
- string.isDigit
- string.isGraph
- string.isHexDigit
- string.isLower
- string.isPrint
- string.isPunct
- string.isSpace
- string.isUpper
- string.string_ge
- string.string_gt
- string.string_le
- string.string_lt
- string.string_lt_tupled
- string.toLower
- string.toUpper
- string.CHR
- string.DEST_STRING
- string.EXPLODE
- string.EXTRACT
- string.FIELDS
- string.FIELDS_tupled
- string.IMPLODE
- string.ORD
- string.STR
- string.SUB
- string.SUBSTRING
- string.TOCHAR
- string.TOKENS
- string.TOKENS_tupled
- string.TRANSLATE
- string_num
- string_num.n2s
- string_num.s2n
- ASCIInumbers
- ASCIInumbers.fromBinString
- ASCIInumbers.fromDecString
- ASCIInumbers.fromHexString
- ASCIInumbers.n2s
- ASCIInumbers.num_from_bin_string
- ASCIInumbers.num_from_dec_string
- ASCIInumbers.num_from_hex_string
- ASCIInumbers.num_from_oct_string
- ASCIInumbers.num_to_bin_string
- ASCIInumbers.num_to_dec_string
- ASCIInumbers.num_to_hex_string
- ASCIInumbers.num_to_oct_string
- ASCIInumbers.s2n
- ASCIInumbers.HEX
- ASCIInumbers.UNHEX
- string
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
- →
- bool
- Data
- List
- list
- Option
- option
- Pair
- ×
- List
- Number
- Natural
- natural
- Natural
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∨
- ¬
- cond
- ⊥
- ⊤
- List
- ::
- @
- []
- all
- concat
- length
- map
- null
- reverse
- tail
- Option
- none
- some
- Pair
- ,
- fst
- snd
- Bool
- Function
- flip
- id
- ∘
- Combinator
- Combinator.s
- HOL4
- arithmetic
- arithmetic.-
- arithmetic.BIT2
- arithmetic.DIV2
- bit
- bit.BIT
- bit.BITS
- bit.BITV
- bool
- bool.literal_case
- bool.ARB
- bool.LET
- bool.TYPE_DEFINITION
- combin
- combin.FAIL
- list
- list.isPREFIX
- list.list_CASE
- list.list_size
- list.EL
- list.FOLDR
- list.TAKE
- logroot
- logroot.LOG
- marker
- marker.Abbrev
- numeral
- numeral.exactlog
- numeral.iDUB
- numeral.iSUB
- numeral.iZ
- numeral.iiSUC
- numeral.internal_mult
- numeral.onecount
- numeral.texp_help
- numposrep
- numposrep.l2n
- numposrep.n2l
- option
- option.option_CASE
- pair
- pair.pair_CASE
- pair.UNCURRY
- prim_rec
- prim_rec.measure
- prim_rec.PRE
- relation
- relation.inv_image
- relation.RESTRICT
- relation.WFREC
- rich_list
- rich_list.LASTN
- rich_list.SEG
- rich_list.SPLITP
- arithmetic
- Number
- Natural
- *
- +
- <
- ≤
- >
- ≥
- ↑
- bit1
- div
- even
- mod
- odd
- suc
- zero
- Natural
- Relation
- empty
- wellFounded
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