Package hol-integer: HOL integer theories

Information

namehol-integer
version1.1
descriptionHOL integer theories
authorHOL OpenTheory Packager <opentheory-packager@hol-theorem-prover.org>
licenseMIT
checksumb6c353cab4f22b6b9c2c106742eae272cbf238d3
requiresbase
hol-base
hol-words
hol-string
hol-ring
hol-quotient
showData.Bool
Data.List
Data.Pair
Function
HOL4
Number.Natural
Relation

Files

Defined Type Operators

Defined Constants

Theorems

¬pred_set.FINITE pred_set.UNIV

¬(integer.int_1 = integer.int_0)

¬integer.tint_eq integer.tint_1 integer.tint_0

integer.int_0 = integer.int_ABS integer.tint_0

integer.int_0 = integer.int_of_num 0

integer.int_1 = integer.int_ABS integer.tint_1

int_bitwise.int_and = int_bitwise.int_bitwise ()

int_bitwise.int_or = int_bitwise.int_bitwise ()

quotient.QUOTIENT integer.tint_eq integer.int_ABS integer.int_REP

x. integer.int_divides x x

x. integer.int_le x x

x. integer.tint_eq x x

integer.int_1 = integer.int_of_num 1

integer_word.w2i words.word_H = integer_word.INT_MAX bool.the_value

integer_word.w2i words.word_L = integer_word.INT_MIN bool.the_value

integer.int_le (integer.int_of_num 0)
    (integer_word.INT_MAX bool.the_value)

integer.int_lt (integer.int_of_num 0)
    (integer_word.UINT_MAX bool.the_value)

integer.int_lt (integer_word.INT_MIN bool.the_value)
    (integer.int_of_num 0)

integer_word.i2w (integer_word.INT_MAX bool.the_value) = words.word_H

integer_word.i2w (integer_word.INT_MIN bool.the_value) = words.word_L

integer_word.i2w (integer_word.UINT_MAX bool.the_value) = words.word_T

b. int_arith.bmarker b b

x. ¬integer.int_lt x x

x. ¬integer.tint_lt x x

integer_word.INT_MAX bool.the_value =
  integer.int_of_num (words.INT_MAX bool.the_value)

integer_word.UINT_MAX bool.the_value =
  integer.int_of_num (words.UINT_MAX bool.the_value)

integer.int_le (integer.int_of_num 0) (integer.int_of_num 1)

integer.int_lt (integer.int_of_num 0) (integer.int_of_num 1)

integer.int_neg (integer.int_of_num 0) = integer.int_of_num 0

integer_word.w2i (words.n2w 0) = integer.int_of_num 0

integer_word.i2w (integer.int_of_num 0) = words.n2w 0

integer_word.saturate_i2sw (integer.int_of_num 0) = words.n2w 0

integer_word.saturate_i2w (integer.int_of_num 0) = words.n2w 0

integer_word.i2w (integer.int_of_num (words.w2n w)) = w

p. integer.int_le (integer.int_of_num 0) (integer.ABS p)

i. int_bitwise.int_not (int_bitwise.int_not i) = i

i. int_bitwise.int_of_bits (int_bitwise.bits_of_int i) = i

x. integer.int_neg (integer.int_neg x) = x

n. integer.int_le (integer.int_of_num 0) (integer.int_of_num n)

n. integer.Num (integer.int_of_num n) = n

x. integer.tint_eq (integer.tint_add integer.tint_0 x) x

x. integer.tint_eq (integer.tint_mul integer.tint_1 x) x

w.
    integer.int_le (integer_word.w2i w)
      (integer_word.INT_MAX bool.the_value)

w.
    integer.int_le (integer_word.INT_MIN bool.the_value)
      (integer_word.w2i w)

w. integer_word.i2w (integer_word.w2i w) = w

w. i. w = integer_word.i2w i

ring.is_ring
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integer.tint_0 = (1, 1)

integer_word.w2i words.word_T = integer.int_neg (integer.int_of_num 1)

integer_word.INT_MIN bool.the_value =
  integer.int_neg (integer.int_of_num (words.INT_MIN bool.the_value))

p. ¬integer.int_lt (integer.ABS p) (integer.int_of_num 0)

a. integer.int_REP a = (select) (integer.int_REP_CLASS a)

x. integer.int_le (integer.int_of_num 0) (integer.int_mul x x)

p. integer.ABS (integer.int_neg p) = integer.ABS p

p. integer.ABS (integer.ABS p) = integer.ABS p

x. integer.int_sub x x = integer.int_of_num 0

x. integer.int_add x (integer.int_of_num 0) = x

x. integer.int_sub x (integer.int_of_num 0) = x

x. integer.int_add (integer.int_of_num 0) x = x

n. integer.ABS (integer.int_of_num n) = integer.int_of_num n

r. integer.int_ABS r = integer.int_ABS_CLASS (integer.tint_eq r)

x.
    integer.tint_eq (integer.tint_add (integer.tint_neg x) x)
      integer.tint_0

w.
    integer_word.saturate_sw2sw w =
    integer_word.saturate_i2sw (integer_word.w2i w)

w.
    integer_word.saturate_sw2w w =
    integer_word.saturate_i2w (integer_word.w2i w)

int_bitwise.int_not =
  int_bitwise.int_bitwise (λx y. ¬y) (integer.int_of_num 0)

int_bitwise.int_xor = int_bitwise.int_bitwise (λx y. ¬(x y))

T1.
    integer.int_neg T1 =
    integer.int_ABS (integer.tint_neg (integer.int_REP T1))

x. integer.int_add x (integer.int_neg x) = integer.int_of_num 0

x. integer.int_mul x (integer.int_of_num 0) = integer.int_of_num 0

x. integer.int_add (integer.int_neg x) x = integer.int_of_num 0

x. integer.int_mul (integer.int_of_num 0) x = integer.int_of_num 0

x. integer.int_sub (integer.int_of_num 0) x = integer.int_neg x

p. integer.int_div p (integer.int_of_num 1) = p

x. integer.int_mul x (integer.int_of_num 1) = x

p. integer.int_quot p (integer.int_of_num 1) = p

x. integer.int_mul (integer.int_of_num 1) x = x

n. 1 arithmetic.BIT2 0 n

x. Omega.fst_nzero x 0 < fst x

w.
    integer_word.saturate_w2sw w =
    integer_word.saturate_i2sw (integer.int_of_num (words.w2n w))

x y. ¬(x + y < x)

integerRing.int_r_canonical_sum_simplify =
  ringNorm.r_canonical_sum_simplify
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_r_spolynom_normalize =
  ringNorm.r_spolynom_normalize
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_r_spolynom_simplify =
  ringNorm.r_spolynom_simplify
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_polynom_normalize =
  ringNorm.polynom_normalize
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_polynom_simplify =
  ringNorm.polynom_simplify
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_r_canonical_sum_scalar =
  ringNorm.r_canonical_sum_scalar
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_r_interp_vl =
  ringNorm.r_interp_vl
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_r_interp_cs =
  ringNorm.r_interp_cs
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_r_interp_sp =
  ringNorm.r_interp_sp
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_interp_p =
  ringNorm.interp_p
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_r_canonical_sum_scalar2 =
  ringNorm.r_canonical_sum_scalar2
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_r_varlist_insert =
  ringNorm.r_varlist_insert
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_r_canonical_sum_merge =
  ringNorm.r_canonical_sum_merge
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_r_canonical_sum_prod =
  ringNorm.r_canonical_sum_prod
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_r_interp_m =
  ringNorm.r_interp_m
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_r_ics_aux =
  ringNorm.r_ics_aux
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_r_ivl_aux =
  ringNorm.r_ivl_aux
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_r_canonical_sum_scalar3 =
  ringNorm.r_canonical_sum_scalar3
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

integerRing.int_r_monom_insert =
  ringNorm.r_monom_insert
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)

i. integer.int_mod i (integer.int_of_num 1) = integer.int_of_num 0

x. Omega.fst1 x fst x = 1

w.
    words.word_abs w =
    words.n2w (integer.Num (integer.ABS (integer_word.w2i w)))

x y. integer.int_ge x y integer.int_le y x

x y. integer.int_gt x y integer.int_lt y x

y x. integer.int_add x y = integer.int_add y x

y x. integer.int_mul x y = integer.int_mul y x

x y. x = y integer.int_le x y

x y. integer.int_lt x y integer.int_le x y

x y. integer.int_le x y integer.int_le y x

x y. integer.int_le x y integer.int_lt y x

x y. integer.int_lt x y integer.int_le y x

x y. integer.int_add y (integer.int_sub x y) = x

x y. integer.int_sub x (integer.int_sub x y) = y

x y. integer.int_add (integer.int_sub x y) y = x

x y. integer.int_sub (integer.int_add x y) x = y

i. integer.Num i = select n. i = integer.int_of_num n

x y. integer.tint_eq x y integer.tint_eq y x

x y. integer.tint_add x y = integer.tint_add y x

x y. integer.tint_mul x y = integer.tint_mul y x

p q. p = q integer.tint_eq p q

lowers. all Omega.fst_nzero lowers x. Omega.evallower x lowers

uppers. all Omega.fst_nzero uppers x. Omega.evalupper x uppers

integer.tint_1 = (1 + 1, 1)

integer_word.INT_MAX bool.the_value =
  integer.int_sub (integer.int_of_num (words.INT_MIN bool.the_value))
    (integer.int_of_num 1)

integer_word.INT_MIN bool.the_value =
  integer.int_sub (integer.int_neg (integer_word.INT_MAX bool.the_value))
    (integer.int_of_num 1)

integer_word.UINT_MAX bool.the_value =
  integer.int_sub (integer.int_of_num (words.dimword bool.the_value))
    (integer.int_of_num 1)

integer.int_of_num (words.w2n (integer_word.i2w n)) =
  integer.int_mod n (integer.int_of_num (words.dimword bool.the_value))

integer_word.w2i (words.word_2comp (words.n2w 1)) =
  integer.int_neg (integer.int_of_num 1)

integer_word.i2w (integer.int_neg (integer.int_of_num 1)) =
  words.word_2comp (words.n2w 1)

x.
    integer.int_neg x =
    integer.int_mul (integer.int_neg (integer.int_of_num 1)) x

x.
    integer.int_add x x =
    integer.int_mul (integer.int_of_num (arithmetic.BIT2 0)) x

p. p = integer.int_neg p p = integer.int_of_num 0

x.
    integer.int_le x (integer.int_neg x)
    integer.int_le x (integer.int_of_num 0)

p. integer.ABS p = p integer.int_le (integer.int_of_num 0) p

x.
    integer.int_le (integer.int_neg x) x
    integer.int_le (integer.int_of_num 0) x

n.
    even n
    integer.int_divides (integer.int_of_num (arithmetic.BIT2 0))
      (integer.int_of_num n)

n. fst (integer.tint_of_num n) = snd (integer.tint_of_num n) + n

x y. ¬(integer.int_le x y integer.int_lt y x)

x y. ¬(integer.int_lt x y integer.int_le y x)

x y. ¬(integer.int_lt x y integer.int_lt y x)

x y. integer.int_le x y ¬integer.int_lt y x

x y. integer.int_sub x y = integer.int_add x (integer.int_neg y)

x y. integer.int_lt x y ¬(x = y)

x y. integer.int_lt x y ¬integer.int_lt y x

x y. ¬integer.int_le x y integer.int_lt y x

x y. ¬integer.int_lt x y integer.int_le y x

x y. integer.int_neg (integer.int_sub x y) = integer.int_sub y x

x y. integer.int_sub x (integer.int_neg y) = integer.int_add x y

x y. integer.int_sub x (integer.int_add x y) = integer.int_neg y

x y. integer.int_sub (integer.int_sub x y) x = integer.int_neg y

x x1. Omega.evallower x x1 Omega.evallower_tupled (x, x1)

x x1. Omega.evalupper x x1 Omega.evalupper_tupled (x, x1)

x y. integer.tint_neg (x, y) = (y, x)

x x1. Omega.sumc x x1 = Omega.sumc_tupled (x, x1)

x x1.
    Omega.dark_shadow_cond_row x x1
    Omega.dark_shadow_cond_row_tupled (x, x1)

x x1. Omega.rshadow_row x x1 Omega.rshadow_row_tupled (x, x1)

x x1. Omega.dark_shadow x x1 Omega.dark_shadow_tupled (x, x1)

x x1.
    Omega.dark_shadow_condition x x1
    Omega.dark_shadow_condition_tupled (x, x1)

integer.int_le x y
  integer.int_lt x (integer.int_add y (integer.int_of_num 1))

integer.int_lt x y
  integer.int_le (integer.int_add x (integer.int_of_num 1)) y

1 < fcp.dimindex bool.the_value
  integer.int_lt (integer.int_of_num 0)
    (integer_word.INT_MAX bool.the_value)

fcp.dimindex bool.the_value fcp.dimindex bool.the_value
  integer.int_le (integer_word.INT_MAX bool.the_value)
    (integer_word.INT_MAX bool.the_value)

fcp.dimindex bool.the_value fcp.dimindex bool.the_value
  integer.int_le (integer_word.INT_MIN bool.the_value)
    (integer_word.INT_MIN bool.the_value)

x. integer.int_lt (integer.int_of_num 0) x ¬(x = integer.int_of_num 0)

x.
    integer.int_le (integer.int_of_num 0) x
    integer.int_le (integer.int_of_num 0) (integer.int_neg x)

x. integer.int_neg x = integer.int_of_num 0 x = integer.int_of_num 0

p. integer.ABS p = integer.int_of_num 0 p = integer.int_of_num 0

x.
    integer.int_le (integer.int_neg x) (integer.int_of_num 0)
    integer.int_le (integer.int_of_num 0) x

x.
    integer.int_le (integer.int_of_num 0) (integer.int_neg x)
    integer.int_le x (integer.int_of_num 0)

p.
    integer.int_le (integer.ABS p) (integer.int_of_num 0)
    p = integer.int_of_num 0

x.
    integer.int_lt (integer.int_neg x) (integer.int_of_num 0)
    integer.int_lt (integer.int_of_num 0) x

x.
    integer.int_lt (integer.int_of_num 0) (integer.int_neg x)
    integer.int_lt x (integer.int_of_num 0)

i.
    integer.int_of_num (integer.Num i) = i
    integer.int_le (integer.int_of_num 0) i

n.
    odd n
    ¬integer.int_divides (integer.int_of_num (arithmetic.BIT2 0))
        (integer.int_of_num n)

n.
    integer.int_of_num (suc n) =
    integer.int_add (integer.int_of_num n) (integer.int_of_num 1)

n.
    ¬(n = 0) integer.int_lt (integer.int_of_num 0) (integer.int_of_num n)

w.
    integer.int_lt (integer_word.w2i w) (integer.int_of_num 0)
    words.word_lt w (words.n2w 0)

T1 T2.
    integer.int_lt T1 T2
    integer.tint_lt (integer.int_REP T1) (integer.int_REP T2)

x y. integer.int_neg x = y x = integer.int_neg y

x y.
    integer.int_neg (integer.int_mul x y) =
    integer.int_mul x (integer.int_neg y)

x y.
    integer.int_neg (integer.int_mul x y) =
    integer.int_mul (integer.int_neg x) y

x y.
    integer.int_sub (integer.int_neg x) y =
    integer.int_neg (integer.int_add x y)

x y. integer.int_neg x = integer.int_neg y x = y

x y.
    integer.int_le (integer.int_neg x) (integer.int_neg y)
    integer.int_le y x

x y.
    integer.int_lt (integer.int_neg x) (integer.int_neg y)
    integer.int_lt y x

x y.
    integer.int_mul (integer.int_neg x) (integer.int_neg y) =
    integer.int_mul x y

x y.
    integer.int_sub (integer.int_neg x) (integer.int_neg y) =
    integer.int_sub y x

t. ¬integer.int_lt t integer.int_0 n. t = integer.int_of_num n

i.
    integer.int_le (integer.int_of_num 0) i n. i = integer.int_of_num n

i.
    integer.int_le (integer.int_of_num 0) i ∃!n. i = integer.int_of_num n

b i.
    int_bitwise.int_bit b (int_bitwise.int_not i)
    ¬int_bitwise.int_bit b i

%%genvar%%1573 i.
    integer.int_le (integer.int_of_num %%genvar%%1573) i
    %%genvar%%1573 integer.Num i

n m.
    integer.int_exp (integer.int_of_num n) m = integer.int_of_num (n m)

x y. x = x + y y = 0

%%genvar%%417 %%genvar%%418.
    %%genvar%%417 < %%genvar%%417 + %%genvar%%418 0 < %%genvar%%418

m n. integer.int_of_num m = integer.int_of_num n m = n

n m.
    integer.int_divides (integer.int_of_num n) (integer.int_of_num m)
    divides.divides n m

m n.
    integer.int_le (integer.int_of_num m) (integer.int_of_num n) m n

m n.
    integer.int_lt (integer.int_of_num m) (integer.int_of_num n) m < n

m n.
    integer.tint_eq (integer.tint_of_num m) (integer.tint_of_num n) m = n

p q. integer.tint_eq p q integer.tint_eq p = integer.tint_eq q

x1 x2.
    integer.tint_eq x1 x2
    integer.tint_eq (integer.tint_neg x1) (integer.tint_neg x2)

t.
    ¬integer.tint_lt t integer.tint_0
    n. integer.tint_eq t (integer.tint_of_num n)

a b.
    words.word_ge a b
    integer.int_ge (integer_word.w2i a) (integer_word.w2i b)

a b.
    words.word_gt a b
    integer.int_gt (integer_word.w2i a) (integer_word.w2i b)

a b.
    words.word_le a b
    integer.int_le (integer_word.w2i a) (integer_word.w2i b)

a b.
    words.word_lt a b
    integer.int_lt (integer_word.w2i a) (integer_word.w2i b)

v w. integer_word.w2i v = integer_word.w2i w v = w

¬integer.int_lt x y
  integer.int_lt y (integer.int_add x (integer.int_of_num 1))

i.
    int_bitwise.int_not i =
    integer.int_sub (integer.int_sub (integer.int_of_num 0) i)
      (integer.int_of_num 1)

n.
    integer.ABS n =
    if integer.int_lt n (integer.int_of_num 0) then integer.int_neg n
    else n

x.
    integer.int_le (integer.int_of_num 0) (integer.int_add x x)
    integer.int_le (integer.int_of_num 0) x

i.
    words.word_mul (words.word_2comp (words.n2w 1)) (integer_word.i2w i) =
    integer_word.i2w (integer.int_neg i)

x.
    integer.int_sub (integer.int_add x (integer.int_of_num 1))
      (integer.int_of_num 1) = x

n.
    n < words.INT_MIN bool.the_value
    integer_word.w2i (words.n2w n) = integer.int_of_num n

T1 T2.
    integer.int_add T1 T2 =
    integer.int_ABS
      (integer.tint_add (integer.int_REP T1) (integer.int_REP T2))

x y. integer.int_max x y = if integer.int_lt x y then y else x

x y. integer.int_min x y = if integer.int_lt x y then x else y

T1 T2.
    integer.int_mul T1 T2 =
    integer.int_ABS
      (integer.tint_mul (integer.int_REP T1) (integer.int_REP T2))

x y.
    integer.int_neg (integer.int_add x y) =
    integer.int_add (integer.int_neg x) (integer.int_neg y)

x y.
    integer.int_le x (integer.int_add x y)
    integer.int_le (integer.int_of_num 0) y

x y.
    integer.int_le y (integer.int_add x y)
    integer.int_le (integer.int_of_num 0) x

x y.
    integer.int_lt x (integer.int_add x y)
    integer.int_lt (integer.int_of_num 0) y

x y.
    integer.int_lt y (integer.int_add x y)
    integer.int_lt (integer.int_of_num 0) x

x y. integer.int_add x y = x y = integer.int_of_num 0

x y. integer.int_add x y = y x = integer.int_of_num 0

p q.
    integer.int_mul (integer.ABS p) (integer.ABS q) =
    integer.ABS (integer.int_mul p q)

a b.
    words.word_add (integer_word.i2w a) (integer_word.i2w b) =
    integer_word.i2w (integer.int_add a b)

a b.
    words.word_mul (integer_word.i2w a) (integer_word.i2w b) =
    integer_word.i2w (integer.int_mul a b)

x y.
    integer.int_le (integer.int_of_num 0) (integer.int_sub x y)
    integer.int_le y x

x y.
    integer.int_lt (integer.int_of_num 0) (integer.int_sub x y)
    integer.int_lt y x

x y. integer.int_sub x y = integer.int_of_num 0 x = y

i.
    integer.int_le i (integer.int_of_num 0)
    n. i = integer.int_neg (integer.int_of_num n)

m n.
    integer.int_add (integer.int_of_num m) (integer.int_of_num n) =
    integer.int_of_num (m + n)

m n.
    integer.int_max (integer.int_of_num m) (integer.int_of_num n) =
    integer.int_of_num (max m n)

m n.
    integer.int_min (integer.int_of_num m) (integer.int_of_num n) =
    integer.int_of_num (min m n)

m n.
    integer.int_mul (integer.int_of_num m) (integer.int_of_num n) =
    integer.int_of_num (m * n)

a b.
    integer_word.signed_saturate_add a b =
    integer_word.saturate_i2sw
      (integer.int_add (integer_word.w2i a) (integer_word.w2i b))

a b.
    integer_word.signed_saturate_sub a b =
    integer_word.saturate_i2sw
      (integer.int_sub (integer_word.w2i a) (integer_word.w2i b))

a b.
    integer_word.i2w
      (integer.int_add (integer_word.w2i a) (integer_word.w2i b)) =
    words.word_add a b

a b.
    integer_word.i2w
      (integer.int_mul (integer_word.w2i a) (integer_word.w2i b)) =
    words.word_mul a b

a b.
    integer_word.i2w
      (integer.int_sub (integer_word.w2i a) (integer_word.w2i b)) =
    words.word_sub a b

p ((Omega.evalupper x [] Omega.evallower x []) ) p

p q r.
    integer.int_divides p q integer.int_divides p (integer.int_mul q r)

p q r.
    integer.int_divides p q integer.int_divides p (integer.int_mul r q)

p q. integer.int_divides p q m. integer.int_mul m p = q

i.
    ¬(i = integer.int_of_num 0)
    integer.int_mod i i = integer.int_of_num 0

p.
    ¬(p = integer.int_of_num 0)
    integer.int_rem p p = integer.int_of_num 0

i.
    fcp.dimindex bool.the_value fcp.dimindex bool.the_value
    words.w2w (integer_word.i2w i) = integer_word.i2w i

x.
    integer.int_lt (integer.int_of_num 0) (integer.int_mul x x)
    ¬(x = integer.int_of_num 0)

x.
    integer.int_add
      (integer.int_add x (integer.int_neg (integer.int_of_num 1)))
      (integer.int_of_num 1) = x

n.
    n words.INT_MAX bool.the_value
    integer_word.w2i (integer_word.i2w (integer.int_of_num n)) =
    integer.int_of_num n

n.
    ¬(integer.int_of_num n = integer.int_of_num 0)
    integer.int_lt (integer.int_of_num 0) (integer.int_of_num n)

w.
    integer_word.saturate_sw2w w =
    if words.word_lt w (words.n2w 0) then words.n2w 0
    else words.saturate_w2w w

rep.
    bool.TYPE_DEFINITION
      (λc. r. integer.tint_eq r r c = integer.tint_eq r) rep

x y.
    x = y integer.int_of_num 0 = integer.int_add y (integer.int_neg x)

x y.
    x = y integer.int_add x (integer.int_neg y) = integer.int_of_num 0

x y.
    integer.int_le x y
    integer.int_le (integer.int_of_num 0)
      (integer.int_add y (integer.int_neg x))

x y. integer.int_le x y integer.int_lt x y x = y

x y.
    integer.int_lt x y
    integer.int_lt (integer.int_of_num 0)
      (integer.int_add y (integer.int_neg x))

x y.
    integer.int_lt x y
    integer.int_lt (integer.int_add x (integer.int_neg y))
      (integer.int_of_num 0)

x y.
    integer.int_lt x y
    integer.int_le (integer.int_add x (integer.int_of_num 1)) y

x y.
    integer.int_le x y
    integer.int_lt x (integer.int_add y (integer.int_of_num 1))

x y. x = y integer.int_lt x y integer.int_lt y x

p q.
    integer.int_divides p (integer.int_mul p q)
    integer.int_divides p (integer.int_mul q p)

x y. integer.int_add x y = integer.int_of_num 0 x = integer.int_neg y

x y. integer.int_add x y = integer.int_of_num 0 y = integer.int_neg x

x y. integer.int_le x y integer.int_le y x x = y

x y. integer.tint_eq x y integer.tint_lt x y integer.tint_lt y x

(n. P (integer.int_of_num n))
  x. integer.int_le (integer.int_of_num 0) x P x

(n. P (integer.int_of_num n))
  x. integer.int_le (integer.int_of_num 0) x P x

(∃!n. P (integer.int_of_num n))
  ∃!x. integer.int_le (integer.int_of_num 0) x P x

i.
    integer_word.saturate_i2w i =
    if integer.int_lt i (integer.int_of_num 0) then words.n2w 0
    else words.saturate_n2w (integer.Num i)

i.
    words.word_msb (integer_word.i2w i)
    integer.int_le (integer.int_of_num (words.INT_MIN bool.the_value))
      (integer.int_mod i
         (integer.int_of_num (words.dimword bool.the_value)))

p.
    ¬(p = integer.int_of_num 0)
    integer.int_div p p = integer.int_of_num 1

