Package hol-words: n-bit words

Information

namehol-words
version1.2
descriptionn-bit words
authorHOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
licenseMIT
checksum43c336407db898b59122b3c99fe426d52eb644c8
requiresbase
hol-base
hol-string
showData.Bool
Data.List
Data.Option
Data.Pair
Function
HOL4
Number.Natural
Relation

Files

Defined Type Operators

Defined Constants

Theorems

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV

words.word_msb words.word_L

¬words.word_msb words.word_H

words.word_lt words.word_L words.word_H

s. pred_set.FINITE s

¬words.word_msb (words.n2w 0)

bitstring.bnot = map (¬)

words.word_lsb = words.word_bit 0

words.reduce_and = words.word_reduce ()

words.reduce_or = words.word_reduce ()

words.reduce_xnor = words.word_reduce ()

bitstring.band = bitstring.bitwise ()

bitstring.bor = bitstring.bitwise ()

bitstring.bxnor = bitstring.bitwise ()

0 < fcp.dimindex bool.the_value

0 < words.dimword bool.the_value

0 < words.INT_MIN bool.the_value

0 < words.UINT_MAX bool.the_value

0 words.INT_MAX bool.the_value

words.word_2comp words.word_L = words.word_L

words.word_lo (words.n2w 0) words.word_L

a. words.word_le words.word_L a

a. words.word_le a words.word_H

a. words.word_le a a

w. words.word_ls w words.word_T

a. words.word_ls a a

rep. bool.TYPE_DEFINITION (λf. ) rep

¬(words.word_L = words.n2w 0)

words.word_lsb (words.word_2comp (words.n2w 1))

words.word_msb (words.word_2comp (words.n2w 1))

words.word_H = words.n2w (words.INT_MAX bool.the_value)

words.word_L = words.n2w (words.INT_MIN bool.the_value)

words.word_L2 = words.word_mul words.word_L words.word_L

words.word_T = words.n2w (words.UINT_MAX bool.the_value)

words.word_from_bin_list = words.l2w (arithmetic.BIT2 0)

words.word_to_bin_list = words.w2l (arithmetic.BIT2 0)

pred_set.FINITE pred_set.UNIV pred_set.FINITE pred_set.UNIV

pred_set.FINITE pred_set.UNIV pred_set.FINITE pred_set.UNIV

fcp.dimindex bool.the_value = 1

fcp.dimindex bool.the_value = arithmetic.BIT2 0

words.dimword bool.the_value = arithmetic.BIT2 0

words.INT_MIN bool.the_value = 1

words.INT_MIN bool.the_value = arithmetic.BIT2 0

words.word_1comp words.word_T = words.n2w 0

fcp.dimindex bool.the_value < words.dimword bool.the_value

words.INT_MAX bool.the_value < words.dimword bool.the_value

words.INT_MIN bool.the_value < words.dimword bool.the_value

1 < words.dimword bool.the_value

1 fcp.dimindex bool.the_value

words.w2n (words.n2w 0) = 0

words.word_1comp (words.n2w 0) = words.word_T

words.word_add words.word_L words.word_H = words.word_T

words.word_from_bin_string words.word_to_bin_string = id

words.word_from_dec_string words.word_to_dec_string = id

words.word_from_hex_string words.word_to_hex_string = id

words.word_from_oct_string words.word_to_oct_string = id

words.word_from_bin_list words.word_to_bin_list = id

words.word_from_dec_list words.word_to_dec_list = id

words.word_from_hex_list words.word_to_hex_list = id

words.word_from_oct_list words.word_to_oct_list = id

v. ¬null (fcp.V2L v)

a. ¬words.word_lo a a

a. ¬words.word_lt a a

w. words.sw2sw w = w

w. words.w2w w = w

w. words.word_ls (words.n2w 0) w

words.word_from_bin_string =
  words.s2w (arithmetic.BIT2 0) ASCIInumbers.UNHEX

words.word_to_bin_string = words.w2s (arithmetic.BIT2 0) ASCIInumbers.HEX

words.word_bit 0 (words.word_2comp (words.n2w 1))

fcp.dimindex bool.the_value = 3

fcp.dimindex bool.the_value = arithmetic.BIT2 1

fcp.dimindex bool.the_value = arithmetic.BIT2 (arithmetic.BIT2 0)

fcp.dimindex bool.the_value = bit1 (arithmetic.BIT2 0)

words.dimword bool.the_value = arithmetic.BIT2 1

words.INT_MIN bool.the_value = arithmetic.BIT2 1

words.word_2comp words.word_T = words.n2w 1

words.n2w (words.dimword bool.the_value) = words.n2w 0

words.w2w (words.n2w 0) = words.n2w 0

words.word_2comp (words.n2w 0) = words.n2w 0

words.word_reverse (words.n2w 0) = words.n2w 0

words.sw2sw (words.n2w 0) = words.n2w 0

words.word_2comp (words.n2w 1) = words.word_T

h. ¬words.word_bit h (words.n2w 0)

n. length (bitstring.rev_count_list n) = n

n. bitstring.v2n (bitstring.n2v n) = n

n. words.word_asr words.word_T n = words.word_T

n. words.word_ror words.word_T n = words.word_T

v. bitstring.shiftr v 0 = v

w. words.word_len w = fcp.dimindex bool.the_value

w. words.w2n w < words.dimword bool.the_value

w. words.bit_count_upto 0 w = 0

w. bitstring.v2w (bitstring.w2v w) = w

w. words.n2w (words.w2n w) = w

a. words.word_1comp (words.word_1comp a) = a

w. words.word_2comp (words.word_2comp w) = w

w. alignment.align 0 w = w

a. words.word_and a a = a

a. words.word_or a a = a

n. fcp.dimindex bool.the_value = suc n

w. n. w = words.n2w n

w. v. w = bitstring.v2w v

words.word_H = words.word_sub words.word_L (words.n2w 1)

words.word_from_dec_list =
  words.l2w (arithmetic.BIT2 (arithmetic.BIT2 1))

words.word_from_oct_list = words.l2w (arithmetic.BIT2 3)

words.word_to_dec_list = words.w2l (arithmetic.BIT2 (arithmetic.BIT2 1))

words.word_to_oct_list = words.w2l (arithmetic.BIT2 3)

fcp.dimindex bool.the_value = 7

fcp.dimindex bool.the_value = arithmetic.BIT2 3

fcp.dimindex bool.the_value = arithmetic.BIT2 (bit1 (arithmetic.BIT2 0))

fcp.dimindex bool.the_value = arithmetic.BIT2 (arithmetic.BIT2 1)

fcp.dimindex bool.the_value = bit1 (arithmetic.BIT2 1)

fcp.dimindex bool.the_value = bit1 (bit1 (arithmetic.BIT2 0))

words.dimword bool.the_value = arithmetic.BIT2 3

words.INT_MIN bool.the_value = arithmetic.BIT2 3

words.w2n (words.n2w 1) = 1

words.n2w_itself (n, bool.the_value) = words.n2w n

words.word_log2 (words.n2w 1) = words.n2w 0

n. words.word_lsb (words.n2w n) odd n

n. bitstring.v2w (bitstring.n2v n) = words.n2w n

v. words.n2w (bitstring.v2n v) = bitstring.v2w v

w. bitstring.fixwidth (length w) w = w

v. fcp.FCP_HD v = head (fcp.V2L v)

v. fcp.FCP_HD v = fcp.fcp_index v 0

v. length (fcp.V2L v) = fcp.dimindex bool.the_value

w. words.word_lsb w fcp.fcp_index w 0

a. words.word_msb a words.word_ls words.word_L a

w. words.saturate_w2w w = words.saturate_n2w (words.w2n w)

w. words.w2w w = words.n2w (words.w2n w)

w. length (bitstring.w2v w) = fcp.dimindex bool.the_value

w. words.word_abs (words.word_2comp w) = words.word_abs w

w. words.word_abs (words.word_abs w) = words.word_abs w

w. words.word_sub w w = words.n2w 0

%%genvar%%8673.
    words.w2n (words.w2w %%genvar%%8673) < words.dimword bool.the_value

w. words.w2n (words.w2w w) words.w2n w

a. words.word_or a (words.word_1comp a) = words.word_T

w. words.word_sub w (words.n2w 0) = w

a. words.word_xor a (words.word_1comp a) = words.word_T

p w. alignment.aligned p (alignment.align p w)

g. fcp.FCP (λi. fcp.fcp_index g i) = g

¬(words.word_2comp (words.n2w 1) = words.n2w 0)

words.word_msb =
  words.word_bit (arithmetic.- (fcp.dimindex bool.the_value) 1)

words.word_from_dec_string =
  words.s2w (arithmetic.BIT2 (arithmetic.BIT2 1)) ASCIInumbers.UNHEX

words.word_from_oct_string =
  words.s2w (arithmetic.BIT2 3) ASCIInumbers.UNHEX

words.word_from_hex_list = words.l2w (arithmetic.BIT2 7)

words.word_to_dec_string =
  words.w2s (arithmetic.BIT2 (arithmetic.BIT2 1)) ASCIInumbers.HEX

words.word_to_oct_string = words.w2s (arithmetic.BIT2 3) ASCIInumbers.HEX

words.word_to_hex_list = words.w2l (arithmetic.BIT2 7)

words.reduce_nand = words.word_reduce (λa b. ¬(a b))

words.reduce_nor = words.word_reduce (λa b. ¬(a b))

words.reduce_xor = words.word_reduce (λx y. ¬(x y))

bitstring.bnand = bitstring.bitwise (λx y. ¬(x y))

bitstring.bnor = bitstring.bitwise (λx y. ¬(x y))

bitstring.bxor = bitstring.bitwise (λx y. ¬(x y))

pred_set.FINITE pred_set.UNIV
  pred_set.FINITE pred_set.UNIV pred_set.FINITE pred_set.UNIV

fcp.dimindex bool.the_value = arithmetic.BIT2 7

fcp.dimindex bool.the_value =
  arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))

fcp.dimindex bool.the_value = arithmetic.BIT2 (bit1 (arithmetic.BIT2 1))

fcp.dimindex bool.the_value =
  arithmetic.BIT2 (bit1 (arithmetic.BIT2 (arithmetic.BIT2 0)))

fcp.dimindex bool.the_value =
  arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0)))

words.dimword bool.the_value =
  arithmetic.BIT2 0 * words.INT_MIN bool.the_value

words.dimword bool.the_value =
  arithmetic.BIT2 0 fcp.dimindex bool.the_value

words.dimword bool.the_value = arithmetic.BIT2 7

words.INT_MAX bool.the_value =
  arithmetic.- (words.INT_MIN bool.the_value) 1

words.INT_MIN bool.the_value = arithmetic.BIT2 7

words.UINT_MAX bool.the_value =
  arithmetic.- (words.dimword bool.the_value) 1

pred_set.FINITE pred_set.UNIV
  pred_set.CARD pred_set.UNIV = fcp.dimindex bool.the_value

arithmetic.- (words.dimword bool.the_value)
    (words.INT_MIN bool.the_value) = words.INT_MIN bool.the_value

words.word_concat (words.n2w 0) (words.n2w 0) = words.n2w 0

n. bitstring.n2v n = bitstring.boolify [] (numposrep.num_to_bin_list n)

%%genvar%%1433.
    %%genvar%%1433 mod fcp.dimindex bool.the_value <
    words.dimword bool.the_value

l. bitstring.v2n l = numposrep.num_from_bin_list (bitstring.bitify [] l)

v. all ((>) (arithmetic.BIT2 0)) (bitstring.bitify [] v)

f. sum_num.SUM 1 f = f 0

w. words.word_msb w words.word_lt w (words.n2w 0)

w.
    words.bit_count w =
    words.bit_count_upto (fcp.dimindex bool.the_value) w

w. words.word_log2 w = words.n2w (bit.LOG2 (words.w2n w))

w. words.word_msb (words.word_1comp w) ¬words.word_msb w

w. words.word_add w (words.word_2comp w) = words.n2w 0

a. words.word_and a (words.word_1comp a) = words.n2w 0

w. words.word_add (words.word_2comp w) w = words.n2w 0

w. words.word_sub (words.n2w 0) w = words.word_2comp w

a. words.word_join (words.n2w 0) a = words.w2w a

v. words.word_div v (words.n2w 1) = v

a' a. ¬(fcp.BIT0A a = fcp.BIT0B a')

n v. length (bitstring.fixwidth n v) = n

n. words.n2w n = fcp.FCP (λi. bit.BIT i n)

L. fcp.L2V L = fcp.FCP (λi. list.EL i L)

v. bitstring.v2w v = fcp.FCP (λi. bitstring.testbit i v)

words.word_from_hex_string =
  words.s2w (arithmetic.BIT2 7) ASCIInumbers.UNHEX

words.word_to_hex_string = words.w2s (arithmetic.BIT2 7) ASCIInumbers.HEX

fcp.dimindex bool.the_value = arithmetic.BIT2 15

fcp.dimindex bool.the_value =
  arithmetic.BIT2 (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))

words.dimword bool.the_value = arithmetic.BIT2 15

words.INT_MIN bool.the_value = arithmetic.BIT2 15

¬pred_set.FINITE pred_set.UNIV fcp.dimindex bool.the_value = 1

¬pred_set.FINITE pred_set.UNIV
  words.dimword bool.the_value = arithmetic.BIT2 0

words.word_lsr (words.word_2comp (words.n2w 1)) 1 = words.word_H

n. words.w2n (words.n2w n) = n mod words.dimword bool.the_value

i. i < fcp.dimindex bool.the_value fcp.fcp_index words.word_T i

n. words.n2w (n mod words.dimword bool.the_value) = words.n2w n

%%genvar%%8890.
    bitstring.v2n %%genvar%%8890 <
    arithmetic.BIT2 0 length %%genvar%%8890

v.
    bitstring.w2v (bitstring.v2w v) =
    bitstring.fixwidth (fcp.dimindex bool.the_value) v

v.
    words.reduce_and (bitstring.v2w v) =
    words.word_reduce () (bitstring.v2w v)

v.
    words.reduce_or (bitstring.v2w v) =
    words.word_reduce () (bitstring.v2w v)

v.
    bitstring.v2w (bitstring.fixwidth (fcp.dimindex bool.the_value) v) =
    bitstring.v2w v

v.
    fcp.V2L v =
    list.GENLIST (fcp.fcp_index v) (fcp.dimindex bool.the_value)

w. alignment.aligned 1 w ¬words.word_lsb w

w. words.word_lsl w 1 = words.word_add w w

m. words.word_mod m (words.n2w 1) = words.n2w 0

v l. length (bitstring.bitify [] v) = length v

v n. length (bitstring.rotate v n) = length v

v. fcp.FCP_TL v = fcp.FCP (λi. fcp.fcp_index v (suc i))

a b. words.word_ge a b words.word_le b a

a b. words.word_gt a b words.word_lt b a

a b. words.word_hi a b words.word_lo b a

a b. words.word_hs a b words.word_ls b a

v w. words.word_add v w = words.word_add w v

a b. words.word_and a b = words.word_and b a

v w. words.word_mul v w = words.word_mul w v

a b. words.word_or a b = words.word_or b a

a b. words.word_xor a b = words.word_xor b a

a b. words.word_lo a b words.word_ls a b

a b. words.word_lt a b words.word_le a b

a b. words.word_le a b words.word_le b a

a b. words.word_lo a b words.word_ls b a

a b. words.word_ls a b words.word_ls b a

a b. words.word_lt a b words.word_le b a

v w. words.word_add v (words.word_sub w v) = w

a b. words.word_and a (words.word_or a b) = a

a b. words.word_or a (words.word_and a b) = a

v w. words.word_sub v (words.word_sub v w) = w

v w. words.word_add (words.word_sub v w) w = v

v w. words.word_sub (words.word_add v w) w = v

v w. words.word_sub (words.word_add w v) w = v

w. words.word_1comp w = fcp.FCP (λi. ¬fcp.fcp_index w i)

h f. fcp.fcp_CASE (fcp.mk_cart h) f = f h

rep.
    bool.TYPE_DEFINITION (λx. x = bool.ARB pred_set.FINITE pred_set.UNIV)
      rep

fcp.dimindex bool.the_value =
  if pred_set.FINITE pred_set.UNIV then pred_set.CARD pred_set.UNIV else 1

fcp.dimindex bool.the_value = arithmetic.BIT2 31

fcp.dimindex bool.the_value =
  arithmetic.BIT2 (bit1 (bit1 (bit1 (bit1 (arithmetic.BIT2 0)))))

words.dimword bool.the_value = arithmetic.BIT2 31

words.INT_MIN bool.the_value = arithmetic.BIT2 31

words.word_2comp v = words.n2w 0 v = words.n2w 0

words.sw2sw (words.word_2comp (words.n2w 1)) =
  words.word_2comp (words.n2w 1)

words.word_reverse (words.word_2comp (words.n2w 1)) =
  words.word_2comp (words.n2w 1)

1 < fcp.dimindex bool.the_value 0 < words.INT_MAX bool.the_value

n.
    words.word_reverse (words.n2w n) =
    words.n2w (bit.BIT_REVERSE (fcp.dimindex bool.the_value) n)

n.
    n mod words.dimword bool.the_value =
    bit.MOD_2EXP (fcp.dimindex bool.the_value) n

v.
    words.w2n (bitstring.v2w v) =
    bit.MOD_2EXP (fcp.dimindex bool.the_value) (bitstring.v2n v)

f. fcp.FCP f = words.word_modify (λi b. f i) (words.n2w 0)

w.
    words.word_1comp w = words.word_sub (words.word_2comp w) (words.n2w 1)

w.
    words.word_2comp w =
    words.n2w (arithmetic.- (words.dimword bool.the_value) (words.w2n w))

w.
    words.word_2comp w = words.word_add (words.word_1comp w) (words.n2w 1)

w.
    words.word_2comp w = words.word_mul (words.word_2comp (words.n2w 1)) w

n. words.word_ls n (words.n2w 0) n = words.n2w 0

w. words.bit_count w = 0 w = words.n2w 0

w. words.w2n w = 0 w = words.n2w 0

P. (f. P (fcp.mk_cart f)) f. P f

f. g. h. g (fcp.mk_cart h) = f h

x x1. words.BIT_SET x x1 = words.BIT_SET_tupled (x, x1)

h l. words.word_bits h l (words.n2w 0) = words.n2w 0

h l. words.word_extract h l (words.n2w 0) = words.n2w 0

l h. words.word_slice h l (words.n2w 0) = words.n2w 0

n v. bitstring.zero_extend n v = list.PAD_LEFT n v

b l. words.l2w b l = words.n2w (numposrep.l2n b l)

b w. words.w2l b w = numposrep.n2l b (words.w2n w)

n w. bitstring.testbit n (bitstring.w2v w) words.word_bit n w

x x1. bitstring.bitify x x1 = bitstring.bitify_tupled (x, x1)

P v. fcp.FCP_EVERY P v all P (fcp.V2L v)

P v. fcp.FCP_EXISTS P v any P (fcp.V2L v)

x x1. sum_num.GSUM x x1 = sum_num.GSUM_tupled (x, x1)

x i. fcp.fcp_index x i = fcp.dest_cart x (fcp.finite_index i)

m a. fcp.:+ a (fcp.fcp_index m a) m = m

w n. words.word_ror w (n * fcp.dimindex bool.the_value) = w

a b. ¬(words.word_lo a b words.word_lo b a)

a b. ¬(words.word_lo a b words.word_ls b a)

a b. ¬(words.word_lt a b words.word_le b a)

a b. ¬(words.word_lt a b words.word_lt b a)

w n. words.word_asr_bv w n = words.word_asr w (words.w2n n)

w n. words.word_lsl_bv w n = words.word_lsl w (words.w2n n)

w n. words.word_lsr_bv w n = words.word_lsr w (words.w2n n)

a b. words.word_nand a b = words.word_1comp (words.word_and a b)

a b. words.word_nor a b = words.word_1comp (words.word_or a b)

w n. words.word_rol_bv w n = words.word_rol w (words.w2n n)

w n. words.word_ror_bv w n = words.word_ror w (words.w2n n)

v w. words.word_sub v w = words.word_add v (words.word_2comp w)

a b. words.word_xnor a b = words.word_1comp (words.word_xor a b)

a b. a = b ¬words.word_lo a b

a b. a = b ¬words.word_lt a b

a b. words.word_lo a b ¬(a = b)

a b. words.word_lt a b ¬(a = b)

a b. ¬words.word_gt a b words.word_le a b

a b. ¬words.word_hi a b words.word_ls a b

a b. ¬words.word_le a b words.word_lt b a

a b. ¬words.word_lo a b words.word_ls b a

a b. ¬words.word_ls a b words.word_lo b a

a b. ¬words.word_lt a b words.word_le b a

w v. words.word_2comp (words.word_sub v w) = words.word_sub w v

v w. words.word_sub v (words.word_2comp w) = words.word_add v w

v w. words.word_add (words.word_2comp w) v = words.word_sub v w

v x. words.word_sub v (words.word_add v x) = words.word_2comp x

w v. words.word_sub (words.word_sub v w) v = words.word_2comp w

v w. words.word_concat v w = words.w2w (words.word_join v w)

words.word_L2 =
  if 1 < fcp.dimindex bool.the_value then words.n2w 0 else words.word_L

fcp.dimindex bool.the_value = arithmetic.BIT2 63

words.dimword bool.the_value = arithmetic.BIT2 63

words.INT_MIN bool.the_value =
  arithmetic.BIT2 0 arithmetic.- (fcp.dimindex bool.the_value) 1

words.INT_MIN bool.the_value = arithmetic.BIT2 63

words.word_msb (words.n2w n)
  words.INT_MIN bool.the_value n mod words.dimword bool.the_value

fcp.dimindex bool.the_value = fcp.dimindex bool.the_value
  words.dimword bool.the_value = words.dimword bool.the_value

