Package hol-words: n-bit words
Information
| name | hol-words |
| version | 1.1 |
| description | n-bit words |
| author | HOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org> |
| license | MIT |
| checksum | 26e1c2e50ed5c51a8f0a48b6388536617bf36e97 |
| requires | base hol-base hol-string |
| show | Data.Bool Data.List Data.Option Data.Pair Function HOL4 Number.Natural Relation |
Files
- Package tarball hol-words-1.1.tgz
- Theory source file hol-words.thy (included in the package tarball)
Defined Type Operators
- HOL4
- fcp
- fcp.bit0
- fcp.bit1
- fcp.cart
- fcp.finite_image
- fcp
Defined Constants
- HOL4
- alignment
- alignment.align
- alignment.aligned
- alignment.byte_align
- alignment.byte_aligned
- bitstring
- bitstring.add
- bitstring.band
- bitstring.bitify
- bitstring.bitify_tupled
- bitstring.bitwise
- bitstring.bnand
- bitstring.bnor
- bitstring.bnot
- bitstring.boolify
- bitstring.bor
- bitstring.bxnor
- bitstring.bxor
- bitstring.extend
- bitstring.field
- bitstring.field_insert
- bitstring.fixwidth
- bitstring.modify
- bitstring.n2v
- bitstring.replicate
- bitstring.rev_count_list
- bitstring.rotate
- bitstring.s2v
- bitstring.shiftl
- bitstring.shiftr
- bitstring.sign_extend
- bitstring.testbit
- bitstring.v2n
- bitstring.v2s
- bitstring.v2w
- bitstring.w2v
- bitstring.zero_extend
- blast
- blast.bcarry
- blast.bsum
- blast.BCARRY
- blast.BSUM
- fcp
- fcp.:+
- fcp.bit0_CASE
- fcp.bit0_size
- fcp.bit1_CASE
- fcp.bit1_size
- fcp.dest_cart
- fcp.dest_finite_image
- fcp.dimindex
- fcp.fcp_CASE
- fcp.fcp_index
- fcp.finite_index
- fcp.mk_cart
- fcp.mk_finite_image
- fcp.BIT0A
- fcp.BIT0B
- fcp.BIT1A
- fcp.BIT1B
- fcp.BIT1C
- fcp.FCP
- fcp.FCP_CONCAT
- fcp.FCP_CONS
- fcp.FCP_EVERY
- fcp.FCP_EXISTS
- fcp.FCP_FOLD
- fcp.FCP_HD
- fcp.FCP_MAP
- fcp.FCP_TL
- fcp.FCP_ZIP
- fcp.HAS_SIZE
- fcp.IS_BIT0A
- fcp.IS_BIT0B
- fcp.IS_BIT1A
- fcp.IS_BIT1B
- fcp.IS_BIT1C
- fcp.L2V
- fcp.V2L
- sum_num
- sum_num.GSUM
- sum_num.GSUM_tupled
- sum_num.SUM
- words
- words.add_with_carry
- words.bit_count
- words.bit_count_upto
- words.bit_field_insert
- words.concat_word_list
- words.dimword
- words.l2w
- words.n2w
- words.n2w_itself
- words.nzcv
- words.reduce_and
- words.reduce_nand
- words.reduce_nor
- words.reduce_or
- words.reduce_xnor
- words.reduce_xor
- words.s2w
- words.saturate_add
- words.saturate_mul
- words.saturate_n2w
- words.saturate_sub
- words.saturate_w2w
- words.sw2sw
- words.w2l
- words.w2n
- words.w2s
- words.w2w
- words.word_1comp
- words.word_2comp
- words.word_H
- words.word_L
- words.word_L2
- words.word_T
- words.word_abs
- words.word_add
- words.word_and
- words.word_asr
- words.word_asr_bv
- words.word_bit
- words.word_bits
- words.word_compare
- words.word_concat
- words.word_div
- words.word_extract
- words.word_from_bin_list
- words.word_from_bin_string
- words.word_from_dec_list
- words.word_from_dec_string
- words.word_from_hex_list
- words.word_from_hex_string
- words.word_from_oct_list
- words.word_from_oct_string
- words.word_ge
- words.word_gt
- words.word_hi
- words.word_hs
- words.word_join
- words.word_le
- words.word_len
- words.word_lo
- words.word_log2
- words.word_ls
- words.word_lsb
- words.word_lsl
- words.word_lsl_bv
- words.word_lsr
- words.word_lsr_bv
- words.word_lt
- words.word_max
- words.word_min
- words.word_mod
- words.word_modify
- words.word_msb
- words.word_mul
- words.word_nand
- words.word_nor
- words.word_or
- words.word_reduce
- words.word_replicate
- words.word_reverse
- words.word_rol
- words.word_rol_bv
- words.word_ror
- words.word_ror_bv
- words.word_rrx
- words.word_sdiv
- words.word_sign_extend
- words.word_signed_bits
- words.word_slice
- words.word_smax
- words.word_smin
- words.word_smod
- words.word_srem
- words.word_sub
- words.word_to_bin_list
- words.word_to_bin_string
- words.word_to_dec_list
- words.word_to_dec_string
- words.word_to_hex_list
- words.word_to_hex_string
- words.word_to_oct_list
- words.word_to_oct_string
- words.word_xnor
- words.word_xor
- words.BIT_SET
- words.BIT_SET_tupled
- words.INT_MAX
- words.INT_MIN
- words.UINT_MAX
- alignment
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%%8627.
words.w2n (words.w2w %%genvar%%8627) < 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%%1387.
%%genvar%%1387 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%%8808.
bitstring.v2n %%genvar%%8808 <
arithmetic.BIT2 0 ↑ length %%genvar%%8808
⊦ ∀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%%50945 b.
words.word_abs (words.word_sub %%genvar%%50945 b) =
words.word_abs (words.word_sub b %%genvar%%50945)
⊦ ∀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%%1747 w.
%%genvar%%1747 = length w ⇒ bitstring.fixwidth %%genvar%%1747 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%%32398 b.
words.word_add %%genvar%%32398 b = words.n2w 0 ⇔
%%genvar%%32398 = 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%%6102 v.
suc %%genvar%%6102 = length v ⇒ bitstring.field %%genvar%%6102 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%%32366 w x.
%%genvar%%32366 = words.word_sub w x ⇔
words.word_add %%genvar%%32366 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%%3216 a b.
alignment.aligned %%genvar%%3216 a ∧
alignment.aligned %%genvar%%3216 b ⇒
alignment.aligned %%genvar%%3216 (words.word_add a b) ∧
alignment.aligned %%genvar%%3216 (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_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))
⊦ ∀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))
⊦ ∃rep.
bool.TYPE_DEFINITION
(λa0.
∀'bit0'.
(∀a0.
(∃a.
a0 =
let a ← a in ind_type.CONSTR 0 a (λn. ind_type.BOTTOM)) ∨
(∃a.
a0 =
let a ← a in
ind_type.CONSTR (suc 0) a (λn. ind_type.BOTTOM)) ⇒
'bit0' a0) ⇒ 'bit0' a0) rep
⊦ 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
⊦ ∃rep.
bool.TYPE_DEFINITION
(λa0.
∀'bit1'.
(∀a0.
(∃a.
a0 =
let a ← a in ind_type.CONSTR 0 a (λn. ind_type.BOTTOM)) ∨
(∃a.
a0 =
let a ← a in
ind_type.CONSTR (suc 0) a (λn. ind_type.BOTTOM)) ∨
a0 =
ind_type.CONSTR (suc (suc 0)) bool.ARB
(λn. ind_type.BOTTOM) ⇒ 'bit1' a0) ⇒ 'bit1' a0) rep
⊦ (∀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
- →
- bool
- Data
- List
- list
- Pair
- ×
- Sum
- Data.Sum.+
- Unit
- Data.Unit.unit
- List
- HOL4
- bool
- bool.itself
- ind_type
- ind_type.recspace
- string
- string.char
- bool
- Number
- Natural
- natural
- Natural
External Constants
- =
- select
- Data
- Bool
- ∀
- ∧
- ⇒
- ∃
- ∃!
- ∨
- ¬
- cond
- ⊥
- ⊤
- List
- ::
- @
- []
- all
- any
- concat
- head
- last
- length
- map
- null
- reverse
- tail
- Pair
- ,
- fst
- snd
- Sum
- Data.Sum.destLeft
- Data.Sum.destRight
- Data.Sum.isLeft
- Data.Sum.isRight
- Data.Sum.left
- Data.Sum.right
- Unit
- Data.Unit.()
- Bool
- Function
- const
- flip
- id
- ∘
- Combinator
- Combinator.s
- HOL4
- arithmetic
- arithmetic.-
- arithmetic.num_CASE
- arithmetic.BIT2
- arithmetic.DIV2
- basicSize
- basicSize.bool_size
- bit
- bit.BIT
- bit.BITS
- bit.BITWISE
- bit.BIT_MODIFY
- bit.BIT_REVERSE
- bit.DIV_2EXP
- bit.LOG2
- bit.MOD_2EXP
- bit.MOD_2EXP_EQ
- bit.MOD_2EXP_MAX
- bit.SBIT
- bit.SIGN_EXTEND
- bit.SLICE
- bool
- bool.the_value
- bool.ARB
- bool.IN
- bool.LET
- bool.TYPE_DEFINITION
- combin
- combin.FAIL
- ind_type
- ind_type.BOTTOM
- ind_type.CONSTR
- ind_type.FCONS
- list
- list.list_CASE
- list.list_size
- list.DROP
- list.EL
- list.FOLDL
- list.GENLIST
- list.GENLIST_AUX
- list.LIST_TO_SET
- list.PAD_LEFT
- list.PAD_RIGHT
- list.SNOC
- list.TAKE
- list.ZIP
- logroot
- logroot.LOG
- marker
- marker.Abbrev
- numeral
- numeral.exactlog
- numeral.iDUB
- numeral.iSUB
- numeral.iZ
- numeral.iiSUC
- numeral.internal_mult
- numeral.onecount
- numeral.texp_help
- numposrep
- numposrep.l2n
- numposrep.n2l
- numposrep.num_from_bin_list
- numposrep.num_to_bin_list
- numposrep.BOOLIFY
- pair
- pair.pair_CASE
- pair.UNCURRY
- pred_set
- pred_set.BIJ
- pred_set.CARD
- pred_set.DELETE
- pred_set.EMPTY
- pred_set.FINITE
- pred_set.GSPEC
- pred_set.IMAGE
- pred_set.INJ
- pred_set.INSERT
- pred_set.INTER
- pred_set.SING
- pred_set.SUBSET
- pred_set.SURJ
- pred_set.UNION
- pred_set.UNIV
- prim_rec
- prim_rec.PRE
- relation
- relation.inv_image
- relation.RESTRICT
- relation.WFREC
- rich_list
- rich_list.AND_EL
- rich_list.COUNT_LIST
- rich_list.LASTN
- rich_list.OR_EL
- string
- string.CHR
- while
- while.LEAST
- ASCIInumbers
- ASCIInumbers.n2s
- ASCIInumbers.s2n
- ASCIInumbers.HEX
- ASCIInumbers.UNHEX
- arithmetic
- Number
- Natural
- *
- +
- <
- ≤
- >
- ≥
- ↑
- bit1
- div
- even
- max
- min
- mod
- odd
- suc
- zero
- Natural
- Relation
- empty
- wellFounded
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%%3008. P %%genvar%%3008) ⇔ 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