p.
    ¬(p = integer.int_of_num 0)
    integer.int_quot p p = integer.int_of_num 1

q.
    ¬(q = integer.int_of_num 0)
    integer.int_div (integer.int_of_num 0) q = integer.int_of_num 0

p.
    ¬(p = integer.int_of_num 0)
    integer.int_mod (integer.int_of_num 0) p = integer.int_of_num 0

q.
    ¬(q = integer.int_of_num 0)
    integer.int_quot (integer.int_of_num 0) q = integer.int_of_num 0

q.
    ¬(q = integer.int_of_num 0)
    integer.int_rem (integer.int_of_num 0) q = integer.int_of_num 0

w.
    integer.int_le (integer_word.INT_MIN bool.the_value)
      (integer_word.w2i (words.sw2sw w))
    integer.int_le (integer_word.w2i (words.sw2sw w))
      (integer_word.INT_MAX bool.the_value)

integer.int_of_num 0 = integer.int_0
  n.
    integer.int_of_num (suc n) =
    integer.int_add (integer.int_of_num n) integer.int_1

integer.tint_of_num 0 = integer.tint_0
  n.
    integer.tint_of_num (suc n) =
    integer.tint_add (integer.tint_of_num n) integer.tint_1

x y.
    ¬(integer.int_lt x y
       integer.int_lt y (integer.int_add x (integer.int_of_num 1)))

x y.
    integer.int_lt x y
    integer.int_le x
      (integer.int_add y (integer.int_neg (integer.int_of_num 1)))

x y. integer.int_lt x y integer.int_le x y ¬(x = y)

a b.
    integer_word.i2w
      (integer.int_add (integer.int_of_num (words.w2n a))
         (integer.int_of_num (words.w2n b))) = words.word_add a b

a b.
    integer_word.i2w
      (integer.int_mul (integer.int_of_num (words.w2n a))
         (integer.int_of_num (words.w2n b))) = words.word_mul a b

a b.
    integer_word.i2w
      (integer.int_sub (integer.int_of_num (words.w2n a))
         (integer.int_of_num (words.w2n b))) = words.word_sub a b

¬(k = integer.int_of_num 0)
  integer.int_mod (integer.int_mod j k) k = integer.int_mod j k

x y z.
    integer.int_lt y z
    integer.int_lt (integer.int_add x y) (integer.int_add x z)

x y z. x = integer.int_sub y z integer.int_add x z = y

x y z.
    integer.int_le x (integer.int_sub y z)
    integer.int_le (integer.int_add x z) y

x y z.
    integer.int_lt x (integer.int_sub y z)
    integer.int_lt (integer.int_add x z) y

x y z. integer.int_sub x y = z x = integer.int_add z y

x y z.
    integer.int_le (integer.int_sub x y) z
    integer.int_le x (integer.int_add z y)

x y z.
    integer.int_lt (integer.int_add x y) z
    integer.int_lt x (integer.int_sub z y)

x y z.
    integer.int_lt (integer.int_sub x y) z
    integer.int_lt x (integer.int_add z y)

z y x.
    integer.int_add x (integer.int_add y z) =
    integer.int_add (integer.int_add x y) z

z y x.
    integer.int_mul x (integer.int_mul y z) =
    integer.int_mul (integer.int_mul x y) z

x y z.
    integer.int_sub x (integer.int_sub y z) =
    integer.int_sub (integer.int_add x z) y

c b a.
    integer.int_add (integer.int_sub a c) b =
    integer.int_sub (integer.int_add a b) c

n x c.
    integer.int_divides n (integer.int_add (integer.int_mul n x) c)
    integer.int_divides n c

x y z. integer.int_add x y = integer.int_add x z y = z

x y z. integer.int_add x z = integer.int_add y z x = y

x y z.
    integer.int_le (integer.int_add x y) (integer.int_add x z)
    integer.int_le y z

x y z.
    integer.int_le (integer.int_add x z) (integer.int_add y z)
    integer.int_le x y

x y z.
    integer.int_lt (integer.int_add x y) (integer.int_add x z)
    integer.int_lt y z

x y z.
    integer.int_lt (integer.int_add x z) (integer.int_add y z)
    integer.int_lt x y

a b c.
    integer.int_add (integer.int_sub a b) (integer.int_sub b c) =
    integer.int_sub a c

x y z.
    integer.int_divides x y integer.int_divides y z
    integer.int_divides x z

x y z. integer.int_le x y integer.int_le y z integer.int_le x z

x y z. integer.int_le x y integer.int_lt y z integer.int_lt x z

x y z. integer.int_lt x y integer.int_le y z integer.int_lt x z

x y z. integer.int_lt x y integer.int_lt y z integer.int_lt x z

i j. i = j n. int_bitwise.int_bit n i int_bitwise.int_bit n j

x x1 x2.
    Omega.calc_nightmare x x1 x2 Omega.calc_nightmare_tupled (x, x1, x2)

x x1 x2.
    Omega.dark_shadow_row x x1 x2
    Omega.dark_shadow_row_tupled (x, x1, x2)

b n i.
    int_bitwise.int_bit b (int_bitwise.int_shift_right n i)
    int_bitwise.int_bit (b + n) i

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

x y z. x + y = x + z y = z

x y z. x + y < x + z y < z

n.
    n words.INT_MIN bool.the_value
    integer_word.w2i
      (integer_word.i2w (integer.int_neg (integer.int_of_num n))) =
    integer.int_neg (integer.int_of_num n)

x1 x2 y.
    integer.tint_eq x1 x2 (integer.tint_lt x1 y integer.tint_lt x2 y)

x1 x2 y.
    integer.tint_eq x1 x2
    integer.tint_eq (integer.tint_add x1 y) (integer.tint_add x2 y)

x1 x2 y.
    integer.tint_eq x1 x2
    integer.tint_eq (integer.tint_mul x1 y) (integer.tint_mul x2 y)

x y1 y2.
    integer.tint_eq y1 y2 (integer.tint_lt x y1 integer.tint_lt x y2)

x y z.
    integer.tint_lt y z
    integer.tint_lt (integer.tint_add x y) (integer.tint_add x z)

x y z.
    integer.tint_add x (integer.tint_add y z) =
    integer.tint_add (integer.tint_add x y) z

x y z.
    integer.tint_mul x (integer.tint_mul y z) =
    integer.tint_mul (integer.tint_mul x y) z

x y z. integer.tint_eq x y integer.tint_eq y z integer.tint_eq x z

x y z. integer.tint_lt x y integer.tint_lt y z integer.tint_lt x z

w.
    integer_word.w2i w =
    if words.word_msb w then
      integer.int_neg (integer.int_of_num (words.w2n (words.word_2comp w)))
    else integer.int_of_num (words.w2n w)

lowers x y.
    Omega.evallower x lowers integer.int_lt x y
    Omega.evallower y lowers

uppers x y.
    Omega.evalupper x uppers integer.int_lt y x
    Omega.evalupper y uppers

x x1 x2.
    int_bitwise.bits_bitwise x x1 x2 =
    int_bitwise.bits_bitwise_tupled (x, x1, x2)

i j.
    ¬(i = integer.int_of_num 0)
    integer.int_div (integer.int_mul i j) i = j

i j.
    ¬(i = integer.int_of_num 0)
    integer.int_div (integer.int_mul j i) i = j

x y.
    integer.int_lt integer.int_0 x integer.int_lt integer.int_0 y
    integer.int_lt integer.int_0 (integer.int_mul x y)

x y.
    integer.tint_lt integer.tint_0 x integer.tint_lt integer.tint_0 y
    integer.tint_lt integer.tint_0 (integer.tint_mul x y)

¬(k = integer.int_of_num 0)
  integer.int_mod (integer.int_neg x) k =
  integer.int_mod (integer.int_sub k x) k

b n m.
    integer.int_of_num (if b then n else m) =
    if b then integer.int_of_num n else integer.int_of_num m

x y z.
    x = integer.int_add y z integer.int_add x (integer.int_neg y) = z

x y z.
    x = integer.int_add y z integer.int_add x (integer.int_neg z) = y

x y z.
    integer.int_le x (integer.int_add y z)
    integer.int_le (integer.int_add x (integer.int_neg z)) y

x y z.
    integer.int_lt x (integer.int_add y z)
    integer.int_lt (integer.int_add x (integer.int_neg y)) z

x y z.
    integer.int_add x y = z y = integer.int_add z (integer.int_neg x)

x y z.
    integer.int_lt (integer.int_add x y) z
    integer.int_lt y (integer.int_add z (integer.int_neg x))

x y z.
    integer.int_lt y (integer.int_add x (integer.int_neg z))
    integer.int_lt (integer.int_add y z) x

x y z.
    integer.int_lt (integer.int_add x (integer.int_neg y)) z
    integer.int_lt x (integer.int_add z y)

x.
    x = integer.int_of_num 0 integer.int_lt (integer.int_of_num 0) x
    integer.int_lt (integer.int_of_num 0) (integer.int_neg x)

i.
    integer.int_le (integer_word.INT_MIN bool.the_value) i
    integer.int_le i (integer_word.INT_MAX bool.the_value)
    integer_word.w2i (integer_word.i2w i) = i

f.
    y.
      x.
        integer.int_lt y x
        (DeepSyntax.eval_form f x
         DeepSyntax.eval_form (DeepSyntax.posinf f) x)

f.
    y.
      x.
        integer.int_lt x y
        (DeepSyntax.eval_form f x
         DeepSyntax.eval_form (DeepSyntax.neginf f) x)

f i j.
    int_bitwise.int_bitwise f i j =
    int_bitwise.int_of_bits
      (int_bitwise.bits_bitwise f (int_bitwise.bits_of_int i)
         (int_bitwise.bits_of_int j))

i j.
    integer.int_le (integer.int_of_num 0) i integer.int_lt i j
    integer.int_mod i j = i

p.
    ¬(p = integer.int_of_num 0)
    q. integer.int_mod (integer.int_mul q p) p = integer.int_of_num 0

p.
    ¬(p = integer.int_of_num 0)
    q. integer.int_rem (integer.int_mul q p) p = integer.int_of_num 0

n m.
    m n
    integer.int_sub (integer.int_of_num n) (integer.int_of_num m) =
    integer.int_of_num (arithmetic.- n m)

P c. (x. P (integer.int_mul c x)) x. P x integer.int_divides c x

f c. Omega.sumc (map f (c :: [])) (integer.int_of_num 1 :: []) = f c

w n.
    ¬words.word_msb w
    integer.int_lt (integer_word.w2i w) (integer.int_of_num n)
    words.w2n w < n

w.
    i.
      w = integer_word.i2w i
      integer.int_le (integer_word.INT_MIN bool.the_value) i
      integer.int_le i (integer_word.INT_MAX bool.the_value)

int_bitwise.int_bit n (int_bitwise.int_of_bits b)
  if n < length (fst b) then list.EL n (fst b) else snd b

¬(k = integer.int_of_num 0)
  integer.int_mod (integer.int_add (integer.int_mul q k) r) k =
  integer.int_mod r k

(x. integer.int_divides x (integer.int_of_num 0))
  x.
    integer.int_divides (integer.int_of_num 0) x x = integer.int_of_num 0

integer.int_of_num 0 = integer.int_add c x
  (integer.int_le (integer.int_of_num 0) (integer.int_add c y)
   integer.int_le x y)

p q r.
    integer.int_divides p q
    (integer.int_divides p (integer.int_add q r) integer.int_divides p r)

p q r.
    integer.int_divides p q
    (integer.int_divides p (integer.int_add r q) integer.int_divides p r)

p q r.
    integer.int_divides p q
    (integer.int_divides p (integer.int_sub q r) integer.int_divides p r)

p q r.
    integer.int_divides p q
    (integer.int_divides p (integer.int_sub r q) integer.int_divides p r)

x y z.
    integer.int_mul x (integer.int_sub y z) =
    integer.int_sub (integer.int_mul x y) (integer.int_mul x z)

z y x.
    integer.int_mul x (integer.int_add y z) =
    integer.int_add (integer.int_mul x y) (integer.int_mul x z)

x y z.
    integer.int_mul (integer.int_add x y) z =
    integer.int_add (integer.int_mul x z) (integer.int_mul y z)

x y z.
    integer.int_mul (integer.int_sub x y) z =
    integer.int_sub (integer.int_mul x z) (integer.int_mul y z)

x y z.
    integer.int_lt x (integer.int_min y z)
    integer.int_lt x y integer.int_lt x z

x y z.
    integer.int_lt (integer.int_max x y) z
    integer.int_lt x z integer.int_lt y z

i.
    integer_word.i2w i =
    if integer.int_lt i (integer.int_of_num 0) then
      words.word_2comp (words.n2w (integer.Num (integer.int_neg i)))
    else words.n2w (integer.Num i)

n i j.
    int_bitwise.int_bit n (int_bitwise.int_and i j)
    int_bitwise.int_bit n i int_bitwise.int_bit n j

n i j.
    int_bitwise.int_bit n (int_bitwise.int_or i j)
    int_bitwise.int_bit n i int_bitwise.int_bit n j

n m p.
    integer.int_mul (integer.int_exp p n) (integer.int_exp p m) =
    integer.int_exp p (n + m)

n.
    int_bitwise.bits_of_num n =
    if n = 0 then []
    else odd n :: int_bitwise.bits_of_num (n div arithmetic.BIT2 0)

P v e. v = e P v v = e P e

P. integer.LEAST_INT P = select i. P i j. integer.int_lt j i ¬P j

x y z.
    integer.tint_mul x (integer.tint_add y z) =
    integer.tint_add (integer.tint_mul x y) (integer.tint_mul x z)

p q.
    ¬(q = integer.int_of_num 0)
    integer.int_div p (integer.int_neg q) =
    integer.int_div (integer.int_neg p) q

p q.
    ¬(q = integer.int_of_num 0)
    integer.int_le (integer.ABS (integer.int_mul (integer.int_quot p q) q))
      (integer.ABS p)

x y.
    integer.int_mul (integer.int_add x y) (integer.int_sub x y) =
    integer.int_sub (integer.int_mul x x) (integer.int_mul y y)

n i.
    int_bitwise.int_shift_right n i =
    bool.LET
      (pair.UNCURRY (λbs r. int_bitwise.int_of_bits (list.DROP n bs, r)))
      (int_bitwise.bits_of_int i)

n m.
    ¬(m = 0)
    integer.int_div (integer.int_of_num n) (integer.int_of_num m) =
    integer.int_of_num (n div m)

n m.
    ¬(m = 0)
    integer.int_mod (integer.int_of_num n) (integer.int_of_num m) =
    integer.int_of_num (n mod m)

p q.
    ¬(q = 0)
    integer.int_quot (integer.int_of_num p) (integer.int_of_num q) =
    integer.int_of_num (p div q)

p q.
    ¬(q = 0)
    integer.int_rem (integer.int_of_num p) (integer.int_of_num q) =
    integer.int_of_num (p mod q)

cs vs f.
    integer.int_mul f (Omega.sumc cs vs) =
    Omega.sumc (map (λx. integer.int_mul f x) cs) vs

uppers lowers.
    all Omega.fst_nzero uppers all Omega.fst_nzero lowers
    Omega.dark_shadow uppers lowers Omega.real_shadow uppers lowers

integer_word.w2i (words.n2w 1) =
  if fcp.dimindex bool.the_value = 1 then
    integer.int_neg (integer.int_of_num 1)
  else integer.int_of_num 1

integer.int_lt (integer_word.INT_MIN bool.the_value)
    (integer_word.INT_MAX bool.the_value)
  integer.int_lt (integer_word.INT_MAX bool.the_value)
    (integer_word.UINT_MAX bool.the_value)
  integer.int_lt (integer_word.UINT_MAX bool.the_value)
    (integer.int_of_num (words.dimword bool.the_value))

i.
    integer_word.saturate_i2sw i =
    if integer.int_le (integer_word.INT_MAX bool.the_value) i then
      words.word_H
    else if integer.int_le i (integer_word.INT_MIN bool.the_value) then
      words.word_L
    else integer_word.i2w i

n.
    integer.int_lt (integer.int_of_num 0) n
    integer.int_mod (integer.int_neg (integer.int_of_num 1)) n =
    integer.int_sub n (integer.int_of_num 1)

n i j.
    int_bitwise.int_bit n (int_bitwise.int_xor i j)
    ¬(int_bitwise.int_bit n i int_bitwise.int_bit n j)

xs.
    Omega.MAP2 (integer.int_of_num 0) integer.int_add [] xs = xs
    Omega.MAP2 (integer.int_of_num 0) integer.int_add xs [] = xs

w.
    integer_word.saturate_w2sw w =
    if fcp.dimindex bool.the_value fcp.dimindex bool.the_value
       words.word_ls (words.w2w words.word_H) w
    then words.word_H
    else words.w2w w

p q.
    ¬(q = integer.int_of_num 0)
    integer.int_mod p (integer.int_neg q) =
    integer.int_neg (integer.int_mod (integer.int_neg p) q)

x y.
    integer.int_mul x y = integer.int_of_num 0
    x = integer.int_of_num 0 y = integer.int_of_num 0

x y.
    integer.int_le (integer.int_of_num 0) x
    integer.int_le (integer.int_of_num 0) y
    integer.int_le (integer.int_of_num 0) (integer.int_add x y)

x y.
    integer.int_le (integer.int_of_num 0) x
    integer.int_le (integer.int_of_num 0) y
    integer.int_le (integer.int_of_num 0) (integer.int_mul x y)

x y.
    integer.int_le (integer.int_of_num 0) x
    integer.int_lt (integer.int_of_num 0) y
    integer.int_lt (integer.int_of_num 0) (integer.int_add x y)

x y.
    integer.int_lt (integer.int_of_num 0) x
    integer.int_le (integer.int_of_num 0) y
    integer.int_lt (integer.int_of_num 0) (integer.int_add x y)

x y.
    integer.int_lt (integer.int_of_num 0) x
    integer.int_lt (integer.int_of_num 0) y
    integer.int_lt (integer.int_of_num 0) (integer.int_add x y)

c d.
    integer.int_lt (integer.int_of_num 0) c
    integer.int_lt (integer.int_of_num 0) d
    integer.int_lt (integer.int_of_num 0) (integer.int_mul c d)

p n.
    integer.int_exp p n = integer.int_of_num 0
    p = integer.int_of_num 0 ¬(n = 0)

bs rest.
    int_bitwise.int_of_bits (bs, rest) =
    if rest then
      int_bitwise.int_not
        (integer.int_of_num (int_bitwise.num_of_bits (map (¬) bs)))
    else integer.int_of_num (int_bitwise.num_of_bits bs)

integer_word.w2i w =
  if words.w2n w < words.INT_MIN bool.the_value then
    integer.int_of_num (words.w2n w)
  else
    integer.int_sub (integer.int_of_num (words.w2n w))
      (integer.int_of_num (words.dimword bool.the_value))

x = y
  integer.int_lt x (integer.int_add y (integer.int_of_num 1))
  integer.int_lt y (integer.int_add x (integer.int_of_num 1))

integer.int_of_num 0 = integer.int_add c x
  (integer.int_le (integer.int_of_num 0)
     (integer.int_add (integer.int_neg c) y)
   integer.int_le (integer.int_neg x) y)

integer.int_le (integer.int_of_num 0) (integer.int_add c x)
  integer.int_le x y
  (integer.int_le (integer.int_of_num 0) (integer.int_add c y) )

integer.int_le (integer.int_of_num 0) (integer.int_add c x)
  integer.int_lt x y (integer.int_of_num 0 = integer.int_add c y )

i.
    integer.int_le (integer_word.INT_MIN bool.the_value) i
    integer.int_le i (integer_word.INT_MAX bool.the_value)
    words.word_abs (integer_word.i2w i) =
    words.n2w (integer.Num (integer.ABS i))

b n i.
    int_bitwise.int_bit b (int_bitwise.int_shift_left n i)
    n b int_bitwise.int_bit (arithmetic.- b n) i

w.
    1 < fcp.dimindex bool.the_value ¬(w = words.word_L)
    integer_word.w2i (words.word_2comp w) =
    integer.int_neg (integer_word.w2i w)

x x1 x2 x3. Omega.MAP2 x x1 x2 x3 = Omega.MAP2_tupled (x, x1, x2, x3)

i j.
    ¬(j = integer.int_of_num 0)
    integer.int_mod i j =
    integer.int_sub i (integer.int_mul (integer.int_div i j) j)

i j.
    ¬(j = integer.int_of_num 0)
    integer.int_rem i j =
    integer.int_sub i (integer.int_mul (integer.int_quot i j) j)

p q.
    (integer.int_divides p (integer.int_neg q) integer.int_divides p q)
    (integer.int_divides (integer.int_neg p) q integer.int_divides p q)

n m.
    p q.
      integer.int_add (integer.int_mul p (integer.int_of_num n))
        (integer.int_mul q (integer.int_of_num m)) =
      integer.int_of_num (gcd.gcd n m)

n f i j.
    int_bitwise.int_bit n (int_bitwise.int_bitwise f i j)
    f (int_bitwise.int_bit n i) (int_bitwise.int_bit n j)

x y.
    ¬(words.word_msb x words.word_msb y)
    integer_word.w2i (words.word_add x y) =
    integer.int_add (integer_word.w2i x) (integer_word.w2i y)

n x y.
    integer.int_lt (integer.int_of_num 0) n
    (x = y integer.int_mul n x = integer.int_mul n y)

n x y.
    integer.int_lt (integer.int_of_num 0) n
    (integer.int_divides x y
     integer.int_divides (integer.int_mul n x) (integer.int_mul n y))

n x y.
    integer.int_lt (integer.int_of_num 0) n
    (integer.int_lt x y
     integer.int_lt (integer.int_mul n x) (integer.int_mul n y))

x y z.
    integer.int_lt (integer.int_of_num 0) x
    (integer.int_le (integer.int_mul x y) (integer.int_mul x z)
     integer.int_le y z)

x y z.
    integer.int_lt (integer.int_of_num 0) x
    (integer.int_lt (integer.int_mul x y) (integer.int_mul x z)
     integer.int_lt y z)

x y z.
    integer.int_mul x y = integer.int_mul x z
    x = integer.int_of_num 0 y = z

x y z.
    integer.int_mul x z = integer.int_mul y z
    z = integer.int_of_num 0 x = y

i.
    integer_word.saturate_i2w i =
    if integer.int_le (integer_word.UINT_MAX bool.the_value) i then
      words.word_T
    else if integer.int_lt i (integer.int_of_num 0) then words.n2w 0
    else words.n2w (integer.Num i)

cs vs ds.
    integer.int_add (Omega.sumc cs vs) (Omega.sumc ds vs) =
    Omega.sumc (Omega.MAP2 (integer.int_of_num 0) integer.int_add cs ds) vs

P. (n. (¬(n = 0) P (n div arithmetic.BIT2 0)) P n) n. P n

rs.
    Omega.nightmare x c uppers lowers rs
    Omega.calc_nightmare x c rs Omega.evalupper x uppers
    Omega.evallower x lowers

a b c d.
    integer.int_sub (integer.int_add a b) (integer.int_add c d) =
    integer.int_add (integer.int_sub a c) (integer.int_sub b d)

w x y z.
    integer.int_le w x integer.int_le y z
    integer.int_le (integer.int_add w y) (integer.int_add x z)

w x y z.
    integer.int_le w x integer.int_lt y z
    integer.int_lt (integer.int_add w y) (integer.int_add x z)

w x y z.
    integer.int_lt w x integer.int_le y z
    integer.int_lt (integer.int_add w y) (integer.int_add x z)

w x y z.
    integer.int_lt w x integer.int_lt y z
    integer.int_lt (integer.int_add w y) (integer.int_add x z)

n i.
    int_bitwise.int_shift_left n i =
    bool.LET
      (pair.UNCURRY
         (λbs r.
            int_bitwise.int_of_bits (list.GENLIST (const ) n @ bs, r)))
      (int_bitwise.bits_of_int i)

x1 y1 x2 y2. integer.tint_eq (x1, y1) (x2, y2) x1 + y2 = x2 + y1

x1 y1 x2 y2. integer.tint_lt (x1, y1) (x2, y2) x1 + y2 < x2 + y1

x1 y1 x2 y2. integer.tint_add (x1, y1) (x2, y2) = (x1 + x2, y1 + y2)

x1 x2 y1 y2. x1 < y1 x2 < y2 x1 + x2 < y1 + y2

n m.
    integer.int_of_num (arithmetic.- n m) =
    if integer.int_lt (integer.int_of_num n) (integer.int_of_num m) then
      integer.int_of_num 0
    else integer.int_sub (integer.int_of_num n) (integer.int_of_num m)

x1 x2 y1 y2.
    integer.tint_eq x1 x2 integer.tint_eq y1 y2
    (integer.tint_lt x1 y1 integer.tint_lt x2 y2)

x1 x2 y1 y2.
    integer.tint_eq x1 x2 integer.tint_eq y1 y2
    integer.tint_eq (integer.tint_add x1 y1) (integer.tint_add x2 y2)

x1 x2 y1 y2.
    integer.tint_eq x1 x2 integer.tint_eq y1 y2
    integer.tint_eq (integer.tint_mul x1 y1) (integer.tint_mul x2 y2)

¬(k = integer.int_of_num 0)
  integer.int_mod
    (integer.int_add (integer.int_mod i k) (integer.int_mod j k)) k =
  integer.int_mod (integer.int_add i j) k

¬(k = integer.int_of_num 0)
  integer.int_mod
    (integer.int_sub (integer.int_mod i k) (integer.int_mod j k)) k =
  integer.int_mod (integer.int_sub i j) k