fcp.dimindex bool.the_value = fcp.dimindex bool.the_value
  words.INT_MAX bool.the_value = words.INT_MAX bool.the_value

fcp.dimindex bool.the_value = fcp.dimindex bool.the_value
  words.INT_MIN bool.the_value = words.INT_MIN bool.the_value

fcp.dimindex bool.the_value = fcp.dimindex bool.the_value
  words.UINT_MAX bool.the_value = words.UINT_MAX bool.the_value

fcp.dimindex bool.the_value < fcp.dimindex bool.the_value
  words.dimword bool.the_value < words.dimword bool.the_value

fcp.dimindex bool.the_value < fcp.dimindex bool.the_value
  words.INT_MAX bool.the_value < words.INT_MAX bool.the_value

fcp.dimindex bool.the_value < fcp.dimindex bool.the_value
  words.INT_MIN bool.the_value < words.INT_MIN bool.the_value

fcp.dimindex bool.the_value < fcp.dimindex bool.the_value
  words.UINT_MAX bool.the_value < words.UINT_MAX bool.the_value

fcp.dimindex bool.the_value fcp.dimindex bool.the_value
  words.dimword bool.the_value words.dimword bool.the_value

fcp.dimindex bool.the_value fcp.dimindex bool.the_value
  words.INT_MAX bool.the_value words.INT_MAX bool.the_value

fcp.dimindex bool.the_value fcp.dimindex bool.the_value
  words.INT_MIN bool.the_value words.INT_MIN bool.the_value

fcp.dimindex bool.the_value fcp.dimindex bool.the_value
  words.UINT_MAX bool.the_value words.UINT_MAX bool.the_value

words.w2n (words.word_2comp (words.n2w 1)) =
  arithmetic.- (words.dimword bool.the_value) 1

(p. alignment.aligned p (words.n2w 0)) w. alignment.aligned 0 w

n. words.n2w (suc n) = words.word_add (words.n2w n) (words.n2w 1)

n.
    words.word_log2 (words.n2w n) =
    words.n2w (bit.LOG2 (n mod words.dimword bool.the_value))

i. i < fcp.dimindex bool.the_value ¬fcp.fcp_index (words.n2w 0) i

v.
    words.word_1comp (bitstring.v2w v) =
    bitstring.v2w
      (bitstring.bnot (bitstring.fixwidth (fcp.dimindex bool.the_value) v))

v.
    words.word_reverse (bitstring.v2w v) =
    bitstring.v2w
      (reverse (bitstring.fixwidth (fcp.dimindex bool.the_value) v))

w.
    words.word_msb w
    fcp.fcp_index w (arithmetic.- (fcp.dimindex bool.the_value) 1)

w.
    words.word_le (words.n2w 0) w
    words.w2n w < words.INT_MIN bool.the_value

w. fcp.dimindex bool.the_value = 1 words.word_2comp w = w

a v. fcp.FCP_CONS a v = fcp.L2V (a :: fcp.V2L v)

i n. bit.BIT i n bool.IN i (words.BIT_SET 0 n)

h l. words.word_extract h l = words.w2w words.word_bits h l

n v. bitstring.sign_extend n v = list.PAD_LEFT (head v) n v

h v. bitstring.field h 0 v = bitstring.fixwidth (suc h) v

n v.
    words.word_lsl (bitstring.v2w v) n =
    bitstring.v2w (bitstring.shiftl v n)

n v.
    bitstring.fixwidth n (bitstring.fixwidth n v) = bitstring.fixwidth n v

m f. sum_num.SUM m f = sum_num.GSUM (0, m) f

m f. sum_num.GSUM (m, 1) f = f m

p w.
    alignment.aligned p (words.word_mul (words.word_lsl (words.n2w 1) p) w)

p w. alignment.aligned p w alignment.align p w = w

p w.
    alignment.align p w = words.word_and w (words.word_lsl words.word_T p)

p w. alignment.align p w = words.word_lsl (words.word_lsr w p) p

n w.
    words.word_replicate n w =
    words.concat_word_list (list.GENLIST (const w) n)

p w. alignment.aligned p w alignment.align p w = w

n a.
    words.word_lsl (words.word_2comp a) n =
    words.word_2comp (words.word_lsl a n)

h w. words.word_slice h 0 w = words.word_bits h 0 w

p w. alignment.align p (alignment.align p w) = alignment.align p w

v n. bitstring.replicate v n = concat (list.GENLIST (const v) n)

v n. length (bitstring.shiftr v n) = arithmetic.- (length v) n

v i. length v i ¬bitstring.testbit i v

f v. fcp.FCP_MAP f v = fcp.L2V (map f (fcp.V2L v))

a b. words.word_hi a b words.w2n a > words.w2n b

a b. words.word_hs a b words.w2n a words.w2n b

a b. words.word_lo a b words.w2n a < words.w2n b

a b. words.word_ls a b words.w2n a words.w2n b

w v. words.word_2comp v = w v = words.word_2comp w

v w.
    words.word_2comp (words.word_mul v w) =
    words.word_mul v (words.word_2comp w)

v w.
    words.word_2comp (words.word_mul v w) =
    words.word_mul (words.word_2comp v) w

%%genvar%%50991 b.
    words.word_abs (words.word_sub %%genvar%%50991 b) =
    words.word_abs (words.word_sub b %%genvar%%50991)

v w.
    words.word_sub (words.word_2comp v) w =
    words.word_2comp (words.word_add v w)

v w. words.w2n v = words.w2n w v = w

v w. words.word_2comp v = words.word_2comp w v = w

v w.
    words.word_sub (words.word_2comp v) (words.word_2comp w) =
    words.word_sub w v

w. n. w = words.n2w n n < words.dimword bool.the_value

words.dimword bool.the_value = arithmetic.BIT2 127

words.INT_MIN bool.the_value = arithmetic.BIT2 127

fcp.FCP (const ) = words.word_T fcp.FCP (const ) = words.n2w 0

n.
    words.saturate_n2w n =
    if words.dimword bool.the_value n then words.word_T else words.n2w n

n.
    words.word_msb (words.n2w n)
    bit.BIT (arithmetic.- (fcp.dimindex bool.the_value) 1) n

n.
    words.word_mul (words.n2w n) words.word_L =
    if even n then words.n2w 0 else words.word_L

i.
    i < fcp.dimindex bool.the_value
    fcp.fcp_index (words.word_2comp (words.n2w 1)) i

n. words.word_lsl (words.n2w 1) n = words.n2w (arithmetic.BIT2 0 n)

x. fcp.dimindex bool.the_value = length x fcp.V2L (fcp.L2V x) = x

v. words.word_lsb (bitstring.v2w v) ¬(v = []) last v

v.
    words.word_msb (bitstring.v2w v)
    bitstring.testbit (arithmetic.- (fcp.dimindex bool.the_value) 1) v

f v. fcp.FCP_MAP f v = fcp.FCP (λi. f (fcp.fcp_index v i))

w.
    words.word_abs w =
    if words.word_lt w (words.n2w 0) then words.word_2comp w else w

w.
    words.sw2sw w =
    words.n2w
      (bit.SIGN_EXTEND (fcp.dimindex bool.the_value)
         (fcp.dimindex bool.the_value) (words.w2n w))

w.
    words.w2w w =
    words.word_extract (arithmetic.- (fcp.dimindex bool.the_value) 1) 0 w

m n. words.word_add (words.n2w m) (words.n2w n) = words.n2w (m + n)

m n. words.word_mul (words.n2w m) (words.n2w n) = words.n2w (m * n)

%%genvar%%1829 w.
    %%genvar%%1829 = length w bitstring.fixwidth %%genvar%%1829 w = w

n.
    bitstring.rev_count_list n =
    list.GENLIST (λi. arithmetic.- (arithmetic.- n 1) i) n

v m. bitstring.shiftr v m = list.TAKE (arithmetic.- (length v) m) v

v w.
    words.word_and (bitstring.v2w v) (bitstring.v2w w) =
    bitstring.v2w (bitstring.band v w)

v w.
    words.word_or (bitstring.v2w v) (bitstring.v2w w) =
    bitstring.v2w (bitstring.bor v w)

v w.
    words.word_xor (bitstring.v2w v) (bitstring.v2w w) =
    bitstring.v2w (bitstring.bxor v w)

v l. length (bitstring.bitify l v) = length l + length v

w n.
    words.word_rol w (n mod fcp.dimindex bool.the_value) =
    words.word_rol w n

w n.
    words.word_ror w (n mod fcp.dimindex bool.the_value) =
    words.word_ror w n

a b.
    words.saturate_add a b = words.saturate_n2w (words.w2n a + words.w2n b)

a b.
    words.saturate_mul a b = words.saturate_n2w (words.w2n a * words.w2n b)

a b.
    words.saturate_sub a b =
    words.n2w (arithmetic.- (words.w2n a) (words.w2n b))

v w. words.word_add v w = words.n2w (words.w2n v + words.w2n w)

v w. words.word_div v w = words.n2w (words.w2n v div words.w2n w)

a b. words.word_max a b = if words.word_lo a b then b else a

a b. words.word_min a b = if words.word_lo a b then a else b

v w. words.word_mod v w = words.n2w (words.w2n v mod words.w2n w)

v w. words.word_mul v w = words.n2w (words.w2n v * words.w2n w)

a b. words.word_smax a b = if words.word_lt a b then b else a

a b. words.word_smin a b = if words.word_lt a b then a else b

v w.
    words.word_2comp (words.word_add v w) =
    words.word_add (words.word_2comp v) (words.word_2comp w)

v w. words.word_add v w = v w = words.n2w 0

v w. words.word_add v w = w v = words.n2w 0

b a. words.word_sub a b = words.n2w 0 a = b

w.
    words.w2n w =
    sum_num.SUM (fcp.dimindex bool.the_value)
      (λi. bit.SBIT (fcp.fcp_index w i) i)

fcp.dimindex bool.the_value =
  if pred_set.FINITE pred_set.UNIV then
    arithmetic.BIT2 0 * fcp.dimindex bool.the_value
  else 1

words.dimword bool.the_value = arithmetic.BIT2 255

words.INT_MIN bool.the_value = arithmetic.BIT2 255

h l w. words.word_bits h l w = words.word_extract h l w

n.
    words.word_2comp (words.n2w n) =
    words.n2w
      (arithmetic.- (words.dimword bool.the_value)
         (n mod words.dimword bool.the_value))

n.
    words.word_lsl words.word_T n =
    words.n2w
      (arithmetic.- (words.dimword bool.the_value) (arithmetic.BIT2 0 n))

i. i < fcp.dimindex bool.the_value fcp.fcp_index (fcp.FCP g) i = g i

n.
    words.word_mul (words.word_2comp (words.n2w n)) words.word_L =
    if even n then words.n2w 0 else words.word_L

bb. (a. bb = fcp.BIT0A a) a. bb = fcp.BIT0B a

w.
    words.reduce_and w =
    if w = words.word_T then words.n2w 1 else words.n2w 0

a.
    ¬words.word_msb a
    a = words.n2w 0 words.word_msb (words.word_2comp a)

w.
    ¬(w = words.n2w 0)
    bit.LOG2 (words.w2n w) < fcp.dimindex bool.the_value

f w. words.word_modify f w = fcp.FCP (λi. f i (fcp.fcp_index w i))

words.n2w_itself =
  relation.WFREC (select R. wellFounded R)
    (λn2w_itself a. pair.pair_CASE a (λn v1. id (words.n2w n)))

a b. a b words.n2w (arithmetic.- a b) = words.n2w 0

n v. length v < n length (bitstring.sign_extend n v) = n

n v. length v < n length (bitstring.zero_extend n v) = n

n w.
    words.word_sign_extend n w =
    words.n2w
      (bit.SIGN_EXTEND n (fcp.dimindex bool.the_value) (words.w2n w))

v n. bitstring.shiftl v n = v @ bitstring.replicate ( :: []) n

v m. bitstring.shiftl v m = list.PAD_RIGHT (length v + m) v

s n. fcp.HAS_SIZE s n pred_set.FINITE s pred_set.CARD s = n

a n.
    words.word_lsl a n =
    words.word_mul (words.n2w (arithmetic.BIT2 0 n)) a

w n. fcp.dimindex bool.the_value n words.word_lsl w n = words.n2w 0

w n. fcp.dimindex bool.the_value n words.word_lsr w n = words.n2w 0

a b. words.word_ge a b words.word_gt a b a = b

a b. words.word_hs a b words.word_hi a b a = b

a b. words.word_le a b words.word_lt a b a = b

a b. words.word_ls a b words.word_lo a b a = b

a b. a = b words.word_lo a b words.word_lo b a

a b. a = b words.word_lt a b words.word_lt b a

%%genvar%%32444 b.
    words.word_add %%genvar%%32444 b = words.n2w 0
    %%genvar%%32444 = words.word_2comp b

a b. words.word_le a b words.word_le b a a = b

a b. words.word_ls a b words.word_ls b a a = b

w.
    v.
      w = bitstring.v2w v
      marker.Abbrev (length v = fcp.dimindex bool.the_value)

f n.
    words.word_modify f (words.n2w n) =
    words.n2w (bit.BIT_MODIFY (fcp.dimindex bool.the_value) f n)

words.dimword bool.the_value = arithmetic.BIT2 511

words.INT_MIN bool.the_value = arithmetic.BIT2 511

(x. fcp.IS_BIT0A (fcp.BIT0A x) ) x. fcp.IS_BIT0A (fcp.BIT0B x)

(x. fcp.IS_BIT0B (fcp.BIT0A x) ) x. fcp.IS_BIT0B (fcp.BIT0B x)

words.word_join (words.word_2comp (words.n2w 1))
    (words.word_2comp (words.n2w 1)) = words.word_2comp (words.n2w 1)

h l v. length (bitstring.field h l v) = arithmetic.- (suc h) l

b f s. words.s2w b f s = words.n2w (ASCIInumbers.s2n b f s)

b f w. words.w2s b f w = ASCIInumbers.n2s b f (words.w2n w)

n.
    n mod words.dimword bool.the_value =
    bit.BITS (arithmetic.- (fcp.dimindex bool.the_value) 1) 0 n

w.
    alignment.byte_aligned w
    alignment.aligned
      (bit.LOG2 (fcp.dimindex bool.the_value div arithmetic.BIT2 3)) w

w.
    alignment.byte_align w =
    alignment.align
      (bit.LOG2 (fcp.dimindex bool.the_value div arithmetic.BIT2 3)) w

w.
    words.reduce_or w =
    if w = words.n2w 0 then words.n2w 0 else words.n2w 1

w.
    words.w2w (words.w2w w) =
    words.w2w
      (words.word_bits (arithmetic.- (fcp.dimindex bool.the_value) 1) 0 w)

f i v. fcp.FCP_FOLD f i v = list.FOLDL f i (fcp.V2L v)

n x. fcp.:+ n x = words.word_modify (λi b. if i = n then x else b)

b v. bitstring.testbit b v bitstring.field b b v = :: []

n v.
    words.word_lsr (bitstring.v2w v) n =
    bitstring.v2w
      (bitstring.shiftr
         (bitstring.fixwidth (fcp.dimindex bool.the_value) v) n)

n v.
    words.word_ror (bitstring.v2w v) n =
    bitstring.v2w
      (bitstring.rotate
         (bitstring.fixwidth (fcp.dimindex bool.the_value) v) n)

%%genvar%%6184 v.
    suc %%genvar%%6184 = length v bitstring.field %%genvar%%6184 0 v = v

p w.
    alignment.aligned p w
    words.bit_count_upto (min (fcp.dimindex bool.the_value) p) w = 0

b w. words.word_bit b w words.word_bits b b w = words.n2w 1

p w.
    alignment.align p w =
    words.word_slice (arithmetic.- (fcp.dimindex bool.the_value) 1) p w

b w. 1 < b words.l2w b (words.w2l b w) = w

w n.
    words.word_lsr w n =
    words.word_bits (arithmetic.- (fcp.dimindex bool.the_value) 1) n w

w m.
    words.w2n (words.word_lsr w m) = words.w2n w div arithmetic.BIT2 0 m

w b.
    b < fcp.dimindex bool.the_value
    (fcp.fcp_index w b words.word_bit b w)

w.
    words.word_reverse w =
    fcp.FCP
      (λi.
         fcp.fcp_index w
           (arithmetic.- (arithmetic.- (fcp.dimindex bool.the_value) 1) i))

w.
    ¬(w = words.n2w 0)
    while.LEAST (λi. fcp.fcp_index w i) < fcp.dimindex bool.the_value

f v.
    words.word_modify f (bitstring.v2w v) =
    bitstring.v2w
      (bitstring.modify f
         (bitstring.fixwidth (fcp.dimindex bool.the_value) v))

P. (n. P (n, bool.the_value)) v v1. P (v, v1)

words.dimword bool.the_value = arithmetic.BIT2 1023

words.INT_MIN bool.the_value = arithmetic.BIT2 1023

words.word_concat (words.word_2comp (words.n2w 1))
    (words.word_2comp (words.n2w 1)) =
  words.w2w (words.word_2comp (words.n2w 1))

h v.
    fcp.FCP_CONS h v =
    fcp.:+ 0 h (fcp.FCP (λi. fcp.fcp_index v (prim_rec.PRE i)))

h l w. h < l words.word_bits h l w = words.n2w 0

h l w. h < l words.word_slice h l w = words.n2w 0

h l w. h < l words.word_extract h l w = words.n2w 0

h l w. words.word_slice h l w = words.word_lsl (words.word_bits h l w) l

p q w. p < q alignment.aligned q w alignment.aligned p w

a b.
    fcp.FCP_ZIP a b = fcp.FCP (λi. (fcp.fcp_index a i, fcp.fcp_index b i))

w m n. words.word_asr (words.word_asr w m) n = words.word_asr w (m + n)

w m n. words.word_lsl (words.word_lsl w m) n = words.word_lsl w (m + n)

w m n. words.word_lsr (words.word_lsr w m) n = words.word_lsr w (m + n)

w m n. words.word_rol (words.word_rol w m) n = words.word_rol w (m + n)

w m n. words.word_ror (words.word_ror w m) n = words.word_ror w (m + n)

%%genvar%%32412 w x.
    %%genvar%%32412 = words.word_sub w x
    words.word_add %%genvar%%32412 x = w

v w x. words.word_add v w = x v = words.word_sub x w

v w x. words.word_sub v w = x v = words.word_add x w

v w x.
    words.word_add v (words.word_add w x) =
    words.word_add (words.word_add v w) x

v w x.
    words.word_mul v (words.word_mul w x) =
    words.word_mul (words.word_mul v w) x

v w x.
    words.word_sub v (words.word_add w x) =
    words.word_sub (words.word_sub v w) x

v w x.
    words.word_sub v (words.word_sub w x) =
    words.word_sub (words.word_add v x) w

a b c.
    words.word_and (words.word_and a b) c =
    words.word_and a (words.word_and b c)

a b c.
    words.word_or (words.word_or a b) c =
    words.word_or a (words.word_or b c)

v w x.
    words.word_sub (words.word_add v w) x =
    words.word_add v (words.word_sub w x)

v w x.
    words.word_sub (words.word_add v w) x =
    words.word_add (words.word_sub v x) w

a b c.
    words.word_xor (words.word_xor a b) c =
    words.word_xor a (words.word_xor b c)

v w x. words.word_add v w = words.word_add v x w = x

v w x. words.word_add v w = words.word_add x w v = x

v w x. words.word_sub v w = words.word_sub v x w = x

v w x. words.word_sub v w = words.word_sub x w v = x

v w x.
    words.word_add (words.word_sub v w) (words.word_sub w x) =
    words.word_sub v x

a b c. words.word_le a b words.word_le b c words.word_le a c

a b c. words.word_le a b words.word_lt b c words.word_lt a c

a b c. words.word_lo a b words.word_lo b c words.word_lo a c

a b c. words.word_lo a b words.word_ls b c words.word_lo a c

a b c. words.word_ls a b words.word_lo b c words.word_lo a c

a b c. words.word_ls a b words.word_ls b c words.word_ls a c

a b c. words.word_lt a b words.word_le b c words.word_lt a c

a b c. words.word_lt a b words.word_lt b c words.word_lt a c

x y.
    words.word_add x y =
    fcp.FCP (λi. blast.BSUM i (fcp.fcp_index x) (fcp.fcp_index y) )

v w.
    words.word_and v w =
    fcp.FCP (λi. fcp.fcp_index v i fcp.fcp_index w i)

v w.
    words.word_or v w = fcp.FCP (λi. fcp.fcp_index v i fcp.fcp_index w i)

v w.
    words.word_xnor v w =
    fcp.FCP (λi. fcp.fcp_index v i fcp.fcp_index w i)

fcp.finite_index =
  select f. x. ∃!n. n < fcp.dimindex bool.the_value f n = x

n i.
    i < fcp.dimindex bool.the_value
    (fcp.fcp_index (words.n2w n) i bit.BIT i n)

n m.
    words.word_and (words.n2w n) (words.n2w m) =
    words.n2w (bit.BITWISE (fcp.dimindex bool.the_value) () n m)

n m.
    words.word_or (words.n2w n) (words.n2w m) =
    words.n2w (bit.BITWISE (fcp.dimindex bool.the_value) () n m)

n m.
    words.word_xnor (words.n2w n) (words.n2w m) =
    words.n2w (bit.BITWISE (fcp.dimindex bool.the_value) () n m)

i a.
    i < fcp.dimindex bool.the_value
    fcp.fcp_index (fcp.L2V a) i = list.EL i a

n v.
    words.word_bit n (bitstring.v2w v)
    n < fcp.dimindex bool.the_value bitstring.testbit n v

n f.
    sum_num.SUM n f = list.FOLDL (λx n. f n + x) 0 (rich_list.COUNT_LIST n)

i v.
    i < fcp.dimindex bool.the_value
    list.EL i (fcp.V2L v) = fcp.fcp_index v i

p w.
    fcp.dimindex bool.the_value p
    (alignment.aligned p w w = words.n2w 0)

w n.
    words.word_rol w n =
    words.word_ror w
      (arithmetic.- (fcp.dimindex bool.the_value)
         (n mod fcp.dimindex bool.the_value))

a b.
    words.saturate_sub a b =
    if words.word_ls a b then words.n2w 0 else words.word_sub a b

a b.
    words.word_xor a b =
    words.word_or (words.word_and a (words.word_1comp b))
      (words.word_and b (words.word_1comp a))

a b. words.word_compare a b = if a = b then words.n2w 1 else words.n2w 0

a b. ¬words.word_lo a b ¬(a = b) words.word_lo b a

a b. ¬words.word_lt a b ¬(a = b) words.word_lt b a

P. (a. P (fcp.BIT0A a)) (a. P (fcp.BIT0B a)) bb. P bb

f v.
    bitstring.modify f v =
    map (pair.UNCURRY f)
      (list.ZIP (bitstring.rev_count_list (length v), v))

fcp.dimindex bool.the_value =
  if pred_set.FINITE pred_set.UNIV then
    arithmetic.BIT2 0 * fcp.dimindex bool.the_value + 1
  else 1

fcp.dimindex bool.the_value =
  if pred_set.FINITE pred_set.UNIV pred_set.FINITE pred_set.UNIV then
    fcp.dimindex bool.the_value + fcp.dimindex bool.the_value
  else 1

words.dimword bool.the_value = arithmetic.BIT2 2047

words.INT_MIN bool.the_value =
  if pred_set.FINITE pred_set.UNIV pred_set.FINITE pred_set.UNIV then
    words.dimword bool.the_value * words.INT_MIN bool.the_value
  else words.INT_MIN bool.the_value

(w. words.word_add w (words.n2w 0) = w)
  w. words.word_add (words.n2w 0) w = w

x y c. blast.bsum x y c (x ¬y) ¬c

n c l. bitstring.extend c (suc n) l = c :: bitstring.extend c n l

h l v.
    words.word_extract h l (bitstring.v2w v) =
    words.w2w (words.word_bits h l (bitstring.v2w v))

h l w.
    fcp.dimindex bool.the_value l words.word_bits h l w = words.n2w 0

h l w.
    fcp.dimindex bool.the_value l
    words.word_extract h l w = words.n2w 0

h l w.
    words.word_bits h l (words.word_slice h l w) = words.word_bits h l w

n l c.
    list.PAD_LEFT c n l = bitstring.extend c (arithmetic.- n (length l)) l

n w.
    words.bit_count_upto n w =
    sum_num.SUM n (λi. if fcp.fcp_index w i then 1 else 0)

n.
    words.word_1comp (words.n2w n) =
    words.n2w
      (arithmetic.- (arithmetic.- (words.dimword bool.the_value) 1)
         (n mod words.dimword bool.the_value))

n.
    n < words.dimword bool.the_value
    bit.BITS (arithmetic.- (fcp.dimindex bool.the_value) 1) 0 n = n

v a. bitstring.boolify a v = reverse (map (λn. ¬(n = 0)) v) @ a

m a v. fcp.fcp_index m a = v fcp.:+ a v m = m

w n.
    words.word_ror w n =
    fcp.FCP (λi. fcp.fcp_index w ((i + n) mod fcp.dimindex bool.the_value))

v w.
    words.word_nand v w =
    fcp.FCP (λi. ¬(fcp.fcp_index v i fcp.fcp_index w i))

v w.
    words.word_nor v w =
    fcp.FCP (λi. ¬(fcp.fcp_index v i fcp.fcp_index w i))

v w.
    words.word_xor v w =
    fcp.FCP (λi. ¬(fcp.fcp_index v i fcp.fcp_index w i))

m.
    ¬(m = words.n2w 0)
    words.w2n (words.word_sub m (words.n2w 1)) < words.w2n m

fcp.FCP =
  λg.
    select f. i. i < fcp.dimindex bool.the_value fcp.fcp_index f i = g i

a b.
    fcp.:+ a b = λm. fcp.FCP (λc. if a = c then b else fcp.fcp_index m c)

a b.
    b a
    words.n2w (arithmetic.- a b) =
    words.word_sub (words.n2w a) (words.n2w b)

b l.
    words.w2l b (words.l2w b l) =
    numposrep.n2l b (numposrep.l2n b l mod words.dimword bool.the_value)

i a.
    i < fcp.dimindex bool.the_value
    fcp.fcp_index (fcp.FCP_TL a) i = fcp.fcp_index a (suc i)

v n.
    words.word_mul v (words.n2w (n + 1)) =
    words.word_add (words.word_mul v (words.n2w n)) v

w h.
    arithmetic.- (fcp.dimindex bool.the_value) 1 h
    words.word_bits h 0 w = w

a b.
    words.word_hs a b
    bool.LET (pair.UNCURRY (λn. pair.UNCURRY (λz. pair.UNCURRY (λp q. p))))
      (words.nzcv a b)

a b.
    words.saturate_add a b =
    if words.word_ls (words.word_sub words.word_T a) b then words.word_T
    else words.word_add a b

x y.
    words.word_ls y x
    words.w2n (words.word_sub x y) =
    arithmetic.- (words.w2n x) (words.w2n y)

a b.
    fcp.fcp_index (words.word_add a b) 0
    ¬(fcp.fcp_index a 0 fcp.fcp_index b 0)

a b.
    words.word_and a b = words.n2w 0
    words.word_add a b = words.word_or a b

a b.
    words.word_and a b = words.n2w 0
    words.word_add a b = words.word_xor a b

x y.
    words.word_lt (words.n2w 0) y words.word_lt y x
    words.word_lt (words.word_sub x y) x

w.
    bitstring.w2v w =
    list.GENLIST
      (λi.
         fcp.fcp_index w
           (arithmetic.- (arithmetic.- (fcp.dimindex bool.the_value) 1) i))
      (fcp.dimindex bool.the_value)

w.
    w = words.n2w 0
    i. i < fcp.dimindex bool.the_value ¬fcp.fcp_index w i

w.
    ¬(w = words.word_T)
    i. i < fcp.dimindex bool.the_value ¬fcp.fcp_index w i

w.
    ¬(w = words.n2w 0)
    i. i < fcp.dimindex bool.the_value fcp.fcp_index w i

words.INT_MAX bool.the_value < words.INT_MIN bool.the_value
  words.INT_MIN bool.the_value words.UINT_MAX bool.the_value
  words.UINT_MAX bool.the_value < words.dimword bool.the_value

h l v.
    bitstring.field h l v =
    bitstring.fixwidth (arithmetic.- (suc h) l) (bitstring.shiftr v l)

h l w.
    words.w2n (words.word_bits h l w) <
    arithmetic.BIT2 0 arithmetic.- (suc h) l

h l w.
    words.w2n (words.word_extract h l w) <
    arithmetic.BIT2 0 arithmetic.- (suc h) l

n a b.
    words.word_lsl (words.word_add a b) n =
    words.word_add (words.word_lsl a n) (words.word_lsl b n)

n.
    n < fcp.dimindex bool.the_value
    (fcp.fcp_index words.word_H n
     n < arithmetic.- (fcp.dimindex bool.the_value) 1)

n.
    n < fcp.dimindex bool.the_value
    (fcp.fcp_index words.word_L n
     n = arithmetic.- (fcp.dimindex bool.the_value) 1)

x.
    pred_set.FINITE pred_set.UNIV x < words.dimword bool.the_value
    words.word_concat (words.n2w 0) (words.n2w x) = words.n2w x

v a. bitstring.bitify a v = reverse (map (λb. if b then 1 else 0) v) @ a

bb. (a. bb = fcp.BIT1A a) (a. bb = fcp.BIT1B a) bb = fcp.BIT1C

P v.
    fcp.FCP_EVERY P v
    i. fcp.dimindex bool.the_value i P (fcp.fcp_index v i)

P v.
    fcp.FCP_EXISTS P v
    i. i < fcp.dimindex bool.the_value P (fcp.fcp_index v i)

a b c.
    words.word_and a (words.word_or b c) =
    words.word_or (words.word_and a b) (words.word_and a c)

a b c.
    words.word_and a (words.word_xor b c) =
    words.word_xor (words.word_and a b) (words.word_and a c)

v w x.
    words.word_mul v (words.word_add w x) =
    words.word_add (words.word_mul v w) (words.word_mul v x)

v w x.
    words.word_mul v (words.word_sub w x) =
    words.word_sub (words.word_mul v w) (words.word_mul v x)

a b c.
    words.word_or a (words.word_and b c) =
    words.word_and (words.word_or a b) (words.word_or a c)

a b c.
    words.word_and (words.word_or a b) c =
    words.word_or (words.word_and a c) (words.word_and b c)

a b c.
    words.word_and (words.word_xor a b) c =
    words.word_xor (words.word_and a c) (words.word_and b c)

v w x.
    words.word_mul (words.word_add v w) x =
    words.word_add (words.word_mul v x) (words.word_mul w x)

v w x.
    words.word_mul (words.word_sub w x) v =
    words.word_sub (words.word_mul w v) (words.word_mul x v)

a b c.
    words.word_or (words.word_and a b) c =
    words.word_and (words.word_or a c) (words.word_or b c)

x y.
    words.word_sub x y =
    fcp.FCP (λi. blast.BSUM i (fcp.fcp_index x) ((¬) fcp.fcp_index y) )

x.
    ¬(x = words.n2w 0)
    suc (words.w2n (words.word_sub x (words.n2w 1))) = words.w2n x

a. fcp.dimindex bool.the_value = 1 a = words.n2w 0 a = words.n2w 1

(a. fcp.mk_cart (fcp.dest_cart a) = a)
  r. (let f r in ) fcp.dest_cart (fcp.mk_cart r) = r

n i.
    i < n
    list.EL i (bitstring.rev_count_list n) =
    arithmetic.- (arithmetic.- n 1) i

m n.
    words.n2w m = words.n2w n
    m mod words.dimword bool.the_value = n mod words.dimword bool.the_value

a b.
    words.word_hi (words.n2w a) (words.n2w b)
    a mod words.dimword bool.the_value > b mod words.dimword bool.the_value

a b.
    words.word_hs (words.n2w a) (words.n2w b)
    a mod words.dimword bool.the_value b mod words.dimword bool.the_value

a b.
    words.word_lo (words.n2w a) (words.n2w b)
    a mod words.dimword bool.the_value < b mod words.dimword bool.the_value

a b.
    words.word_ls (words.n2w a) (words.n2w b)
    a mod words.dimword bool.the_value b mod words.dimword bool.the_value

b w.
    words.word_bit b w
    b arithmetic.- (fcp.dimindex bool.the_value) 1 fcp.fcp_index w b

h w.
    arithmetic.- (fcp.dimindex bool.the_value) 1 h
    words.word_extract h 0 w = words.w2w w

v w.
    bitstring.v2w v = bitstring.v2w w
    bitstring.fixwidth (fcp.dimindex bool.the_value) v =
    bitstring.fixwidth (fcp.dimindex bool.the_value) w

m a b c. fcp.:+ a c (fcp.:+ a b m) = fcp.:+ a c m

w n.
    fcp.dimindex bool.the_value n
    words.word_asr w n =
    if words.word_msb w then words.word_T else words.n2w 0

w n.
    words.word_rol (words.word_ror w n) n = w
    words.word_ror (words.word_rol w n) n = w

w h.
    words.w2n w < arithmetic.BIT2 0 suc h words.word_extract h 0 w = w

x y.
    words.word_lo x y
    ¬blast.BCARRY (fcp.dimindex bool.the_value) (fcp.fcp_index x)
        ((¬) fcp.fcp_index y)

a b.
    words.word_lo a b
    bool.LET
      (pair.UNCURRY (λn. pair.UNCURRY (λz. pair.UNCURRY (λc v. ¬c))))
      (words.nzcv a b)

x n a.
    length (list.PAD_LEFT x n a) = if length a < n then n else length a

x n a.
    length (list.PAD_RIGHT x n a) = if length a < n then n else length a

x y c. blast.bcarry x y c x y (x y) c

h l v.
    words.word_bits h l (bitstring.v2w v) =
    bitstring.v2w
      (bitstring.field h l
         (bitstring.fixwidth (fcp.dimindex bool.the_value) v))

h a b. length b = suc h bitstring.field h 0 (a @ b) = b

n f. (m. m < n f m = 0) sum_num.SUM n f = 0

n w. words.bit_count_upto n w = 0 i. i < n ¬fcp.fcp_index w i

v.
    words.w2w (bitstring.v2w v) =
    bitstring.v2w
      (bitstring.fixwidth
         (if fcp.dimindex bool.the_value < fcp.dimindex bool.the_value then
            fcp.dimindex bool.the_value
          else fcp.dimindex bool.the_value) v)

w.
    words.saturate_w2w w =
    if fcp.dimindex bool.the_value fcp.dimindex bool.the_value
       words.word_ls (words.w2w words.word_T) w
    then words.word_T
    else words.w2w w

a b f. fcp.:+ x y (fcp.FCP f) = fcp.FCP (λc. if x = c then y else f c)

h l w n.
    words.word_lsr (words.word_bits h l w) n = words.word_bits h (l + n) w

b n.
    words.word_bit b (words.n2w n)
    b arithmetic.- (fcp.dimindex bool.the_value) 1 bit.BIT b n

v w.
    words.word_nand (bitstring.v2w v) (bitstring.v2w w) =
    bitstring.v2w
      (bitstring.bnand (bitstring.fixwidth (fcp.dimindex bool.the_value) v)
         (bitstring.fixwidth (fcp.dimindex bool.the_value) w))

v w.
    words.word_nor (bitstring.v2w v) (bitstring.v2w w) =
    bitstring.v2w
      (bitstring.bnor (bitstring.fixwidth (fcp.dimindex bool.the_value) v)
         (bitstring.fixwidth (fcp.dimindex bool.the_value) w))

v w.
    words.word_xnor (bitstring.v2w v) (bitstring.v2w w) =
    bitstring.v2w
      (bitstring.bxnor (bitstring.fixwidth (fcp.dimindex bool.the_value) v)
         (bitstring.fixwidth (fcp.dimindex bool.the_value) w))

w n.
    words.bit_count_upto (suc n) w =
    (if fcp.fcp_index w n then 1 else 0) + words.bit_count_upto n w

m n.
    n < fcp.dimindex bool.the_value
    words.word_lsr m n =
    words.word_div m (words.n2w (arithmetic.BIT2 0 n))

a b.
    words.word_ge a b
    bool.LET
      (pair.UNCURRY (λn. pair.UNCURRY (λz. pair.UNCURRY (λc v. n v))))
      (words.nzcv a b)

P.
    (a. P (fcp.BIT1A a)) (a. P (fcp.BIT1B a)) P fcp.BIT1C bb. P bb

words.INT_MIN bool.the_value = arithmetic.BIT2 16383

(x. fcp.IS_BIT1A (fcp.BIT1A x) )
  (x. fcp.IS_BIT1A (fcp.BIT1B x) ) (fcp.IS_BIT1A fcp.BIT1C )

(x. fcp.IS_BIT1B (fcp.BIT1A x) )
  (x. fcp.IS_BIT1B (fcp.BIT1B x) ) (fcp.IS_BIT1B fcp.BIT1C )

(x. fcp.IS_BIT1C (fcp.BIT1A x) )
  (x. fcp.IS_BIT1C (fcp.BIT1B x) ) (fcp.IS_BIT1C fcp.BIT1C )

(n. words.word_lo (words.n2w 0) n ¬(n = words.n2w 0))
  n. ¬words.word_lo n (words.n2w 0)

w.
    words.sw2sw w =
    words.word_add
      (if words.word_msb w then
         words.word_lsl (words.word_2comp (words.n2w 1))
           (fcp.dimindex bool.the_value)
       else words.n2w 0) (words.w2w w)

w.
    words.sw2sw w =
    words.word_or
      (if words.word_msb w then
         words.word_lsl (words.word_2comp (words.n2w 1))
           (fcp.dimindex bool.the_value)
       else words.n2w 0) (words.w2w w)

bitstring.v2s =
  map
    (λb.
       if b then
         string.CHR
           (bit1 (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))))
       else
         string.CHR
           (arithmetic.BIT2 (bit1 (bit1 (bit1 (arithmetic.BIT2 0))))))

a n.
    a < words.dimword bool.the_value
    words.n2w (a div arithmetic.BIT2 0 n) =
    words.word_lsr (words.n2w a) n

n m.
    words.word_nand (words.n2w n) (words.n2w m) =
    words.n2w
      (bit.BITWISE (fcp.dimindex bool.the_value) (λa b. ¬(a b)) n m)

n m.
    words.word_nor (words.n2w n) (words.n2w m) =
    words.n2w
      (bit.BITWISE (fcp.dimindex bool.the_value) (λa b. ¬(a b)) n m)

n m.
    words.word_xor (words.n2w n) (words.n2w m) =
    words.n2w
      (bit.BITWISE (fcp.dimindex bool.the_value) (λx y. ¬(x y)) n m)

p w.
    alignment.aligned p w
    words.word_and w (words.n2w (arithmetic.- (arithmetic.BIT2 0 p) 1)) =
    words.n2w 0

p w.
    alignment.align p w =
    words.n2w
      ((words.w2n w div arithmetic.BIT2 0 p) * arithmetic.BIT2 0 p)

m y.
    ¬(y = words.n2w 0) 0 < m
    words.w2n (words.word_lsr y m) < words.w2n y

a b.
    words.word_hi a b
    bool.LET
      (pair.UNCURRY (λn. pair.UNCURRY (λz. pair.UNCURRY (λc v. c ¬z))))
      (words.nzcv a b)

a b.
    words.word_ls a b
    bool.LET
      (pair.UNCURRY (λn. pair.UNCURRY (λz. pair.UNCURRY (λc v. ¬c z))))
      (words.nzcv a b)

a b.
    words.word_lt a b
    bool.LET
      (pair.UNCURRY (λn. pair.UNCURRY (λz. pair.UNCURRY (λc v. ¬(n v)))))
      (words.nzcv a b)

a b.
    words.w2w (words.word_add a b) =
    words.word_bits (arithmetic.- (fcp.dimindex bool.the_value) 1) 0
      (words.word_add (words.w2w a) (words.w2w b))

a b.
    words.w2w (words.word_mul a b) =
    words.word_bits (arithmetic.- (fcp.dimindex bool.the_value) 1) 0
      (words.word_mul (words.w2w a) (words.w2w b))

x y.
    words.word_le (words.n2w 0) x words.word_le (words.n2w 0) y
    (words.word_le x y words.word_ls x y)

x y.
    words.word_le (words.n2w 0) x words.word_le (words.n2w 0) y
    (words.word_lt x y words.word_lo x y)

v w.
    words.word_join v w =
    bool.LET
      (bool.LET
         (λcv cw.
            words.word_or (words.word_lsl cv (fcp.dimindex bool.the_value))
              cw) (words.w2w v)) (words.w2w w)

words.dimword bool.the_value = arithmetic.BIT2 32767

words.word_rrx (, words.n2w 0) = (, words.n2w 0)
  words.word_rrx (, words.n2w 0) = (, words.word_L)

h l n.
    h < fcp.dimindex bool.the_value
    words.n2w (bit.BITS h l n) = words.word_bits h l (words.n2w n)

h l v.
    words.word_slice h l (bitstring.v2w v) =
    bitstring.v2w
      (bitstring.shiftl
         (bitstring.field h l
            (bitstring.fixwidth (fcp.dimindex bool.the_value) v)) l)

f0 f1. fn. (a. fn (fcp.BIT0A a) = f0 a) a. fn (fcp.BIT0B a) = f1 a

f g.
    (i. i < fcp.dimindex bool.the_value fcp.fcp_index f i = g i)
    fcp.FCP g = f

x y.
    x = y
    i.
      i < fcp.dimindex bool.the_value
      fcp.fcp_index x i = fcp.fcp_index y i

w h l.
    fcp.dimindex bool.the_value fcp.dimindex bool.the_value
    words.word_extract h l (words.w2w w) = words.word_extract h l w

w n.
    words.word_lsr w n =
    fcp.FCP
      (λi. i + n < fcp.dimindex bool.the_value fcp.fcp_index w (i + n))

v w.
    (x.
       x < fcp.dimindex bool.the_value
       (words.word_bit x v words.word_bit x w)) v = w

f w i.
    i < fcp.dimindex bool.the_value
    (fcp.fcp_index (words.word_modify f w) i f i (fcp.fcp_index w i))

p w.
    alignment.aligned p w
    p = 0 words.word_extract (arithmetic.- p 1) 0 w = words.n2w 0

p w.
    alignment.align p w =
    if p = 0 then w
    else words.word_sub w (words.word_extract (arithmetic.- p 1) 0 w)

v i.
    i < length v
    (bitstring.testbit i v
     list.EL (arithmetic.- (arithmetic.- (length v) 1) i) v)

f n.
    fcp.fcp_index (fcp.FCP f) n =
    if n < fcp.dimindex bool.the_value then f n
    else combin.FAIL fcp.fcp_index FCP out of bounds (fcp.FCP f) n

w i.
    i < fcp.dimindex bool.the_value
    (fcp.fcp_index (words.w2w w) i
     i < fcp.dimindex bool.the_value fcp.fcp_index w i)

w n.
    words.w2n w * arithmetic.BIT2 0 n < words.dimword bool.the_value
    words.word_lsr (words.word_lsl w n) n = w

a b.
    ¬words.word_msb a ¬words.word_msb b
    words.w2n (words.word_add a b) = words.w2n a + words.w2n b

w.
    words.word_abs w =
    fcp.FCP
      (λi.
         ¬words.word_msb w fcp.fcp_index w i
         words.word_msb w fcp.fcp_index (words.word_2comp w) i)

h l n.
    words.word_bits h l (words.n2w n) =
    words.n2w
      (bit.BITS (min h (arithmetic.- (fcp.dimindex bool.the_value) 1)) l n)