integer.int_le (integer.int_of_num 0) (integer.int_add c x)
  integer.int_lt x (integer.int_neg y)
  (integer.int_of_num 0 = integer.int_add (integer.int_neg c) y )

integer.int_le (integer.int_of_num 0) (integer.int_add c x)
  integer.int_lt y (integer.int_neg x)
  (integer.int_le (integer.int_of_num 0)
     (integer.int_add (integer.int_neg c) y) )

((Omega.evalupper x ups Omega.evallower x lows) ) ex'
  (Omega.evalupper x ups Omega.evallower x lows) ex'

x y z.
    ¬(x = integer.int_of_num 0)
    (y = z integer.int_mul x y = integer.int_mul x z)

p q r.
    ¬(p = integer.int_of_num 0)
    (integer.int_divides (integer.int_mul p q) (integer.int_mul p r)
     integer.int_divides q r)

p q r.
    ¬(q = integer.int_of_num 0)
    (integer.int_divides (integer.int_mul p q) (integer.int_mul r q)
     integer.int_divides p r)

x y z.
    ¬(x = integer.int_of_num 0)
    integer.int_mul x y = integer.int_mul x z y = z

x y z.
    ¬(z = integer.int_of_num 0)
    integer.int_mul x z = integer.int_mul y z x = y

n.
    words.INT_MIN bool.the_value n n < words.dimword bool.the_value
    integer_word.w2i (words.n2w n) =
    integer.int_neg
      (integer.int_of_num (arithmetic.- (words.dimword bool.the_value) n))

rs x uppers lowers c.
    Omega.nightmare x c uppers lowers rs
    Omega.evalupper x uppers Omega.evallower x lowers

b i.
    int_bitwise.int_bit b i
    if integer.int_lt i (integer.int_of_num 0) then
      ¬bit.BIT b (integer.Num (int_bitwise.int_not i))
    else bit.BIT b (integer.Num i)

integer.int_le (integer.int_of_num 0) (integer.int_add c x)
  (integer.int_le (integer.int_of_num 0)
     (integer.int_add (integer.int_neg c) (integer.int_neg x))
   integer.int_of_num 0 = integer.int_add c x)

i.
    int_bitwise.bits_of_int i =
    if integer.int_lt i (integer.int_of_num 0) then
      (map (¬)
         (int_bitwise.bits_of_num (integer.Num (int_bitwise.int_not i))),
       )
    else (int_bitwise.bits_of_num (integer.Num i), )

q.
    ¬(q = integer.int_of_num 0)
    p.
      integer.int_mod p q = integer.int_of_num 0
      k. p = integer.int_mul k q

q.
    ¬(q = integer.int_of_num 0)
    p.
      integer.int_rem p q = integer.int_of_num 0
      k. p = integer.int_mul k q

lowers c L.
    0 < c all Omega.fst_nzero lowers Omega.dark_shadow_row c L lowers
    Omega.rshadow_row (c, L) lowers

(p. integer.int_exp p 0 = integer.int_of_num 1)
  p n. integer.int_exp p (suc n) = integer.int_mul p (integer.int_exp p n)

x y d.
    integer.int_lt (integer.int_of_num 0) d
    c.
      integer.int_lt (integer.int_of_num 0) c
      integer.int_lt x (integer.int_add y (integer.int_mul c d))

x y d.
    integer.int_lt (integer.int_of_num 0) d
    c.
      integer.int_lt (integer.int_of_num 0) c
      integer.int_lt (integer.int_sub y (integer.int_mul c d)) x

x y.
    integer.int_add (integer.int_mul x x) (integer.int_mul y y) =
    integer.int_of_num 0
    x = integer.int_of_num 0 y = integer.int_of_num 0

p q.
    ¬(q = integer.int_of_num 0)
    integer.int_mod p q = integer.int_of_num 0
    integer.int_mul (integer.int_div p q) q = p

f x y d.
    DeepSyntax.alldivide f d
    (DeepSyntax.eval_form (DeepSyntax.neginf f) x
     DeepSyntax.eval_form (DeepSyntax.neginf f)
       (integer.int_add x (integer.int_mul y d)))

f x y d.
    DeepSyntax.alldivide f d
    (DeepSyntax.eval_form (DeepSyntax.posinf f) x
     DeepSyntax.eval_form (DeepSyntax.posinf f)
       (integer.int_add x (integer.int_mul y d)))

lowers x.
    Omega.evallower x lowers
    d R.
      bool.IN (d, R) (list.LIST_TO_SET lowers)
      integer.int_le R (integer.int_mul (integer.int_of_num d) x)

uppers x.
    Omega.evalupper x uppers
    c L.
      bool.IN (c, L) (list.LIST_TO_SET uppers)
      integer.int_le (integer.int_mul (integer.int_of_num c) x) L

((Omega.evalupper x ups Omega.evallower x lows) ex) ex'
  (Omega.evalupper x ups Omega.evallower x lows) ex ex'

j.
    integer.int_le (integer_word.INT_MIN bool.the_value) j
    integer.int_le j (integer_word.INT_MAX bool.the_value)
    fcp.dimindex bool.the_value fcp.dimindex bool.the_value
    words.sw2sw (integer_word.i2w j) = integer_word.i2w j

p q r.
    gcd.gcd p q = 1
    (integer.int_divides (integer.int_of_num p)
       (integer.int_mul (integer.int_of_num q) r)
     integer.int_divides (integer.int_of_num p) r)

uppers lowers x.
    Omega.evalupper x uppers Omega.evallower x lowers
    all Omega.fst_nzero uppers all Omega.fst_nzero lowers
    Omega.real_shadow uppers lowers

x y.
    Omega.modhat x y =
    integer.int_sub x
      (integer.int_mul y
         (integer.int_div
            (integer.int_add
               (integer.int_mul (integer.int_of_num (arithmetic.BIT2 0)) x)
               y)
            (integer.int_mul (integer.int_of_num (arithmetic.BIT2 0)) y)))

x x1 x2 x3 x4.
    Omega.nightmare x x1 x2 x3 x4
    Omega.nightmare_tupled (x, x1, x2, x3, x4)

n m x.
    ¬(m = 0)
    (integer.int_lt (integer.int_of_num n)
       (integer.int_mul (integer.int_of_num m) x)
     integer.int_lt
       (integer.int_div (integer.int_of_num n) (integer.int_of_num m)) x)

m n p.
    n m ¬(p = integer.int_of_num 0)
    integer.int_mod (integer.int_exp p m) (integer.int_exp p n) =
    integer.int_of_num 0

(a. integer.int_ABS_CLASS (integer.int_REP_CLASS a) = a)
  c.
    (r. integer.tint_eq r r c = integer.tint_eq r)
    integer.int_REP_CLASS (integer.int_ABS_CLASS c) = c

(lowers. Omega.real_shadow [] lowers )
  upper ls lowers.
    Omega.real_shadow (upper :: ls) lowers
    Omega.rshadow_row upper lowers Omega.real_shadow ls lowers

((Omega.evalupper x ups Omega.evallower x lows) ) ex' p
  ((Omega.evalupper x ups Omega.evallower x lows) ex') p

x d.
    integer.int_lt (integer.int_of_num 0) d
    k.
      integer.int_lt (integer.int_of_num 0)
        (integer.int_add x (integer.int_mul k d))
      integer.int_le (integer.int_add x (integer.int_mul k d)) d

x d.
    integer.int_lt (integer.int_of_num 0) d
    k.
      integer.int_lt (integer.int_of_num 0)
        (integer.int_sub x (integer.int_mul k d))
      integer.int_le (integer.int_sub x (integer.int_mul k d)) d

x.
    integer.int_divides (integer.int_of_num 1) x
    (integer.int_divides x (integer.int_of_num 1)
     x = integer.int_of_num 1 x = integer.int_neg (integer.int_of_num 1))

m n p q.
    integer.int_add (integer.int_mul p (integer.int_of_num m))
      (integer.int_mul q (integer.int_of_num n)) = integer.int_of_num 1
    gcd.gcd m n = 1

a b.
    fcp.dimindex bool.the_value fcp.dimindex bool.the_value
    fcp.dimindex bool.the_value fcp.dimindex bool.the_value
    (integer_word.w2i a = integer_word.w2i b
     words.sw2sw a = words.sw2sw b)

(a. integer.int_ABS_CLASS (integer.int_REP_CLASS a) = a)
  r.
    (let c r in r. integer.tint_eq r r c = integer.tint_eq r)
    integer.int_REP_CLASS (integer.int_ABS_CLASS r) = r

m n x.
    integer.int_lt (integer.int_of_num 0) m
    (integer.int_le (integer.int_of_num 0)
       (integer.int_add (integer.int_mul m x) n)
     integer.int_le (integer.int_of_num 0)
       (integer.int_add x (integer.int_div n m)))

w.
    integer_word.saturate_sw2sw w =
    if fcp.dimindex bool.the_value fcp.dimindex bool.the_value then
      words.sw2sw w
    else if words.word_le (words.sw2sw words.word_H) w then words.word_H
    else if words.word_le w (words.sw2sw words.word_L) then words.word_L
    else words.w2w w

p q.
    ¬(q = integer.int_of_num 0)
    integer.int_rem (integer.int_neg p) q =
    integer.int_neg (integer.int_rem p q)
    integer.int_rem p (integer.int_neg q) = integer.int_rem p q

x y.
    integer.int_lt x (integer.int_add x (integer.int_of_num (bit1 y)))
    integer.int_lt x
      (integer.int_add x (integer.int_of_num (arithmetic.BIT2 y)))
    ¬integer.int_lt x
        (integer.int_add x (integer.int_neg (integer.int_of_num y)))

f d i.
    DeepSyntax.alldivide f d
    integer.int_lt (integer.int_of_num 0) i integer.int_le i d
    DeepSyntax.eval_form (DeepSyntax.neginf f) i
    x. DeepSyntax.eval_form f x

f d i.
    DeepSyntax.alldivide f d
    integer.int_lt (integer.int_of_num 0) i integer.int_le i d
    DeepSyntax.eval_form (DeepSyntax.posinf f) i
    x. DeepSyntax.eval_form f x

P.
    P [] (bs. P bs P ( :: bs)) (bs. P bs P ( :: bs)) v. P v

((Omega.evalupper x ups Omega.evallower x lows) ex) ex' p
  ((Omega.evalupper x ups Omega.evallower x lows) ex ex') p

i.
    integer_word.toString i =
    if integer.int_lt i (integer.int_of_num 0) then
      (string.CHR
         (arithmetic.BIT2
            (arithmetic.BIT2
               (arithmetic.BIT2
                  (arithmetic.BIT2
                     (arithmetic.BIT2 (arithmetic.BIT2 0)))))) :: []) @
      ASCIInumbers.num_to_dec_string (integer.Num (integer.int_neg i))
    else ASCIInumbers.num_to_dec_string (integer.Num i)

m x y.
    ¬(m = 0)
    (integer.int_mul (integer.int_of_num m) x = y
     integer.int_divides (integer.int_of_num m) y
     x = integer.int_div y (integer.int_of_num m))

m n p.
    n m ¬(p = integer.int_of_num 0)
    integer.int_div (integer.int_exp p m) (integer.int_exp p n) =
    integer.int_exp p (arithmetic.- m n)

f cs c v vs.
    Omega.sumc (map f (c :: cs)) (v :: vs) =
    integer.int_add (integer.int_mul (f c) v) (Omega.sumc (map f cs) vs)

uppers lowers.
    all Omega.fst_nzero uppers all Omega.fst_nzero lowers
    ((x. Omega.evalupper x uppers Omega.evallower x lowers)
     Omega.real_shadow uppers lowers
     Omega.dark_shadow_condition uppers lowers)

p q.
    ¬(q = integer.int_of_num 0)
    integer.int_quot (integer.int_neg p) q =
    integer.int_neg (integer.int_quot p q)
    integer.int_quot p (integer.int_neg q) =
    integer.int_neg (integer.int_quot p q)

p q k.
    ¬(q = integer.int_of_num 0)
    integer.int_mod p q = integer.int_of_num 0
    integer.int_div (integer.int_mul k p) q =
    integer.int_mul k (integer.int_div p q)

p q k.
    ¬(q = integer.int_of_num 0)
    integer.int_rem p q = integer.int_of_num 0
    integer.int_quot (integer.int_mul k p) q =
    integer.int_mul k (integer.int_quot p q)

n c x y.
    integer.int_divides (integer.int_mul n x)
      (integer.int_add (integer.int_mul n y) c)
    integer.int_divides (integer.int_mul n x)
      (integer.int_add (integer.int_mul n y) c) integer.int_divides n c

p q.
    integer.int_divides p q
    integer.int_mod q p = integer.int_of_num 0
    ¬(p = integer.int_of_num 0)
    p = integer.int_of_num 0 q = integer.int_of_num 0

x1 y1 x2 y2.
    integer.tint_mul (x1, y1) (x2, y2) =
    (x1 * x2 + y1 * y2, x1 * y2 + y1 * x2)

x y.
    ¬(integer_word.w2i (words.word_add x y) =
       integer.int_add (integer_word.w2i x) (integer_word.w2i y))
    (words.word_msb x words.word_msb y)
    ¬(words.word_msb x words.word_msb (words.word_add x y))

p.
    (n. p = integer.int_of_num n ¬(n = 0))
    (n. p = integer.int_neg (integer.int_of_num n) ¬(n = 0))
    p = integer.int_of_num 0

i.
    integer.int_le (integer_word.INT_MIN bool.the_value) i
    integer.int_le i (integer_word.INT_MAX bool.the_value)
    fcp.dimindex bool.the_value fcp.dimindex bool.the_value
    (i = integer_word.w2i (integer_word.i2w i)
     integer_word.i2w i = words.sw2sw (integer_word.i2w i))

P d x0.
    (x. P x P (integer.int_add x d)) P x0
    c.
      integer.int_lt (integer.int_of_num 0) c
      P (integer.int_add x0 (integer.int_mul c d))

P d x0.
    (x. P x P (integer.int_sub x d)) P x0
    c.
      integer.int_lt (integer.int_of_num 0) c
      P (integer.int_sub x0 (integer.int_mul c d))

(lowers. Omega.dark_shadow [] lowers )
  uppers lowers c L.
    Omega.dark_shadow ((c, L) :: uppers) lowers
    Omega.dark_shadow_row c L lowers Omega.dark_shadow uppers lowers

low d x.
    integer.int_lt low x integer.int_le x (integer.int_add low d)
    j.
      x = integer.int_add low j integer.int_lt (integer.int_of_num 0) j
      integer.int_le j d

high d x.
    integer.int_le (integer.int_sub high d) x integer.int_lt x high
    j.
      x = integer.int_sub high j
      integer.int_lt (integer.int_of_num 0) j integer.int_le j d

c L x.
    integer.int_le (integer.int_mul (integer.int_of_num c) x) L 0 < c
    lowers.
      all Omega.fst_nzero lowers Omega.evallower x lowers
      Omega.rshadow_row (c, L) lowers

n m.
    n < words.dimword bool.the_value m fcp.dimindex bool.the_value
    integer.Num
      (integer.int_mod (integer_word.w2i (words.n2w n))
         (integer.int_exp (integer.int_of_num (arithmetic.BIT2 0)) m)) =
    n mod arithmetic.BIT2 0 m

((Omega.evalupper x ups Omega.evallower x lows) ex)
  integer.int_le r (integer.int_mul (integer.int_of_num c) x)
  (Omega.evalupper x ups Omega.evallower x ((c, r) :: lows)) ex

((Omega.evalupper x ups Omega.evallower x lows) ex)
  integer.int_le (integer.int_mul (integer.int_of_num c) x) r
  (Omega.evalupper x ((c, r) :: ups) Omega.evallower x lows) ex

(lowers. Omega.dark_shadow_condition [] lowers )
  uppers lowers c L.
    Omega.dark_shadow_condition ((c, L) :: uppers) lowers
    Omega.dark_shadow_cond_row (c, L) lowers
    Omega.dark_shadow_condition uppers lowers

x1 x2 y1 y2.
    integer.int_le (integer.int_of_num 0) x1
    integer.int_le (integer.int_of_num 0) y1 integer.int_lt x1 x2
    integer.int_lt y1 y2
    integer.int_lt (integer.int_mul x1 y1) (integer.int_mul x2 y2)

n i.
    n < fcp.dimindex bool.the_value
    integer.int_le (integer_word.INT_MIN bool.the_value) i
    integer.int_le i (integer_word.INT_MAX bool.the_value)
    integer_word.i2w
      (integer.int_div i
         (integer.int_exp (integer.int_of_num (arithmetic.BIT2 0)) n)) =
    words.word_asr (integer_word.i2w i) n

n m.
    (even n
     integer.int_exp (integer.int_neg (integer.int_of_num m)) n =
     integer.int_of_num (m n))
    (odd n
     integer.int_exp (integer.int_neg (integer.int_of_num m)) n =
     integer.int_neg (integer.int_of_num (m n)))

a b.
    integer_word.signed_saturate_add a b =
    bool.LET
      (bool.LET
         (λsum msba.
            if (msba words.word_msb b) ¬(msba words.word_msb sum)
            then if msba then words.word_L else words.word_H
            else sum) (words.word_add a b)) (words.word_msb a)

P.
    (x. P x []) (x c y cs. P x cs P x ((c, y) :: cs)) v v1. P v v1

P.
    (lowers. P [] lowers)
    (c L uppers lowers. P uppers lowers P ((c, L) :: uppers) lowers)
    v v1. P v v1

low high x.
    integer.int_lt low x integer.int_le x high
    integer.int_lt low high
    (x = high
     integer.int_lt low x
     integer.int_le x (integer.int_sub high (integer.int_of_num 1)))

uppers lowers.
    all Omega.fst_nzero uppers all Omega.fst_nzero lowers
    all Omega.fst1 uppers all Omega.fst1 lowers
    ((x. Omega.evalupper x uppers Omega.evallower x lowers)
     Omega.real_shadow uppers lowers)

(x. Omega.evallower x [] )
  y x cs c.
    Omega.evallower x ((c, y) :: cs)
    integer.int_le y (integer.int_mul (integer.int_of_num c) x)
    Omega.evallower x cs

(x. Omega.evalupper x [] )
  y x cs c.
    Omega.evalupper x ((c, y) :: cs)
    integer.int_le (integer.int_mul (integer.int_of_num c) x) y
    Omega.evalupper x cs

int_bitwise.num_of_bits [] = 0
  (bs.
     int_bitwise.num_of_bits ( :: bs) =
     arithmetic.BIT2 0 * int_bitwise.num_of_bits bs)
  bs.
    int_bitwise.num_of_bits ( :: bs) =
    1 + arithmetic.BIT2 0 * int_bitwise.num_of_bits bs

i n.
    integer.int_lt (integer.int_of_num 0) n
    integer.int_rem i n =
    if integer.int_lt i (integer.int_of_num 0) then
      integer.int_add
        (integer.int_sub
           (integer.int_mod (integer.int_sub i (integer.int_of_num 1)) n)
           n) (integer.int_of_num 1)
    else integer.int_mod i n

P a b.
    P (integer.int_of_num (arithmetic.- a b))
    integer.int_le (integer.int_of_num b) (integer.int_of_num a)
    P
      (integer.int_add (integer.int_of_num a)
         (integer.int_neg (integer.int_of_num b)))
    integer.int_lt (integer.int_of_num a) (integer.int_of_num b)
    P (integer.int_of_num 0)

a b.
    integer_word.signed_saturate_sub a b =
    if b = words.word_L then
      if words.word_le (words.n2w 0) a then words.word_H
      else words.word_add a words.word_L
    else if fcp.dimindex bool.the_value = 1 then
      words.word_and a (words.word_1comp b)
    else integer_word.signed_saturate_add a (words.word_2comp b)

((Omega.evalupper x ups Omega.evallower x lows) ex)
  integer.int_le r (integer.int_mul (integer.int_of_num c) x) p
  ((Omega.evalupper x ups Omega.evallower x ((c, r) :: lows)) ex) p

((Omega.evalupper x ups Omega.evallower x lows) ex)
  integer.int_le (integer.int_mul (integer.int_of_num c) x) r p
  ((Omega.evalupper x ((c, r) :: ups) Omega.evallower x lows) ex) p

cs vs c v.
    Omega.sumc [] vs = integer.int_of_num 0
    Omega.sumc cs [] = integer.int_of_num 0
    Omega.sumc (c :: cs) (v :: vs) =
    integer.int_add (integer.int_mul c v) (Omega.sumc cs vs)

int_bitwise.bits_of_num =
  relation.WFREC
    (select R.
       wellFounded R n. ¬(n = 0) R (n div arithmetic.BIT2 0) n)
    (λbits_of_num n.
       id
         (if n = 0 then []
          else odd n :: bits_of_num (n div arithmetic.BIT2 0)))

c d.
    ¬(c = integer.int_of_num 0)
    (¬integer.int_divides c d
     i.
       integer.int_le (integer.int_of_num 1) i
       integer.int_le i
         (integer.int_sub (integer.ABS c) (integer.int_of_num 1))
       integer.int_divides c (integer.int_add d i))

x y.
    integer.int_mul x y = integer.int_of_num 1
    x = integer.int_of_num 1 y = integer.int_of_num 1
    x = integer.int_neg (integer.int_of_num 1)
    y = integer.int_neg (integer.int_of_num 1)

uppers lowers.
    Omega.real_shadow uppers lowers
    c d L R.
      bool.IN (c, L) (list.LIST_TO_SET uppers)
      bool.IN (d, R) (list.LIST_TO_SET lowers)
      integer.int_le (integer.int_mul (integer.int_of_num c) R)
        (integer.int_mul (integer.int_of_num d) L)

n d.
    ¬(n = 0)
    (¬integer.int_divides (integer.int_of_num n) d
     i.
       (integer.int_le (integer.int_of_num 1) i
        integer.int_le i
          (integer.int_sub (integer.int_of_num n)
             (integer.int_of_num 1)))
       integer.int_divides (integer.int_of_num n) (integer.int_add d i))

i j k.
    ¬(k = integer.int_of_num 0)
    (integer.int_mod i k = integer.int_of_num 0
     integer.int_mod j k = integer.int_of_num 0)
    integer.int_div (integer.int_add i j) k =
    integer.int_add (integer.int_div i k) (integer.int_div j k)

p q.
    ¬(q = integer.int_of_num 0)
    if integer.int_lt q (integer.int_of_num 0) then
      integer.int_lt q (integer.int_mod p q)
      integer.int_le (integer.int_mod p q) (integer.int_of_num 0)
    else
      integer.int_le (integer.int_of_num 0) (integer.int_mod p q)
      integer.int_lt (integer.int_mod p q) q

p q k.
    (r.
       p = integer.int_add (integer.int_mul k q) r
       (if integer.int_lt (integer.int_of_num 0) p then
          integer.int_le (integer.int_of_num 0) r
        else integer.int_le r (integer.int_of_num 0))
       integer.int_lt (integer.ABS r) (integer.ABS q))
    integer.int_quot p q = k

p q r.
    integer.int_lt (integer.ABS r) (integer.ABS q)
    (if integer.int_lt (integer.int_of_num 0) p then
       integer.int_le (integer.int_of_num 0) r
     else integer.int_le r (integer.int_of_num 0))
    (k. p = integer.int_add (integer.int_mul k q) r)
    integer.int_rem p q = r

n m x.
    ¬(m = 0)
    (integer.int_lt (integer.int_mul (integer.int_of_num m) x)
       (integer.int_of_num n)
     integer.int_lt x
       (if integer.int_divides (integer.int_of_num m)
             (integer.int_of_num n)
        then integer.int_div (integer.int_of_num n) (integer.int_of_num m)
        else
          integer.int_add
            (integer.int_div (integer.int_of_num n) (integer.int_of_num m))
            (integer.int_of_num 1)))

P.
    (x c. P x c []) (x c d R rs. P x c rs P x c ((d, R) :: rs))
    v v1 v2. P v v1 v2

P.
    (c L. P c L []) (c L d R rs. P c L rs P c L ((d, R) :: rs))
    v v1 v2. P v v1 v2

P.
    (v0. P v0 []) (v4 v5. P [] (v4 :: v5))
    (c cs cs vs. P cs vs P (c :: cs) (cs :: vs)) cs vs. P cs vs

i j q.
    (r.
       i = integer.int_add (integer.int_mul q j) r
       if integer.int_lt j (integer.int_of_num 0) then
         integer.int_lt j r integer.int_le r (integer.int_of_num 0)
       else integer.int_le (integer.int_of_num 0) r integer.int_lt r j)
    integer.int_div i j = q

i j m.
    (q.
       i = integer.int_add (integer.int_mul q j) m
       if integer.int_lt j (integer.int_of_num 0) then
         integer.int_lt j m integer.int_le m (integer.int_of_num 0)
       else integer.int_le (integer.int_of_num 0) m integer.int_lt m j)
    integer.int_mod i j = m

uppers lowers m.
    all Omega.fst_nzero uppers all Omega.fst_nzero lowers
    all (λp. fst p m) uppers
    ((x. Omega.evalupper x uppers Omega.evallower x lowers)
     Omega.dark_shadow uppers lowers
     x. Omega.nightmare x m uppers lowers lowers)

p q r.
    (q int_arith.bmarker p int_arith.bmarker p q)
    (q int_arith.bmarker p r int_arith.bmarker p q r)
    ((int_arith.bmarker p q) r int_arith.bmarker p q r)

uppers lowers L x.
    Omega.rshadow_row (1, L) lowers Omega.evallower x lowers
    Omega.evalupper x uppers all Omega.fst_nzero lowers
    all Omega.fst1 uppers
    x.
      integer.int_le x L Omega.evalupper x uppers
      Omega.evallower x lowers

(v0. Omega.sumc v0 [] = integer.int_of_num 0)
  (v5 v4. Omega.sumc [] (v4 :: v5) = integer.int_of_num 0)
  vs v cs c.
    Omega.sumc (c :: cs) (v :: vs) =
    integer.int_add (integer.int_mul c v) (Omega.sumc cs vs)

P.
    (t.
       P
         (string.CHR
            (arithmetic.BIT2
               (arithmetic.BIT2
                  (arithmetic.BIT2
                     (arithmetic.BIT2
                        (arithmetic.BIT2 (arithmetic.BIT2 0)))))) :: t))
    (t.
       P
         (string.CHR
            (bit1
               (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 1)))) ::
          t)) P [] (v4 v1. P (v4 :: v1)) v. P v