h l n.
    words.word_slice h l (words.n2w n) =
    words.n2w
      (bit.SLICE (min h (arithmetic.- (fcp.dimindex bool.the_value) 1)) l
         n)

h l w.
    words.word_signed_bits h l w =
    words.word_sign_extend
      (arithmetic.- (min (suc h) (fcp.dimindex bool.the_value)) l)
      (words.word_bits h l w)

n w.
    words.word_replicate n w =
    fcp.FCP
      (λi.
         i < n * fcp.dimindex bool.the_value
         fcp.fcp_index w (i mod fcp.dimindex bool.the_value))

a b.
    bitstring.add a b =
    bool.LET
      (λm.
         bitstring.zero_extend m
           (bitstring.n2v (bitstring.v2n a + bitstring.v2n b)))
      (max (length a) (length b))

f g. (x. x < n f x = g x) sum_num.SUM n f = sum_num.SUM n g

w h l.
    words.word_bits h l (words.w2w w) =
    words.w2w
      (words.word_bits
         (min h (arithmetic.- (fcp.dimindex bool.the_value) 1)) l w)

(f. sum_num.SUM 0 f = 0)
  m f. sum_num.SUM (suc m) f = sum_num.SUM m f + f m

n i.
    fcp.fcp_index (words.n2w n) i
    if i < fcp.dimindex bool.the_value then bit.BIT i n
    else combin.FAIL fcp.fcp_index index too large (words.n2w n) i

m n.
    words.word_and (words.n2w n)
      (words.n2w (arithmetic.- (arithmetic.BIT2 0 m) 1)) =
    words.n2w (n mod arithmetic.BIT2 0 m)

i x y c.
    blast.BSUM i x y c blast.bsum (x i) (y i) (blast.BCARRY i x y c)

v i.
    fcp.fcp_index (bitstring.v2w v) i
    if i < fcp.dimindex bool.the_value then bitstring.testbit i v
    else combin.FAIL fcp.fcp_index index too large (bitstring.v2w v) i

v1 v2.
    pred_set.FINITE pred_set.UNIV pred_set.FINITE pred_set.UNIV
    words.word_join (bitstring.v2w v1) (bitstring.v2w v2) =
    bitstring.v2w
      (v1 @ bitstring.fixwidth (fcp.dimindex bool.the_value) v2)

w n.
    n < fcp.dimindex bool.the_value
    (list.EL n (bitstring.w2v w)
     fcp.fcp_index w
       (arithmetic.- (arithmetic.- (fcp.dimindex bool.the_value) 1) n))

a b.
    words.word_gt a b
    bool.LET
      (pair.UNCURRY
         (λn. pair.UNCURRY (λz. pair.UNCURRY (λc v. ¬z (n v)))))
      (words.nzcv a b)

a b.
    words.word_le a b
    bool.LET
      (pair.UNCURRY
         (λn. pair.UNCURRY (λz. pair.UNCURRY (λc v. z ¬(n v)))))
      (words.nzcv a b)

words.concat_word_list [] = words.n2w 0
  h t.
    words.concat_word_list (h :: t) =
    words.word_or (words.w2w h)
      (words.word_lsl (words.concat_word_list t)
         (fcp.dimindex bool.the_value))

m n f. m n ¬(f n = 0) sum_num.SUM m f < sum_num.SUM (suc n) f

b v.
    bitstring.testbit b v
    bool.LET (λn. b < n list.EL (arithmetic.- (arithmetic.- n 1) b) v)
      (length v)

n v.
    bitstring.fixwidth n v =
    bool.LET
      (λl.
         if l < n then bitstring.zero_extend n v
         else list.DROP (arithmetic.- l n) v) (length v)

n f.
    words.word_reduce f (words.n2w n) =
    fcp.FCP
      (const
         (bool.LET (λl. list.FOLDL f (head l) (tail l))
            (numposrep.BOOLIFY (fcp.dimindex bool.the_value) n [])))

n.
    words.w2w (words.n2w n) =
    if fcp.dimindex bool.the_value fcp.dimindex bool.the_value then
      words.n2w n
    else
      words.n2w
        (bit.BITS (arithmetic.- (fcp.dimindex bool.the_value) 1) 0 n)

a b.
    fcp.FCP_CONCAT a b =
    fcp.FCP
      (λi.
         if i < fcp.dimindex bool.the_value then fcp.fcp_index b i
         else
           fcp.fcp_index a (arithmetic.- i (fcp.dimindex bool.the_value)))

w n.
    words.word_asr w n =
    fcp.FCP
      (λi.
         if fcp.dimindex bool.the_value i + n then words.word_msb w
         else fcp.fcp_index w (i + n))

w n.
    words.word_lsl w n =
    fcp.FCP
      (λi.
         i < fcp.dimindex bool.the_value n i
         fcp.fcp_index w (arithmetic.- i n))

w.
    words.w2n (words.w2w w) =
    if fcp.dimindex bool.the_value fcp.dimindex bool.the_value then
      words.w2n w
    else
      words.w2n
        (words.word_bits (arithmetic.- (fcp.dimindex bool.the_value) 1) 0
           w)

w.
    words.sw2sw (words.sw2sw w) =
    if fcp.dimindex bool.the_value < fcp.dimindex bool.the_value
       fcp.dimindex bool.the_value < fcp.dimindex bool.the_value
    then words.sw2sw (words.w2w w)
    else words.sw2sw w

f v.
    words.word_reduce f (bitstring.v2w v) =
    bool.LET (λl. bitstring.v2w (list.FOLDL f (head l) (tail l) :: []))
      (bitstring.fixwidth (fcp.dimindex bool.the_value) v)

(a. fcp.mk_finite_image (fcp.dest_finite_image a) = a)
  r.
    (let x r in x = bool.ARB pred_set.FINITE pred_set.UNIV)
    fcp.dest_finite_image (fcp.mk_finite_image r) = r

i n.
    i < fcp.dimindex bool.the_value
    (fcp.fcp_index
       (words.word_sub (words.word_lsl (words.n2w 1) n) (words.n2w 1)) i
     i < n)

a b.
    words.saturate_mul a b =
    if pred_set.FINITE pred_set.UNIV
       words.word_ls (words.w2w words.word_T)
         (words.word_mul (words.w2w a) (words.w2w b))
    then words.word_T
    else words.word_mul a b

a b.
    words.word_lo a (words.word_2comp b)
    ¬(b = words.n2w 0)
    (a = words.n2w 0 words.word_lo b (words.word_2comp a))

a b.
    words.word_lo (words.word_2comp a) b
    ¬(b = words.n2w 0)
    (a = words.n2w 0 words.word_lo (words.word_2comp b) a)

c a.
    words.word_ls a (words.word_add c a)
    a = words.n2w 0 c = words.n2w 0
    words.word_lo a (words.word_2comp c)

words.INT_MIN bool.the_value = arithmetic.BIT2 262143

(n.
     words.word_ls (words.word_2comp (words.n2w 1)) n
     n = words.word_2comp (words.n2w 1))
  n. words.word_ls n (words.word_2comp (words.n2w 1))

i v.
    i < fcp.dimindex bool.the_value
    (words.word_bit i (bitstring.v2w v)
     bool.LET (λl. ¬null l last l) (bitstring.shiftr v i))

%%genvar%%3244 a b.
    alignment.aligned %%genvar%%3244 a
    alignment.aligned %%genvar%%3244 b
    alignment.aligned %%genvar%%3244 (words.word_add a b)
    alignment.aligned %%genvar%%3244 (words.word_sub a b)

p a b.
    alignment.aligned p a words.w2n b < arithmetic.BIT2 0 p
    alignment.align p (words.word_add a b) = a

v.
    1 < fcp.dimindex bool.the_value
    fcp.dimindex bool.the_value =
    arithmetic.- (fcp.dimindex bool.the_value) 1
    fcp.FCP_TL v = fcp.L2V (tail (fcp.V2L v))

a.
    words.word_msb a
    if arithmetic.- (fcp.dimindex bool.the_value) 1 = 0 a = words.word_L
    then words.word_msb (words.word_2comp a)
    else ¬words.word_msb (words.word_2comp a)

bitstring.s2v =
  map
    (λc.
       c =
       string.CHR
         (bit1 (arithmetic.BIT2 (bit1 (bit1 (arithmetic.BIT2 0)))))
       c =
       string.CHR
         (arithmetic.BIT2
            (bit1 (arithmetic.BIT2 (bit1 (arithmetic.BIT2 1))))))

h l s.
    bitstring.field_insert h l s =
    bitstring.modify
      (λi. cond (l i i h) (bitstring.testbit (arithmetic.- i l) s))

h l a.
    words.bit_field_insert h l a =
    words.word_modify
      (λi. cond (l i i h) (fcp.fcp_index a (arithmetic.- i l)))

n m.
    words.word_xor (words.n2w n) (words.n2w m) =
    words.n2w
      (bit.BITWISE (suc (max (bit.LOG2 n) (bit.LOG2 m))) (λx y. ¬(x y)) n
         m)

b c2n n2c s.
    words.w2s b n2c (words.s2w b c2n s) =
    ASCIInumbers.n2s b n2c
      (ASCIInumbers.s2n b c2n s mod words.dimword bool.the_value)

m v.
    v < arithmetic.- (fcp.dimindex bool.the_value) 1
    words.word_mod m (words.n2w (arithmetic.BIT2 0 suc v)) =
    words.word_bits v 0 m

x y.
    fcp.dimindex bool.the_value fcp.dimindex bool.the_value
    y < words.dimword bool.the_value
    (words.w2w x = words.n2w y x = words.n2w y)

c a.
    words.word_lo a (words.word_add c a)
    ¬(c = words.n2w 0)
    (a = words.n2w 0 words.word_lo a (words.word_2comp c))

x y.
    words.word_le (words.n2w 0) y words.word_le y x
    words.word_le (words.n2w 0) (words.word_sub x y)
    words.word_le (words.word_sub x y) x

x y.
    words.word_lt (words.n2w 0) y words.word_lt y x
    words.word_lt (words.n2w 0) (words.word_sub x y)
    words.word_lt (words.word_sub x y) x

a b.
    words.word_1comp (words.word_and a b) =
    words.word_or (words.word_1comp a) (words.word_1comp b)
    words.word_1comp (words.word_or a b) =
    words.word_and (words.word_1comp a) (words.word_1comp b)

P.
    P pred_set.EMPTY
    (s. P s e. ¬bool.IN e s P (pred_set.INSERT e s)) s. P s

words.dimword bool.the_value = arithmetic.BIT2 524287

(a' a. ¬(fcp.BIT1A a = fcp.BIT1B a'))
  (a. ¬(fcp.BIT1A a = fcp.BIT1C)) a. ¬(fcp.BIT1B a = fcp.BIT1C)

h l w.
    fcp.dimindex bool.the_value = arithmetic.- (h + 1) l
    words.word_extract h l w = words.w2w (words.word_extract h l w)

v.
    words.sw2sw (bitstring.v2w v) =
    if fcp.dimindex bool.the_value < fcp.dimindex bool.the_value then
      bitstring.v2w
        (bitstring.sign_extend (fcp.dimindex bool.the_value)
           (bitstring.fixwidth (fcp.dimindex bool.the_value) v))
    else bitstring.v2w (bitstring.fixwidth (fcp.dimindex bool.the_value) v)

n m.
    words.word_lsl (words.n2w m) n =
    if arithmetic.- (fcp.dimindex bool.the_value) 1 < n then words.n2w 0
    else words.n2w (m * arithmetic.BIT2 0 n)

n v w.
    bitstring.fixwidth n v = bitstring.fixwidth n w
    i. i < n (bitstring.testbit i v bitstring.testbit i w)

n.
    words.saturate_w2w (words.n2w n) =
    bool.LET
      (λm.
         if fcp.dimindex bool.the_value fcp.dimindex bool.the_value
            words.dimword bool.the_value m
         then words.word_T
         else words.n2w m) (n mod words.dimword bool.the_value)

a b.
    words.word_ge a b
    (words.word_msb b words.word_msb a) words.w2n a words.w2n b
    words.word_msb b ¬words.word_msb a

a b.
    words.word_gt a b
    (words.word_msb b words.word_msb a) words.w2n a > words.w2n b
    words.word_msb b ¬words.word_msb a

a b.
    words.word_le a b
    (words.word_msb a words.word_msb b) words.w2n a words.w2n b
    words.word_msb a ¬words.word_msb b

a b.
    words.word_lt a b
    (words.word_msb a words.word_msb b) words.w2n a < words.w2n b
    words.word_msb a ¬words.word_msb b

(n. ¬words.word_lo (words.word_2comp (words.n2w 1)) n)
  n.
    words.word_lo n (words.word_2comp (words.n2w 1))
    ¬(n = words.word_2comp (words.n2w 1))

(a a'. fcp.BIT0A a = fcp.BIT0A a' a = a')
  a a'. fcp.BIT0B a = fcp.BIT0B a' a = a'

(a a'. fcp.BIT1A a = fcp.BIT1A a' a = a')
  a a'. fcp.BIT1B a = fcp.BIT1B a' a = a'

h1 l1 h2 l2 w.
    words.word_bits h2 l2 (words.word_bits h1 l1 w) =
    words.word_bits (min h1 (h2 + l1)) (l2 + l1) w

n i v.
    list.EL i (bitstring.zero_extend n v)
    arithmetic.- n (length v) i
    list.EL (arithmetic.- i (arithmetic.- n (length v))) v

n v.
    bitstring.fixwidth n v =
    bool.LET
      (λl.
         if l < n then bitstring.extend (arithmetic.- n l) v
         else list.DROP (arithmetic.- l n) v) (length v)

n l k j h.
    words.word_extract j k (words.word_bits h l n) =
    words.word_extract (min h (j + l)) (k + l) n

w h l.
    arithmetic.- (fcp.dimindex bool.the_value) 1 < h
    words.word_bits h l w =
    words.word_bits (arithmetic.- (fcp.dimindex bool.the_value) 1) l w

P.
    P (words.n2w 0)
    (n.
       suc n < words.dimword bool.the_value P (words.n2w n)
       P (words.n2w (suc n))) w. P w

h l.
    words.word_bits h l =
    λw.
      fcp.FCP
        (λi.
           i + l min h (arithmetic.- (fcp.dimindex bool.the_value) 1)
           fcp.fcp_index w (i + l))

h l.
    words.word_slice h l =
    λw.
      fcp.FCP
        (λi.
           l i
           i min h (arithmetic.- (fcp.dimindex bool.the_value) 1)
           fcp.fcp_index w i)

a b.
    fcp.dimindex bool.the_value fcp.dimindex bool.the_value
    fcp.dimindex bool.the_value fcp.dimindex bool.the_value
    (words.w2n a = words.w2n b words.w2w a = words.w2w b)

w.
    ¬(w = words.n2w 0)
    v.
      v =
      words.word_add (words.word_mul (words.word_div v w) w)
        (words.word_mod v w) words.word_lo (words.word_mod v w) w

(a. bitstring.boolify a [] = a)
  a n l.
    bitstring.boolify a (n :: l) = bitstring.boolify (¬(n = 0) :: a) l

words.word_rrx (, words.word_2comp (words.n2w 1)) = (, words.word_H)
  words.word_rrx (, words.word_2comp (words.n2w 1)) =
  (, words.word_2comp (words.n2w 1))

(a f f1. fcp.bit0_CASE (fcp.BIT0A a) f f1 = f a)
  a f f1. fcp.bit0_CASE (fcp.BIT0B a) f f1 = f1 a

a.
    ¬(arithmetic.- (fcp.dimindex bool.the_value) 1 = 0 a = words.n2w 0
       a = words.word_L)
    (¬words.word_msb a words.word_msb (words.word_2comp a))

(v0 l. bitstring.extend v0 0 l = l)
  c n l. bitstring.extend c (suc n) l = bitstring.extend c n (c :: l)

p m n f.
    sum_num.GSUM (p, m + n) f =
    sum_num.GSUM (p, m) f + sum_num.GSUM (p + m, n) f

m n f.
    (q. m q q < n ¬(f q = 0)) sum_num.SUM m f < sum_num.SUM n f

f0 f1 f2.
    fn.
      (a. fn (fcp.BIT1A a) = f0 a) (a. fn (fcp.BIT1B a) = f1 a)
      fn fcp.BIT1C = f2

f v1 v2.
    bitstring.bitwise f v1 v2 =
    bool.LET
      (λm.
         map (pair.UNCURRY f)
           (list.ZIP (bitstring.fixwidth m v1, bitstring.fixwidth m v2)))
      (max (length v1) (length v2))

words.INT_MIN bool.the_value = arithmetic.BIT2 4194303

(f a. fcp.bit0_size f (fcp.BIT0A a) = 1 + f a)
  f a. fcp.bit0_size f (fcp.BIT0B a) = 1 + f a

c w.
    words.word_rrx (c, w) =
    (words.word_lsb w,
     fcp.FCP
       (λi.
          if i = arithmetic.- (fcp.dimindex bool.the_value) 1 then c
          else fcp.fcp_index (words.word_lsr w 1) i))

p a b.
    alignment.aligned p b
    (alignment.aligned p (words.word_add a b) alignment.aligned p a)
    (alignment.aligned p (words.word_sub a b) alignment.aligned p a)

m a b c d.
    ¬(a = b) fcp.:+ a c (fcp.:+ b d m) = fcp.:+ b d (fcp.:+ a c m)

i x y c.
    blast.BSUM i (λi. bit.BIT i x) (λi. bit.BIT i y) c
    bit.BIT i (x + y + if c then 1 else 0)

p n f. (m. p m m < p + n f m = 0) sum_num.GSUM (p, n) f = 0

w n.
    words.word_asr w n =
    if words.word_msb w then
      words.word_or
        (words.word_slice (arithmetic.- (fcp.dimindex bool.the_value) 1)
           (arithmetic.- (fcp.dimindex bool.the_value) n) words.word_T)
        (words.word_lsr w n)
    else words.word_lsr w n

w n.
    words.w2w (words.word_lsl w n) =
    if n < fcp.dimindex bool.the_value then
      words.word_lsl
        (words.w2w
           (words.word_bits
              (arithmetic.- (arithmetic.- (fcp.dimindex bool.the_value) 1)
                 n) 0 w)) n
    else words.n2w 0

w.
    words.reduce_and w =
    bool.LET (λl. list.FOLDL words.word_and (head l) (tail l))
      (list.GENLIST
         (λi.
            bool.LET (λn. words.word_extract n n w)
              (arithmetic.- (arithmetic.- (fcp.dimindex bool.the_value) 1)
                 i)) (fcp.dimindex bool.the_value))

w.
    words.reduce_nand w =
    bool.LET (λl. list.FOLDL words.word_nand (head l) (tail l))
      (list.GENLIST
         (λi.
            bool.LET (λn. words.word_extract n n w)
              (arithmetic.- (arithmetic.- (fcp.dimindex bool.the_value) 1)
                 i)) (fcp.dimindex bool.the_value))

w.
    words.reduce_nor w =
    bool.LET (λl. list.FOLDL words.word_nor (head l) (tail l))
      (list.GENLIST
         (λi.
            bool.LET (λn. words.word_extract n n w)
              (arithmetic.- (arithmetic.- (fcp.dimindex bool.the_value) 1)
                 i)) (fcp.dimindex bool.the_value))

w.
    words.reduce_or w =
    bool.LET (λl. list.FOLDL words.word_or (head l) (tail l))
      (list.GENLIST
         (λi.
            bool.LET (λn. words.word_extract n n w)
              (arithmetic.- (arithmetic.- (fcp.dimindex bool.the_value) 1)
                 i)) (fcp.dimindex bool.the_value))

w.
    words.reduce_xnor w =
    bool.LET (λl. list.FOLDL words.word_xnor (head l) (tail l))
      (list.GENLIST
         (λi.
            bool.LET (λn. words.word_extract n n w)
              (arithmetic.- (arithmetic.- (fcp.dimindex bool.the_value) 1)
                 i)) (fcp.dimindex bool.the_value))

w.
    words.reduce_xor w =
    bool.LET (λl. list.FOLDL words.word_xor (head l) (tail l))
      (list.GENLIST
         (λi.
            bool.LET (λn. words.word_extract n n w)
              (arithmetic.- (arithmetic.- (fcp.dimindex bool.the_value) 1)
                 i)) (fcp.dimindex bool.the_value))

w.
    ¬(w = words.n2w 0)
    bit.LOG2 (words.w2n w) =
    arithmetic.- (arithmetic.- (fcp.dimindex bool.the_value) 1)
      (while.LEAST
         (λi.
            fcp.fcp_index w
              (arithmetic.- (arithmetic.- (fcp.dimindex bool.the_value) 1)
                 i)))

words.dimword bool.the_value = arithmetic.BIT2 8388607

n i v.
    list.EL i (bitstring.sign_extend n v) =
    if i < arithmetic.- n (length v) then list.EL 0 v
    else list.EL (arithmetic.- i (arithmetic.- n (length v))) v

a b h.
    h < fcp.dimindex bool.the_value
    words.word_extract h 0
      (words.word_add (words.word_extract h 0 a)
         (words.word_extract h 0 b)) =
    words.word_extract h 0 (words.word_add a b)

a b h.
    h < fcp.dimindex bool.the_value
    words.word_extract h 0
      (words.word_mul (words.word_extract h 0 a)
         (words.word_extract h 0 b)) =
    words.word_extract h 0 (words.word_mul a b)

v1 v2.
    words.word_join (bitstring.v2w v1) (bitstring.v2w v2) =
    if pred_set.FINITE pred_set.UNIV pred_set.FINITE pred_set.UNIV then
      bitstring.v2w
        (v1 @ bitstring.fixwidth (fcp.dimindex bool.the_value) v2)
    else
      combin.FAIL words.word_join bad domain (bitstring.v2w v1)
        (bitstring.v2w v2)

w i.
    i < fcp.dimindex bool.the_value
    (fcp.fcp_index (words.sw2sw w) i
     if i < fcp.dimindex bool.the_value
        fcp.dimindex bool.the_value < fcp.dimindex bool.the_value
     then fcp.fcp_index w i
     else words.word_msb w)

c a.
    words.word_ls (words.word_add c a) a
    c = words.n2w 0
    ¬(a = words.n2w 0)
    (words.word_lo (words.word_2comp c) a a = words.word_2comp c)

x y.
    pred_set.FINITE pred_set.UNIV
    fcp.dimindex bool.the_value fcp.dimindex bool.the_value
    y < words.dimword bool.the_value
    (words.word_concat (words.n2w 0) x = words.n2w y x = words.n2w y)

f w.
    words.word_reduce f w =
    fcp.FCP
      (const
         (bool.LET (λl. list.FOLDL f (head l) (tail l))
            (list.GENLIST
               (λi.
                  fcp.fcp_index w
                    (arithmetic.-
                       (arithmetic.- (fcp.dimindex bool.the_value) 1) i))
               (fcp.dimindex bool.the_value))))

n v.
    words.word_asr (bitstring.v2w v) n =
    bool.LET
      (λl.
         bitstring.v2w
           (bitstring.sign_extend (fcp.dimindex bool.the_value)
              (if fcp.dimindex bool.the_value n then head l :: []
               else bitstring.shiftr l n)))
      (bitstring.fixwidth (fcp.dimindex bool.the_value) v)

c a.
    words.word_rrx (c, words.n2w a) =
    (odd a,
     words.n2w
       (bit.BITS (arithmetic.- (fcp.dimindex bool.the_value) 1) 1 a +
        bit.SBIT c (arithmetic.- (fcp.dimindex bool.the_value) 1)))

p m n f.
    m n ¬(f (p + n) = 0)
    sum_num.GSUM (p, m) f < sum_num.GSUM (p, suc n) f

a b.
    words.word_le a b
    words.word_ls words.word_L a
    (words.word_lo b words.word_L words.word_ls a b)
    words.word_lo a words.word_L words.word_lo b words.word_L
    words.word_ls a b

a b.
    words.word_lt a b
    words.word_ls words.word_L a
    (words.word_lo b words.word_L words.word_lo a b)
    words.word_lo a words.word_L words.word_lo b words.word_L
    words.word_lo a b

c a.
    words.word_lo (words.word_add c a) a
    ¬(a = words.n2w 0)
    (¬(c = words.n2w 0) words.word_lo (words.word_2comp c) a
     a = words.word_2comp c)

(n v.
     bitstring.zero_extend n v =
     bitstring.extend (arithmetic.- n (length v)) v)
  n v.
    bitstring.sign_extend n v =
    bitstring.extend (head v) (arithmetic.- n (length v)) v

h l a.
    words.word_bits h l a =
    if l h then
      words.word_and (words.word_lsr a l)
        (words.word_sub
           (words.word_lsl (words.n2w (arithmetic.BIT2 0))
              (arithmetic.- h l)) (words.n2w 1))
    else words.n2w 0

h l a.
    words.word_extract h l a =
    if l h then
      words.word_and (words.word_lsr a l)
        (words.word_sub
           (words.word_lsl (words.n2w (arithmetic.BIT2 0))
              (arithmetic.- h l)) (words.n2w 1))
    else words.n2w 0

w m.
    words.word_mul w m =
    list.FOLDL
      (λa j.
         words.word_add a
           (fcp.FCP
              (λi.
                 fcp.fcp_index w j j i
                 fcp.fcp_index m (arithmetic.- i j)))) (words.n2w 0)
      (rich_list.COUNT_LIST (fcp.dimindex bool.the_value))

n i.
    words.BIT_SET i n =
    if n = 0 then pred_set.EMPTY
    else if odd n then
      pred_set.INSERT i (words.BIT_SET (suc i) (n div arithmetic.BIT2 0))
    else words.BIT_SET (suc i) (n div arithmetic.BIT2 0)

n w.
    words.word_asr w n =
    if words.word_msb w then
      words.word_or
        (words.n2w
           (arithmetic.- (words.dimword bool.the_value)
              (arithmetic.BIT2 0
               arithmetic.- (fcp.dimindex bool.the_value)
                 (min n (fcp.dimindex bool.the_value)))))
        (words.word_lsr w n)
    else words.word_lsr w n

v1 v2.
    pred_set.FINITE pred_set.UNIV pred_set.FINITE pred_set.UNIV
    words.word_concat (bitstring.v2w v1) (bitstring.v2w v2) =
    bitstring.v2w
      (bitstring.fixwidth
         (min (fcp.dimindex bool.the_value)
            (fcp.dimindex bool.the_value + fcp.dimindex bool.the_value))
         (v1 @ bitstring.fixwidth (fcp.dimindex bool.the_value) v2))

words.INT_MIN bool.the_value = arithmetic.BIT2 67108863

(m n.
     words.word_mul (words.n2w m) (words.word_2comp (words.n2w n)) =
     words.word_2comp (words.n2w (m * n)))
  m n.
    words.word_mul (words.word_2comp (words.n2w m))
      (words.word_2comp (words.n2w n)) = words.n2w (m * n)

h l n.
    words.word_signed_bits h l (words.n2w n) =
    words.n2w
      (bit.SIGN_EXTEND
         (arithmetic.- (min (suc h) (fcp.dimindex bool.the_value)) l)
         (fcp.dimindex bool.the_value)
         (bit.BITS (min h (arithmetic.- (fcp.dimindex bool.the_value) 1)) l
            n))

h l a.
    words.word_extract h l a =
    words.w2w
      (if l h then
         words.word_and (words.word_lsr a l)
           (words.word_sub
              (words.word_lsl (words.n2w (arithmetic.BIT2 0))
                 (arithmetic.- h l)) (words.n2w 1))
       else words.n2w 0)

c2n n2c b w.
    1 < b (x. x < b c2n (n2c x) = x)
    words.s2w b c2n (words.w2s b n2c w) = w

h l a b.
    l h length b l
    bitstring.field h l (a @ b) =
    bitstring.field (arithmetic.- h (length b)) (arithmetic.- l (length b))
      a

h l.
    words.word_signed_bits h l =
    λw.
      fcp.FCP
        (λi.
           l min h (arithmetic.- (fcp.dimindex bool.the_value) 1)
           fcp.fcp_index w
             (min (i + l)
                (min h (arithmetic.- (fcp.dimindex bool.the_value) 1))))

a b.
    words.word_xor (words.word_1comp a) (words.word_1comp b) =
    words.word_xor a b
    words.word_xor a (words.word_1comp b) =
    words.word_1comp (words.word_xor a b)
    words.word_xor (words.word_1comp a) b =
    words.word_1comp (words.word_xor a b)

words.dimword bool.the_value = arithmetic.BIT2 134217727

a.
    words.word_or words.word_T a = words.word_T
    words.word_or a words.word_T = words.word_T
    words.word_or (words.n2w 0) a = a words.word_or a (words.n2w 0) = a
    words.word_or a a = a

(n f. sum_num.GSUM (n, 0) f = 0)
  n m f. sum_num.GSUM (n, suc m) f = sum_num.GSUM (n, m) f + f (n + m)

words.INT_MIN bool.the_value = arithmetic.BIT2 268435455

¬words.word_lt (words.n2w 0) (words.word_2comp (words.n2w 1))
  ¬words.word_le (words.n2w 0) (words.word_2comp (words.n2w 1))
  words.word_lt (words.word_2comp (words.n2w 1)) (words.n2w 0)
  words.word_le (words.word_2comp (words.n2w 1)) (words.n2w 0)

n q a.
    0 < n 0 < q a < q * n
    arithmetic.- (q * n) a mod n = arithmetic.- n (a mod n) mod n

w n.
    words.word_ror w n =
    bool.LET
      (λx.
         words.word_or
           (words.word_bits (arithmetic.- (fcp.dimindex bool.the_value) 1)
              x w)
           (words.word_lsl (words.word_bits (arithmetic.- x 1) 0 w)
              (arithmetic.- (fcp.dimindex bool.the_value) x)))
      (n mod fcp.dimindex bool.the_value)

w m.
    words.word_ror_bv w m =
    fcp.FCP
      (λk.
         list.FOLDL
           (λa j.
              a
              words.word_mod m (words.n2w (fcp.dimindex bool.the_value)) =
              words.n2w j
              fcp.fcp_index w ((j + k) mod fcp.dimindex bool.the_value))
           (rich_list.COUNT_LIST (fcp.dimindex bool.the_value)))

m a w b.
    fcp.fcp_index (fcp.:+ a w m) b =
    if b < fcp.dimindex bool.the_value then
      if a = b then w else fcp.fcp_index m b
    else combin.FAIL fcp.fcp_index index out of range (fcp.:+ a w m) b

a b.
    words.word_sdiv a b =
    if words.word_msb a then
      if words.word_msb b then
        words.word_div (words.word_2comp a) (words.word_2comp b)
      else words.word_2comp (words.word_div (words.word_2comp a) b)
    else if words.word_msb b then
      words.word_2comp (words.word_div a (words.word_2comp b))
    else words.word_div a b

a b.
    words.word_srem a b =
    if words.word_msb a then
      if words.word_msb b then
        words.word_2comp
          (words.word_mod (words.word_2comp a) (words.word_2comp b))
      else words.word_2comp (words.word_mod (words.word_2comp a) b)
    else if words.word_msb b then words.word_mod a (words.word_2comp b)
    else words.word_mod a b

x y.
    words.add_with_carry (x, words.word_1comp y, ) =
    (words.word_sub x y, words.word_ls y x,
     ¬(words.word_msb x words.word_msb y)
     ¬(words.word_msb (words.word_sub x y) words.word_msb x))

words.dimword bool.the_value = arithmetic.BIT2 536870911

p n f g.
    (x. p x x < p + n f x = g x)
    sum_num.GSUM (p, n) f = sum_num.GSUM (p, n) g

a b h.
    arithmetic.- (fcp.dimindex bool.the_value) 1 h
    fcp.dimindex bool.the_value fcp.dimindex bool.the_value
    words.word_extract h 0 (words.word_add a b) =
    words.word_add (words.word_extract h 0 a) (words.word_extract h 0 b)

a b h.
    arithmetic.- (fcp.dimindex bool.the_value) 1 h
    fcp.dimindex bool.the_value fcp.dimindex bool.the_value
    words.word_extract h 0 (words.word_mul a b) =
    words.word_mul (words.word_extract h 0 a) (words.word_extract h 0 b)

a.
    words.word_and words.word_T a = a words.word_and a words.word_T = a
    words.word_and (words.n2w 0) a = words.n2w 0
    words.word_and a (words.n2w 0) = words.n2w 0 words.word_and a a = a

(f a. fcp.bit1_size f (fcp.BIT1A a) = 1 + f a)
  (f a. fcp.bit1_size f (fcp.BIT1B a) = 1 + f a)
  f. fcp.bit1_size f fcp.BIT1C = 0

words.INT_MIN bool.the_value = arithmetic.BIT2 1073741823

h l v.
    length v fcp.dimindex bool.the_value
    fcp.dimindex bool.the_value = arithmetic.- (suc h) l
    fcp.dimindex bool.the_value < fcp.dimindex bool.the_value
    words.word_extract h l (bitstring.v2w v) =
    bitstring.v2w (bitstring.field h l v)

p w x.
    (alignment.aligned p
       (words.word_add w
          (words.word_mul (words.word_lsl (words.n2w 1) p) x))
     alignment.aligned p w)
    (alignment.aligned p
       (words.word_sub w
          (words.word_mul (words.word_lsl (words.n2w 1) p) x))
     alignment.aligned p w)

i a b.
    pred_set.FINITE pred_set.UNIV pred_set.FINITE pred_set.UNIV
    i < fcp.dimindex bool.the_value
    (fcp.fcp_index (words.word_join a b) i
     if i < fcp.dimindex bool.the_value then fcp.fcp_index b i
     else fcp.fcp_index a (arithmetic.- i (fcp.dimindex bool.the_value)))

x h y.
    fcp.dimindex bool.the_value fcp.dimindex bool.the_value
    arithmetic.- (fcp.dimindex bool.the_value) 1 h
    y < words.dimword bool.the_value
    (words.word_extract h 0 x = words.n2w y x = words.n2w y)

a.
    words.word_xor words.word_T a = words.word_1comp a
    words.word_xor a words.word_T = words.word_1comp a
    words.word_xor (words.n2w 0) a = a
    words.word_xor a (words.n2w 0) = a words.word_xor a a = words.n2w 0

(x y c. blast.BCARRY 0 x y c c)
  i x y c.
    blast.BCARRY (suc i) x y c
    blast.bcarry (x i) (y i) (blast.BCARRY i x y c)

h l n w.
    h < fcp.dimindex bool.the_value
    words.word_bits h l (words.word_lsl w n) =
    if n h then
      words.word_lsl
        (words.word_bits (arithmetic.- h n) (arithmetic.- l n) w)
        (arithmetic.- n l)
    else words.n2w 0

h l n w.
    h < fcp.dimindex bool.the_value
    words.word_extract h l (words.word_lsl w n) =
    if n h then
      words.word_lsl
        (words.word_extract (arithmetic.- h n) (arithmetic.- l n) w)
        (arithmetic.- n l)
    else words.n2w 0

h l n w.
    fcp.dimindex bool.the_value + l h + n
    words.word_lsl (words.word_extract h l w) n =
    words.word_lsl
      (words.word_extract
         (arithmetic.- (fcp.dimindex bool.the_value + l) (n + 1)) l w) n

words.dimword bool.the_value = arithmetic.BIT2 2147483647

h m' m l w.
    l m m' = m + 1 m < h
    words.word_or (words.word_slice h m' w) (words.word_slice m l w) =
    words.word_slice h l w

p m n f.
    (q. m + p q q < n + p ¬(f q = 0))
    sum_num.GSUM (p, m) f < sum_num.GSUM (p, n) f

(a. words.word_lsl a 0 = a) (a. words.word_asr a 0 = a)
  (a. words.word_lsr a 0 = a) (a. words.word_rol a 0 = a)
  a. words.word_ror a 0 = a

v h l i.
    i < arithmetic.- (suc h) l
    (list.EL i (bitstring.field h l v)
     suc h i + length v
     list.EL (arithmetic.- (i + length v) (suc h)) v)

n c x1 x2 y1 y2.
    (i. i < n (x1 i x2 i) (y1 i y2 i))
    (blast.BCARRY n x1 y1 c blast.BCARRY n x2 y2 c)

n c x1 x2 y1 y2.
    (i. i n (x1 i x2 i) (y1 i y2 i))
    (blast.BSUM n x1 y1 c blast.BSUM n x2 y2 c)

P.
    (n f. P (n, 0) f) (n m f. P (n, m) f P (n, suc m) f)
    v v1 v2. P (v, v1) v2

(a. bitstring.bitify a [] = a)
  (l a. bitstring.bitify a ( :: l) = bitstring.bitify (0 :: a) l)
  l a. bitstring.bitify a ( :: l) = bitstring.bitify (1 :: a) l

v1 v2.
    words.word_concat (bitstring.v2w v1) (bitstring.v2w v2) =
    if pred_set.FINITE pred_set.UNIV pred_set.FINITE pred_set.UNIV then
      bitstring.v2w
        (bitstring.fixwidth
           (min (fcp.dimindex bool.the_value)
              (fcp.dimindex bool.the_value + fcp.dimindex bool.the_value))
           (v1 @ bitstring.fixwidth (fcp.dimindex bool.the_value) v2))
    else
      combin.FAIL words.word_concat bad domain (bitstring.v2w v1)
        (bitstring.v2w v2)

h l a b.
    h < l + fcp.dimindex bool.the_value
    words.bit_field_insert h l a b =
    bool.LET
      (λmask.
         words.word_or
           (words.word_and (words.word_lsl (words.w2w a) l) mask)
           (words.word_and b (words.word_1comp mask)))
      (words.word_slice h l (words.word_2comp (words.n2w 1)))

n a.
    words.word_ror (words.n2w a) n =
    bool.LET
      (λx.
         words.n2w
           (bit.BITS (arithmetic.- (fcp.dimindex bool.the_value) 1) x a +
            bit.BITS (arithmetic.- x 1) 0 a *
            arithmetic.BIT2 0
            arithmetic.- (fcp.dimindex bool.the_value) x))
      (n mod fcp.dimindex bool.the_value)

v m.
    bitstring.rotate v m =
    bool.LET
      (λl.
         bool.LET
           (λx.
              if l = 0 x = 0 then v
              else
                bitstring.field (arithmetic.- x 1) 0 v @
                bitstring.field (arithmetic.- l 1) x v) (m mod l))
      (length v)

words.word_mul words.word_L2 words.word_L2 = words.word_L2
  words.word_mul words.word_L words.word_L2 = words.word_L2
  (n.
     words.word_mul (words.n2w n) words.word_L2 =
     if even n then words.n2w 0 else words.word_L2)
  n.
    words.word_mul (words.word_2comp (words.n2w n)) words.word_L2 =
    if even n then words.n2w 0 else words.word_L2

w m.
    words.word_rol_bv w m =
    fcp.FCP
      (λk.
         list.FOLDL
           (λa j.
              a
              words.word_mod m (words.n2w (fcp.dimindex bool.the_value)) =
              words.n2w j
              fcp.fcp_index w
                ((k +
                  arithmetic.- (fcp.dimindex bool.the_value) j mod
                  fcp.dimindex bool.the_value) mod
                 fcp.dimindex bool.the_value))
           (rich_list.COUNT_LIST (fcp.dimindex bool.the_value)))

w h l m n.
    words.word_extract h l (words.word_extract m n w) =
    words.word_extract
      (min m
         (min (h + n)
            (min (arithmetic.- (fcp.dimindex bool.the_value) 1)
               (arithmetic.- (fcp.dimindex bool.the_value + n) 1))))
      (l + n) w

(m n.
     words.word_add (words.word_2comp (words.n2w m))
       (words.word_2comp (words.n2w n)) =
     words.word_2comp (words.n2w (m + n)))
  m n.
    words.word_add (words.n2w m) (words.word_2comp (words.n2w n)) =
    if n m then words.n2w (arithmetic.- m n)
    else words.word_2comp (words.n2w (arithmetic.- n m))

(v w.
     words.word_and (words.w2w v) (words.w2w w) =
     words.w2w (words.word_and v w))
  (v w.
     words.word_or (words.w2w v) (words.w2w w) =
     words.w2w (words.word_or v w))
  v w.
    words.word_xor (words.w2w v) (words.w2w w) =
    words.w2w (words.word_xor v w)

(m n.
     m < bit1 n
     m = arithmetic.- (bit1 n) 1 m < arithmetic.- (bit1 n) 1)
  m n. m < arithmetic.BIT2 n m = bit1 n m < bit1 n

words.word_extract h l (words.n2w n) =
  if fcp.dimindex bool.the_value fcp.dimindex bool.the_value then
    words.n2w
      (bit.BITS (min h (arithmetic.- (fcp.dimindex bool.the_value) 1)) l n)
  else
    words.n2w
      (bit.BITS
         (min (min h (arithmetic.- (fcp.dimindex bool.the_value) 1))
            (arithmetic.- (fcp.dimindex bool.the_value) 1 + l)) l n)

i n w.
    i < n
    (list.EL i (bitstring.fixwidth n w)
     if length w < n then
       arithmetic.- n (length w) i
       list.EL (arithmetic.- i (arithmetic.- n (length w))) w
     else list.EL (i + arithmetic.- (length w) n) w)

i v n d.
    n < d i < arithmetic.- d n 0 < d
    (list.EL i (bitstring.shiftr (bitstring.fixwidth d v) n)
     d i + length v list.EL (arithmetic.- (i + length v) d) v)

(m n.
     words.n2w m = words.n2w n
     bit.MOD_2EXP_EQ (fcp.dimindex bool.the_value) m n)
  (n.
     words.n2w n = words.word_2comp (words.n2w 1)
     bit.MOD_2EXP_MAX (fcp.dimindex bool.the_value) n)
  n.
    words.word_2comp (words.n2w 1) = words.n2w n
    bit.MOD_2EXP_MAX (fcp.dimindex bool.the_value) n

(a f f1 v. fcp.bit1_CASE (fcp.BIT1A a) f f1 v = f a)
  (a f f1 v. fcp.bit1_CASE (fcp.BIT1B a) f f1 v = f1 a)
  f f1 v. fcp.bit1_CASE fcp.BIT1C f f1 v = v

i x y c.
    0 < i
    (blast.BCARRY i (λi. bit.BIT i x) (λi. bit.BIT i y) c
     bit.BIT i
       (bit.BITS (arithmetic.- i 1) 0 x + bit.BITS (arithmetic.- i 1) 0 y +
        if c then 1 else 0))

a b.
    words.word_ge (words.n2w a) (words.n2w b)
    bool.LET
      (bool.LET
         (λsa sb.
            (sa sb)
            a mod words.dimword bool.the_value
            b mod words.dimword bool.the_value ¬sa sb)
         (bit.BIT (arithmetic.- (fcp.dimindex bool.the_value) 1) a))
      (bit.BIT (arithmetic.- (fcp.dimindex bool.the_value) 1) b)

a b.
    words.word_gt (words.n2w a) (words.n2w b)
    bool.LET
      (bool.LET
         (λsa sb.
            (sa sb)
            a mod words.dimword bool.the_value >
            b mod words.dimword bool.the_value ¬sa sb)
         (bit.BIT (arithmetic.- (fcp.dimindex bool.the_value) 1) a))
      (bit.BIT (arithmetic.- (fcp.dimindex bool.the_value) 1) b)

a b.
    words.word_le (words.n2w a) (words.n2w b)
    bool.LET
      (bool.LET
         (λsa sb.
            (sa sb)
            a mod words.dimword bool.the_value
            b mod words.dimword bool.the_value sa ¬sb)
         (bit.BIT (arithmetic.- (fcp.dimindex bool.the_value) 1) a))
      (bit.BIT (arithmetic.- (fcp.dimindex bool.the_value) 1) b)

a b.
    words.word_lt (words.n2w a) (words.n2w b)
    bool.LET
      (bool.LET
         (λsa sb.
            (sa sb)
            a mod words.dimword bool.the_value <
            b mod words.dimword bool.the_value sa ¬sb)
         (bit.BIT (arithmetic.- (fcp.dimindex bool.the_value) 1) a))
      (bit.BIT (arithmetic.- (fcp.dimindex bool.the_value) 1) b)

M M' f f1.
    M = M' (a. M' = fcp.BIT0A a f a = f' a)
    (a. M' = fcp.BIT0B a f1 a = f1' a)
    fcp.bit0_CASE M f f1 = fcp.bit0_CASE M' f' f1'

P.
    (a. P a []) (a l. P (0 :: a) l P a ( :: l))
    (a l. P (1 :: a) l P a ( :: l)) v v1. P v v1

(f. sum_num.SUM 0 f = 0)
  (m f.
     sum_num.SUM (bit1 m) f =
     sum_num.SUM (arithmetic.- (bit1 m) 1) f +
     f (arithmetic.- (bit1 m) 1))
  m f.
    sum_num.SUM (arithmetic.BIT2 m) f = sum_num.SUM (bit1 m) f + f (bit1 m)

(n. words.word_lsl (words.n2w 0) n = words.n2w 0)
  (n. words.word_asr (words.n2w 0) n = words.n2w 0)
  (n. words.word_lsr (words.n2w 0) n = words.n2w 0)
  (n. words.word_rol (words.n2w 0) n = words.n2w 0)
  n. words.word_ror (words.n2w 0) n = words.n2w 0

v w.
    pred_set.FINITE pred_set.UNIV pred_set.FINITE pred_set.UNIV
    fcp.dimindex bool.the_value + fcp.dimindex bool.the_value
    fcp.dimindex bool.the_value
    words.word_extract (arithmetic.- (fcp.dimindex bool.the_value) 1) 0
      (words.word_concat v w) = w
    words.word_extract
      (arithmetic.-
         (fcp.dimindex bool.the_value + fcp.dimindex bool.the_value) 1)
      (fcp.dimindex bool.the_value) (words.word_concat v w) = v

P.
    (i n.
       (¬(n = 0) odd n P (suc i) (n div arithmetic.BIT2 0))
       (¬(n = 0) ¬odd n P (suc i) (n div arithmetic.BIT2 0)) P i n)
    v v1. P v v1

sum_num.GSUM_tupled =
  relation.WFREC
    (select R. wellFounded R f m n. R ((n, m), f) ((n, suc m), f))
    (λGSUM_tupled a.
       pair.pair_CASE a
         (λv f.
            pair.pair_CASE v
              (λn v3.
                 arithmetic.num_CASE v3 (id 0)
                   (λm. id (GSUM_tupled ((n, m), f) + f (n + m))))))

c a b.
    words.word_lo a (words.word_add b c)
    if words.word_ls c a then
      bool.LET
        (λx.
           words.word_lo x b
           (c = words.n2w 0
            words.word_lo b (words.word_add (words.word_2comp a) x)))
        (words.n2w (arithmetic.- (words.w2n a) (words.w2n c)))
    else
      words.word_lo b (words.word_2comp c)
      words.word_lo (words.word_add (words.word_2comp c) a) b

c a b.
    words.word_ls a (words.word_add b c)
    if words.word_ls c a then
      bool.LET
        (λx.
           words.word_ls x b
           (c = words.n2w 0
            words.word_lo b (words.word_add (words.word_2comp a) x)))
        (words.n2w (arithmetic.- (words.w2n a) (words.w2n c)))
    else
      words.word_lo b (words.word_2comp c)
      words.word_ls (words.word_add (words.word_2comp c) a) b

m n f.
    sum_num.SUM m f = sum_num.SUM n f
    m n (q. m q q < n f q = 0)
    n < m q. n q q < m f q = 0

b c a.
    words.word_lo (words.word_add a b) c
    if words.word_ls b c then
      bool.LET
        (λx.
           words.word_lo a x
           ¬(b = words.n2w 0)
           words.word_ls (words.word_add (words.word_2comp c) x) a)
        (words.n2w (arithmetic.- (words.w2n c) (words.w2n b)))
    else
      words.word_ls (words.word_2comp b) a
      words.word_lo a (words.word_add (words.word_2comp b) c)

b c a.
    words.word_ls (words.word_add a b) c
    if words.word_ls b c then
      bool.LET
        (λx.
           words.word_ls a x
           ¬(b = words.n2w 0)
           words.word_ls (words.word_add (words.word_2comp c) x) a)
        (words.n2w (arithmetic.- (words.w2n c) (words.w2n b)))
    else
      words.word_ls (words.word_2comp b) a
      words.word_ls a (words.word_add (words.word_2comp b) c)

a b.
    words.nzcv a b =
    bool.LET
      (λq.
         bool.LET
           (λr.
              (words.word_msb r, r = words.n2w 0,
               bit.BIT (fcp.dimindex bool.the_value) q b = words.n2w 0,
               ¬(words.word_msb a words.word_msb b)
               ¬(words.word_msb r words.word_msb a))) (words.n2w q))
      (words.w2n a + words.w2n (words.word_2comp b))

(v0 l. bitstring.extend v0 0 l = l)
  (c n l.
     bitstring.extend c (bit1 n) l =
     bitstring.extend c (arithmetic.- (bit1 n) 1) (c :: l))
  c n l.
    bitstring.extend c (arithmetic.BIT2 n) l =
    bitstring.extend c (bit1 n) (c :: l)

words.INT_MIN bool.the_value = arithmetic.BIT2 70368744177663

s t.
    words.word_smod s t =
    bool.LET
      (bool.LET
         (λabs_s abs_t.
            bool.LET
              (λu.
                 if u = words.n2w 0 then u
                 else if words.word_msb s then
                   if words.word_msb t then words.word_2comp u
                   else words.word_add (words.word_2comp u) t
                 else if words.word_msb t then words.word_add u t
                 else u) (words.word_mod abs_s abs_t))
         (if words.word_msb s then words.word_2comp s else s))
      (if words.word_msb t then words.word_2comp t else t)

a b c.
    pred_set.FINITE pred_set.UNIV pred_set.FINITE pred_set.UNIV
    pred_set.FINITE pred_set.UNIV
    fcp.dimindex bool.the_value =
    fcp.dimindex bool.the_value + fcp.dimindex bool.the_value
    fcp.dimindex bool.the_value =
    fcp.dimindex bool.the_value + fcp.dimindex bool.the_value
    fcp.dimindex bool.the_value =
    fcp.dimindex bool.the_value + fcp.dimindex bool.the_value
    words.word_concat (words.word_concat a b) c =
    words.word_concat a (words.word_concat b c)

words.dimword bool.the_value = arithmetic.BIT2 140737488355327

x y carry_in.
    words.add_with_carry (x, y, carry_in) =
    bool.LET
      (λunsigned_sum.
         bool.LET
           (λresult.
              bool.LET
                (bool.LET
                   (λcarry_out overflow. (result, carry_out, overflow))
                   (¬(words.w2n result = unsigned_sum)))
                ((words.word_msb x words.word_msb y)
                 ¬(words.word_msb x words.word_msb result)))
           (words.n2w unsigned_sum))
      (words.w2n x + words.w2n y + if carry_in then 1 else 0)

(n v w.
     words.word_and (words.word_lsl w n) (words.word_lsl v n) =
     words.word_lsl (words.word_and w v) n)
  (n v w.
     words.word_or (words.word_lsl w n) (words.word_lsl v n) =
     words.word_lsl (words.word_or w v) n)
  n v w.
    words.word_xor (words.word_lsl w n) (words.word_lsl v n) =
    words.word_lsl (words.word_xor w v) n

(n v w.
     words.word_and (words.word_lsr w n) (words.word_lsr v n) =
     words.word_lsr (words.word_and w v) n)
  (n v w.
     words.word_or (words.word_lsr w n) (words.word_lsr v n) =
     words.word_lsr (words.word_or w v) n)
  n v w.
    words.word_xor (words.word_lsr w n) (words.word_lsr v n) =
    words.word_lsr (words.word_xor w v) n

(n v w.
     words.word_and (words.word_rol w n) (words.word_rol v n) =
     words.word_rol (words.word_and w v) n)
  (n v w.
     words.word_or (words.word_rol w n) (words.word_rol v n) =
     words.word_rol (words.word_or w v) n)
  n v w.
    words.word_xor (words.word_rol w n) (words.word_rol v n) =
    words.word_rol (words.word_xor w v) n

(n v w.
     words.word_and (words.word_ror w n) (words.word_ror v n) =
     words.word_ror (words.word_and w v) n)
  (n v w.
     words.word_or (words.word_ror w n) (words.word_ror v n) =
     words.word_ror (words.word_or w v) n)
  n v w.
    words.word_xor (words.word_ror w n) (words.word_ror v n) =
    words.word_ror (words.word_xor w v) n

M M' f f1 v.
    M = M' (a. M' = fcp.BIT1A a f a = f' a)
    (a. M' = fcp.BIT1B a f1 a = f1' a) (M' = fcp.BIT1C v = v')
    fcp.bit1_CASE M f f1 v = fcp.bit1_CASE M' f' f1' v'

h m l w.
    arithmetic.- h m = fcp.dimindex bool.the_value
    arithmetic.- (m + 1) l = fcp.dimindex bool.the_value
    arithmetic.- (h + 1) l = fcp.dimindex bool.the_value
    ¬(fcp.dimindex bool.the_value = 1)
    words.word_concat (words.word_extract h (m + 1) w)
      (words.word_extract m l w) = words.word_extract h l w

h m m' l s w.
    l m m' h m' = m + 1 s = arithmetic.- m' l
    words.word_add (words.word_lsl (words.word_extract h m' w) s)
      (words.word_extract m l w) =
    words.word_extract
      (min h
         (min (arithmetic.- (fcp.dimindex bool.the_value + l) 1)
            (arithmetic.- (fcp.dimindex bool.the_value) 1))) l w

h m m' l s w.
    l m m' h m' = m + 1 s = arithmetic.- m' l
    words.word_or (words.word_lsl (words.word_extract h m' w) s)
      (words.word_extract m l w) =
    words.word_extract
      (min h
         (min (arithmetic.- (fcp.dimindex bool.the_value + l) 1)
            (arithmetic.- (fcp.dimindex bool.the_value) 1))) l w

n a b.
    n < fcp.dimindex bool.the_value
    (fcp.fcp_index (words.word_add a b) n
     if n = 0 then ¬(fcp.fcp_index a 0 fcp.fcp_index b 0)
     else if fcp.fcp_index
               (words.word_add (words.word_bits (arithmetic.- n 1) 0 a)
                  (words.word_bits (arithmetic.- n 1) 0 b)) n
     then fcp.fcp_index a n fcp.fcp_index b n
     else ¬(fcp.fcp_index a n fcp.fcp_index b n))

p m n f.
    sum_num.GSUM (p, m) f = sum_num.GSUM (p, n) f
    m n (q. p + m q q < p + n f q = 0)
    n < m q. p + n q q < p + m f q = 0

v w.
    words.word_mul (words.n2w 0) v = words.n2w 0
    words.word_mul v (words.n2w 0) = words.n2w 0
    words.word_mul (words.n2w 1) v = v
    words.word_mul v (words.n2w 1) = v
    words.word_mul (words.word_add v (words.n2w 1)) w =
    words.word_add (words.word_mul v w) w
    words.word_mul v (words.word_add w (words.n2w 1)) =
    words.word_add v (words.word_mul v w)

bitstring.bitify_tupled =
  relation.WFREC
    (select R.
       wellFounded R (l a. R (0 :: a, l) (a, :: l))
       l a. R (1 :: a, l) (a, :: l))
    (λbitify_tupled a'.
       pair.pair_CASE a'
         (λa v1.
            list.list_CASE v1 (id a)
              (λv2 l.
                 if v2 then id (bitify_tupled (1 :: a, l))
                 else id (bitify_tupled (0 :: a, l)))))

(n f. sum_num.GSUM (n, 0) f = 0)
  (n m f.
     sum_num.GSUM (n, bit1 m) f =
     sum_num.GSUM (n, arithmetic.- (bit1 m) 1) f +
     f (n + arithmetic.- (bit1 m) 1))
  n m f.
    sum_num.GSUM (n, arithmetic.BIT2 m) f =
    sum_num.GSUM (n, bit1 m) f + f (n + bit1 m)

(h l w.
     fcp.dimindex bool.the_value fcp.dimindex bool.the_value + l
     fcp.dimindex bool.the_value h
     words.word_extract h l w =
     words.word_extract (arithmetic.- (fcp.dimindex bool.the_value) 1) l
       w)
  h l w.
    fcp.dimindex bool.the_value + l < fcp.dimindex bool.the_value
    fcp.dimindex bool.the_value + l h
    words.word_extract h l w =
    words.word_extract (arithmetic.- (fcp.dimindex bool.the_value + l) 1) l
      w

words.INT_MIN bool.the_value = arithmetic.BIT2 4611686018427387903

h m m' l s n w.
    l m m' h m' = m + 1 s = arithmetic.- m' l + n
    words.word_add (words.word_lsl (words.word_extract h m' w) s)
      (words.word_lsl (words.word_extract m l w) n) =
    words.word_lsl
      (words.word_extract
         (min h
            (min (arithmetic.- (fcp.dimindex bool.the_value + l) 1)
               (arithmetic.- (fcp.dimindex bool.the_value) 1))) l w) n

h m m' l s n w.
    l m m' h m' = m + 1 s = arithmetic.- m' l + n
    words.word_or (words.word_lsl (words.word_extract h m' w) s)
      (words.word_lsl (words.word_extract m l w) n) =
    words.word_lsl
      (words.word_extract
         (min h
            (min (arithmetic.- (fcp.dimindex bool.the_value + l) 1)
               (arithmetic.- (fcp.dimindex bool.the_value) 1))) l w) n

words.dimword bool.the_value = arithmetic.BIT2 9223372036854775807

(h l v w.
     words.word_and (words.word_bits h l v) (words.word_bits h l w) =
     words.word_bits h l (words.word_and v w))
  (h l v w.
     words.word_or (words.word_bits h l v) (words.word_bits h l w) =
     words.word_bits h l (words.word_or v w))
  h l v w.
    words.word_xor (words.word_bits h l v) (words.word_bits h l w) =
    words.word_bits h l (words.word_xor v w)

(h l v w.
     words.word_and (words.word_slice h l v) (words.word_slice h l w) =
     words.word_slice h l (words.word_and v w))
  (h l v w.
     words.word_or (words.word_slice h l v) (words.word_slice h l w) =
     words.word_slice h l (words.word_or v w))
  h l v w.
    words.word_xor (words.word_slice h l v) (words.word_slice h l w) =
    words.word_slice h l (words.word_xor v w)

(h l v w.
     words.word_and (words.word_extract h l v) (words.word_extract h l w) =
     words.word_extract h l (words.word_and v w))
  (h l v w.
     words.word_or (words.word_extract h l v) (words.word_extract h l w) =
     words.word_extract h l (words.word_or v w))
  h l v w.
    words.word_xor (words.word_extract h l v) (words.word_extract h l w) =
    words.word_extract h l (words.word_xor v w)

w m.
    words.word_lsl_bv w m =
    if fcp.dimindex bool.the_value = 1 then
      fcp.FCP (const (¬fcp.fcp_index m 0 fcp.fcp_index w 0))
    else
      fcp.FCP
        (λk.
           list.FOLDL
             (λa j.
                a
                words.word_bits
                  (bit.LOG2 (arithmetic.- (fcp.dimindex bool.the_value) 1))
                  0 m = words.n2w j j k
                fcp.fcp_index w (arithmetic.- k j))
             (rich_list.COUNT_LIST (fcp.dimindex bool.the_value))
           words.word_bits (arithmetic.- (fcp.dimindex bool.the_value) 1)
             (bit.LOG2 (arithmetic.- (fcp.dimindex bool.the_value) 1) + 1)
             m = words.n2w 0)

(x y c. blast.BCARRY 0 x y c c)
  (i x y c.
     blast.BCARRY (bit1 i) x y c
     blast.bcarry (x (arithmetic.- (bit1 i) 1))
       (y (arithmetic.- (bit1 i) 1))
       (blast.BCARRY (arithmetic.- (bit1 i) 1) x y c))
  i x y c.
    blast.BCARRY (arithmetic.BIT2 i) x y c
    blast.bcarry (x (bit1 i)) (y (bit1 i)) (blast.BCARRY (bit1 i) x y c)

w m.
    words.word_lsr_bv w m =
    if fcp.dimindex bool.the_value = 1 then
      fcp.FCP (const (¬fcp.fcp_index m 0 fcp.fcp_index w 0))
    else
      fcp.FCP
        (λk.
           list.FOLDL
             (λa j.
                a
                words.word_bits
                  (bit.LOG2 (arithmetic.- (fcp.dimindex bool.the_value) 1))
                  0 m = words.n2w j k + j < fcp.dimindex bool.the_value
                fcp.fcp_index w (k + j))
             (rich_list.COUNT_LIST (fcp.dimindex bool.the_value))
           words.word_bits (arithmetic.- (fcp.dimindex bool.the_value) 1)
             (bit.LOG2 (arithmetic.- (fcp.dimindex bool.the_value) 1) + 1)
             m = words.n2w 0)

(w n.
     n < words.dimword bool.the_value
     words.word_lsl w n = words.word_lsl_bv w (words.n2w n))
  (w n.
     n < words.dimword bool.the_value
     words.word_asr w n = words.word_asr_bv w (words.n2w n))
  (w n.
     n < words.dimword bool.the_value
     words.word_lsr w n = words.word_lsr_bv w (words.n2w n))
  (w n.
     words.word_ror w n =
     words.word_ror_bv w (words.n2w (n mod fcp.dimindex bool.the_value)))
  w n.
    words.word_rol w n =
    words.word_rol_bv w (words.n2w (n mod fcp.dimindex bool.the_value))

((a b. fst (words.add_with_carry (a, b, )) = words.word_add a b)
   (a b.
      fst (words.add_with_carry (a, words.word_1comp b, )) =
      words.word_sub a b)
   a b.
     fst (words.add_with_carry (words.word_1comp a, b, )) =
     words.word_sub b a)
  (n a.
     fst (words.add_with_carry (a, words.n2w n, )) =
     words.word_sub a (words.word_1comp (words.n2w n)))
  n b.
    fst (words.add_with_carry (words.n2w n, b, )) =
    words.word_sub b (words.word_1comp (words.n2w n))

w m.
    words.word_asr_bv w m =
    if fcp.dimindex bool.the_value = 1 then
      fcp.FCP (const (fcp.fcp_index w 0))
    else
      fcp.FCP
        (λk.
           list.FOLDL
             (λa j.
                a
                words.word_bits
                  (bit.LOG2 (arithmetic.- (fcp.dimindex bool.the_value) 1))
                  0 m = words.n2w j fcp.fcp_index (words.word_asr w j) k)
              (rich_list.COUNT_LIST (fcp.dimindex bool.the_value))
           words.word_bits (arithmetic.- (fcp.dimindex bool.the_value) 1)
             (bit.LOG2 (arithmetic.- (fcp.dimindex bool.the_value) 1) + 1)
             m = words.n2w 0
           words.word_lo
             (words.n2w (arithmetic.- (fcp.dimindex bool.the_value) 1)) m
           fcp.fcp_index w (arithmetic.- (fcp.dimindex bool.the_value) 1))

words.BIT_SET_tupled =
  relation.WFREC
    (select R.
       wellFounded R
       (i n.
          ¬(n = 0) odd n R (suc i, n div arithmetic.BIT2 0) (i, n))
       i n. ¬(n = 0) ¬odd n R (suc i, n div arithmetic.BIT2 0) (i, n))
    (λBIT_SET_tupled a.
       pair.pair_CASE a
         (λi n.
            id
              (if n = 0 then pred_set.EMPTY
               else if odd n then
                 pred_set.INSERT i
                   (BIT_SET_tupled (suc i, n div arithmetic.BIT2 0))
               else BIT_SET_tupled (suc i, n div arithmetic.BIT2 0))))

(n m.
     words.word_and (words.n2w n) (words.n2w m) =
     words.n2w
       (bit.BITWISE (suc (min (bit.LOG2 n) (bit.LOG2 m))) () n m))
  (n m.
     words.word_and (words.n2w n) (words.word_1comp (words.n2w m)) =
     words.n2w (bit.BITWISE (suc (bit.LOG2 n)) (λa b. a ¬b) n m))
  (n m.
     words.word_and (words.word_1comp (words.n2w m)) (words.n2w n) =
     words.n2w (bit.BITWISE (suc (bit.LOG2 n)) (λa b. a ¬b) n m))
  n m.
    words.word_and (words.word_1comp (words.n2w n))
      (words.word_1comp (words.n2w m)) =
    words.word_1comp
      (words.n2w
         (bit.BITWISE (suc (max (bit.LOG2 n) (bit.LOG2 m))) () n m))

(n m.
     words.word_or (words.n2w n) (words.n2w m) =
     words.n2w
       (bit.BITWISE (suc (max (bit.LOG2 n) (bit.LOG2 m))) () n m))
  (n m.
     words.word_or (words.n2w n) (words.word_1comp (words.n2w m)) =
     words.word_1comp
       (words.n2w (bit.BITWISE (suc (bit.LOG2 m)) (λa b. a ¬b) m n)))
  (n m.
     words.word_or (words.word_1comp (words.n2w m)) (words.n2w n) =
     words.word_1comp
       (words.n2w (bit.BITWISE (suc (bit.LOG2 m)) (λa b. a ¬b) m n)))
  n m.
    words.word_or (words.word_1comp (words.n2w n))
      (words.word_1comp (words.n2w m)) =
    words.word_1comp
      (words.n2w
         (bit.BITWISE (suc (min (bit.LOG2 n) (bit.LOG2 m))) () n m))

words.INT_MIN bool.the_value =
  arithmetic.BIT2 19807040628566084398385987583

words.dimword bool.the_value =
  arithmetic.BIT2 39614081257132168796771975167

(v w. words.word_add (words.word_2comp w) v = words.word_sub v w)
  (v w. words.word_add v (words.word_2comp w) = words.word_sub v w)
  (x y z.
     words.word_add (words.word_mul (words.word_2comp x) y) z =
     words.word_sub z (words.word_mul x y))
  (x y z.
     words.word_add z (words.word_mul (words.word_2comp x) y) =
     words.word_sub z (words.word_mul x y))
  (x.
     words.word_mul (words.word_2comp (words.n2w 1)) x =
     words.word_2comp x)
  (x y z.
     words.word_sub z (words.word_mul (words.word_2comp x) y) =
     words.word_add z (words.word_mul x y))
  x y z.
    words.word_sub (words.word_mul (words.word_2comp x) y) z =
    words.word_2comp (words.word_add (words.word_mul x y) z)

w v n.
    words.word_reverse (words.word_reverse w) = w
    words.word_reverse (words.word_lsl w n) =
    words.word_lsr (words.word_reverse w) n
    words.word_reverse (words.word_lsr w n) =
    words.word_lsl (words.word_reverse w) n
    words.word_reverse (words.word_or w v) =
    words.word_or (words.word_reverse w) (words.word_reverse v)
    words.word_reverse (words.word_and w v) =
    words.word_and (words.word_reverse w) (words.word_reverse v)
    words.word_reverse (words.word_xor w v) =
    words.word_xor (words.word_reverse w) (words.word_reverse v)
    words.word_reverse (words.word_1comp w) =
    words.word_1comp (words.word_reverse w)
    words.word_reverse (words.n2w 0) = words.n2w 0
    words.word_reverse (words.word_2comp (words.n2w 1)) =
    words.word_2comp (words.n2w 1)
    (words.word_reverse w = words.n2w 0 w = words.n2w 0)
    (words.word_reverse w = words.word_2comp (words.n2w 1)
     w = words.word_2comp (words.n2w 1))

words.INT_MIN bool.the_value =
  arithmetic.BIT2 85070591730234615865843651857942052863

words.dimword bool.the_value =
  arithmetic.BIT2 170141183460469231731687303715884105727

(w x.
     (alignment.aligned 1
        (words.word_add w
           (words.word_mul (words.n2w (arithmetic.BIT2 0)) x))
      alignment.aligned 1 w)
     (alignment.aligned 1
        (words.word_sub w
           (words.word_mul (words.n2w (arithmetic.BIT2 0)) x))
      alignment.aligned 1 w))
  (x.
     alignment.aligned 1
       (words.word_mul (words.n2w (arithmetic.BIT2 0)) x)
     alignment.aligned 1
       (words.word_mul (words.word_2comp (words.n2w (arithmetic.BIT2 0)))
          x))
  (w x.
     (alignment.aligned (arithmetic.BIT2 0)
        (words.word_add w
           (words.word_mul (words.n2w (arithmetic.BIT2 1)) x))
      alignment.aligned (arithmetic.BIT2 0) w)
     (alignment.aligned (arithmetic.BIT2 0)
        (words.word_sub w
           (words.word_mul (words.n2w (arithmetic.BIT2 1)) x))
      alignment.aligned (arithmetic.BIT2 0) w))
  (x.
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_mul (words.n2w (arithmetic.BIT2 1)) x)
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_mul (words.word_2comp (words.n2w (arithmetic.BIT2 1)))
          x))
  (w x.
     (alignment.aligned 3
        (words.word_add w
           (words.word_mul (words.n2w (arithmetic.BIT2 3)) x))
      alignment.aligned 3 w)
     (alignment.aligned 3
        (words.word_sub w
           (words.word_mul (words.n2w (arithmetic.BIT2 3)) x))
      alignment.aligned 3 w))
  x.
    alignment.aligned 3
      (words.word_mul (words.n2w (arithmetic.BIT2 3)) x)
    alignment.aligned 3
      (words.word_mul (words.word_2comp (words.n2w (arithmetic.BIT2 3))) x)

(v n.
     words.word_or (bitstring.v2w v) (words.n2w n) =
     words.word_or (bitstring.v2w v) (bitstring.v2w (bitstring.n2v n)))
  (v n.
     words.word_or (words.n2w n) (bitstring.v2w v) =
     words.word_or (bitstring.v2w (bitstring.n2v n)) (bitstring.v2w v))
  (v n.
     words.word_and (bitstring.v2w v) (words.n2w n) =
     words.word_and (bitstring.v2w v) (bitstring.v2w (bitstring.n2v n)))
  (v n.
     words.word_and (words.n2w n) (bitstring.v2w v) =
     words.word_and (bitstring.v2w (bitstring.n2v n)) (bitstring.v2w v))
  (v n.
     words.word_xor (bitstring.v2w v) (words.n2w n) =
     words.word_xor (bitstring.v2w v) (bitstring.v2w (bitstring.n2v n)))
  (v n.
     words.word_xor (words.n2w n) (bitstring.v2w v) =
     words.word_xor (bitstring.v2w (bitstring.n2v n)) (bitstring.v2w v))
  (v n.
     words.word_nor (bitstring.v2w v) (words.n2w n) =
     words.word_nor (bitstring.v2w v) (bitstring.v2w (bitstring.n2v n)))
  (v n.
     words.word_nor (words.n2w n) (bitstring.v2w v) =
     words.word_nor (bitstring.v2w (bitstring.n2v n)) (bitstring.v2w v))
  (v n.
     words.word_nand (bitstring.v2w v) (words.n2w n) =
     words.word_nand (bitstring.v2w v) (bitstring.v2w (bitstring.n2v n)))
  (v n.
     words.word_nand (words.n2w n) (bitstring.v2w v) =
     words.word_nand (bitstring.v2w (bitstring.n2v n)) (bitstring.v2w v))
  (v n.
     words.word_xnor (bitstring.v2w v) (words.n2w n) =
     words.word_xnor (bitstring.v2w v) (bitstring.v2w (bitstring.n2v n)))
  (v n.
     words.word_xnor (words.n2w n) (bitstring.v2w v) =
     words.word_xnor (bitstring.v2w (bitstring.n2v n)) (bitstring.v2w v))
  (v n.
     words.word_concat (bitstring.v2w v) (words.n2w n) =
     words.word_concat (bitstring.v2w v)
       (bitstring.v2w (bitstring.n2v n)))
  (v n.
     words.word_concat (words.n2w n) (bitstring.v2w v) =
     words.word_concat (bitstring.v2w (bitstring.n2v n))
       (bitstring.v2w v))
  (v n.
     words.word_join (bitstring.v2w v) (words.n2w n) =
     words.word_join (bitstring.v2w v) (bitstring.v2w (bitstring.n2v n)))
  v n.
    words.word_join (words.n2w n) (bitstring.v2w v) =
    words.word_join (bitstring.v2w (bitstring.n2v n)) (bitstring.v2w v)

(v.
     words.word_2comp (bitstring.v2w v) =
     words.word_2comp (words.n2w (bitstring.v2n v)))
  (v.
     words.word_log2 (bitstring.v2w v) =
     words.word_log2 (words.n2w (bitstring.v2n v)))
  (v n.
     bitstring.v2w v = words.n2w n
     words.n2w (bitstring.v2n v) = words.n2w n)
  (v n.
     words.n2w n = bitstring.v2w v
     words.n2w n = words.n2w (bitstring.v2n v))
  (v w.
     words.word_add (bitstring.v2w v) w =
     words.word_add (words.n2w (bitstring.v2n v)) w)
  (v w.
     words.word_add w (bitstring.v2w v) =
     words.word_add w (words.n2w (bitstring.v2n v)))
  (v w.
     words.word_sub (bitstring.v2w v) w =
     words.word_sub (words.n2w (bitstring.v2n v)) w)
  (v w.
     words.word_sub w (bitstring.v2w v) =
     words.word_sub w (words.n2w (bitstring.v2n v)))
  (v w.
     words.word_mul (bitstring.v2w v) w =
     words.word_mul (words.n2w (bitstring.v2n v)) w)
  (v w.
     words.word_mul w (bitstring.v2w v) =
     words.word_mul w (words.n2w (bitstring.v2n v)))
  (v w.
     words.word_sdiv (bitstring.v2w v) w =
     words.word_sdiv (words.n2w (bitstring.v2n v)) w)
  (v w.
     words.word_sdiv w (bitstring.v2w v) =
     words.word_sdiv w (words.n2w (bitstring.v2n v)))
  (v w.
     words.word_div (bitstring.v2w v) w =
     words.word_div (words.n2w (bitstring.v2n v)) w)
  (v w.
     words.word_div w (bitstring.v2w v) =
     words.word_div w (words.n2w (bitstring.v2n v)))
  (v w.
     words.word_mod (bitstring.v2w v) w =
     words.word_mod (words.n2w (bitstring.v2n v)) w)
  (v w.
     words.word_mod w (bitstring.v2w v) =
     words.word_mod w (words.n2w (bitstring.v2n v)))
  (v w.
     words.word_lt (bitstring.v2w v) w
     words.word_lt (words.n2w (bitstring.v2n v)) w)
  (v w.
     words.word_lt w (bitstring.v2w v)
     words.word_lt w (words.n2w (bitstring.v2n v)))
  (v w.
     words.word_gt (bitstring.v2w v) w
     words.word_gt (words.n2w (bitstring.v2n v)) w)
  (v w.
     words.word_gt w (bitstring.v2w v)
     words.word_gt w (words.n2w (bitstring.v2n v)))
  (v w.
     words.word_le (bitstring.v2w v) w
     words.word_le (words.n2w (bitstring.v2n v)) w)
  (v w.
     words.word_le w (bitstring.v2w v)
     words.word_le w (words.n2w (bitstring.v2n v)))
  (v w.
     words.word_ge (bitstring.v2w v) w
     words.word_ge (words.n2w (bitstring.v2n v)) w)
  (v w.
     words.word_ge w (bitstring.v2w v)
     words.word_ge w (words.n2w (bitstring.v2n v)))
  (v w.
     words.word_lo (bitstring.v2w v) w
     words.word_lo (words.n2w (bitstring.v2n v)) w)
  (v w.
     words.word_lo w (bitstring.v2w v)
     words.word_lo w (words.n2w (bitstring.v2n v)))
  (v w.
     words.word_hi (bitstring.v2w v) w
     words.word_hi (words.n2w (bitstring.v2n v)) w)
  (v w.
     words.word_hi w (bitstring.v2w v)
     words.word_hi w (words.n2w (bitstring.v2n v)))
  (v w.
     words.word_ls (bitstring.v2w v) w
     words.word_ls (words.n2w (bitstring.v2n v)) w)
  (v w.
     words.word_ls w (bitstring.v2w v)
     words.word_ls w (words.n2w (bitstring.v2n v)))
  (v w.
     words.word_hs (bitstring.v2w v) w
     words.word_hs (words.n2w (bitstring.v2n v)) w)
  v w.
    words.word_hs w (bitstring.v2w v)
    words.word_hs w (words.n2w (bitstring.v2n v))

(x. alignment.aligned 3 (words.n2w (arithmetic.BIT2 (bit1 (bit1 x)))))
  (x.
     alignment.aligned (arithmetic.BIT2 0)
       (words.n2w (arithmetic.BIT2 (bit1 x))))
  (x. alignment.aligned 1 (words.n2w (arithmetic.BIT2 x)))
  (x.
     alignment.aligned 3
       (words.word_2comp (words.n2w (arithmetic.BIT2 (bit1 (bit1 x))))))
  (x.
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_2comp (words.n2w (arithmetic.BIT2 (bit1 x)))))
  (x.
     alignment.aligned 1
       (words.word_2comp (words.n2w (arithmetic.BIT2 x))))
  (x y f.
     alignment.aligned 3
       (words.word_add y (words.n2w (bit1 (bit1 (bit1 (f x))))))
     alignment.aligned 3 (words.word_add y (words.n2w 7)))
  (x y f.
     alignment.aligned 3
       (words.word_add y (words.n2w (bit1 (bit1 (arithmetic.BIT2 x)))))
     alignment.aligned 3 (words.word_add y (words.n2w 3)))
  (x y f.
     alignment.aligned 3
       (words.word_add y (words.n2w (bit1 (arithmetic.BIT2 (bit1 x)))))
     alignment.aligned 3 (words.word_add y (words.n2w 1)))
  (x y f.
     alignment.aligned 3
       (words.word_add y
          (words.n2w (bit1 (arithmetic.BIT2 (arithmetic.BIT2 x)))))
     alignment.aligned 3
       (words.word_add y (words.n2w (bit1 (arithmetic.BIT2 0)))))
  (x y f.
     alignment.aligned 3
       (words.word_add y (words.n2w (arithmetic.BIT2 (bit1 (bit1 x)))))
     alignment.aligned 3 y)
  (x y f.
     alignment.aligned 3
       (words.word_add y
          (words.n2w (arithmetic.BIT2 (bit1 (arithmetic.BIT2 x)))))
     alignment.aligned 3
       (words.word_add y (words.n2w (arithmetic.BIT2 1))))
  (x y f.
     alignment.aligned 3
       (words.word_add y
          (words.n2w (arithmetic.BIT2 (arithmetic.BIT2 (bit1 x)))))
     alignment.aligned 3
       (words.word_add y (words.n2w (arithmetic.BIT2 0))))
  (x y f.
     alignment.aligned 3
       (words.word_add y
          (words.n2w
             (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 x)))))
     alignment.aligned 3
       (words.word_add y
          (words.n2w (arithmetic.BIT2 (arithmetic.BIT2 0)))))
  (x y f.
     alignment.aligned 3
       (words.word_sub y (words.n2w (bit1 (bit1 (bit1 (f x))))))
     alignment.aligned 3 (words.word_sub y (words.n2w 7)))
  (x y f.
     alignment.aligned 3
       (words.word_sub y (words.n2w (bit1 (bit1 (arithmetic.BIT2 x)))))
     alignment.aligned 3 (words.word_sub y (words.n2w 3)))
  (x y f.
     alignment.aligned 3
       (words.word_sub y (words.n2w (bit1 (arithmetic.BIT2 (bit1 x)))))
     alignment.aligned 3 (words.word_sub y (words.n2w 1)))
  (x y f.
     alignment.aligned 3
       (words.word_sub y
          (words.n2w (bit1 (arithmetic.BIT2 (arithmetic.BIT2 x)))))
     alignment.aligned 3
       (words.word_sub y (words.n2w (bit1 (arithmetic.BIT2 0)))))
  (x y f.
     alignment.aligned 3
       (words.word_sub y (words.n2w (arithmetic.BIT2 (bit1 (bit1 x)))))
     alignment.aligned 3 y)
  (x y f.
     alignment.aligned 3
       (words.word_sub y
          (words.n2w (arithmetic.BIT2 (bit1 (arithmetic.BIT2 x)))))
     alignment.aligned 3
       (words.word_sub y (words.n2w (arithmetic.BIT2 1))))
  (x y f.
     alignment.aligned 3
       (words.word_sub y
          (words.n2w (arithmetic.BIT2 (arithmetic.BIT2 (bit1 x)))))
     alignment.aligned 3
       (words.word_sub y (words.n2w (arithmetic.BIT2 0))))
  (x y f.
     alignment.aligned 3
       (words.word_sub y
          (words.n2w
             (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 x)))))
     alignment.aligned 3
       (words.word_sub y
          (words.n2w (arithmetic.BIT2 (arithmetic.BIT2 0)))))
  (x y f.
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_add y (words.n2w (bit1 (bit1 (f x)))))
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_add y (words.n2w 3)))
  (x y.
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_add y (words.n2w (bit1 (arithmetic.BIT2 x))))
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_add y (words.n2w 1)))
  (x y.
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_add y (words.n2w (arithmetic.BIT2 (bit1 x))))
     alignment.aligned (arithmetic.BIT2 0) y)
  (x y.
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_add y
          (words.n2w (arithmetic.BIT2 (arithmetic.BIT2 x))))
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_add y (words.n2w (arithmetic.BIT2 0))))
  (x y f.
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_sub y (words.n2w (bit1 (bit1 (f x)))))
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_sub y (words.n2w 3)))
  (x y.
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_sub y (words.n2w (bit1 (arithmetic.BIT2 x))))
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_sub y (words.n2w 1)))
  (x y.
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_sub y (words.n2w (arithmetic.BIT2 (bit1 x))))
     alignment.aligned (arithmetic.BIT2 0) y)
  (x y.
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_sub y
          (words.n2w (arithmetic.BIT2 (arithmetic.BIT2 x))))
     alignment.aligned (arithmetic.BIT2 0)
       (words.word_sub y (words.n2w (arithmetic.BIT2 0))))
  (x y f.
     alignment.aligned 1 (words.word_add y (words.n2w (bit1 (f x))))
     alignment.aligned 1 (words.word_add y (words.n2w 1)))
  (x y f.
     alignment.aligned 1 (words.word_sub y (words.n2w (bit1 (f x))))
     alignment.aligned 1 (words.word_sub y (words.n2w 1)))
  (x y.
     alignment.aligned 1
       (words.word_add y (words.n2w (arithmetic.BIT2 x)))
     alignment.aligned 1 y)
  x y.
    alignment.aligned 1
      (words.word_sub y (words.n2w (arithmetic.BIT2 x)))
    alignment.aligned 1 y