P.
    (c L. P (c, L) [])
    (c L d R t. P (c, L) t P (c, L) ((d, R) :: t))
    v v1 v2. P (v, v1) v2

(uppery upperc. Omega.rshadow_row (upperc, uppery) [] )
  uppery upperc rs lowery lowerc.
    Omega.rshadow_row (upperc, uppery) ((lowerc, lowery) :: rs)
    integer.int_le (integer.int_mul (integer.int_of_num upperc) lowery)
      (integer.int_mul (integer.int_of_num lowerc) uppery)
    Omega.rshadow_row (upperc, uppery) rs

int_bitwise.num_of_bits =
  relation.WFREC
    (select R. wellFounded R (bs. R bs ( :: bs)) bs. R bs ( :: bs))
    (λnum_of_bits a.
       list.list_CASE a (id 0)
         (λv bs.
            if v then id (1 + arithmetic.BIT2 0 * num_of_bits bs)
            else id (arithmetic.BIT2 0 * num_of_bits bs)))

uppers lowers m.
    all Omega.fst_nzero uppers all Omega.fst_nzero lowers
    all (λp. fst p m) uppers
    ((x. Omega.evalupper x uppers Omega.evallower x lowers)
     Omega.real_shadow uppers lowers
     (Omega.dark_shadow uppers lowers
      x. Omega.nightmare x m uppers lowers lowers))

q.
    ¬(q = integer.int_of_num 0)
    p.
      p =
      integer.int_add (integer.int_mul (integer.int_quot p q) q)
        (integer.int_rem p q)
      (if integer.int_lt (integer.int_of_num 0) p then
         integer.int_le (integer.int_of_num 0) (integer.int_rem p q)
       else integer.int_le (integer.int_rem p q) (integer.int_of_num 0))
      integer.int_lt (integer.ABS (integer.int_rem p q)) (integer.ABS q)

Omega.dark_shadow_tupled =
  relation.WFREC
    (select R.
       wellFounded R
       L c lowers uppers. R (uppers, lowers) ((c, L) :: uppers, lowers))
    (λdark_shadow_tupled a.
       pair.pair_CASE a
         (λv lowers.
            list.list_CASE v (id )
              (λv2 uppers.
                 pair.pair_CASE v2
                   (λc L.
                      id
                        (Omega.dark_shadow_row c L lowers
                         dark_shadow_tupled (uppers, lowers))))))

(m n.
     integer.int_mul (integer.int_of_num m) (integer.int_of_num n) =
     integer.int_of_num (m * n))
  (x y.
     integer.int_mul (integer.int_neg x) y =
     integer.int_neg (integer.int_mul x y))
  (x y.
     integer.int_mul x (integer.int_neg y) =
     integer.int_neg (integer.int_mul x y))
  x. integer.int_neg (integer.int_neg x) = x

Omega.dark_shadow_condition_tupled =
  relation.WFREC
    (select R.
       wellFounded R
       L c lowers uppers. R (uppers, lowers) ((c, L) :: uppers, lowers))
    (λdark_shadow_condition_tupled a.
       pair.pair_CASE a
         (λv lowers.
            list.list_CASE v (id )
              (λv2 uppers.
                 pair.pair_CASE v2
                   (λc L.
                      id
                        (Omega.dark_shadow_cond_row (c, L) lowers
                         dark_shadow_condition_tupled (uppers, lowers))))))

p n m.
    integer.int_exp p 0 = integer.int_of_num 1
    integer.int_exp (integer.int_of_num n) m = integer.int_of_num (n m)
    integer.int_exp (integer.int_neg (integer.int_of_num n)) (bit1 m) =
    integer.int_neg (integer.int_of_num (n bit1 m))
    integer.int_exp (integer.int_neg (integer.int_of_num n))
      (arithmetic.BIT2 m) = integer.int_of_num (n arithmetic.BIT2 m)

n m p.
    integer.int_exp p 0 = integer.int_of_num 1
    integer.int_exp (integer.int_of_num n) m = integer.int_of_num (n m)
    integer.int_exp (integer.int_neg (integer.int_of_num n)) (bit1 m) =
    integer.int_neg (integer.int_of_num (n bit1 m))
    integer.int_exp (integer.int_neg (integer.int_of_num n))
      (arithmetic.BIT2 m) = integer.int_of_num (n arithmetic.BIT2 m)

Omega.evallower_tupled =
  relation.WFREC
    (select R. wellFounded R y c cs x. R (x, cs) (x, (c, y) :: cs))
    (λevallower_tupled a.
       pair.pair_CASE a
         (λx v1.
            list.list_CASE v1 (id )
              (λv2 cs.
                 pair.pair_CASE v2
                   (λc y.
                      id
                        (integer.int_le y
                           (integer.int_mul (integer.int_of_num c) x)
                         evallower_tupled (x, cs))))))

Omega.evalupper_tupled =
  relation.WFREC
    (select R. wellFounded R y c cs x. R (x, cs) (x, (c, y) :: cs))
    (λevalupper_tupled a.
       pair.pair_CASE a
         (λx v1.
            list.list_CASE v1 (id )
              (λv2 cs.
                 pair.pair_CASE v2
                   (λc y.
                      id
                        (integer.int_le
                           (integer.int_mul (integer.int_of_num c) x) y
                         evalupper_tupled (x, cs))))))

uppers lowers c L x.
    0 < c Omega.rshadow_row (c, L) lowers Omega.evalupper x uppers
    Omega.evallower x lowers all Omega.fst_nzero uppers
    all Omega.fst1 lowers
    y.
      integer.int_le (integer.int_mul (integer.int_of_num c) y) L
      Omega.evalupper y uppers Omega.evallower y lowers

Omega.sumc_tupled =
  relation.WFREC
    (select R. wellFounded R v c vs cs. R (cs, vs) (c :: cs, v :: vs))
    (λsumc_tupled a.
       pair.pair_CASE a
         (λv0 v3.
            list.list_CASE v3 (id (integer.int_of_num 0))
              (λv vs.
                 list.list_CASE v0 (id (integer.int_of_num 0))
                   (λc cs.
                      id
                        (integer.int_add (integer.int_mul c v)
                           (sumc_tupled (cs, vs)))))))

p q.
    (integer.ABS p = q
     p = q integer.int_lt (integer.int_of_num 0) q
     p = integer.int_neg q integer.int_le (integer.int_of_num 0) q)
    (q = integer.ABS p
     p = q integer.int_lt (integer.int_of_num 0) q
     p = integer.int_neg q integer.int_le (integer.int_of_num 0) q)

q.
    ¬(q = integer.int_of_num 0)
    p.
      p =
      integer.int_add (integer.int_mul (integer.int_div p q) q)
        (integer.int_mod p q)
      if integer.int_lt q (integer.int_of_num 0) then
        integer.int_lt q (integer.int_mod p q)
        integer.int_le (integer.int_mod p q) (integer.int_of_num 0)
      else
        integer.int_le (integer.int_of_num 0) (integer.int_mod p q)
        integer.int_lt (integer.int_mod p q) q

n m.
    (integer.int_lt (integer.int_of_num n) (integer.int_of_num m)
     n < m)
    (integer.int_lt (integer.int_neg (integer.int_of_num n))
       (integer.int_neg (integer.int_of_num m)) m < n)
    (integer.int_lt (integer.int_neg (integer.int_of_num n))
       (integer.int_of_num m) ¬(n = 0) ¬(m = 0))
    (integer.int_lt (integer.int_of_num n)
       (integer.int_neg (integer.int_of_num m)) )

uppers lowers.
    Omega.dark_shadow uppers lowers
    c d L R.
      bool.IN (c, L) (list.LIST_TO_SET uppers)
      bool.IN (d, R) (list.LIST_TO_SET lowers)
      integer.int_ge
        (integer.int_sub (integer.int_mul (integer.int_of_num d) L)
           (integer.int_mul (integer.int_of_num c) R))
        (integer.int_mul
           (integer.int_sub (integer.int_of_num c) (integer.int_of_num 1))
           (integer.int_sub (integer.int_of_num d) (integer.int_of_num 1)))

integer_word.fromString =
  relation.WFREC (select R. wellFounded R)
    (λfromString a.
       list.list_CASE a
         (id (integer.int_of_num (ASCIInumbers.num_from_dec_string [])))
         (λv2 t.
            bool.literal_case
              (λv4.
                 if v4 =
                    string.CHR
                      (arithmetic.BIT2
                         (arithmetic.BIT2
                            (arithmetic.BIT2
                               (arithmetic.BIT2
                                  (arithmetic.BIT2 (arithmetic.BIT2 0))))))
                 then
                   id
                     (integer.int_neg
                        (integer.int_of_num
                           (ASCIInumbers.num_from_dec_string t)))
                 else if v4 =
                         string.CHR
                           (bit1
                              (arithmetic.BIT2
                                 (arithmetic.BIT2 (arithmetic.BIT2 1))))
                 then
                   id
                     (integer.int_neg
                        (integer.int_of_num
                           (ASCIInumbers.num_from_dec_string t)))
                 else
                   id
                     (integer.int_of_num
                        (ASCIInumbers.num_from_dec_string (v4 :: t)))) v2))

(c L. Omega.dark_shadow_row c L [] )
  rs d c R L.
    Omega.dark_shadow_row c L ((d, R) :: rs)
    integer.int_ge
      (integer.int_sub (integer.int_mul (integer.int_of_num d) L)
         (integer.int_mul (integer.int_of_num c) R))
      (integer.int_mul
         (integer.int_sub (integer.int_of_num c) (integer.int_of_num 1))
         (integer.int_sub (integer.int_of_num d) (integer.int_of_num 1)))
    Omega.dark_shadow_row c L rs

m a x b p q.
    integer.int_add (integer.int_mul p (integer.int_of_num a))
      (integer.int_mul q (integer.int_of_num m)) = integer.int_of_num 1
    ¬(m = 0) ¬(a = 0)
    (integer.int_divides (integer.int_of_num m)
       (integer.int_add (integer.int_mul (integer.int_of_num a) x) b)
     t.
       x =
       integer.int_add (integer.int_mul (integer.int_neg p) b)
         (integer.int_mul t (integer.int_of_num m)))

p q.
    (integer.int_lt (integer.int_of_num 0) (integer.int_mul p q)
     integer.int_lt (integer.int_of_num 0) p
     integer.int_lt (integer.int_of_num 0) q
     integer.int_lt p (integer.int_of_num 0)
     integer.int_lt q (integer.int_of_num 0))
    (integer.int_lt (integer.int_mul p q) (integer.int_of_num 0)
     integer.int_lt (integer.int_of_num 0) p
     integer.int_lt q (integer.int_of_num 0)
     integer.int_lt p (integer.int_of_num 0)
     integer.int_lt (integer.int_of_num 0) q)

f d x.
    DeepSyntax.alldivide f d integer.int_lt (integer.int_of_num 0) d
    DeepSyntax.eval_form f x
    (i.
       integer.int_lt (integer.int_of_num 0) i integer.int_le i d
       DeepSyntax.eval_form (DeepSyntax.neginf f) i)
    j b.
      integer.int_lt (integer.int_of_num 0) j integer.int_le j d
      bool.IN b (DeepSyntax.Bset f)
      DeepSyntax.eval_form f (integer.int_add b j)

P.
    (x c uppers lowers. P x c uppers lowers [])
    (x c uppers lowers d R rs.
       P x c uppers lowers rs P x c uppers lowers ((d, R) :: rs))
    v v1 v2 v3 v4. P v v1 v2 v3 v4

c x cs vs.
    integer.int_lt (integer.int_of_num 0) c
    (integer.int_of_num 0 =
     integer.int_add (integer.int_mul c x) (Omega.sumc cs vs)
     s.
       x =
       integer.int_add
         (integer.int_mul
            (integer.int_neg (integer.int_add c (integer.int_of_num 1))) s)
         (Omega.sumc
            (map
               (λx.
                  Omega.modhat x
                    (integer.int_add c (integer.int_of_num 1))) cs) vs)
       integer.int_of_num 0 =
       integer.int_add (integer.int_mul c x) (Omega.sumc cs vs))

f d x.
    DeepSyntax.alldivide f d integer.int_lt (integer.int_of_num 0) d
    DeepSyntax.eval_form f x
    (i.
       integer.int_lt (integer.int_of_num 0) i integer.int_le i d
       DeepSyntax.eval_form (DeepSyntax.posinf f) i)
    j b.
      integer.int_lt (integer.int_of_num 0) j integer.int_le j d
      bool.IN b (DeepSyntax.Aset f)
      DeepSyntax.eval_form f (integer.int_add b (integer.int_neg j))

%%genvar%%4435 x c.
    ¬(c = integer.int_of_num 0)
    (%%genvar%%4435 (integer.int_div x c)
     k r.
       x = integer.int_add (integer.int_mul k c) r
       (integer.int_lt c (integer.int_of_num 0) integer.int_lt c r
        integer.int_le r (integer.int_of_num 0)
        ¬integer.int_lt c (integer.int_of_num 0)
        integer.int_le (integer.int_of_num 0) r integer.int_lt r c)
       %%genvar%%4435 k)

%%genvar%%4385 x c.
    ¬(c = integer.int_of_num 0)
    (%%genvar%%4385 (integer.int_div x c)
     k r.
       x = integer.int_add (integer.int_mul k c) r
       (integer.int_lt c (integer.int_of_num 0) integer.int_lt c r
        integer.int_le r (integer.int_of_num 0)
        ¬integer.int_lt c (integer.int_of_num 0)
        integer.int_le (integer.int_of_num 0) r integer.int_lt r c)
       %%genvar%%4385 k)

%%genvar%%4462 x c.
    ¬(c = integer.int_of_num 0)
    (%%genvar%%4462 (integer.int_mod x c)
     q r.
       x = integer.int_add (integer.int_mul q c) r
       (integer.int_lt c (integer.int_of_num 0) integer.int_lt c r
        integer.int_le r (integer.int_of_num 0)
        ¬integer.int_lt c (integer.int_of_num 0)
        integer.int_le (integer.int_of_num 0) r integer.int_lt r c)
       %%genvar%%4462 r)

%%genvar%%4410 x c.
    ¬(c = integer.int_of_num 0)
    (%%genvar%%4410 (integer.int_mod x c)
     k r.
       x = integer.int_add (integer.int_mul k c) r
       (integer.int_lt c (integer.int_of_num 0) integer.int_lt c r
        integer.int_le r (integer.int_of_num 0)
        ¬integer.int_lt c (integer.int_of_num 0)
        integer.int_le (integer.int_of_num 0) r integer.int_lt r c)
       %%genvar%%4410 r)

i j.
    ¬(j = integer.int_of_num 0)
    integer.int_quot i j =
    if integer.int_lt (integer.int_of_num 0) j then
      if integer.int_le (integer.int_of_num 0) i then
        integer.int_of_num (integer.Num i div integer.Num j)
      else
        integer.int_neg
          (integer.int_of_num
             (integer.Num (integer.int_neg i) div integer.Num j))
    else if integer.int_le (integer.int_of_num 0) i then
      integer.int_neg
        (integer.int_of_num
           (integer.Num i div integer.Num (integer.int_neg j)))
    else
      integer.int_of_num
        (integer.Num (integer.int_neg i) div
         integer.Num (integer.int_neg j))

(m n. integer.int_of_num m = integer.int_of_num n m = n)
  (x y. integer.int_neg x = integer.int_neg y x = y)
  n m.
    (integer.int_of_num n = integer.int_neg (integer.int_of_num m)
     n = 0 m = 0)
    (integer.int_neg (integer.int_of_num n) = integer.int_of_num m
     n = 0 m = 0)

p q.
    (integer.int_le (integer.ABS p) q
     integer.int_le p q integer.int_le (integer.int_neg q) p)
    (integer.int_le q (integer.ABS p)
     integer.int_le q p integer.int_le p (integer.int_neg q))
    (integer.int_le (integer.int_neg (integer.ABS p)) q
     integer.int_le (integer.int_neg q) p integer.int_le p q)
    (integer.int_le q (integer.int_neg (integer.ABS p))
     integer.int_le p (integer.int_neg q) integer.int_le q p)

p q.
    (integer.int_lt (integer.ABS p) q
     integer.int_lt p q integer.int_lt (integer.int_neg q) p)
    (integer.int_lt q (integer.ABS p)
     integer.int_lt q p integer.int_lt p (integer.int_neg q))
    (integer.int_lt (integer.int_neg (integer.ABS p)) q
     integer.int_lt (integer.int_neg q) p integer.int_lt p q)
    (integer.int_lt q (integer.int_neg (integer.ABS p))
     integer.int_lt p (integer.int_neg q) integer.int_lt q p)

f d.
    DeepSyntax.alldivide f d integer.int_lt (integer.int_of_num 0) d
    ((x. DeepSyntax.eval_form f x)
     (i.
        const
          (integer.int_lt (integer.int_of_num 0) i integer.int_le i d)
          i DeepSyntax.eval_form (DeepSyntax.neginf f) i)
     b j.
       (bool.IN b (DeepSyntax.Bset f)
        const
          (integer.int_lt (integer.int_of_num 0) j integer.int_le j d)
          j) DeepSyntax.eval_form f (integer.int_add b j))

x.
    (d d0. x = DeepSyntax.Conjn d d0)
    (d d0. x = DeepSyntax.Disjn d d0) (d. x = DeepSyntax.Negn d)
    (b. x = DeepSyntax.UnrelatedBool b) (i. x = DeepSyntax.xLT i)
    (i. x = DeepSyntax.LTx i) (i. x = DeepSyntax.xEQ i)
    i i0. x = DeepSyntax.xDivided i i0

Omega.rshadow_row_tupled =
  relation.WFREC
    (select R.
       wellFounded R
       lowery lowerc rs uppery upperc.
         R ((upperc, uppery), rs)
           ((upperc, uppery), (lowerc, lowery) :: rs))
    (λrshadow_row_tupled a.
       pair.pair_CASE a
         (λv v1.
            list.list_CASE v1 (id )
              (λv2 rs.
                 pair.pair_CASE v2
                   (λlowerc lowery.
                      pair.pair_CASE v
                        (λupperc uppery.
                           id
                             (integer.int_le
                                (integer.int_mul
                                   (integer.int_of_num upperc) lowery)
                                (integer.int_mul
                                   (integer.int_of_num lowerc) uppery)
                              rshadow_row_tupled
                                ((upperc, uppery), rs)))))))

(x c. Omega.calc_nightmare x c [] )
  x rs d c R.
    Omega.calc_nightmare x c ((d, R) :: rs)
    (i.
       (integer.int_le (integer.int_of_num 0) i
        integer.int_le i
          (integer.int_div
             (integer.int_sub
                (integer.int_sub
                   (integer.int_mul (integer.int_of_num c)
                      (integer.int_of_num d)) (integer.int_of_num c))
                (integer.int_of_num d)) (integer.int_of_num c)))
       integer.int_mul (integer.int_of_num d) x = integer.int_add R i)
    Omega.calc_nightmare x c rs

rs x c uppers lowers.
    Omega.nightmare x c uppers lowers rs
    i d R.
      integer.int_le (integer.int_of_num 0) i
      integer.int_le i
        (integer.int_div
           (integer.int_sub
              (integer.int_sub
                 (integer.int_mul (integer.int_of_num d)
                    (integer.int_of_num c)) (integer.int_of_num c))
              (integer.int_of_num d)) (integer.int_of_num c))
      bool.IN (d, R) (list.LIST_TO_SET rs) Omega.evalupper x uppers
      Omega.evallower x lowers
      integer.int_mul (integer.int_of_num d) x = integer.int_add R i

f d.
    DeepSyntax.alldivide f d integer.int_lt (integer.int_of_num 0) d
    ((x. DeepSyntax.eval_form f x)
     (i.
        const
          (integer.int_lt (integer.int_of_num 0) i integer.int_le i d)
          i DeepSyntax.eval_form (DeepSyntax.posinf f) i)
     b j.
       (bool.IN b (DeepSyntax.Aset f)
        const
          (integer.int_lt (integer.int_of_num 0) j integer.int_le j d)
          j)
       DeepSyntax.eval_form f
         (integer.int_add b
            (integer.int_mul (integer.int_neg (integer.int_of_num 1)) j)))

m n p.
    integer.int_mul p (integer.int_of_num 0) = integer.int_of_num 0
    integer.int_mul (integer.int_of_num 0) p = integer.int_of_num 0
    integer.int_mul (integer.int_of_num m) (integer.int_of_num n) =
    integer.int_of_num (m * n)
    integer.int_mul (integer.int_neg (integer.int_of_num m))
      (integer.int_of_num n) =
    integer.int_neg (integer.int_of_num (m * n))
    integer.int_mul (integer.int_of_num m)
      (integer.int_neg (integer.int_of_num n)) =
    integer.int_neg (integer.int_of_num (m * n))
    integer.int_mul (integer.int_neg (integer.int_of_num m))
      (integer.int_neg (integer.int_of_num n)) = integer.int_of_num (m * n)

(n m.
     ¬(m = 0)
     integer.int_div (integer.int_of_num n) (integer.int_of_num m) =
     integer.int_of_num (n div m))
  (p q.
     ¬(q = integer.int_of_num 0)
     integer.int_div p (integer.int_neg q) =
     integer.int_div (integer.int_neg p) q)
  (m n. integer.int_of_num m = integer.int_of_num n m = n)
  (x.
     integer.int_neg x = integer.int_of_num 0 x = integer.int_of_num 0)
  x. integer.int_neg (integer.int_neg x) = x

(n m.
     ¬(m = 0)
     integer.int_mod (integer.int_of_num n) (integer.int_of_num m) =
     integer.int_of_num (n mod m))
  (p q.
     ¬(q = integer.int_of_num 0)
     integer.int_mod p (integer.int_neg q) =
     integer.int_neg (integer.int_mod (integer.int_neg p) q))
  (x. integer.int_neg (integer.int_neg x) = x)
  (m n. integer.int_of_num m = integer.int_of_num n m = n)
  x. integer.int_neg x = integer.int_of_num 0 x = integer.int_of_num 0

P.
    (d d0. P d P d0 P (DeepSyntax.Conjn d d0))
    (d d0. P d P d0 P (DeepSyntax.Disjn d d0))
    (d. P d P (DeepSyntax.Negn d))
    (b. P (DeepSyntax.UnrelatedBool b)) (i. P (DeepSyntax.xLT i))
    (i. P (DeepSyntax.LTx i)) (i. P (DeepSyntax.xEQ i))
    (i i0. P (DeepSyntax.xDivided i i0)) d. P d

m n p.
    integer.int_sub p (integer.int_of_num 0) = p
    integer.int_sub (integer.int_of_num 0) p = integer.int_neg p
    integer.int_sub (integer.int_of_num m) (integer.int_of_num n) =
    integer.int_add (integer.int_of_num m)
      (integer.int_neg (integer.int_of_num n))
    integer.int_sub (integer.int_neg (integer.int_of_num m))
      (integer.int_of_num n) =
    integer.int_add (integer.int_neg (integer.int_of_num m))
      (integer.int_neg (integer.int_of_num n))
    integer.int_sub (integer.int_of_num m)
      (integer.int_neg (integer.int_of_num n)) =
    integer.int_add (integer.int_of_num m) (integer.int_of_num n)
    integer.int_sub (integer.int_neg (integer.int_of_num m))
      (integer.int_neg (integer.int_of_num n)) =
    integer.int_add (integer.int_neg (integer.int_of_num m))
      (integer.int_of_num n)

Omega.dark_shadow_row_tupled =
  relation.WFREC
    (select R'.
       wellFounded R' R d rs L c. R' (c, L, rs) (c, L, (d, R) :: rs))
    (λdark_shadow_row_tupled a.
       pair.pair_CASE a
         (λc v1.
            pair.pair_CASE v1
              (λL v3.
                 list.list_CASE v3 (id )
                   (λv4 rs.
                      pair.pair_CASE v4
                        (λd R.
                           id
                             (integer.int_ge
                                (integer.int_sub
                                   (integer.int_mul (integer.int_of_num d)
                                      L)
                                   (integer.int_mul (integer.int_of_num c)
                                      R))
                                (integer.int_mul
                                   (integer.int_sub (integer.int_of_num c)
                                      (integer.int_of_num 1))
                                   (integer.int_sub (integer.int_of_num d)
                                      (integer.int_of_num 1)))
                              dark_shadow_row_tupled (c, L, rs)))))))