External Type Operators

External Constants

Assumptions

pred_set.FINITE pred_set.EMPTY

wellFounded empty

wellFounded (<)

pred_set.UNIV = λx.

¬(pred_set.UNIV = pred_set.EMPTY)

rich_list.AND_EL = all id

rich_list.OR_EL = any id

pred_set.CARD pred_set.EMPTY = 0

bit.BIT 0 = odd

x. x = x

x. bool.IN x pred_set.UNIV

t. t

n. 0 n

m. m m

s. pred_set.SUBSET s pred_set.UNIV

q. q

¬(t ¬t)

bit.LOG2 = logroot.LOG (arithmetic.BIT2 0)

numposrep.num_to_bin_list = numposrep.n2l (arithmetic.BIT2 0)

numposrep.num_from_bin_list = numposrep.l2n (arithmetic.BIT2 0)

bool.IN = λx f. f x

bool.LET = λf x. f x

1 = suc 0

combin.FAIL x y = x

arithmetic.DIV2 (bit1 x) = x

list.DROP 0 l = l

list.TAKE 0 l = []

¬¬p p

x. ¬bool.IN x pred_set.EMPTY

x. pred_set.FINITE (pred_set.INSERT x pred_set.EMPTY)

x. id x = x

x. marker.Abbrev x x