(c L. Omega.dark_shadow_cond_row (c, L) [] )
  t d c R L.
    Omega.dark_shadow_cond_row (c, L) ((d, R) :: t)
    ¬(i.
         integer.int_lt
           (integer.int_mul
              (integer.int_mul (integer.int_of_num c)
                 (integer.int_of_num d)) i)
           (integer.int_mul (integer.int_of_num c) R)
         integer.int_le (integer.int_mul (integer.int_of_num c) R)
           (integer.int_mul (integer.int_of_num d) L)
         integer.int_lt (integer.int_mul (integer.int_of_num d) L)
           (integer.int_mul
              (integer.int_mul (integer.int_of_num c)
                 (integer.int_of_num d))
              (integer.int_add i (integer.int_of_num 1))))
    Omega.dark_shadow_cond_row (c, L) t

m a x b d p q.
    d = gcd.gcd a m
    integer.int_of_num d =
    integer.int_add (integer.int_mul p (integer.int_of_num a))
      (integer.int_mul q (integer.int_of_num m)) ¬(d = 0) ¬(m = 0)
    ¬(a = 0)
    (integer.int_divides (integer.int_of_num m)
       (integer.int_add (integer.int_mul (integer.int_of_num a) x) b)
     integer.int_divides (integer.int_of_num d) b
     t.
       x =
       integer.int_add
         (integer.int_mul (integer.int_neg p)
            (integer.int_div b (integer.int_of_num d)))
         (integer.int_mul t
            (integer.int_div (integer.int_of_num m)
               (integer.int_of_num d))))

integer_word.fromString
    (string.CHR
       (arithmetic.BIT2
          (arithmetic.BIT2
             (arithmetic.BIT2
                (arithmetic.BIT2
                   (arithmetic.BIT2 (arithmetic.BIT2 0)))))) :: t) =
  integer.int_neg
    (integer.int_of_num (ASCIInumbers.num_from_dec_string t))
  integer_word.fromString
    (string.CHR
       (bit1 (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 1)))) ::
     t) =
  integer.int_neg
    (integer.int_of_num (ASCIInumbers.num_from_dec_string t))
  integer_word.fromString [] =
  integer.int_of_num (ASCIInumbers.num_from_dec_string [])
  integer_word.fromString (v4 :: v1) =
  if v4 =
     string.CHR
       (arithmetic.BIT2
          (arithmetic.BIT2
             (arithmetic.BIT2
                (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 0))))))
  then
    integer.int_neg
      (integer.int_of_num (ASCIInumbers.num_from_dec_string v1))
  else if v4 =
          string.CHR
            (bit1 (arithmetic.BIT2 (arithmetic.BIT2 (arithmetic.BIT2 1))))
  then
    integer.int_neg
      (integer.int_of_num (ASCIInumbers.num_from_dec_string v1))
  else integer.int_of_num (ASCIInumbers.num_from_dec_string (v4 :: v1))

(p q.
     ¬(q = 0)
     integer.int_rem (integer.int_of_num p) (integer.int_of_num q) =
     integer.int_of_num (p mod q))
  (p q.
     ¬(q = integer.int_of_num 0)
     integer.int_rem (integer.int_neg p) q =
     integer.int_neg (integer.int_rem p q)
     integer.int_rem p (integer.int_neg q) = integer.int_rem p q)
  (x. integer.int_neg (integer.int_neg x) = x)
  (m n. integer.int_of_num m = integer.int_of_num n m = n)
  x. integer.int_neg x = integer.int_of_num 0 x = integer.int_of_num 0

(p q.
     ¬(q = 0)
     integer.int_quot (integer.int_of_num p) (integer.int_of_num q) =
     integer.int_of_num (p div q))
  (p q.
     ¬(q = integer.int_of_num 0)
     integer.int_quot (integer.int_neg p) q =
     integer.int_neg (integer.int_quot p q)
     integer.int_quot p (integer.int_neg q) =
     integer.int_neg (integer.int_quot p q))
  (m n. integer.int_of_num m = integer.int_of_num n m = n)
  (x.
     integer.int_neg x = integer.int_of_num 0 x = integer.int_of_num 0)
  x. integer.int_neg (integer.int_neg x) = x

(f1 f2.
     DeepSyntax.neginf (DeepSyntax.Conjn f1 f2) =
     DeepSyntax.Conjn (DeepSyntax.neginf f1) (DeepSyntax.neginf f2))
  (f1 f2.
     DeepSyntax.neginf (DeepSyntax.Disjn f1 f2) =
     DeepSyntax.Disjn (DeepSyntax.neginf f1) (DeepSyntax.neginf f2))
  (f.
     DeepSyntax.neginf (DeepSyntax.Negn f) =
     DeepSyntax.Negn (DeepSyntax.neginf f))
  (b.
     DeepSyntax.neginf (DeepSyntax.UnrelatedBool b) =
     DeepSyntax.UnrelatedBool b)
  (i. DeepSyntax.neginf (DeepSyntax.xLT i) = DeepSyntax.UnrelatedBool )
  (i. DeepSyntax.neginf (DeepSyntax.LTx i) = DeepSyntax.UnrelatedBool )
  (i. DeepSyntax.neginf (DeepSyntax.xEQ i) = DeepSyntax.UnrelatedBool )
  i1 i2.
    DeepSyntax.neginf (DeepSyntax.xDivided i1 i2) =
    DeepSyntax.xDivided i1 i2

(f1 f2.
     DeepSyntax.posinf (DeepSyntax.Conjn f1 f2) =
     DeepSyntax.Conjn (DeepSyntax.posinf f1) (DeepSyntax.posinf f2))
  (f1 f2.
     DeepSyntax.posinf (DeepSyntax.Disjn f1 f2) =
     DeepSyntax.Disjn (DeepSyntax.posinf f1) (DeepSyntax.posinf f2))
  (f.
     DeepSyntax.posinf (DeepSyntax.Negn f) =
     DeepSyntax.Negn (DeepSyntax.posinf f))
  (b.
     DeepSyntax.posinf (DeepSyntax.UnrelatedBool b) =
     DeepSyntax.UnrelatedBool b)
  (i. DeepSyntax.posinf (DeepSyntax.xLT i) = DeepSyntax.UnrelatedBool )
  (i. DeepSyntax.posinf (DeepSyntax.LTx i) = DeepSyntax.UnrelatedBool )
  (i. DeepSyntax.posinf (DeepSyntax.xEQ i) = DeepSyntax.UnrelatedBool )
  i1 i2.
    DeepSyntax.posinf (DeepSyntax.xDivided i1 i2) =
    DeepSyntax.xDivided i1 i2

(x uppers lowers c. Omega.nightmare x c uppers lowers [] )
  x uppers rs lowers d c R.
    Omega.nightmare x c uppers lowers ((d, R) :: rs)
    (i.
       (integer.int_le (integer.int_of_num 0) i
        integer.int_le i
          (integer.int_div
             (integer.int_sub
                (integer.int_sub
                   (integer.int_mul (integer.int_of_num c)
                      (integer.int_of_num d)) (integer.int_of_num c))
                (integer.int_of_num d)) (integer.int_of_num c)))
       integer.int_mul (integer.int_of_num d) x = integer.int_add R i
       Omega.evalupper x uppers Omega.evallower x lowers)
    Omega.nightmare x c uppers lowers rs

m n.
    integer.int_mod (integer.int_of_num 0) (integer.int_of_num (bit1 n)) =
    integer.int_of_num 0
    integer.int_mod (integer.int_of_num 0)
      (integer.int_of_num (arithmetic.BIT2 n)) = integer.int_of_num 0
    integer.int_mod (integer.int_of_num m) (integer.int_of_num (bit1 n)) =
    integer.int_of_num (m mod bit1 n)
    integer.int_mod (integer.int_of_num m)
      (integer.int_of_num (arithmetic.BIT2 n)) =
    integer.int_of_num (m mod arithmetic.BIT2 n)
    integer.int_mod x (integer.int_of_num (bit1 n)) =
    integer.int_sub x
      (integer.int_mul (integer.int_div x (integer.int_of_num (bit1 n)))
         (integer.int_of_num (bit1 n)))
    integer.int_mod x (integer.int_of_num (arithmetic.BIT2 n)) =
    integer.int_sub x
      (integer.int_mul
         (integer.int_div x (integer.int_of_num (arithmetic.BIT2 n)))
         (integer.int_of_num (arithmetic.BIT2 n)))

p n m.
    integer.int_add (integer.int_of_num 0) p = p
    integer.int_add p (integer.int_of_num 0) = p
    integer.int_add (integer.int_of_num n) (integer.int_of_num m) =
    integer.int_of_num (n + m)
    integer.int_add (integer.int_of_num n)
      (integer.int_neg (integer.int_of_num m)) =
    (if m n then integer.int_of_num (arithmetic.- n m)
     else integer.int_neg (integer.int_of_num (arithmetic.- m n)))
    integer.int_add (integer.int_neg (integer.int_of_num n))
      (integer.int_of_num m) =
    (if n m then integer.int_of_num (arithmetic.- m n)
     else integer.int_neg (integer.int_of_num (arithmetic.- n m)))
    integer.int_add (integer.int_neg (integer.int_of_num n))
      (integer.int_neg (integer.int_of_num m)) =
    integer.int_neg (integer.int_of_num (n + m))

Omega.calc_nightmare_tupled =
  relation.WFREC
    (select R'.
       wellFounded R' R d rs c x. R' (x, c, rs) (x, c, (d, R) :: rs))
    (λcalc_nightmare_tupled a.
       pair.pair_CASE a
         (λx v1.
            pair.pair_CASE v1
              (λc v3.
                 list.list_CASE v3 (id )
                   (λv4 rs.
                      pair.pair_CASE v4
                        (λd R.
                           id
                             ((i.
                                 (integer.int_le (integer.int_of_num 0) i
                                  integer.int_le i
                                    (integer.int_div
                                       (integer.int_sub
                                          (integer.int_sub
                                             (integer.int_mul
                                                (integer.int_of_num c)
                                                (integer.int_of_num d))
                                             (integer.int_of_num c))
                                          (integer.int_of_num d))
                                       (integer.int_of_num c)))
                                 integer.int_mul (integer.int_of_num d) x =
                                 integer.int_add R i)
                              calc_nightmare_tupled (x, c, rs)))))))

P.
    (pad f. P pad f [] [])
    (pad f y ys. P pad f [] ys P pad f [] (y :: ys))
    (pad f x xs. P pad f xs [] P pad f (x :: xs) [])
    (pad f x xs y ys. P pad f xs ys P pad f (x :: xs) (y :: ys))
    v v1 v2 v3. P v v1 v2 v3

(pad f. Omega.MAP2 pad f [] [] = [])
  (ys y pad f.
     Omega.MAP2 pad f [] (y :: ys) = f pad y :: Omega.MAP2 pad f [] ys)
  (xs x pad f.
     Omega.MAP2 pad f (x :: xs) [] = f x pad :: Omega.MAP2 pad f xs [])
  ys y xs x pad f.
    Omega.MAP2 pad f (x :: xs) (y :: ys) = f x y :: Omega.MAP2 pad f xs ys

i j.
    ¬(j = integer.int_of_num 0)
    integer.int_div i j =
    if integer.int_lt (integer.int_of_num 0) j then
      if integer.int_le (integer.int_of_num 0) i then
        integer.int_of_num (integer.Num i div integer.Num j)
      else
        integer.int_add
          (integer.int_neg
             (integer.int_of_num
                (integer.Num (integer.int_neg i) div integer.Num j)))
          (if integer.Num (integer.int_neg i) mod integer.Num j = 0 then
             integer.int_of_num 0
           else integer.int_neg (integer.int_of_num 1))
    else if integer.int_le (integer.int_of_num 0) i then
      integer.int_add
        (integer.int_neg
           (integer.int_of_num
              (integer.Num i div integer.Num (integer.int_neg j))))
        (if integer.Num i mod integer.Num (integer.int_neg j) = 0 then
           integer.int_of_num 0
         else integer.int_neg (integer.int_of_num 1))
    else
      integer.int_of_num
        (integer.Num (integer.int_neg i) div
         integer.Num (integer.int_neg j))

(a0 a1.
     DeepSyntax.deep_form_size (DeepSyntax.Conjn a0 a1) =
     1 + (DeepSyntax.deep_form_size a0 + DeepSyntax.deep_form_size a1))
  (a0 a1.
     DeepSyntax.deep_form_size (DeepSyntax.Disjn a0 a1) =
     1 + (DeepSyntax.deep_form_size a0 + DeepSyntax.deep_form_size a1))
  (a.
     DeepSyntax.deep_form_size (DeepSyntax.Negn a) =
     1 + DeepSyntax.deep_form_size a)
  (a.
     DeepSyntax.deep_form_size (DeepSyntax.UnrelatedBool a) =
     1 + basicSize.bool_size a)
  (a. DeepSyntax.deep_form_size (DeepSyntax.xLT a) = 1)
  (a. DeepSyntax.deep_form_size (DeepSyntax.LTx a) = 1)
  (a. DeepSyntax.deep_form_size (DeepSyntax.xEQ a) = 1)
  a0 a1. DeepSyntax.deep_form_size (DeepSyntax.xDivided a0 a1) = 1

Omega.dark_shadow_cond_row_tupled =
  relation.WFREC
    (select R.
       wellFounded R
       lowery lowerc rs uppery upperc.
         R ((upperc, uppery), rs)
           ((upperc, uppery), (lowerc, lowery) :: rs))
    (λdark_shadow_cond_row_tupled a.
       pair.pair_CASE a
         (λv v1.
            list.list_CASE v1 (id )
              (λv2 t.
                 pair.pair_CASE v2
                   (λd R.
                      pair.pair_CASE v
                        (λc L.
                           id
                             (¬(i.
                                   integer.int_lt
                                     (integer.int_mul
                                        (integer.int_mul
                                           (integer.int_of_num c)
                                           (integer.int_of_num d)) i)
                                     (integer.int_mul
                                        (integer.int_of_num c) R)
                                   integer.int_le
                                     (integer.int_mul
                                        (integer.int_of_num c) R)
                                     (integer.int_mul
                                        (integer.int_of_num d) L)
                                   integer.int_lt
                                     (integer.int_mul
                                        (integer.int_of_num d) L)
                                     (integer.int_mul
                                        (integer.int_mul
                                           (integer.int_of_num c)
                                           (integer.int_of_num d))
                                        (integer.int_add i
                                           (integer.int_of_num 1))))
                              dark_shadow_cond_row_tupled ((c, L), t)))))))

p n m.
    integer.int_add (integer.int_of_num 0) p = p
    integer.int_add p (integer.int_of_num 0) = p
    integer.int_neg (integer.int_of_num 0) = integer.int_of_num 0
    integer.int_neg (integer.int_neg p) = p
    integer.int_add (integer.int_of_num n) (integer.int_of_num m) =
    integer.int_of_num (numeral.iZ (n + m))
    integer.int_add (integer.int_of_num n)
      (integer.int_neg (integer.int_of_num m)) =
    (if m n then integer.int_of_num (arithmetic.- n m)
     else integer.int_neg (integer.int_of_num (arithmetic.- m n)))
    integer.int_add (integer.int_neg (integer.int_of_num n))
      (integer.int_of_num m) =
    (if n m then integer.int_of_num (arithmetic.- m n)
     else integer.int_neg (integer.int_of_num (arithmetic.- n m)))
    integer.int_add (integer.int_neg (integer.int_of_num n))
      (integer.int_neg (integer.int_of_num m)) =
    integer.int_neg (integer.int_of_num (numeral.iZ (n + m)))

f0 f1 f2 f3 f4 f5 f6 f7.
    fn.
      (a0 a1. fn (DeepSyntax.Conjn a0 a1) = f0 a0 a1 (fn a0) (fn a1))
      (a0 a1. fn (DeepSyntax.Disjn a0 a1) = f1 a0 a1 (fn a0) (fn a1))
      (a. fn (DeepSyntax.Negn a) = f2 a (fn a))
      (a. fn (DeepSyntax.UnrelatedBool a) = f3 a)
      (a. fn (DeepSyntax.xLT a) = f4 a)
      (a. fn (DeepSyntax.LTx a) = f5 a)
      (a. fn (DeepSyntax.xEQ a) = f6 a)
      a0 a1. fn (DeepSyntax.xDivided a0 a1) = f7 a0 a1

(f1 f2 d.
     DeepSyntax.alldivide (DeepSyntax.Conjn f1 f2) d
     DeepSyntax.alldivide f1 d DeepSyntax.alldivide f2 d)
  (f1 f2 d.
     DeepSyntax.alldivide (DeepSyntax.Disjn f1 f2) d
     DeepSyntax.alldivide f1 d DeepSyntax.alldivide f2 d)
  (f d.
     DeepSyntax.alldivide (DeepSyntax.Negn f) d
     DeepSyntax.alldivide f d)
  (b d. DeepSyntax.alldivide (DeepSyntax.UnrelatedBool b) d )
  (i d. DeepSyntax.alldivide (DeepSyntax.xLT i) d )
  (i d. DeepSyntax.alldivide (DeepSyntax.LTx i) d )
  (i d. DeepSyntax.alldivide (DeepSyntax.xEQ i) d )
  i1 i2 d.
    DeepSyntax.alldivide (DeepSyntax.xDivided i1 i2) d
    integer.int_divides i1 d

(f1 f2 x.
     DeepSyntax.eval_form (DeepSyntax.Conjn f1 f2) x
     DeepSyntax.eval_form f1 x DeepSyntax.eval_form f2 x)
  (f1 f2 x.
     DeepSyntax.eval_form (DeepSyntax.Disjn f1 f2) x
     DeepSyntax.eval_form f1 x DeepSyntax.eval_form f2 x)
  (f x.
     DeepSyntax.eval_form (DeepSyntax.Negn f) x
     ¬DeepSyntax.eval_form f x)
  (b x. DeepSyntax.eval_form (DeepSyntax.UnrelatedBool b) x b)
  (i x. DeepSyntax.eval_form (DeepSyntax.xLT i) x integer.int_lt x i)
  (i x. DeepSyntax.eval_form (DeepSyntax.LTx i) x integer.int_lt i x)
  (i x. DeepSyntax.eval_form (DeepSyntax.xEQ i) x x = i)
  i1 i2 x.
    DeepSyntax.eval_form (DeepSyntax.xDivided i1 i2) x
    integer.int_divides i1 (integer.int_add x i2)

Omega.nightmare_tupled =
  relation.WFREC
    (select R'.
       wellFounded R'
       R d rs lowers uppers c x.
         R' (x, c, uppers, lowers, rs)
           (x, c, uppers, lowers, (d, R) :: rs))
    (λnightmare_tupled a.
       pair.pair_CASE a
         (λx v1.
            pair.pair_CASE v1
              (λc v3.
                 pair.pair_CASE v3
                   (λuppers v5.
                      pair.pair_CASE v5
                        (λlowers v7.
                           list.list_CASE v7 (id )
                             (λv8 rs.
                                pair.pair_CASE v8
                                  (λd R.
                                     id
                                       ((i.
                                           (integer.int_le
                                              (integer.int_of_num 0) i
                                            integer.int_le i
                                              (integer.int_div
                                                 (integer.int_sub
                                                    (integer.int_sub
                                                       (integer.int_mul
                                                          (integer.int_of_num
                                                             c)
                                                          (integer.int_of_num
                                                             d))
                                                       (integer.int_of_num
                                                          c))
                                                    (integer.int_of_num d))
                                                 (integer.int_of_num c)))
                                           integer.int_mul
                                             (integer.int_of_num d) x =
                                           integer.int_add R i
                                           Omega.evalupper x uppers
                                           Omega.evallower x lowers)
                                        nightmare_tupled
                                          (x, c, uppers, lowers,
                                           rs)))))))))

n m.
    (integer.int_lt (integer.int_of_num 0) (integer.int_of_num (bit1 n))
     )
    (integer.int_lt (integer.int_of_num 0)
       (integer.int_of_num (arithmetic.BIT2 n)) )
    (integer.int_lt (integer.int_of_num 0) (integer.int_of_num 0) )
    (integer.int_lt (integer.int_of_num 0)
       (integer.int_neg (integer.int_of_num n)) )
    (integer.int_lt (integer.int_of_num n) (integer.int_of_num 0) )
    (integer.int_lt (integer.int_neg (integer.int_of_num (bit1 n)))
       (integer.int_of_num 0) )
    (integer.int_lt
       (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)))
       (integer.int_of_num 0) )
    (integer.int_lt (integer.int_of_num n) (integer.int_of_num m)
     n < m)
    (integer.int_lt (integer.int_neg (integer.int_of_num (bit1 n)))
       (integer.int_of_num m) )
    (integer.int_lt
       (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)))
       (integer.int_of_num m) )
    (integer.int_lt (integer.int_of_num n)
       (integer.int_neg (integer.int_of_num m)) )
    (integer.int_lt (integer.int_neg (integer.int_of_num n))
       (integer.int_neg (integer.int_of_num m)) m < n)

n m.
    (integer.int_gt (integer.int_of_num (bit1 n)) (integer.int_of_num 0)
     )
    (integer.int_gt (integer.int_of_num (arithmetic.BIT2 n))
       (integer.int_of_num 0) )
    (integer.int_gt (integer.int_of_num 0) (integer.int_of_num 0) )
    (integer.int_gt (integer.int_neg (integer.int_of_num n))
       (integer.int_of_num 0) )
    (integer.int_gt (integer.int_of_num 0) (integer.int_of_num n) )
    (integer.int_gt (integer.int_of_num 0)
       (integer.int_neg (integer.int_of_num (bit1 n))) )
    (integer.int_gt (integer.int_of_num 0)
       (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n))) )
    (integer.int_gt (integer.int_of_num m) (integer.int_of_num n)
     n < m)
    (integer.int_gt (integer.int_of_num m)
       (integer.int_neg (integer.int_of_num (bit1 n))) )
    (integer.int_gt (integer.int_of_num m)
       (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n))) )
    (integer.int_gt (integer.int_neg (integer.int_of_num m))
       (integer.int_of_num n) )
    (integer.int_gt (integer.int_neg (integer.int_of_num m))
       (integer.int_neg (integer.int_of_num n)) m < n)

P.
    (f r1 r2. P f ([], r1) ([], r2))
    (f r1 b2 bs2 r2.
       P f ([], r1) (bs2, r2) P f ([], r1) (b2 :: bs2, r2))
    (f b1 bs1 r1 r2.
       P f (bs1, r1) ([], r2) P f (b1 :: bs1, r1) ([], r2))
    (f b1 bs1 r1 b2 bs2 r2.
       P f (bs1, r1) (bs2, r2) P f (b1 :: bs1, r1) (b2 :: bs2, r2))
    v v1 v2 v3 v4. P v (v1, v2) (v3, v4)

m n a b u v p q x d.
    d = gcd.gcd (u * m) (a * n)
    integer.int_of_num d =
    integer.int_add
      (integer.int_mul (integer.int_mul p (integer.int_of_num u))
         (integer.int_of_num m))
      (integer.int_mul (integer.int_mul q (integer.int_of_num a))
         (integer.int_of_num n)) ¬(m = 0) ¬(n = 0) ¬(a = 0)
    ¬(u = 0)
    (integer.int_divides (integer.int_of_num m)
       (integer.int_add (integer.int_mul (integer.int_of_num a) x) b)
     integer.int_divides (integer.int_of_num n)
       (integer.int_add (integer.int_mul (integer.int_of_num u) x) v)
     integer.int_divides
       (integer.int_mul (integer.int_of_num m) (integer.int_of_num n))
       (integer.int_add
          (integer.int_add (integer.int_mul (integer.int_of_num d) x)
             (integer.int_mul (integer.int_mul v (integer.int_of_num m))
                p))
          (integer.int_mul (integer.int_mul b (integer.int_of_num n)) q))
     integer.int_divides (integer.int_of_num d)
       (integer.int_sub (integer.int_mul (integer.int_of_num a) v)
          (integer.int_mul (integer.int_of_num u) b)))

(pos f1 f2.
     DeepSyntax.Aset pos (DeepSyntax.Conjn f1 f2) =
     pred_set.UNION (DeepSyntax.Aset pos f1) (DeepSyntax.Aset pos f2))
  (pos f1 f2.
     DeepSyntax.Aset pos (DeepSyntax.Disjn f1 f2) =
     pred_set.UNION (DeepSyntax.Aset pos f1) (DeepSyntax.Aset pos f2))
  (pos f.
     DeepSyntax.Aset pos (DeepSyntax.Negn f) = DeepSyntax.Aset (¬pos) f)
  (pos b.
     DeepSyntax.Aset pos (DeepSyntax.UnrelatedBool b) = pred_set.EMPTY)
  (pos i.
     DeepSyntax.Aset pos (DeepSyntax.xLT i) =
     if pos then pred_set.INSERT i pred_set.EMPTY else pred_set.EMPTY)
  (pos i.
     DeepSyntax.Aset pos (DeepSyntax.LTx i) =
     if pos then pred_set.EMPTY
     else
       pred_set.INSERT (integer.int_add i (integer.int_of_num 1))
         pred_set.EMPTY)
  (pos i.
     DeepSyntax.Aset pos (DeepSyntax.xEQ i) =
     if pos then
       pred_set.INSERT (integer.int_add i (integer.int_of_num 1))
         pred_set.EMPTY
     else pred_set.INSERT i pred_set.EMPTY)
  pos i1 i2.
    DeepSyntax.Aset pos (DeepSyntax.xDivided i1 i2) = pred_set.EMPTY

n m.
    (integer.int_ge (integer.int_of_num 0) (integer.int_of_num 0) )
    (integer.int_ge (integer.int_of_num n) (integer.int_of_num 0) )
    (integer.int_ge (integer.int_neg (integer.int_of_num (bit1 n)))
       (integer.int_of_num 0) )
    (integer.int_ge
       (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)))
       (integer.int_of_num 0) )
    (integer.int_ge (integer.int_of_num 0) (integer.int_of_num (bit1 n))
     )
    (integer.int_ge (integer.int_of_num 0)
       (integer.int_of_num (arithmetic.BIT2 n)) )
    (integer.int_ge (integer.int_of_num 0)
       (integer.int_neg (integer.int_of_num (bit1 n))) )
    (integer.int_ge (integer.int_of_num 0)
       (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n))) )
    (integer.int_ge (integer.int_of_num m) (integer.int_of_num n)
     n m)
    (integer.int_ge (integer.int_neg (integer.int_of_num (bit1 m)))
       (integer.int_of_num n) )
    (integer.int_ge
       (integer.int_neg (integer.int_of_num (arithmetic.BIT2 m)))
       (integer.int_of_num n) )
    (integer.int_ge (integer.int_of_num m)
       (integer.int_neg (integer.int_of_num n)) )
    (integer.int_ge (integer.int_neg (integer.int_of_num m))
       (integer.int_neg (integer.int_of_num n)) m n)

n m.
    (integer.int_le (integer.int_of_num 0) (integer.int_of_num 0) )
    (integer.int_le (integer.int_of_num 0) (integer.int_of_num n) )
    (integer.int_le (integer.int_of_num 0)
       (integer.int_neg (integer.int_of_num (bit1 n))) )
    (integer.int_le (integer.int_of_num 0)
       (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n))) )
    (integer.int_le (integer.int_of_num (bit1 n)) (integer.int_of_num 0)
     )
    (integer.int_le (integer.int_of_num (arithmetic.BIT2 n))
       (integer.int_of_num 0) )
    (integer.int_le (integer.int_neg (integer.int_of_num (bit1 n)))
       (integer.int_of_num 0) )
    (integer.int_le
       (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)))
       (integer.int_of_num 0) )
    (integer.int_le (integer.int_of_num n) (integer.int_of_num m)
     n m)
    (integer.int_le (integer.int_of_num n)
       (integer.int_neg (integer.int_of_num (bit1 m))) )
    (integer.int_le (integer.int_of_num n)
       (integer.int_neg (integer.int_of_num (arithmetic.BIT2 m))) )
    (integer.int_le (integer.int_neg (integer.int_of_num n))
       (integer.int_of_num m) )
    (integer.int_le (integer.int_neg (integer.int_of_num n))
       (integer.int_neg (integer.int_of_num m)) m n)

(pos f1 f2.
     DeepSyntax.Bset pos (DeepSyntax.Conjn f1 f2) =
     pred_set.UNION (DeepSyntax.Bset pos f1) (DeepSyntax.Bset pos f2))
  (pos f1 f2.
     DeepSyntax.Bset pos (DeepSyntax.Disjn f1 f2) =
     pred_set.UNION (DeepSyntax.Bset pos f1) (DeepSyntax.Bset pos f2))
  (pos f.
     DeepSyntax.Bset pos (DeepSyntax.Negn f) = DeepSyntax.Bset (¬pos) f)
  (pos b.
     DeepSyntax.Bset pos (DeepSyntax.UnrelatedBool b) = pred_set.EMPTY)
  (pos i.
     DeepSyntax.Bset pos (DeepSyntax.xLT i) =
     if pos then pred_set.EMPTY
     else
       pred_set.INSERT
         (integer.int_add i (integer.int_neg (integer.int_of_num 1)))
         pred_set.EMPTY)
  (pos i.
     DeepSyntax.Bset pos (DeepSyntax.LTx i) =
     if pos then pred_set.INSERT i pred_set.EMPTY else pred_set.EMPTY)
  (pos i.
     DeepSyntax.Bset pos (DeepSyntax.xEQ i) =
     if pos then
       pred_set.INSERT
         (integer.int_add i (integer.int_neg (integer.int_of_num 1)))
         pred_set.EMPTY
     else pred_set.INSERT i pred_set.EMPTY)
  pos i1 i2.
    DeepSyntax.Bset pos (DeepSyntax.xDivided i1 i2) = pred_set.EMPTY

(a0 a1 a0' a1'.
     DeepSyntax.Conjn a0 a1 = DeepSyntax.Conjn a0' a1'
     a0 = a0' a1 = a1')
  (a0 a1 a0' a1'.
     DeepSyntax.Disjn a0 a1 = DeepSyntax.Disjn a0' a1'
     a0 = a0' a1 = a1')
  (a a'. DeepSyntax.Negn a = DeepSyntax.Negn a' a = a')
  (a a'.
     DeepSyntax.UnrelatedBool a = DeepSyntax.UnrelatedBool a' a a')
  (a a'. DeepSyntax.xLT a = DeepSyntax.xLT a' a = a')
  (a a'. DeepSyntax.LTx a = DeepSyntax.LTx a' a = a')
  (a a'. DeepSyntax.xEQ a = DeepSyntax.xEQ a' a = a')
  a0 a1 a0' a1'.
    DeepSyntax.xDivided a0 a1 = DeepSyntax.xDivided a0' a1'
    a0 = a0' a1 = a1'

(r2 r1 f.
     int_bitwise.bits_bitwise f ([], r1) ([], r2) = ([], f r1 r2))
  (r2 r1 f bs2 b2.
     int_bitwise.bits_bitwise f ([], r1) (b2 :: bs2, r2) =
     bool.LET (pair.UNCURRY (λbs r. (f r1 b2 :: bs, r)))
       (int_bitwise.bits_bitwise f ([], r1) (bs2, r2)))
  (r2 r1 f bs1 b1.
     int_bitwise.bits_bitwise f (b1 :: bs1, r1) ([], r2) =
     bool.LET (pair.UNCURRY (λbs r. (f b1 r2 :: bs, r)))
       (int_bitwise.bits_bitwise f (bs1, r1) ([], r2)))
  r2 r1 f bs2 bs1 b2 b1.
    int_bitwise.bits_bitwise f (b1 :: bs1, r1) (b2 :: bs2, r2) =
    bool.LET (pair.UNCURRY (λbs r. (f b1 b2 :: bs, r)))
      (int_bitwise.bits_bitwise f (bs1, r1) (bs2, r2))

m n.
    integer.int_quot (integer.int_of_num 0) (integer.int_of_num (bit1 n)) =
    integer.int_of_num 0
    integer.int_quot (integer.int_of_num 0)
      (integer.int_of_num (arithmetic.BIT2 n)) = integer.int_of_num 0
    integer.int_quot (integer.int_of_num m) (integer.int_of_num (bit1 n)) =
    integer.int_of_num (m div bit1 n)
    integer.int_quot (integer.int_of_num m)
      (integer.int_of_num (arithmetic.BIT2 n)) =
    integer.int_of_num (m div arithmetic.BIT2 n)
    integer.int_quot (integer.int_neg (integer.int_of_num m))
      (integer.int_of_num (bit1 n)) =
    integer.int_neg (integer.int_of_num (m div bit1 n))
    integer.int_quot (integer.int_neg (integer.int_of_num m))
      (integer.int_of_num (arithmetic.BIT2 n)) =
    integer.int_neg (integer.int_of_num (m div arithmetic.BIT2 n))
    integer.int_quot (integer.int_of_num m)
      (integer.int_neg (integer.int_of_num (bit1 n))) =
    integer.int_neg (integer.int_of_num (m div bit1 n))
    integer.int_quot (integer.int_of_num m)
      (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n))) =
    integer.int_neg (integer.int_of_num (m div arithmetic.BIT2 n))
    integer.int_quot (integer.int_neg (integer.int_of_num m))
      (integer.int_neg (integer.int_of_num (bit1 n))) =
    integer.int_of_num (m div bit1 n)
    integer.int_quot (integer.int_neg (integer.int_of_num m))
      (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n))) =
    integer.int_of_num (m div arithmetic.BIT2 n)

m n.
    integer.int_rem (integer.int_of_num 0) (integer.int_of_num (bit1 n)) =
    integer.int_of_num 0
    integer.int_rem (integer.int_of_num 0)
      (integer.int_of_num (arithmetic.BIT2 n)) = integer.int_of_num 0
    integer.int_rem (integer.int_of_num m) (integer.int_of_num (bit1 n)) =
    integer.int_of_num (m mod bit1 n)
    integer.int_rem (integer.int_of_num m)
      (integer.int_of_num (arithmetic.BIT2 n)) =
    integer.int_of_num (m mod arithmetic.BIT2 n)
    integer.int_rem (integer.int_neg (integer.int_of_num m))
      (integer.int_of_num (bit1 n)) =
    integer.int_neg (integer.int_of_num (m mod bit1 n))
    integer.int_rem (integer.int_neg (integer.int_of_num m))
      (integer.int_of_num (arithmetic.BIT2 n)) =
    integer.int_neg (integer.int_of_num (m mod arithmetic.BIT2 n))
    integer.int_rem (integer.int_of_num m)
      (integer.int_neg (integer.int_of_num (bit1 n))) =
    integer.int_of_num (m mod bit1 n)
    integer.int_rem (integer.int_of_num m)
      (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n))) =
    integer.int_of_num (m mod arithmetic.BIT2 n)
    integer.int_rem (integer.int_neg (integer.int_of_num m))
      (integer.int_neg (integer.int_of_num (bit1 n))) =
    integer.int_neg (integer.int_of_num (m mod bit1 n))
    integer.int_rem (integer.int_neg (integer.int_of_num m))
      (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n))) =
    integer.int_neg (integer.int_of_num (m mod arithmetic.BIT2 n))

Omega.MAP2_tupled =
  relation.WFREC
    (select R.
       wellFounded R
       (y ys f pad. R (pad, f, [], ys) (pad, f, [], y :: ys))
       (x xs f pad. R (pad, f, xs, []) (pad, f, x :: xs, []))
       y x ys xs f pad. R (pad, f, xs, ys) (pad, f, x :: xs, y :: ys))
    (λMAP2_tupled a.
       pair.pair_CASE a
         (λpad v1.
            pair.pair_CASE v1
              (λf v3.
                 pair.pair_CASE v3
                   (λv4 v5.
                      list.list_CASE v4
                        (list.list_CASE v5 (id [])
                           (λy ys.
                              id
                                (f pad y :: MAP2_tupled (pad, f, [], ys))))
                        (λx xs.
                           list.list_CASE v5
                             (id (f x pad :: MAP2_tupled (pad, f, xs, [])))
                             (λy' ys'.
                                id
                                  (f x y' ::
                                   MAP2_tupled (pad, f, xs, ys'))))))))

n m.
    (integer.int_of_num 0 = integer.int_of_num 0 )
    (integer.int_of_num 0 = integer.int_of_num (bit1 n) )
    (integer.int_of_num 0 = integer.int_of_num (arithmetic.BIT2 n) )
    (integer.int_of_num 0 = integer.int_neg (integer.int_of_num (bit1 n))
     )
    (integer.int_of_num 0 =
     integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)) )
    (integer.int_of_num (bit1 n) = integer.int_of_num 0 )
    (integer.int_of_num (arithmetic.BIT2 n) = integer.int_of_num 0 )
    (integer.int_neg (integer.int_of_num (bit1 n)) = integer.int_of_num 0
     )
    (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)) =
     integer.int_of_num 0 )
    (integer.int_of_num n = integer.int_of_num m n = m)
    (integer.int_of_num (bit1 n) = integer.int_neg (integer.int_of_num m)
     )
    (integer.int_of_num (arithmetic.BIT2 n) =
     integer.int_neg (integer.int_of_num m) )
    (integer.int_neg (integer.int_of_num (bit1 n)) = integer.int_of_num m
     )
    (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)) =
     integer.int_of_num m )
    (integer.int_neg (integer.int_of_num n) =
     integer.int_neg (integer.int_of_num m) n = m)

M M' f f1 f2 f3 f4 f5 f6 f7.
    M = M' (a0 a1. M' = DeepSyntax.Conjn a0 a1 f a0 a1 = f' a0 a1)
    (a0 a1. M' = DeepSyntax.Disjn a0 a1 f1 a0 a1 = f1' a0 a1)
    (a. M' = DeepSyntax.Negn a f2 a = f2' a)
    (a. M' = DeepSyntax.UnrelatedBool a f3 a = f3' a)
    (a. M' = DeepSyntax.xLT a f4 a = f4' a)
    (a. M' = DeepSyntax.LTx a f5 a = f5' a)
    (a. M' = DeepSyntax.xEQ a f6 a = f6' a)
    (a0 a1. M' = DeepSyntax.xDivided a0 a1 f7 a0 a1 = f7' a0 a1)
    DeepSyntax.deep_form_CASE M f f1 f2 f3 f4 f5 f6 f7 =
    DeepSyntax.deep_form_CASE M' f' f1' f2' f3' f4' f5' f6' f7'

n m p.
    (integer.int_divides (integer.int_of_num 0) (integer.int_of_num 0)
     )
    (integer.int_divides (integer.int_of_num 0)
       (integer.int_of_num (bit1 n)) )
    (integer.int_divides (integer.int_of_num 0)
       (integer.int_of_num (arithmetic.BIT2 n)) )
    (integer.int_divides p (integer.int_of_num 0) )
    (integer.int_divides (integer.int_of_num (bit1 n))
       (integer.int_of_num m) m mod bit1 n = 0)
    (integer.int_divides (integer.int_of_num (arithmetic.BIT2 n))
       (integer.int_of_num m) m mod arithmetic.BIT2 n = 0)
    (integer.int_divides (integer.int_of_num (bit1 n))
       (integer.int_neg (integer.int_of_num m)) m mod bit1 n = 0)
    (integer.int_divides (integer.int_of_num (arithmetic.BIT2 n))
       (integer.int_neg (integer.int_of_num m))
     m mod arithmetic.BIT2 n = 0)
    (integer.int_divides (integer.int_neg (integer.int_of_num (bit1 n)))
       (integer.int_of_num m) m mod bit1 n = 0)
    (integer.int_divides
       (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)))
       (integer.int_of_num m) m mod arithmetic.BIT2 n = 0)
    (integer.int_divides (integer.int_neg (integer.int_of_num (bit1 n)))
       (integer.int_neg (integer.int_of_num m)) m mod bit1 n = 0)
    (integer.int_divides
       (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n)))
       (integer.int_neg (integer.int_of_num m))
     m mod arithmetic.BIT2 n = 0)

integer.int_add (integer.int_of_num n) (integer.int_of_num m) =
  integer.int_of_num (n + m)
  integer.int_add (integer.int_neg (integer.int_of_num n))
    (integer.int_of_num m) =
  (if n m then integer.int_of_num (arithmetic.- m n)
   else integer.int_neg (integer.int_of_num (arithmetic.- n m)))
  integer.int_add (integer.int_of_num n)
    (integer.int_neg (integer.int_of_num m)) =
  (if m n then integer.int_of_num (arithmetic.- n m)
   else integer.int_neg (integer.int_of_num (arithmetic.- m n)))
  integer.int_add (integer.int_neg (integer.int_of_num n))
    (integer.int_neg (integer.int_of_num m)) =
  integer.int_neg (integer.int_of_num (n + m))
  integer.int_mul (integer.int_of_num n) (integer.int_of_num m) =
  integer.int_of_num (n * m)
  integer.int_mul (integer.int_neg (integer.int_of_num n))
    (integer.int_of_num m) = integer.int_neg (integer.int_of_num (n * m))
  integer.int_mul (integer.int_of_num n)
    (integer.int_neg (integer.int_of_num m)) =
  integer.int_neg (integer.int_of_num (n * m))
  integer.int_mul (integer.int_neg (integer.int_of_num n))
    (integer.int_neg (integer.int_of_num m)) = integer.int_of_num (n * m)
  (integer.int_of_num n = integer.int_of_num m n = m)
  (integer.int_of_num n = integer.int_neg (integer.int_of_num m)
   n = 0 m = 0)
  (integer.int_neg (integer.int_of_num n) = integer.int_of_num m
   n = 0 m = 0)
  (integer.int_neg (integer.int_of_num n) =
   integer.int_neg (integer.int_of_num m) n = m)
  integer.int_neg (integer.int_neg x) = x
  integer.int_neg (integer.int_of_num 0) = integer.int_of_num 0

rep.
    bool.TYPE_DEFINITION
      (λa0'.
         'deep_form'.
           (a0'.
              (a0 a1.
                 a0' =
                 (let a0 a0 in
                  λa1.
                    ind_type.CONSTR 0 (bool.ARB, bool.ARB, bool.ARB)
                      (ind_type.FCONS a0
                         (ind_type.FCONS a1 (λn. ind_type.BOTTOM)))) a1
                 'deep_form' a0 'deep_form' a1)
              (a0 a1.
                 a0' =
                 (let a0 a0 in
                  λa1.
                    ind_type.CONSTR (suc 0) (bool.ARB, bool.ARB, bool.ARB)
                      (ind_type.FCONS a0
                         (ind_type.FCONS a1 (λn. ind_type.BOTTOM)))) a1
                 'deep_form' a0 'deep_form' a1)
              (a.
                 a0' =
                 (let a a in
                  ind_type.CONSTR (suc (suc 0))
                    (bool.ARB, bool.ARB, bool.ARB)
                    (ind_type.FCONS a (λn. ind_type.BOTTOM)))
                 'deep_form' a)
              (a.
                 a0' =
                 let a a in
                 ind_type.CONSTR (suc (suc (suc 0)))
                   (a, bool.ARB, bool.ARB) (λn. ind_type.BOTTOM))
              (a.
                 a0' =
                 let a a in
                 ind_type.CONSTR (suc (suc (suc (suc 0))))
                   (bool.ARB, a, bool.ARB) (λn. ind_type.BOTTOM))
              (a.
                 a0' =
                 let a a in
                 ind_type.CONSTR (suc (suc (suc (suc (suc 0)))))
                   (bool.ARB, a, bool.ARB) (λn. ind_type.BOTTOM))
              (a.
                 a0' =
                 let a a in
                 ind_type.CONSTR (suc (suc (suc (suc (suc (suc 0))))))
                   (bool.ARB, a, bool.ARB) (λn. ind_type.BOTTOM))
              (a0 a1.
                 a0' =
                 (let a0 a0 in
                  λa1.
                    ind_type.CONSTR
                      (suc (suc (suc (suc (suc (suc (suc 0)))))))
                      (bool.ARB, a0, a1) (λn. ind_type.BOTTOM)) a1)
              'deep_form' a0') 'deep_form' a0') rep

int_bitwise.bits_bitwise_tupled =
  relation.WFREC
    (select R.
       wellFounded R
       (b2 r2 bs2 r1 f.
          R (f, ([], r1), bs2, r2) (f, ([], r1), b2 :: bs2, r2))
       (b1 r2 r1 bs1 f.
          R (f, (bs1, r1), [], r2) (f, (b1 :: bs1, r1), [], r2))
       b2 b1 r2 bs2 r1 bs1 f.
         R (f, (bs1, r1), bs2, r2) (f, (b1 :: bs1, r1), b2 :: bs2, r2))
    (λbits_bitwise_tupled a.
       pair.pair_CASE a
         (λf v1.
            pair.pair_CASE v1
              (λv2 v3.
                 pair.pair_CASE v2
                   (λv4 r1.
                      pair.pair_CASE v3
                        (λv6 r2.
                           list.list_CASE v6
                             (list.list_CASE v4 (id ([], f r1 r2))
                                (λb1 bs1.
                                   id
                                     (bool.LET
                                        (pair.UNCURRY
                                           (λbs r. (f b1 r2 :: bs, r)))
                                        (bits_bitwise_tupled
                                           (f, (bs1, r1), [], r2)))))
                             (λb2 bs2.
                                list.list_CASE v4
                                  (id
                                     (bool.LET
                                        (pair.UNCURRY
                                           (λbs r. (f r1 b2 :: bs, r)))
                                        (bits_bitwise_tupled
                                           (f, ([], r1), bs2, r2))))
                                  (λb1' bs1'.
                                     id
                                       (bool.LET
                                          (pair.UNCURRY
                                             (λbs r. (f b1' b2 :: bs, r)))
                                          (bits_bitwise_tupled
                                             (f, (bs1', r1), bs2,
                                              r2))))))))))

m n.
    integer.int_div (integer.int_of_num 0) (integer.int_of_num (bit1 n)) =
    integer.int_of_num 0
    integer.int_div (integer.int_of_num 0)
      (integer.int_of_num (arithmetic.BIT2 n)) = integer.int_of_num 0
    integer.int_div (integer.int_of_num m) (integer.int_of_num (bit1 n)) =
    integer.int_of_num (m div bit1 n)
    integer.int_div (integer.int_of_num m)
      (integer.int_of_num (arithmetic.BIT2 n)) =
    integer.int_of_num (m div arithmetic.BIT2 n)
    integer.int_div (integer.int_neg (integer.int_of_num m))
      (integer.int_of_num (bit1 n)) =
    integer.int_add (integer.int_neg (integer.int_of_num (m div bit1 n)))
      (if m mod bit1 n = 0 then integer.int_of_num 0
       else integer.int_neg (integer.int_of_num 1))
    integer.int_div (integer.int_neg (integer.int_of_num m))
      (integer.int_of_num (arithmetic.BIT2 n)) =
    integer.int_add
      (integer.int_neg (integer.int_of_num (m div arithmetic.BIT2 n)))
      (if m mod arithmetic.BIT2 n = 0 then integer.int_of_num 0
       else integer.int_neg (integer.int_of_num 1))
    integer.int_div (integer.int_of_num m)
      (integer.int_neg (integer.int_of_num (bit1 n))) =
    integer.int_add (integer.int_neg (integer.int_of_num (m div bit1 n)))
      (if m mod bit1 n = 0 then integer.int_of_num 0
       else integer.int_neg (integer.int_of_num 1))
    integer.int_div (integer.int_of_num m)
      (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n))) =
    integer.int_add
      (integer.int_neg (integer.int_of_num (m div arithmetic.BIT2 n)))
      (if m mod arithmetic.BIT2 n = 0 then integer.int_of_num 0
       else integer.int_neg (integer.int_of_num 1))
    integer.int_div (integer.int_neg (integer.int_of_num m))
      (integer.int_neg (integer.int_of_num (bit1 n))) =
    integer.int_of_num (m div bit1 n)
    integer.int_div (integer.int_neg (integer.int_of_num m))
      (integer.int_neg (integer.int_of_num (arithmetic.BIT2 n))) =
    integer.int_of_num (m div arithmetic.BIT2 n)

((a. bool.IN a (DeepSyntax.Aset pos (DeepSyntax.Conjn f1 f2)) P a)
   (a. bool.IN a (DeepSyntax.Aset pos f1) P a)
   a. bool.IN a (DeepSyntax.Aset pos f2) P a)
  ((a. bool.IN a (DeepSyntax.Aset pos (DeepSyntax.Disjn f1 f2)) P a)
   (a. bool.IN a (DeepSyntax.Aset pos f1) P a)
   a. bool.IN a (DeepSyntax.Aset pos f2) P a)
  ((a. bool.IN a (DeepSyntax.Aset (DeepSyntax.Negn f)) P a)
   a. bool.IN a (DeepSyntax.Aset f) P a)
  ((a. bool.IN a (DeepSyntax.Aset (DeepSyntax.Negn f)) P a)
   a. bool.IN a (DeepSyntax.Aset f) P a)
  ((a.
      bool.IN a (DeepSyntax.Aset pos (DeepSyntax.UnrelatedBool a0))
      P a) )
  ((a. bool.IN a (DeepSyntax.Aset (DeepSyntax.xLT i)) P a) P i)
  ((a. bool.IN a (DeepSyntax.Aset (DeepSyntax.xLT i)) P a) )
  ((a. bool.IN a (DeepSyntax.Aset (DeepSyntax.LTx i)) P a) )
  ((a. bool.IN a (DeepSyntax.Aset (DeepSyntax.LTx i)) P a)
   P (integer.int_add i (integer.int_of_num 1)))
  ((a. bool.IN a (DeepSyntax.Aset (DeepSyntax.xEQ i)) P a)
   P (integer.int_add i (integer.int_of_num 1)))
  ((a. bool.IN a (DeepSyntax.Aset (DeepSyntax.xEQ i)) P a) P i)
  ((a.
      bool.IN a (DeepSyntax.Aset pos (DeepSyntax.xDivided i1 i2)) P a)
   )

((b. bool.IN b (DeepSyntax.Bset pos (DeepSyntax.Conjn f1 f2)) P b)
   (b. bool.IN b (DeepSyntax.Bset pos f1) P b)
   b. bool.IN b (DeepSyntax.Bset pos f2) P b)
  ((b. bool.IN b (DeepSyntax.Bset pos (DeepSyntax.Disjn f1 f2)) P b)
   (b. bool.IN b (DeepSyntax.Bset pos f1) P b)
   b. bool.IN b (DeepSyntax.Bset pos f2) P b)
  ((b. bool.IN b (DeepSyntax.Bset (DeepSyntax.Negn f)) P b)
   b. bool.IN b (DeepSyntax.Bset f) P b)
  ((b. bool.IN b (DeepSyntax.Bset (DeepSyntax.Negn f)) P b)
   b. bool.IN b (DeepSyntax.Bset f) P b)
  ((b.
      bool.IN b (DeepSyntax.Bset pos (DeepSyntax.UnrelatedBool b0))
      P b) )
  ((b. bool.IN b (DeepSyntax.Bset (DeepSyntax.xLT i)) P b) )
  ((b. bool.IN b (DeepSyntax.Bset (DeepSyntax.xLT i)) P b)
   P (integer.int_add i (integer.int_neg (integer.int_of_num 1))))
  ((b. bool.IN b (DeepSyntax.Bset (DeepSyntax.LTx i)) P b) P i)
  ((b. bool.IN b (DeepSyntax.Bset (DeepSyntax.LTx i)) P b) )
  ((b. bool.IN b (DeepSyntax.Bset (DeepSyntax.xEQ i)) P b)
   P (integer.int_add i (integer.int_neg (integer.int_of_num 1))))
  ((b. bool.IN b (DeepSyntax.Bset (DeepSyntax.xEQ i)) P b) P i)
  ((b.
      bool.IN b (DeepSyntax.Bset pos (DeepSyntax.xDivided i1 i2)) P b)
   )

(a0 a1 f f1 f2 f3 f4 f5 f6 f7.
     DeepSyntax.deep_form_CASE (DeepSyntax.Conjn a0 a1) f f1 f2 f3 f4 f5 f6
       f7 = f a0 a1)
  (a0 a1 f f1 f2 f3 f4 f5 f6 f7.
     DeepSyntax.deep_form_CASE (DeepSyntax.Disjn a0 a1) f f1 f2 f3 f4 f5 f6
       f7 = f1 a0 a1)
  (a f f1 f2 f3 f4 f5 f6 f7.
     DeepSyntax.deep_form_CASE (DeepSyntax.Negn a) f f1 f2 f3 f4 f5 f6 f7 =
     f2 a)
  (a f f1 f2 f3 f4 f5 f6 f7.
     DeepSyntax.deep_form_CASE (DeepSyntax.UnrelatedBool a) f f1 f2 f3 f4
       f5 f6 f7 = f3 a)
  (a f f1 f2 f3 f4 f5 f6 f7.
     DeepSyntax.deep_form_CASE (DeepSyntax.xLT a) f f1 f2 f3 f4 f5 f6 f7 =
     f4 a)
  (a f f1 f2 f3 f4 f5 f6 f7.
     DeepSyntax.deep_form_CASE (DeepSyntax.LTx a) f f1 f2 f3 f4 f5 f6 f7 =
     f5 a)
  (a f f1 f2 f3 f4 f5 f6 f7.
     DeepSyntax.deep_form_CASE (DeepSyntax.xEQ a) f f1 f2 f3 f4 f5 f6 f7 =
     f6 a)
  a0 a1 f f1 f2 f3 f4 f5 f6 f7.
    DeepSyntax.deep_form_CASE (DeepSyntax.xDivided a0 a1) f f1 f2 f3 f4 f5
      f6 f7 = f7 a0 a1

(a1' a1 a0' a0. ¬(DeepSyntax.Conjn a0 a1 = DeepSyntax.Disjn a0' a1'))
  (a1 a0 a. ¬(DeepSyntax.Conjn a0 a1 = DeepSyntax.Negn a))
  (a1 a0 a. ¬(DeepSyntax.Conjn a0 a1 = DeepSyntax.UnrelatedBool a))
  (a1 a0 a. ¬(DeepSyntax.Conjn a0 a1 = DeepSyntax.xLT a))
  (a1 a0 a. ¬(DeepSyntax.Conjn a0 a1 = DeepSyntax.LTx a))
  (a1 a0 a. ¬(DeepSyntax.Conjn a0 a1 = DeepSyntax.xEQ a))
  (a1' a1 a0' a0.
     ¬(DeepSyntax.Conjn a0 a1 = DeepSyntax.xDivided a0' a1'))
  (a1 a0 a. ¬(DeepSyntax.Disjn a0 a1 = DeepSyntax.Negn a))
  (a1 a0 a. ¬(DeepSyntax.Disjn a0 a1 = DeepSyntax.UnrelatedBool a))
  (a1 a0 a. ¬(DeepSyntax.Disjn a0 a1 = DeepSyntax.xLT a))
  (a1 a0 a. ¬(DeepSyntax.Disjn a0 a1 = DeepSyntax.LTx a))
  (a1 a0 a. ¬(DeepSyntax.Disjn a0 a1 = DeepSyntax.xEQ a))
  (a1' a1 a0' a0.
     ¬(DeepSyntax.Disjn a0 a1 = DeepSyntax.xDivided a0' a1'))
  (a' a. ¬(DeepSyntax.Negn a = DeepSyntax.UnrelatedBool a'))
  (a' a. ¬(DeepSyntax.Negn a = DeepSyntax.xLT a'))
  (a' a. ¬(DeepSyntax.Negn a = DeepSyntax.LTx a'))
  (a' a. ¬(DeepSyntax.Negn a = DeepSyntax.xEQ a'))
  (a1 a0 a. ¬(DeepSyntax.Negn a = DeepSyntax.xDivided a0 a1))
  (a' a. ¬(DeepSyntax.UnrelatedBool a = DeepSyntax.xLT a'))
  (a' a. ¬(DeepSyntax.UnrelatedBool a = DeepSyntax.LTx a'))
  (a' a. ¬(DeepSyntax.UnrelatedBool a = DeepSyntax.xEQ a'))
  (a1 a0 a. ¬(DeepSyntax.UnrelatedBool a = DeepSyntax.xDivided a0 a1))
  (a' a. ¬(DeepSyntax.xLT a = DeepSyntax.LTx a'))
  (a' a. ¬(DeepSyntax.xLT a = DeepSyntax.xEQ a'))
  (a1 a0 a. ¬(DeepSyntax.xLT a = DeepSyntax.xDivided a0 a1))
  (a' a. ¬(DeepSyntax.LTx a = DeepSyntax.xEQ a'))
  (a1 a0 a. ¬(DeepSyntax.LTx a = DeepSyntax.xDivided a0 a1))
  a1 a0 a. ¬(DeepSyntax.xEQ a = DeepSyntax.xDivided a0 a1)