b. basicSize.bool_size b = 0

b. ¬bit.BIT b 0

n. ¬(n < n)

n. 0 < suc 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.

arithmetic.BIT2 0 = suc 1

¬(p q) p

x. x = x

t. ¬¬t t

n. ¬(suc n = 0)

c. arithmetic.- c c = 0

n. n * 0 = 0

n. min n n = n

l. reverse (reverse l) = l

l. l @ [] = l

f. pred_set.IMAGE f pred_set.EMPTY = pred_set.EMPTY

x. Data.Sum.isLeft x Data.Sum.isRight x

flip = λf x y. f y x

e. f. f bool.the_value = e

¬(p q) ¬q

¬(p q) ¬p

¬(p q) ¬q

t1 t2. (let x t2 in t1) = t1

A. A ¬A

t. ¬t t

t. (t ) ¬t

b. bit.BIT b (arithmetic.BIT2 0 b)

n. 0 < arithmetic.BIT2 0 n

n. odd n ¬even n

x. numeral.iDUB x = x + x

m. m * 1 = m

q. q div 1 = q

k. k mod 1 = 0

l. null l l = []

l. length (reverse l) = length l

l. list.TAKE (length l) l = l

x. ¬Data.Sum.isLeft x Data.Sum.isRight x

x. ¬Data.Sum.isRight x Data.Sum.isLeft x

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

x y. const x y = x

m n. m m + n

n m. arithmetic.- n m n

P. P Data.Unit.() xx. P xx

P. P bool.the_value ii. P ii

() = λp q. p q p

head (list.GENLIST f (suc n)) = f 0

x. pred_set.CARD (pred_set.INSERT x pred_set.EMPTY) = 1

t. t t

t. (t ) (t )

n. arithmetic.DIV2 n = n div arithmetic.BIT2 0

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

m. suc m = m + 1

n. suc n = 1 + n

n. n 0 n = 0

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

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

l. null l length l = 0

l. rich_list.AND_EL l list.FOLDL () l

l. rich_list.OR_EL l list.FOLDL () l

x. (fst x, snd x) = x

x y. ¬(Data.Sum.left x = Data.Sum.right y)

x y. fst (x, y) = x

x y. snd (x, y) = y

h t. head (h :: t) = h

x s. ¬(pred_set.INSERT x s = pred_set.EMPTY)

b t. (if b then t else t) = t

h l. bit.BITS h l 0 = 0

l h. bit.SLICE h l 0 = 0

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

P x. bool.IN x P P x

f n. length (list.GENLIST f n) = n

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

n. ¬(n = 0) 0 < n

n. arithmetic.BIT2 0 * n = n + n

l. 0 < length l ¬null l

l. length l = 0 l = []

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

x. Data.Sum.isLeft x Data.Sum.left (Data.Sum.destLeft x) = x

x. Data.Sum.isRight x Data.Sum.right (Data.Sum.destRight x) = x

(%%genvar%%3036. P %%genvar%%3036) P P

x y. x = y y = x

x s. pred_set.FINITE (pred_set.DELETE s x) pred_set.FINITE s

x s. pred_set.FINITE (pred_set.INSERT x s) pred_set.FINITE s