(integer.int_add (integer.int_of_num n) (integer.int_of_num m) =
   integer.int_of_num (n + m)
   integer.int_add (integer.int_neg (integer.int_of_num n))
     (integer.int_of_num m) =
   (if n m then integer.int_of_num (arithmetic.- m n)
    else integer.int_neg (integer.int_of_num (arithmetic.- n m)))
   integer.int_add (integer.int_of_num n)
     (integer.int_neg (integer.int_of_num m)) =
   (if m n then integer.int_of_num (arithmetic.- n m)
    else integer.int_neg (integer.int_of_num (arithmetic.- m n)))
   integer.int_add (integer.int_neg (integer.int_of_num n))
     (integer.int_neg (integer.int_of_num m)) =
   integer.int_neg (integer.int_of_num (n + m))
   integer.int_mul (integer.int_of_num n) (integer.int_of_num m) =
   integer.int_of_num (n * m)
   integer.int_mul (integer.int_neg (integer.int_of_num n))
     (integer.int_of_num m) =
   integer.int_neg (integer.int_of_num (n * m))
   integer.int_mul (integer.int_of_num n)
     (integer.int_neg (integer.int_of_num m)) =
   integer.int_neg (integer.int_of_num (n * m))
   integer.int_mul (integer.int_neg (integer.int_of_num n))
     (integer.int_neg (integer.int_of_num m)) =
   integer.int_of_num (n * m)
   (integer.int_of_num n = integer.int_of_num m n = m)
   (integer.int_of_num n = integer.int_neg (integer.int_of_num m)
    n = 0 m = 0)
   (integer.int_neg (integer.int_of_num n) = integer.int_of_num m
    n = 0 m = 0)
   (integer.int_neg (integer.int_of_num n) =
    integer.int_neg (integer.int_of_num m) n = m)
   integer.int_neg (integer.int_neg x) = x
   integer.int_neg (integer.int_of_num 0) = integer.int_of_num 0)
  integer.int_0 = integer.int_of_num 0
  integer.int_1 = integer.int_of_num 1
  (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 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. arithmetic.- n m = if m < n then numeral.iSUB n m else 0)
  (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))
  t. ( t t) (t t) ( t ) (t ) (t t t)

ring.is_ring
    (ring.recordtype.ring integer.int_0 integer.int_1 integer.int_add
       integer.int_mul integer.int_neg)
  (vm p.
     integerRing.int_interp_p vm p =
     integerRing.int_r_interp_cs vm (integerRing.int_polynom_simplify p))
  (((vm c. integerRing.int_interp_p vm (ringNorm.Pconst c) = c)
    (vm i.
       integerRing.int_interp_p vm (ringNorm.Pvar i) =
       quote.varmap_find i vm)
    (vm p1 p2.
       integerRing.int_interp_p vm (ringNorm.Pplus p1 p2) =
       integer.int_add (integerRing.int_interp_p vm p1)
         (integerRing.int_interp_p vm p2))
    (vm p1 p2.
       integerRing.int_interp_p vm (ringNorm.Pmult p1 p2) =
       integer.int_mul (integerRing.int_interp_p vm p1)
         (integerRing.int_interp_p vm p2))
    vm p1.
      integerRing.int_interp_p vm (ringNorm.Popp p1) =
      integer.int_neg (integerRing.int_interp_p vm p1))
   (x v2 v1.
      quote.varmap_find quote.End_idx (quote.Node_vm x v1 v2) = x)
   (x v2 v1 i1.
      quote.varmap_find (quote.Right_idx i1) (quote.Node_vm x v1 v2) =
      quote.varmap_find i1 v2)
   (x v2 v1 i1.
      quote.varmap_find (quote.Left_idx i1) (quote.Node_vm x v1 v2) =
      quote.varmap_find i1 v1)
   i. quote.varmap_find i quote.Empty_vm = select x. )
  ((t2 t1 l2 l1 c2 c1.
      integerRing.int_r_canonical_sum_merge (canonical.Cons_monom c1 l1 t1)
        (canonical.Cons_monom c2 l2 t2) =
      prelim.compare (prelim.list_compare quote.index_compare l1 l2)
        (canonical.Cons_monom c1 l1
           (integerRing.int_r_canonical_sum_merge t1
              (canonical.Cons_monom c2 l2 t2)))
        (canonical.Cons_monom (integer.int_add c1 c2) l1
           (integerRing.int_r_canonical_sum_merge t1 t2))
        (canonical.Cons_monom c2 l2
           (integerRing.int_r_canonical_sum_merge
              (canonical.Cons_monom c1 l1 t1) t2)))
   (t2 t1 l2 l1 c1.
      integerRing.int_r_canonical_sum_merge (canonical.Cons_monom c1 l1 t1)
        (canonical.Cons_varlist l2 t2) =
      prelim.compare (prelim.list_compare quote.index_compare l1 l2)
        (canonical.Cons_monom c1 l1
           (integerRing.int_r_canonical_sum_merge t1
              (canonical.Cons_varlist l2 t2)))
        (canonical.Cons_monom (integer.int_add c1 integer.int_1) l1
           (integerRing.int_r_canonical_sum_merge t1 t2))
        (canonical.Cons_varlist l2
           (integerRing.int_r_canonical_sum_merge
              (canonical.Cons_monom c1 l1 t1) t2)))
   (t2 t1 l2 l1 c2.
      integerRing.int_r_canonical_sum_merge (canonical.Cons_varlist l1 t1)
        (canonical.Cons_monom c2 l2 t2) =
      prelim.compare (prelim.list_compare quote.index_compare l1 l2)
        (canonical.Cons_varlist l1
           (integerRing.int_r_canonical_sum_merge t1
              (canonical.Cons_monom c2 l2 t2)))
        (canonical.Cons_monom (integer.int_add integer.int_1 c2) l1
           (integerRing.int_r_canonical_sum_merge t1 t2))
        (canonical.Cons_monom c2 l2
           (integerRing.int_r_canonical_sum_merge
              (canonical.Cons_varlist l1 t1) t2)))
   (t2 t1 l2 l1.
      integerRing.int_r_canonical_sum_merge (canonical.Cons_varlist l1 t1)
        (canonical.Cons_varlist l2 t2) =
      prelim.compare (prelim.list_compare quote.index_compare l1 l2)
        (canonical.Cons_varlist l1
           (integerRing.int_r_canonical_sum_merge t1
              (canonical.Cons_varlist l2 t2)))
        (canonical.Cons_monom (integer.int_add integer.int_1 integer.int_1)
           l1 (integerRing.int_r_canonical_sum_merge t1 t2))
        (canonical.Cons_varlist l2
           (integerRing.int_r_canonical_sum_merge
              (canonical.Cons_varlist l1 t1) t2)))
   (s1.
      integerRing.int_r_canonical_sum_merge s1 canonical.Nil_monom = s1)
   (v6 v5 v4.
      integerRing.int_r_canonical_sum_merge canonical.Nil_monom
        (canonical.Cons_monom v4 v5 v6) = canonical.Cons_monom v4 v5 v6)
   v8 v7.
     integerRing.int_r_canonical_sum_merge canonical.Nil_monom
       (canonical.Cons_varlist v7 v8) = canonical.Cons_varlist v7 v8)
  ((t2 l2 l1 c2 c1.
      integerRing.int_r_monom_insert c1 l1
        (canonical.Cons_monom c2 l2 t2) =
      prelim.compare (prelim.list_compare quote.index_compare l1 l2)
        (canonical.Cons_monom c1 l1 (canonical.Cons_monom c2 l2 t2))
        (canonical.Cons_monom (integer.int_add c1 c2) l1 t2)
        (canonical.Cons_monom c2 l2
           (integerRing.int_r_monom_insert c1 l1 t2)))
   (t2 l2 l1 c1.
      integerRing.int_r_monom_insert c1 l1 (canonical.Cons_varlist l2 t2) =
      prelim.compare (prelim.list_compare quote.index_compare l1 l2)
        (canonical.Cons_monom c1 l1 (canonical.Cons_varlist l2 t2))
        (canonical.Cons_monom (integer.int_add c1 integer.int_1) l1 t2)
        (canonical.Cons_varlist l2
           (integerRing.int_r_monom_insert c1 l1 t2)))
   l1 c1.
     integerRing.int_r_monom_insert c1 l1 canonical.Nil_monom =
     canonical.Cons_monom c1 l1 canonical.Nil_monom)
  ((t2 l2 l1 c2.
      integerRing.int_r_varlist_insert l1 (canonical.Cons_monom c2 l2 t2) =
      prelim.compare (prelim.list_compare quote.index_compare l1 l2)
        (canonical.Cons_varlist l1 (canonical.Cons_monom c2 l2 t2))
        (canonical.Cons_monom (integer.int_add integer.int_1 c2) l1 t2)
        (canonical.Cons_monom c2 l2
           (integerRing.int_r_varlist_insert l1 t2)))
   (t2 l2 l1.
      integerRing.int_r_varlist_insert l1 (canonical.Cons_varlist l2 t2) =
      prelim.compare (prelim.list_compare quote.index_compare l1 l2)
        (canonical.Cons_varlist l1 (canonical.Cons_varlist l2 t2))
        (canonical.Cons_monom (integer.int_add integer.int_1 integer.int_1)
           l1 t2)
        (canonical.Cons_varlist l2
           (integerRing.int_r_varlist_insert l1 t2)))
   l1.
     integerRing.int_r_varlist_insert l1 canonical.Nil_monom =
     canonical.Cons_varlist l1 canonical.Nil_monom)
  ((c0 c l t.
      integerRing.int_r_canonical_sum_scalar c0
        (canonical.Cons_monom c l t) =
      canonical.Cons_monom (integer.int_mul c0 c) l
        (integerRing.int_r_canonical_sum_scalar c0 t))
   (c0 l t.
      integerRing.int_r_canonical_sum_scalar c0
        (canonical.Cons_varlist l t) =
      canonical.Cons_monom c0 l
        (integerRing.int_r_canonical_sum_scalar c0 t))
   c0.
     integerRing.int_r_canonical_sum_scalar c0 canonical.Nil_monom =
     canonical.Nil_monom)
  ((l0 c l t.
      integerRing.int_r_canonical_sum_scalar2 l0
        (canonical.Cons_monom c l t) =
      integerRing.int_r_monom_insert c
        (prelim.list_merge quote.index_lt l0 l)
        (integerRing.int_r_canonical_sum_scalar2 l0 t))
   (l0 l t.
      integerRing.int_r_canonical_sum_scalar2 l0
        (canonical.Cons_varlist l t) =
      integerRing.int_r_varlist_insert
        (prelim.list_merge quote.index_lt l0 l)
        (integerRing.int_r_canonical_sum_scalar2 l0 t))
   l0.
     integerRing.int_r_canonical_sum_scalar2 l0 canonical.Nil_monom =
     canonical.Nil_monom)
  ((c0 l0 c l t.
      integerRing.int_r_canonical_sum_scalar3 c0 l0
        (canonical.Cons_monom c l t) =
      integerRing.int_r_monom_insert (integer.int_mul c0 c)
        (prelim.list_merge quote.index_lt l0 l)
        (integerRing.int_r_canonical_sum_scalar3 c0 l0 t))
   (c0 l0 l t.
      integerRing.int_r_canonical_sum_scalar3 c0 l0
        (canonical.Cons_varlist l t) =
      integerRing.int_r_monom_insert c0
        (prelim.list_merge quote.index_lt l0 l)
        (integerRing.int_r_canonical_sum_scalar3 c0 l0 t))
   c0 l0.
     integerRing.int_r_canonical_sum_scalar3 c0 l0 canonical.Nil_monom =
     canonical.Nil_monom)
  ((c1 l1 t1 s2.
      integerRing.int_r_canonical_sum_prod (canonical.Cons_monom c1 l1 t1)
        s2 =
      integerRing.int_r_canonical_sum_merge
        (integerRing.int_r_canonical_sum_scalar3 c1 l1 s2)
        (integerRing.int_r_canonical_sum_prod t1 s2))
   (l1 t1 s2.
      integerRing.int_r_canonical_sum_prod (canonical.Cons_varlist l1 t1)
        s2 =
      integerRing.int_r_canonical_sum_merge
        (integerRing.int_r_canonical_sum_scalar2 l1 s2)
        (integerRing.int_r_canonical_sum_prod t1 s2))
   s2.
     integerRing.int_r_canonical_sum_prod canonical.Nil_monom s2 =
     canonical.Nil_monom)
  ((c l t.
      integerRing.int_r_canonical_sum_simplify
        (canonical.Cons_monom c l t) =
      if c = integer.int_0 then integerRing.int_r_canonical_sum_simplify t
      else if c = integer.int_1 then
        canonical.Cons_varlist l
          (integerRing.int_r_canonical_sum_simplify t)
      else
        canonical.Cons_monom c l
          (integerRing.int_r_canonical_sum_simplify t))
   (l t.
      integerRing.int_r_canonical_sum_simplify
        (canonical.Cons_varlist l t) =
      canonical.Cons_varlist l
        (integerRing.int_r_canonical_sum_simplify t))
   integerRing.int_r_canonical_sum_simplify canonical.Nil_monom =
   canonical.Nil_monom)
  ((vm x. integerRing.int_r_ivl_aux vm x [] = quote.varmap_find x vm)
   vm x x' t'.
     integerRing.int_r_ivl_aux vm x (x' :: t') =
     integer.int_mul (quote.varmap_find x vm)
       (integerRing.int_r_ivl_aux vm x' t'))
  ((vm. integerRing.int_r_interp_vl vm [] = integer.int_1)
   vm x t.
     integerRing.int_r_interp_vl vm (x :: t) =
     integerRing.int_r_ivl_aux vm x t)
  ((vm c. integerRing.int_r_interp_m vm c [] = c)
   vm c x t.
     integerRing.int_r_interp_m vm c (x :: t) =
     integer.int_mul c (integerRing.int_r_ivl_aux vm x t))
  ((vm a. integerRing.int_r_ics_aux vm a canonical.Nil_monom = a)
   (vm a l t.
      integerRing.int_r_ics_aux vm a (canonical.Cons_varlist l t) =
      integer.int_add a
        (integerRing.int_r_ics_aux vm (integerRing.int_r_interp_vl vm l)
           t))
   vm a c l t.
     integerRing.int_r_ics_aux vm a (canonical.Cons_monom c l t) =
     integer.int_add a
       (integerRing.int_r_ics_aux vm (integerRing.int_r_interp_m vm c l)
          t))
  ((vm.
      integerRing.int_r_interp_cs vm canonical.Nil_monom = integer.int_0)
   (vm l t.
      integerRing.int_r_interp_cs vm (canonical.Cons_varlist l t) =
      integerRing.int_r_ics_aux vm (integerRing.int_r_interp_vl vm l) t)
   vm c l t.
     integerRing.int_r_interp_cs vm (canonical.Cons_monom c l t) =
     integerRing.int_r_ics_aux vm (integerRing.int_r_interp_m vm c l) t)
  ((i.
      integerRing.int_polynom_normalize (ringNorm.Pvar i) =
      canonical.Cons_varlist (i :: []) canonical.Nil_monom)
   (c.
      integerRing.int_polynom_normalize (ringNorm.Pconst c) =
      canonical.Cons_monom c [] canonical.Nil_monom)
   (pl pr.
      integerRing.int_polynom_normalize (ringNorm.Pplus pl pr) =
      integerRing.int_r_canonical_sum_merge
        (integerRing.int_polynom_normalize pl)
        (integerRing.int_polynom_normalize pr))
   (pl pr.
      integerRing.int_polynom_normalize (ringNorm.Pmult pl pr) =
      integerRing.int_r_canonical_sum_prod
        (integerRing.int_polynom_normalize pl)
        (integerRing.int_polynom_normalize pr))
   p.
     integerRing.int_polynom_normalize (ringNorm.Popp p) =
     integerRing.int_r_canonical_sum_scalar3
       (integer.int_neg integer.int_1) []
       (integerRing.int_polynom_normalize p))
  x.
    integerRing.int_polynom_simplify x =
    integerRing.int_r_canonical_sum_simplify
      (integerRing.int_polynom_normalize x)

External Type Operators

External Constants

Assumptions

words.word_msb words.word_L

wellFounded empty

wellFounded (<)

¬pred_set.FINITE pred_set.UNIV

0 = 0

¬words.word_msb (words.n2w 0)

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

words.word_2comp words.word_L = words.word_L

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

quotient.QUOTIENT (=) id id

x. x = x

x. bool.IN x pred_set.UNIV

t. t

a. divides.divides a 0

n. 0 n

m. m m

s. pred_set.SUBSET pred_set.EMPTY s

s. pred_set.SUBSET s s

q. q

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

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

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

1 = suc 0

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

words.w2n (words.n2w 0) = 0

¬¬p p

x. ¬bool.IN 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 < 0)

n. 0 < suc n

x. numeral.iZ x = x

(¬) = λ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

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

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

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

¬(p q) p

x. x = x

c. arithmetic.- c c = 0

a. gcd.gcd 0 a = a

a. gcd.gcd a 0 = a

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

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

R. quotient.EQUIV R quotient.PARTIAL_EQUIV R

e. f. f bool.the_value = e

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

words.w2n (words.n2w 1) = 1

¬(p q) ¬q

¬(p q) ¬p

¬(p q) ¬q

A. A ¬A

t. ¬t t

t. (t ) ¬t

b. bit.BIT b (arithmetic.BIT2 0 b)

n. 0 < arithmetic.BIT2 0 n

n. even n ¬odd n

n. odd n ¬even n

m. m * 1 = m

q. q div 1 = q

q. q div suc 0 = q

k. k mod suc 0 = 0

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

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

x y. const x y = x

x. (select y. y = x) = x

m n. m m + n

n m. arithmetic.- n m n

() = λp q. p q p

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.INT_MAX bool.the_value =
  arithmetic.- (words.INT_MIN bool.the_value) 1

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

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

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. 1 arithmetic.BIT2 0 n

n. n 0 n = 0

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

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

x. (fst x, snd x) = x

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

x y. fst (x, y) = x

x y. snd (x, y) = y

h t. head (h :: t) = h

b t. (if b then t else t) = t

a b. gcd.is_gcd a b (gcd.gcd a b)

f x. bool.literal_case f x = f x

f x. bool.LET f x = f x

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

f n. length (list.GENLIST f n) = n

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

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

n. ¬(n = 0) 0 < n

l. length l = 0 l = []

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

(%%genvar%%3928. P %%genvar%%3928) P P

x y. x = y y = x

t1 t2. t1 t2 t2 t1

A B. A B B A

a b. gcd.gcd a b = gcd.gcd b a

m n. m * n = n * m

m n. m + n = n + m

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

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

s. pred_set.FINITE s f. pred_set.FINITE (pred_set.IMAGE f s)

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

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

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

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

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

(¬A ) (A )

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

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

x. even x x mod arithmetic.BIT2 0 = 0

n. bit1 n = n + (n + suc 0)

n. 0 < n 0 div n = 0

n. 0 < n 0 mod n = 0

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

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_mul (words.word_2comp (words.n2w 1)) w

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

A B. A B ¬A B

m n. m < n suc m n

m n. ¬(m < n) n m

m n. ¬(m n) n < m

m. m = 0 n. m = suc n

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

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

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

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

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

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.dimword bool.the_value words.dimword bool.the_value

n. arithmetic.BIT2 n = n + (n + suc (suc 0))

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

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

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

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

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

(p. P p) p_1 p_2. P (p_1, p_2)

map (λx. x) l = l map id l = l

x y. bool.IN x (pred_set.INSERT y pred_set.EMPTY) x = y

c1 c2. c1 = c2 string.ORD c1 = string.ORD c2

m n. ¬(m < n n < suc m)

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

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. 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

n m. arithmetic.- (suc n) (suc m) = arithmetic.- n m

n l. length (list.DROP n l) = arithmetic.- (length l) n

n. even n m. n = arithmetic.BIT2 0 * m