t1 t2. t1 t2 t2 t1

A B. A B B A

m n. m > n n < m

n m. n m m n

m n. m * n = n * m

m n. m + n = n + m

m n. min m n = min n m

m n. m < n m n

m n. m n n m

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

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

s. pred_set.FINITE s f. pred_set.FINITE (pred_set.IMAGE f s)

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

(¬A ) (A )

1 < b x < b x

n. bit1 n = n + (n + suc 0)

n. 0 < n 0 div n = 0

n. 0 < n 0 mod n = 0

n. ¬(n = 0) bit.BIT (bit.LOG2 n) n

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

m n. m < n suc m n

m n. ¬(m < n) n m

m n. ¬(m n) n < m

m n. ¬(m > n) m n

n f. null (list.GENLIST f n) n = 0

m. m = 0 n. m = suc n

l1 l2. list.DROP (length l1) (l1 @ l2) = l2

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

s. pred_set.SING s x. s = pred_set.INSERT x pred_set.EMPTY

s. (x. bool.IN x s) ¬(s = pred_set.EMPTY)

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

(x. Data.Sum.isLeft (Data.Sum.left x))
  y. ¬Data.Sum.isLeft (Data.Sum.right y)

(x. Data.Sum.isRight (Data.Sum.right x))
  y. ¬Data.Sum.isRight (Data.Sum.left y)

n. odd n n mod arithmetic.BIT2 0 = 1

n. arithmetic.BIT2 n = n + (n + suc (suc 0))

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

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

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

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

x y. bool.IN x (pred_set.INSERT y pred_set.EMPTY) x = y

x l. list.SNOC x l = l @ x :: []

m n. 0 < n m mod n < n

r n. r < n r div n = 0

n k. k < n k mod n = k

m n. ¬(m n) suc n m

m n. ¬(m n) suc m n

m n. suc (m + n) = m + suc n

n h. bit.SLICE h 0 n = bit.BITS h 0 n

i n. bit.LOG2 n < i ¬bit.BIT i n

n m. ¬(suc n m) m n

m n. bool.IN m (list.LIST_TO_SET (rich_list.COUNT_LIST n)) m < n

m n. suc m = suc n m = n

m n. suc m < suc n m < n

n m. suc n suc m n m

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

m n. m + n = m n = 0

n m. arithmetic.- (suc n) (suc m) = arithmetic.- n m

n l. length (list.DROP n l) = arithmetic.- (length l) n

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

s. pred_set.FINITE s t. pred_set.SUBSET t s pred_set.FINITE t

P (bool.LET (λx. N x) M) bool.LET (λx. P (N x)) M

a. 1 < a logroot.LOG a 1 = 0

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

n. min n 0 = 0 min 0 n = 0

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

f. id f = f f id = f

s. pred_set.SING s pred_set.CARD s = 1 pred_set.FINITE s

x y. x y x < y + 1

x n. bit.DIV_2EXP x n = n div arithmetic.BIT2 0 x

x n. bit.MOD_2EXP x n = n mod arithmetic.BIT2 0 x

m n. max m n = if m < n then n else m

m n. min m n = if m < n then m else n

i n. bit.BIT i n arithmetic.BIT2 0 i n

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

m n. n < m n arithmetic.- m 1

m n. m * suc n = m + m * n

x n. bit.SBIT (bit.BIT x n) x = bit.SLICE x x n

n m. bit.BIT n (arithmetic.BIT2 0 m) m = n

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

P l. ¬all P l any ((¬) P) l

P l. ¬any P l all ((¬) P) l

s t.
    pred_set.FINITE (pred_set.UNION s t)
    pred_set.FINITE s pred_set.FINITE t

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

list.GENLIST f (suc n) = f 0 :: list.GENLIST (f suc) n

0 < x y 0 < x y = 0

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

m n. n < m p. p + n = m

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

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

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

P t. (x. x = t P x) () P

ss. (x. ss = Data.Sum.left x) y. ss = Data.Sum.right y

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

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

x s. bool.IN x s pred_set.INSERT x (pred_set.DELETE s x) = s

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

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

b n. bit.SBIT b n = if b then arithmetic.BIT2 0 n else 0

m n. m = n m n n m

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

m n. m n m < n m = n

m n. m n m > n m = n

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

m n. n m arithmetic.- m n + n = m

b n. ¬bit.BIT b n bit.SLICE b b n = 0

n i. bit.BIT n (i div arithmetic.BIT2 0) bit.BIT (suc n) i

i n. n < arithmetic.BIT2 0 i ¬bit.BIT i n

n k. k mod arithmetic.BIT2 0 n < arithmetic.BIT2 0 n

n l. n length l length (list.TAKE n l) = n

n f. 0 < n head (list.GENLIST f n) = f 0

n. 0 < n k. k * n mod n = 0

f n. tail (list.GENLIST f (suc n)) = list.GENLIST (f suc) n

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

(null [] ) h t. null (h :: t)

list.GENLIST f 0 = [] list.GENLIST f n = list.GENLIST_AUX f n []

¬(¬A B) A ¬B

h l n. h < l bit.BITS h l n = 0

h l n. h < l bit.SLICE h l n = 0

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

l. ¬(l = []) list.EL (prim_rec.PRE (length l)) l = last l

f s. pred_set.IMAGE f s = pred_set.GSPEC (λx. (f x, bool.IN x s))

rich_list.COUNT_LIST 0 = []
  n. rich_list.COUNT_LIST (suc n) = list.SNOC n (rich_list.COUNT_LIST n)

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

r n. r < n (n + r) div n = 1

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

h n. bit.BITS h 0 n = n mod arithmetic.BIT2 0 suc h

a b. ¬(a = b) ¬bit.BIT a (arithmetic.BIT2 0 b)

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

l b. 0 < b numposrep.l2n b l < b length l

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

list.EL 0 = head list.EL (suc n) (l :: ls) = list.EL n ls

¬(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 m * p n * p

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

m n p. arithmetic.- m n p m n + p

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

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

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

m n p. min m (min n p) = min (min m n) p

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

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

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

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

m n p. m n n p m p

n. n length l1 list.TAKE n (l1 @ l2) = list.TAKE n l1

n. 1 n = 1 n 1 = n

l1 x l2. list.SNOC x l1 @ l2 = l1 @ x :: l2

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

l. ¬(l = []) rich_list.LASTN 1 l = last l :: []

l. 0 < length l length (tail l) = arithmetic.- (length l) 1

f g n. map f (list.GENLIST g n) = list.GENLIST (f g) n

P x. (y. P y y = x) (select) P = x

s t. s = t x. bool.IN x s bool.IN x t

s t. pred_set.SUBSET s t x. bool.IN x s bool.IN x t

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

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

f v. bool.IN v (pred_set.GSPEC f) x. (v, ) = f x

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

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

b n. bit.BIT b n bit.SLICE b b n = arithmetic.BIT2 0 b

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

x y. 0 < y (x mod y = x x < y)

a b. a < b arithmetic.BIT2 0 a < arithmetic.BIT2 0 b

a b. a b arithmetic.BIT2 0 a arithmetic.BIT2 0 b

m n. 0 < m * n 0 < m 0 < n

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

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

n m. n m = 0 n = 0 0 < m

b n. bit.BIT b (arithmetic.- (arithmetic.BIT2 0 n) 1) b < n

n. 0 < n k. k mod n mod n = k mod n

n. all P (list.GENLIST f n) i. i < n P (f i)

n. any P (list.GENLIST f n) i. i < n P (f i)

l f. ¬null l map f (tail l) = tail (map f l)

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

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

n a b. bit.MOD_2EXP_EQ n a b bit.MOD_2EXP n a = bit.MOD_2EXP n b

h l n. bit.BITS h l n < arithmetic.BIT2 0 arithmetic.- (suc h) l

h l n. bit.BITS h l (bit.SLICE h l n) = bit.BITS h l n

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

n. ¬(n mod arithmetic.BIT2 0 = 1) n mod arithmetic.BIT2 0 = 0

f x s.
    pred_set.IMAGE f (pred_set.INSERT x s) =
    pred_set.INSERT (f x) (pred_set.IMAGE f s)

f n x. x < n list.EL x (list.GENLIST f n) = f x

P. P 0 (n. P n P (suc n)) i. P i

rich_list.COUNT_LIST 0 = []
  n. rich_list.COUNT_LIST (suc n) = 0 :: map suc (rich_list.COUNT_LIST n)

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

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

m n. bit.BIT 0 (m + n) ¬(bit.BIT 0 m bit.BIT 0 n)

h a. a < arithmetic.BIT2 0 suc h bit.BITS h 0 a = a

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

concat [] = [] h t. concat (h :: t) = h @ concat t

x y s. bool.IN x (pred_set.INSERT y s) x = y bool.IN x s

b t1 t2. (if b then t1 else t2) (¬b t1) (b t2)

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

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

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

n a s. n < s ¬bit.BIT n (a * arithmetic.BIT2 0 s)

h l n.
    bit.BITS h l n =
    bit.MOD_2EXP (arithmetic.- (suc h) l) (bit.DIV_2EXP l n)

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

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

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

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

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

h l n. n < arithmetic.BIT2 0 l bit.BITS h l n = 0

n x l. x < n list.EL x (list.TAKE n l) = list.EL x l

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

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

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

l P. all P l n. n < length l P (list.EL n l)

s t x. bool.IN x (pred_set.UNION s t) bool.IN x s bool.IN x t

s t.
    pred_set.INTER s t =
    pred_set.GSPEC (λx. (x, bool.IN x s bool.IN x t))

s t.
    pred_set.UNION s t =
    pred_set.GSPEC (λx. (x, bool.IN x s bool.IN x t))

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

n a.
    bit.MOD_2EXP_MAX n a
    bit.MOD_2EXP n a = arithmetic.- (arithmetic.BIT2 0 n) 1

x n. x < arithmetic.BIT2 0 n x = 0 bit.LOG2 x < n

x y. 1 < x y 1 < x 0 < y

n a. ¬(bit.BITS n n a = 1) bit.BITS n n a = 0

n l.
    n length l
    list.DROP n l = rich_list.LASTN (arithmetic.- (length l) n) l

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

c n s.
    list.PAD_LEFT c n s =
    list.GENLIST (const c) (arithmetic.- n (length s)) @ s

c n s.
    list.PAD_RIGHT c n s =
    s @ list.GENLIST (const c) (arithmetic.- n (length s))

n a s. bit.BIT (n + s) (a * arithmetic.BIT2 0 s) bit.BIT n a

n l1 l2. n < length l1 list.EL n (l1 @ l2) = list.EL n l1

f s t. pred_set.BIJ f s t pred_set.INJ f s t pred_set.SURJ f s t

s x y. bool.IN x (pred_set.DELETE s y) bool.IN x s ¬(x = y)

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

e f. fn. fn 0 = e n. fn (suc n) = f n (fn n)

h l x n. h < l + x ¬bit.BIT x (bit.BITS h l n)

x y. x * y = 1 x = 1 y = 1

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

f e x l. list.FOLDL f e (list.SNOC x l) = f (list.FOLDL f e l) x

reverse [] = [] h t. reverse (h :: t) = reverse t @ h :: []

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

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

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

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

b1 b2 x. b1 x = b2 x x = 0 b1 = b2

i n op a b. n i ¬bit.BIT i (bit.BITWISE n op a b)

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

n m. (i. i n ¬bit.BIT i m) bit.BITS n 0 m = 0

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

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

y s f. bool.IN y (pred_set.IMAGE f s) x. y = f x bool.IN x s

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

s.
    pred_set.FINITE s
    x.
      pred_set.CARD (pred_set.INSERT x s) =
      if bool.IN x s then pred_set.CARD s else suc (pred_set.CARD s)

m n p.
    arithmetic.- m (arithmetic.- n p) =
    if n p then m else arithmetic.- (m + p) n

m n p.
    m + arithmetic.- n p = if n p then m else arithmetic.- (m + n) p

m n p.
    arithmetic.- m n + p = if m n then p else arithmetic.- (m + p) n

b. 1 < b n m. b n = b m n = m

b. 1 < b n m. b m < b n m < n

b. 1 < b n m. b m b n m n

S.
    pred_set.FINITE S
    t f.
      pred_set.BIJ f S t pred_set.FINITE t
      pred_set.CARD S = pred_set.CARD t

(l. list.EL 0 l = head l) l n. list.EL (suc n) l = list.EL n (tail 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'

a b x y. a < x b < y a * b < x * y

k n. 0 < n r q. k = q * n + r r < n

Fn. f. c i r. f (ind_type.CONSTR c i r) = Fn c i r (λn. f (r n))

(∃!x. P x) (x. P x) x y. P x P y x = y

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

n. 0 < n x r. (x * n + r) div n = x + r div n

n. 0 < n j k. (j + k mod n) mod n = (j + k) mod n

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

l1 n.
    length l1 n
    l2. list.EL n (l1 @ l2) = list.EL (arithmetic.- n (length l1)) l2

(f. list.GENLIST f 0 = [])
  f n. list.GENLIST f (suc n) = list.SNOC (f n) (list.GENLIST f n)

(n. n 0 = 1) m n. m suc n = m * m n

x n f a. x < n (bit.BIT x (bit.BIT_MODIFY n f a) f x (bit.BIT x a))

n p.
    arithmetic.BIT2 0 p n n < arithmetic.BIT2 0 suc p
    bit.LOG2 n = p

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)

(f v. const v f = const v) f v. f const v = const (f v)

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

x n a.
    x < n
    (bit.BIT x (bit.BIT_REVERSE n a)
     bit.BIT (arithmetic.- (arithmetic.- n 1) x) a)

n a s.
    s n
    (bit.BIT n (a * arithmetic.BIT2 0 s) bit.BIT (arithmetic.- n s) a)

m n l. m + n < length l list.EL m (list.DROP n l) = list.EL (m + n) l

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

(v f. arithmetic.num_CASE 0 v f = v)
  n v f. arithmetic.num_CASE (suc n) v f = f n

(a f. ind_type.FCONS a f 0 = a)
  a f n. ind_type.FCONS a f (suc n) = f n

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

h l a b.
    bit.BITS h l (a * arithmetic.BIT2 0 suc h + b) = bit.BITS h l b

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

n f g. list.GENLIST f n = list.GENLIST g n x. x < n f x = g x

f.
    (x y. f x = f y x = y)
    s. pred_set.FINITE (pred_set.IMAGE f s) pred_set.FINITE s

(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

h a b.
    bit.BITS h 0 (bit.BITS h 0 a * bit.BITS h 0 b) = bit.BITS h 0 (a * b)

h a b.
    bit.BITS h 0 (bit.BITS h 0 a + bit.BITS h 0 b) = bit.BITS h 0 (a + b)

b n. ¬(n = 0) n < arithmetic.BIT2 0 b i. i < b bit.BIT i n

n. 0 < n j k. (j mod n) * (k mod n) mod n = j * k mod n

n. 0 < n j k. (j mod n + k mod n) mod n = (j + k) mod n

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 h l a. l + n h (bit.BIT n (bit.BITS h l a) bit.BIT (l + n) a)

b h l n. bit.BIT b (bit.SLICE h l n) l b b h bit.BIT b n

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

s.
    pred_set.FINITE s
    t.
      pred_set.FINITE t
      pred_set.CARD (pred_set.UNION s t) +
      pred_set.CARD (pred_set.INTER s t) =
      pred_set.CARD s + pred_set.CARD t

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 n m. n = arithmetic.BIT2 0 * m)
    (odd n m. n = suc (arithmetic.BIT2 0 * m))

P P' Q Q'. (Q (P P')) (P' (Q Q')) (P Q P' Q')

x l.
    all ((>) (arithmetic.BIT2 0)) l x < length l
    (bit.BIT x (numposrep.num_from_bin_list l) list.EL x l = 1)

(y x. Data.Sum.left x = Data.Sum.left y x = y)
  y x. Data.Sum.right x = Data.Sum.right y x = y

h1 l1 h2 l2 n.
    bit.BITS h2 l2 (bit.BITS h1 l1 n) =
    bit.BITS (min h1 (h2 + l1)) (l2 + l1) n

n p q. 0 < n 0 < q n * (p mod q) = n * p mod n * q

m n k. 0 < n 0 < k m div n mod k = m mod n * k div n

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

l1 l2.
    length l1 = length l2
    length (list.ZIP (l1, l2)) = length l1
    length (list.ZIP (l1, l2)) = length l2

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)

n a b.
    bit.BITWISE (suc n) (λc v. ¬c) a b =
    arithmetic.- (arithmetic.- (arithmetic.BIT2 0 suc n) 1)
      (bit.BITS n 0 a)

n a b. 1 < a 0 < b logroot.LOG a (a n * b) = n + logroot.LOG a b

x n op a b.
    x < n
    (bit.BIT x (bit.BITWISE n op a b) op (bit.BIT x a) (bit.BIT x b))

l1 l2.
    l1 = l2
    length l1 = length l2 x. x < length l1 list.EL x l1 = list.EL x l2

l1 l2.
    length l1 = length l2
    (x. x < length l1 list.EL x l1 = list.EL x l2) l1 = l2

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

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

(m m * n m = 0 0 < n) (m n * m m = 0 0 < n)

Q P.
    (n. P n) (n. (m. m < n ¬P m) P n Q n) Q (while.LEAST P)

a n.
    1 < a 0 < n a logroot.LOG a n n n < a suc (logroot.LOG a n)

(m a. numposrep.BOOLIFY 0 m a = a)
  n m a.
    numposrep.BOOLIFY (suc n) m a =
    numposrep.BOOLIFY n (arithmetic.DIV2 m) (odd m :: a)

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)

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

h1 l1 h2 l2 n.
    h2 + l1 h1
    bit.BITS h2 l2 (bit.BITS h1 l1 n) = bit.BITS (h2 + l1) (l2 + l1) n

h l n.
    l suc h
    bit.SBIT (bit.BIT (suc h) n) (arithmetic.- (suc h) l) +
    bit.BITS h l n = bit.BITS (suc h) l n

l1 l2 n.
    length l1 = length l2 n < length l1
    list.EL n (list.ZIP (l1, l2)) = (list.EL n l1, list.EL n l2)

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

h m l n.
    suc m h l m
    bit.SLICE h (suc m) n + bit.SLICE m l n = bit.SLICE h l n

P.
    P pred_set.EMPTY
    (s.
       pred_set.FINITE s P s
       e. ¬bool.IN e s P (pred_set.INSERT e s))
    s. pred_set.FINITE s P s

list.ZIP ([], []) = []
  x1 l1 x2 l2.
    list.ZIP (x1 :: l1, x2 :: l2) = (x1, x2) :: list.ZIP (l1, l2)

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

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.DROP n [] = [])
  n x xs.
    list.DROP n (x :: xs) =
    if n = 0 then x :: xs else list.DROP (arithmetic.- n 1) xs

(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)

n m p. (p < max m n p < m p < n) (max m n < p m < p n < p)

n m p. (min m n < p m < p n < p) (p < min m n p < m p < n)

n m p. (min m n p m p n p) (p min m n p m p n)

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

h l a b.
    (x. l x x h (bit.BIT x a bit.BIT x b))
    bit.BITS h l a = bit.BITS h l b

(n x. 0 < n (x + n) mod n = x mod n)
  n x. 0 < n (n + x) mod n = x mod n

h l a b.
    b < arithmetic.BIT2 0 l
    bit.BITS h l (a * arithmetic.BIT2 0 l + b) =
    bit.BITS h l (a * arithmetic.BIT2 0 l)

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'

f s t.
    pred_set.SURJ f s t
    (x. bool.IN x s bool.IN (f x) t)
    x. bool.IN x t y. bool.IN y s f y = x

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

l h n.
    bit.SIGN_EXTEND l h n =
    bool.LET
      (λm.
         if bit.BIT (arithmetic.- l 1) n then
           arithmetic.- (arithmetic.BIT2 0 h) (arithmetic.BIT2 0 l) + m
         else m) (n mod arithmetic.BIT2 0 l)

a b n.
    ¬(n = 0) arithmetic.BIT2 0 a n n < arithmetic.BIT2 0 b
    i. a i i < b bit.BIT i n

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)

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

f s t.
    pred_set.INJ f s t
    (x. bool.IN x s bool.IN (f x) t)
    x y. bool.IN x s bool.IN y s f x = f y x = y

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

(op x y. bit.BITWISE 0 op x y = 0)
  n op x y.
    bit.BITWISE (suc n) op x y =
    bit.BITWISE n op x y + bit.SBIT (op (bit.BIT n x) (bit.BIT n y)) n

l l' b b' f f'.
    l = l' b = b'
    (x a. bool.IN x (list.LIST_TO_SET l') f a x = f' a x)
    list.FOLDL f b l = list.FOLDL f' b' l'

n a b.
    bit.BIT (suc n) (a + b)
    if bit.BIT (suc n) (bit.BITS n 0 a + bit.BITS n 0 b) then
      bit.BIT (suc n) a bit.BIT (suc n) b
    else ¬(bit.BIT (suc n) a bit.BIT (suc n) b)

l h n i.
    ¬(l = 0)
    (bit.BIT i (bit.SIGN_EXTEND l h n)
     if l h i < l then bit.BIT i (n mod arithmetic.BIT2 0 l)
     else i < h bit.BIT (arithmetic.- l 1) n)

f.
    (x y z. f x (f y z) = f (f x y) z) (x y. f x y = f y x)
    x y z. f x (f y z) = f y (f x z)

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

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

(f l. list.GENLIST_AUX f 0 l = l)
  (f n l.
     list.GENLIST_AUX f (bit1 n) l =
     list.GENLIST_AUX f (arithmetic.- (bit1 n) 1)
       (f (arithmetic.- (bit1 n) 1) :: l))
  f n l.
    list.GENLIST_AUX f (arithmetic.BIT2 n) l =
    list.GENLIST_AUX f (bit1 n) (f (bit1 n) :: l)

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