r x.
    ringNorm.polynom_simplify r x =
    ringNorm.r_canonical_sum_simplify r (ringNorm.polynom_normalize r x)

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

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

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

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

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

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

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

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

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

m n. even (m + n) even m even n

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)

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

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

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

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

E P.
    quotient.EQUIV E (bool.RES_FORALL (quotient.respects E) P () P)

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

0 < x y 0 < x y = 0

a b c. divides.divides a b divides.divides a (b * c)

a b. divides.divides a b q. b = q * a

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

m n. n < m p. p + n = m

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

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

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

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

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

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

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

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

(even 0 ) n. even (suc n) ¬even n

(odd 0 ) n. odd (suc n) ¬odd n

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

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

m n. m = n m n n m

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

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

m n. odd (m + n) ¬(odd m odd n)

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. 0 < n k. k * n mod n = 0

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

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

¬(¬A B) A ¬B

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

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

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

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

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

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

(x y) (z w) x z y w

(x y) (z w) x z y w

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 < arithmetic.- n p m + p < n

m n p. arithmetic.- m n p m n + p

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

m n p. m + (n + p) = 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. 1 n = 1 n 1 = n

P l. all P l e. bool.IN e (list.LIST_TO_SET l) P e

s t. s = t x. bool.IN x s bool.IN x t

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_add v w = words.word_add v x w = x

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

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

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

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

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

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

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

n m. gcd.gcd n m = 0 n = 0 m = 0

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

m n. 0 < m 0 < n 0 < m * n

a b. b a 0 < b 0 < a div b

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

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

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

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

f n x. x < n list.EL x (list.GENLIST f n) = f x

P. P 0 (n. P n P (suc n)) n. P n

E. quotient.EQUIV E x y. E x y E x = E y

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

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

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

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

x y s. bool.IN x (pred_set.INSERT y s) x = y bool.IN x s

x s t.
    pred_set.SUBSET (pred_set.INSERT x s) t
    bool.IN x t pred_set.SUBSET s t

b t1 t2. (if b then t1 else t2) (¬b t1) (b t2)

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

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

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

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

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

s t x. bool.IN x (pred_set.UNION s t) bool.IN x s bool.IN x t

P Q R.
    pred_set.SUBSET (pred_set.UNION P Q) R
    pred_set.SUBSET P R pred_set.SUBSET Q R

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 (words.word_add v w) x =
    words.word_add (words.word_mul v x) (words.word_mul w x)

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

(∃!) = λP. () P x y. P x P y x = y

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

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_ls (words.n2w a) (words.n2w b)
    a mod words.dimword bool.the_value b mod words.dimword bool.the_value

x y. 1 < x y 1 < x 0 < y

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

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

(n. bit.LOG2 (bit1 n) = numeral_bit.iLOG2 (numeral.iDUB n))
  n. bit.LOG2 (arithmetic.BIT2 n) = numeral_bit.iLOG2 (bit1 n)

n i a. bit.BIT i (a div arithmetic.BIT2 0 n) bit.BIT (i + n) a

n l1 l2. n < length l1 list.EL n (l1 @ l2) = list.EL n l1

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

r.
    ring.is_ring r
    vm p.
      ringNorm.r_interp_cs r vm (ringNorm.polynom_simplify r p) =
      ringNorm.interp_p r vm p

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

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

e f. fn. fn 0 = e n. fn (suc n) = f n (fn n)

x y. x * y = 1 x = 1 y = 1

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

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

m n p. m * n < m * p 0 < m n < p

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

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

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

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

m n p.
    m + arithmetic.- n p = if n p then m else arithmetic.- (m + n) p

a b c. gcd.gcd a b = 1 divides.divides b (a * c) divides.divides b c

b. 1 < b n m. b m < b n m < n

b. 1 < b n m. b m b n m n

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

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

R abs rep.
    quotient.QUOTIENT R abs rep
    f.
      () f bool.RES_FORALL (quotient.respects R) (quotient.--> abs id f)

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

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

REL abs rep.
    quotient.QUOTIENT REL abs rep
    x1 x2. REL x1 x2 REL x1 (rep (abs x2))

R abs rep. quotient.QUOTIENT R abs rep x y. x = y R (rep x) (rep y)

(n. n 0 = 1) m n. m suc n = m * m n

n m. ¬(n = 0) i j. i * n = j * m + gcd.gcd m n

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

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

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

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

m n l. m + n < length l list.EL m (list.DROP n l) = list.EL (m + n) l

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)

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))

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

(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

x n.
    (n div arithmetic.BIT2 0 x) * arithmetic.BIT2 0 x =
    arithmetic.- n (n mod arithmetic.BIT2 0 x)

n a.
    ¬(a = 0) a mod arithmetic.BIT2 0 n = 0 arithmetic.BIT2 0 n a

(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)

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. m = arithmetic.- n p m + p = n m 0 n p

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

m n. 0 < n 0 < m x. x mod n * m mod n = x mod n

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)

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

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

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

R1 R2 f g. quotient.===> R1 R2 f g x y. R1 x y R2 (f x) (g y)

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

h l a.
    l h
    bit.BITS h l (a * arithmetic.BIT2 0 l) =
    bit.BITS (arithmetic.- h l) 0 a

(n. arithmetic.- 0 n = 0)
  m n.
    arithmetic.- (suc m) n = if m < n then 0 else suc (arithmetic.- m n)

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

p q n. 0 < n q p n arithmetic.- p q = n p div n q

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

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

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

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

x y z. 0 < z (y div z = x x * z y y < suc x * z)

n m a.
    n < m a < arithmetic.BIT2 0 m
    a div arithmetic.BIT2 0 n < arithmetic.BIT2 0 m

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

numeral_bit.iLOG2 0 = 0
  (n. numeral_bit.iLOG2 (bit1 n) = 1 + numeral_bit.iLOG2 n)
  n. numeral_bit.iLOG2 (arithmetic.BIT2 n) = 1 + numeral_bit.iLOG2 n

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

(m * n < m 0 < m n = 0) (m * n < n 0 < n m = 0)

r.
    (vm. ringNorm.r_interp_vl r vm [] = ring.ring_R1 r)
    vm x t.
      ringNorm.r_interp_vl r vm (x :: t) = ringNorm.r_ivl_aux r vm x t

R abs rep.
    quotient.QUOTIENT R abs rep
    f g.
      quotient.===> R () f g
      (bool.RES_FORALL (quotient.respects R) f
       bool.RES_FORALL (quotient.respects R) g)

(x. bool.IN x (list.LIST_TO_SET []) )
  x h t.
    bool.IN x (list.LIST_TO_SET (h :: t))
    x = h bool.IN x (list.LIST_TO_SET t)

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

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)

R1 abs1 rep1.
    quotient.QUOTIENT R1 abs1 rep1
    R2 abs2 rep2.
      quotient.QUOTIENT R2 abs2 rep2
      quotient.QUOTIENT (quotient.===> R1 R2) (quotient.--> rep1 abs2)
        (quotient.--> abs1 rep2)

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

a b c.
    gcd.is_gcd a b c
    divides.divides c a divides.divides c b
    d. divides.divides d a divides.divides d b divides.divides d c

R.
    quotient.PARTIAL_EQUIV R
    (x. R x x) x y. R x y R x x R y y R x = R y

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)

R abs rep.
    quotient.QUOTIENT R abs rep
    x1 x2 y1 y2. R x1 x2 R y1 y2 (R x1 y1 R x2 y2)

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)

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

(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)

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

R1 abs1 rep1.
    quotient.QUOTIENT R1 abs1 rep1
    R2 abs2 rep2.
      quotient.QUOTIENT R2 abs2 rep2
      f. (λx. f x) = quotient.--> rep1 abs2 (λx. rep2 (f (abs1 x)))

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

n.
    0 < n
    m p. m mod n = 0 p mod n = 0 (m + p) div n = m div n + p div 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)

r.
    (vm c. ringNorm.r_interp_m r vm c [] = c)
    vm c x t.
      ringNorm.r_interp_m r vm c (x :: t) =
      ring.ring_RM r c (ringNorm.r_ivl_aux r vm x t)

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

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

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

n m.
    ¬(n = 0) ¬(m = 0)
    p q. n = p * gcd.gcd n m m = q * gcd.gcd n m gcd.gcd p q = 1

a b.
    arithmetic.BIT2 0 b a a mod arithmetic.BIT2 0 b = 0
    arithmetic.- (a div arithmetic.BIT2 0 b) 1 =
    arithmetic.- a 1 div arithmetic.BIT2 0 b

r.
    (vm x. ringNorm.r_ivl_aux r vm x [] = quote.varmap_find x vm)
    vm x x' t'.
      ringNorm.r_ivl_aux r vm x (x' :: t') =
      ring.ring_RM r (quote.varmap_find x vm)
        (ringNorm.r_ivl_aux r vm x' t')

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))

R1 abs1 rep1.
    quotient.QUOTIENT R1 abs1 rep1
    R2 abs2 rep2.
      quotient.QUOTIENT R2 abs2 rep2
      f g x y. quotient.===> R1 R2 f g R1 x y R2 (f x) (g y)

(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))

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

R abs rep.
    quotient.QUOTIENT R abs rep
    (a. abs (rep a) = a) (a. R (rep a) (rep a))
    r s. R r s R r r R s s abs r = abs s

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))

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

r.
    (c0 c l t.
       ringNorm.r_canonical_sum_scalar r c0 (canonical.Cons_monom c l t) =
       canonical.Cons_monom (ring.ring_RM r c0 c) l
         (ringNorm.r_canonical_sum_scalar r c0 t))
    (c0 l t.
       ringNorm.r_canonical_sum_scalar r c0 (canonical.Cons_varlist l t) =
       canonical.Cons_monom c0 l
         (ringNorm.r_canonical_sum_scalar r c0 t))
    c0.
      ringNorm.r_canonical_sum_scalar r c0 canonical.Nil_monom =
      canonical.Nil_monom

r.
    (vm. ringNorm.r_interp_cs r vm canonical.Nil_monom = ring.ring_R0 r)
    (vm l t.
       ringNorm.r_interp_cs r vm (canonical.Cons_varlist l t) =
       ringNorm.r_ics_aux r vm (ringNorm.r_interp_vl r vm l) t)
    vm c l t.
      ringNorm.r_interp_cs r vm (canonical.Cons_monom c l t) =
      ringNorm.r_ics_aux r vm (ringNorm.r_interp_m r vm c l) t

n i a.
    bit.BIT i
      (arithmetic.- (arithmetic.BIT2 0 n)
         (a mod arithmetic.BIT2 0 n))
    a mod arithmetic.BIT2 0 n = 0 i = n
    ¬(a mod arithmetic.BIT2 0 n = 0) i < n
    ¬bit.BIT i (arithmetic.- (a mod arithmetic.BIT2 0 n) 1)

r.
    (c1 l1 t1 s2.
       ringNorm.r_canonical_sum_prod r (canonical.Cons_monom c1 l1 t1) s2 =
       ringNorm.r_canonical_sum_merge r
         (ringNorm.r_canonical_sum_scalar3 r c1 l1 s2)
         (ringNorm.r_canonical_sum_prod r t1 s2))
    (l1 t1 s2.
       ringNorm.r_canonical_sum_prod r (canonical.Cons_varlist l1 t1) s2 =
       ringNorm.r_canonical_sum_merge r
         (ringNorm.r_canonical_sum_scalar2 r l1 s2)
         (ringNorm.r_canonical_sum_prod r t1 s2))
    s2.
      ringNorm.r_canonical_sum_prod r canonical.Nil_monom s2 =
      canonical.Nil_monom

r.
    (l0 c l t.
       ringNorm.r_canonical_sum_scalar2 r l0 (canonical.Cons_monom c l t) =
       ringNorm.r_monom_insert r c (prelim.list_merge quote.index_lt l0 l)
         (ringNorm.r_canonical_sum_scalar2 r l0 t))
    (l0 l t.
       ringNorm.r_canonical_sum_scalar2 r l0 (canonical.Cons_varlist l t) =
       ringNorm.r_varlist_insert r (prelim.list_merge quote.index_lt l0 l)
         (ringNorm.r_canonical_sum_scalar2 r l0 t))
    l0.
      ringNorm.r_canonical_sum_scalar2 r l0 canonical.Nil_monom =
      canonical.Nil_monom

(x v2 v1. quote.varmap_find quote.End_idx (quote.Node_vm x v1 v2) = x)
  (x v2 v1 i1.
     quote.varmap_find (quote.Right_idx i1) (quote.Node_vm x v1 v2) =
     quote.varmap_find i1 v2)
  (x v2 v1 i1.
     quote.varmap_find (quote.Left_idx i1) (quote.Node_vm x v1 v2) =
     quote.varmap_find i1 v1)
  i. quote.varmap_find i quote.Empty_vm = select x.

r.
    (c l t.
       ringNorm.r_canonical_sum_simplify r (canonical.Cons_monom c l t) =
       if c = ring.ring_R0 r then ringNorm.r_canonical_sum_simplify r t
       else if c = ring.ring_R1 r then
         canonical.Cons_varlist l (ringNorm.r_canonical_sum_simplify r t)
       else
         canonical.Cons_monom c l
           (ringNorm.r_canonical_sum_simplify r t))
    (l t.
       ringNorm.r_canonical_sum_simplify r (canonical.Cons_varlist l t) =
       canonical.Cons_varlist l (ringNorm.r_canonical_sum_simplify r t))
    ringNorm.r_canonical_sum_simplify r canonical.Nil_monom =
    canonical.Nil_monom

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)

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 i a.
    i + n < m a < arithmetic.BIT2 0 m
    (bit.BIT i
       (arithmetic.- (arithmetic.BIT2 0 m)
          ((a div arithmetic.BIT2 0 n +
            if a mod arithmetic.BIT2 0 n = 0 then 0 else 1) mod
           arithmetic.BIT2 0 m))
     bit.BIT (i + n)
       (arithmetic.- (arithmetic.BIT2 0 m)
          (a mod arithmetic.BIT2 0 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)

(x f a. bit.BITWISE x f 0 0 = numeral_bit.iBITWISE x f 0 0)
  (x f a. bit.BITWISE x f a 0 = numeral_bit.iBITWISE x f a 0)
  (x f b. bit.BITWISE x f 0 b = numeral_bit.iBITWISE x f 0 b)
  x f a b. bit.BITWISE x f a b = numeral_bit.iBITWISE x f a b

r.
    (vm a. ringNorm.r_ics_aux r vm a canonical.Nil_monom = a)
    (vm a l t.
       ringNorm.r_ics_aux r vm a (canonical.Cons_varlist l t) =
       ring.ring_RP r a
         (ringNorm.r_ics_aux r vm (ringNorm.r_interp_vl r vm l) t))
    vm a c l t.
      ringNorm.r_ics_aux r vm a (canonical.Cons_monom c l t) =
      ring.ring_RP r a
        (ringNorm.r_ics_aux r vm (ringNorm.r_interp_m r vm c l) t)

r.
    (c0 l0 c l t.
       ringNorm.r_canonical_sum_scalar3 r c0 l0
         (canonical.Cons_monom c l t) =
       ringNorm.r_monom_insert r (ring.ring_RM r c0 c)
         (prelim.list_merge quote.index_lt l0 l)
         (ringNorm.r_canonical_sum_scalar3 r c0 l0 t))
    (c0 l0 l t.
       ringNorm.r_canonical_sum_scalar3 r c0 l0
         (canonical.Cons_varlist l t) =
       ringNorm.r_monom_insert r c0 (prelim.list_merge quote.index_lt l0 l)
         (ringNorm.r_canonical_sum_scalar3 r c0 l0 t))
    c0 l0.
      ringNorm.r_canonical_sum_scalar3 r c0 l0 canonical.Nil_monom =
      canonical.Nil_monom

(opr a b. numeral_bit.iBITWISE 0 opr a b = 0)
  (x opr a b.
     numeral_bit.iBITWISE (bit1 x) opr a b =
     bool.LET (λw. if opr (odd a) (odd b) then bit1 w else numeral.iDUB w)
       (numeral_bit.iBITWISE (arithmetic.- (bit1 x) 1) opr
          (arithmetic.DIV2 a) (arithmetic.DIV2 b)))
  x opr a b.
    numeral_bit.iBITWISE (arithmetic.BIT2 x) opr a b =
    bool.LET (λw. if opr (odd a) (odd b) then bit1 w else numeral.iDUB w)
      (numeral_bit.iBITWISE (bit1 x) opr (arithmetic.DIV2 a)
         (arithmetic.DIV2 b))

(r i.
     ringNorm.polynom_normalize r (ringNorm.Pvar i) =
     canonical.Cons_varlist (i :: []) canonical.Nil_monom)
  (r c.
     ringNorm.polynom_normalize r (ringNorm.Pconst c) =
     canonical.Cons_monom c [] canonical.Nil_monom)
  (r pl pr.
     ringNorm.polynom_normalize r (ringNorm.Pplus pl pr) =
     ringNorm.r_canonical_sum_merge r (ringNorm.polynom_normalize r pl)
       (ringNorm.polynom_normalize r pr))
  (r pl pr.
     ringNorm.polynom_normalize r (ringNorm.Pmult pl pr) =
     ringNorm.r_canonical_sum_prod r (ringNorm.polynom_normalize r pl)
       (ringNorm.polynom_normalize r pr))
  r p.
    ringNorm.polynom_normalize r (ringNorm.Popp p) =
    ringNorm.r_canonical_sum_scalar3 r (ring.ring_RN r (ring.ring_R1 r)) []
      (ringNorm.polynom_normalize r p)

(a a0 f f0 f1. ring.ring_R0 (ring.recordtype.ring a a0 f f0 f1) = a)
  (a a0 f f0 f1. ring.ring_R1 (ring.recordtype.ring a a0 f f0 f1) = a0)
  (a a0 f f0 f1. ring.ring_RP (ring.recordtype.ring a a0 f f0 f1) = f)
  (a a0 f f0 f1. ring.ring_RM (ring.recordtype.ring a a0 f f0 f1) = f0)
  a a0 f f0 f1. ring.ring_RN (ring.recordtype.ring a a0 f f0 f1) = f1

r.
    (t2 l2 l1 c2.
       ringNorm.r_varlist_insert r l1 (canonical.Cons_monom c2 l2 t2) =
       prelim.compare (prelim.list_compare quote.index_compare l1 l2)
         (canonical.Cons_varlist l1 (canonical.Cons_monom c2 l2 t2))
         (canonical.Cons_monom (ring.ring_RP r (ring.ring_R1 r) c2) l1 t2)
         (canonical.Cons_monom c2 l2
            (ringNorm.r_varlist_insert r l1 t2)))
    (t2 l2 l1.
       ringNorm.r_varlist_insert r l1 (canonical.Cons_varlist l2 t2) =
       prelim.compare (prelim.list_compare quote.index_compare l1 l2)
         (canonical.Cons_varlist l1 (canonical.Cons_varlist l2 t2))
         (canonical.Cons_monom
            (ring.ring_RP r (ring.ring_R1 r) (ring.ring_R1 r)) l1 t2)
         (canonical.Cons_varlist l2 (ringNorm.r_varlist_insert r l1 t2)))
    l1.
      ringNorm.r_varlist_insert r l1 canonical.Nil_monom =
      canonical.Cons_varlist l1 canonical.Nil_monom

(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))

(r vm c. ringNorm.interp_p r vm (ringNorm.Pconst c) = c)
  (r vm i.
     ringNorm.interp_p r vm (ringNorm.Pvar i) = quote.varmap_find i vm)
  (r vm p1 p2.
     ringNorm.interp_p r vm (ringNorm.Pplus p1 p2) =
     ring.ring_RP r (ringNorm.interp_p r vm p1)
       (ringNorm.interp_p r vm p2))
  (r vm p1 p2.
     ringNorm.interp_p r vm (ringNorm.Pmult p1 p2) =
     ring.ring_RM r (ringNorm.interp_p r vm p1)
       (ringNorm.interp_p r vm p2))
  r vm p1.
    ringNorm.interp_p r vm (ringNorm.Popp p1) =
    ring.ring_RN r (ringNorm.interp_p r vm p1)

r.
    (t2 l2 l1 c2 c1.
       ringNorm.r_monom_insert r c1 l1 (canonical.Cons_monom c2 l2 t2) =
       prelim.compare (prelim.list_compare quote.index_compare l1 l2)
         (canonical.Cons_monom c1 l1 (canonical.Cons_monom c2 l2 t2))
         (canonical.Cons_monom (ring.ring_RP r c1 c2) l1 t2)
         (canonical.Cons_monom c2 l2
            (ringNorm.r_monom_insert r c1 l1 t2)))
    (t2 l2 l1 c1.
       ringNorm.r_monom_insert r c1 l1 (canonical.Cons_varlist l2 t2) =
       prelim.compare (prelim.list_compare quote.index_compare l1 l2)
         (canonical.Cons_monom c1 l1 (canonical.Cons_varlist l2 t2))
         (canonical.Cons_monom (ring.ring_RP r c1 (ring.ring_R1 r)) l1 t2)
         (canonical.Cons_varlist l2
            (ringNorm.r_monom_insert r c1 l1 t2)))
    l1 c1.
      ringNorm.r_monom_insert r c1 l1 canonical.Nil_monom =
      canonical.Cons_monom c1 l1 canonical.Nil_monom

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))

r.
    ring.is_ring r
    (n m. ring.ring_RP r n m = ring.ring_RP r m n)
    (n m p.
       ring.ring_RP r n (ring.ring_RP r m p) =
       ring.ring_RP r (ring.ring_RP r n m) p)
    (n m. ring.ring_RM r n m = ring.ring_RM r m n)
    (n m p.
       ring.ring_RM r n (ring.ring_RM r m p) =
       ring.ring_RM r (ring.ring_RM r n m) p)
    (n. ring.ring_RP r (ring.ring_R0 r) n = n)
    (n. ring.ring_RM r (ring.ring_R1 r) n = n)
    (n. ring.ring_RP r n (ring.ring_RN r n) = ring.ring_R0 r)
    n m p.
      ring.ring_RM r (ring.ring_RP r n m) p =
      ring.ring_RP r (ring.ring_RM r n p) (ring.ring_RM r m p)

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))

r.
    (t2 t1 l2 l1 c2 c1.
       ringNorm.r_canonical_sum_merge r (canonical.Cons_monom c1 l1 t1)
         (canonical.Cons_monom c2 l2 t2) =
       prelim.compare (prelim.list_compare quote.index_compare l1 l2)
         (canonical.Cons_monom c1 l1
            (ringNorm.r_canonical_sum_merge r t1
               (canonical.Cons_monom c2 l2 t2)))
         (canonical.Cons_monom (ring.ring_RP r c1 c2) l1
            (ringNorm.r_canonical_sum_merge r t1 t2))
         (canonical.Cons_monom c2 l2
            (ringNorm.r_canonical_sum_merge r
               (canonical.Cons_monom c1 l1 t1) t2)))
    (t2 t1 l2 l1 c1.
       ringNorm.r_canonical_sum_merge r (canonical.Cons_monom c1 l1 t1)
         (canonical.Cons_varlist l2 t2) =
       prelim.compare (prelim.list_compare quote.index_compare l1 l2)
         (canonical.Cons_monom c1 l1
            (ringNorm.r_canonical_sum_merge r t1
               (canonical.Cons_varlist l2 t2)))
         (canonical.Cons_monom (ring.ring_RP r c1 (ring.ring_R1 r)) l1
            (ringNorm.r_canonical_sum_merge r t1 t2))
         (canonical.Cons_varlist l2
            (ringNorm.r_canonical_sum_merge r
               (canonical.Cons_monom c1 l1 t1) t2)))
    (t2 t1 l2 l1 c2.
       ringNorm.r_canonical_sum_merge r (canonical.Cons_varlist l1 t1)
         (canonical.Cons_monom c2 l2 t2) =
       prelim.compare (prelim.list_compare quote.index_compare l1 l2)
         (canonical.Cons_varlist l1
            (ringNorm.r_canonical_sum_merge r t1
               (canonical.Cons_monom c2 l2 t2)))
         (canonical.Cons_monom (ring.ring_RP r (ring.ring_R1 r) c2) l1
            (ringNorm.r_canonical_sum_merge r t1 t2))
         (canonical.Cons_monom c2 l2
            (ringNorm.r_canonical_sum_merge r
               (canonical.Cons_varlist l1 t1) t2)))
    (t2 t1 l2 l1.
       ringNorm.r_canonical_sum_merge r (canonical.Cons_varlist l1 t1)
         (canonical.Cons_varlist l2 t2) =
       prelim.compare (prelim.list_compare quote.index_compare l1 l2)
         (canonical.Cons_varlist l1
            (ringNorm.r_canonical_sum_merge r t1
               (canonical.Cons_varlist l2 t2)))
         (canonical.Cons_monom
            (ring.ring_RP r (ring.ring_R1 r) (ring.ring_R1 r)) l1
            (ringNorm.r_canonical_sum_merge r t1 t2))
         (canonical.Cons_varlist l2
            (ringNorm.r_canonical_sum_merge r
               (canonical.Cons_varlist l1 t1) t2)))
    (s1. ringNorm.r_canonical_sum_merge r s1 canonical.Nil_monom = s1)
    (v6 v5 v4.
       ringNorm.r_canonical_sum_merge r canonical.Nil_monom
         (canonical.Cons_monom v4 v5 v6) = canonical.Cons_monom v4 v5 v6)
    v8 v7.
      ringNorm.r_canonical_sum_merge r canonical.Nil_monom
        (canonical.Cons_varlist v7 v8) = canonical.Cons_varlist v7 v8

(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