;
; File :        Anrd.events
;
; Author:       Diederik Verkest
;
; Organization: IMEC, VSDM division
;               Kapeldreef 75,
;               B-3001 Leuven
;               Belgium
;
; Contents:     event file for pc-nqthm to define
;               - the division algorithm Adapted Non Restoring Division (ANRD)
;                 and to prove its correctness with respect to integer
;                 sign-magnitude division.
;               - an implementation of the algorithm on an ALU and the
;                 proof of correctness for the implementation wrt to ANRD.
;
; References:   D. Verkest, L. Claesen, H. De Man, "A Proof of the Non
;               Restoring Division algorithm and its implementation on the
;               Cathedral-II ALU", in Designing Correct Circuits, Eds. J.
;               Staunstrup and R. Sharp, Elseviers Science Publishers B.V.
;               (North-Holland), 1992, pp. 173 - 192
;
;               D. Verkest, L. Claesen, H. De Man, "On the use of the
;               Boyer-Moore theorem prover for correctness proofs of
;               parameterized hardware modules", in Formal VLSI
; Specification and Synthesis (VLSI Design Methods I),
;               Ed. L. J. M. Claesen, Elseviers Science Publishers B.V.
;               (North-Holland), 1990, pp. 99 - 116
;; [Flat file needed; this line removed by Matt K.] (PROVEALL "nrd" '(

Event: Start with the initial nqthm theory.

Theorem: plus-1 (1 + x) = (1 + x)

Theorem: plus-right-id (y ∉ N) → ((x + y) = fix (x))

Theorem: plus-add1 (x + (1 + y)) = if y ∈ N then 1 + (x + y)

else 1 + x endif Theorem: commutativity2-of-plus (x + y + z) = (y + x + z)

Theorem: commutativity-of-plus (x + y) = (y + x)

Theorem: associativity-of-plus ((x + y) + z) = (x + y + z)

Theorem: plus-equal-0 ((a + b) = 0) = ((a ≃ 0) ∧ (b ≃ 0))

Theorem: plus-cancellation ((a + b) = (a + c)) = (fix (b) = fix (c))

Theorem: times-zero2 (y ∉ N) → ((x ∗ y) = 0)

Theorem: distributivity-of-times-over-plus (x ∗ (y + z)) = ((x ∗ y) + (x ∗ z))

Theorem: times-add1 (x ∗ (1 + y)) = if y ∈ N then x + (x ∗ y)

else fix (x) endif

Theorem: commutativity-of-times (x ∗ y) = (y ∗ x)

Theorem: commutativity2-of-times (x ∗ y ∗ z) = (y ∗ x ∗ z)

Theorem: associativity-of-times ((x ∗ y) ∗ z) = (x ∗ y ∗ z)

Theorem: equal-times-0 ((x ∗ y) = 0) = ((x ≃ 0) ∨ (y ≃ 0))

Theorem: times-1 (1 ∗ x) = fix (x)

Theorem: equal-bools (((bool1 = t) ∨ (bool1 = f)) ∧ ((bool2 = t) ∨ (bool2 = f))) → ((bool1 = bool2 ) = ((bool1 → bool2 ) ∧ (bool2 → bool1 )))

Event: Disable equal-bools.

Theorem: lessp-times ((y ∗ x) < (x ∗ z)) = ((x ≄ 0) ∧ (y < z))

Theorem: times-2-not-1 (2 ∗ x) ≠ 1

Definition: twoto (n) = if n ∈ N

then if n ≃ 0 then 1

else 2 ∗ twoto (n − 1) endif else 0 endif

Theorem: twoto-plus ((j ∈ N) ∧ (k ∈ N)) → (twoto (j + k) = (twoto (j ) ∗ twoto (k)))

Theorem: twoto-by-0 twoto (0) = 1

Theorem: twoto-never-0 (i ∈ N) → (0 < twoto (i))

Theorem: difference-elim ((y ∈ N) ∧ (y ≮ x)) → ((x + (y − x)) = y)

Theorem: difference-2 (x − 2) = ((x − 1) − 1)

Theorem: difference-x-x (x − x) = 0

Theorem: difference-plus ((j + x) − j ) = fix (x)

Theorem: difference-plus-cancellation ((a + x) − (a + y)) = (x − y)

Theorem: pathological-difference (x < y) → ((x − y) = 0)

Theorem: difference-crock1 ((x + (y − z)) − y) = if y < z then x − y

else x − z endif

Theorem: difference-difference ((x − y) − z) = (x − (y + z))

Theorem: lessp-difference ((x − y) < x) = ((x ≄ 0) ∧ (y ≄ 0))

Theorem: difference-add1 ((1 + x) − y) = if y < (1 + x) then 1 + (x − y)

else 0 endif

Theorem: remainder-quotient ((x mod y) + (y ∗ (x ÷ y))) = fix (x)

Theorem: remainder-by-nonnumber (x ∉ N) → ((y mod x) = fix (y))

Theorem: lessp-remainder ((x mod y) < y) = (y ≄ 0)

Theorem: remainder-quotient-elim ((y ≄ 0) ∧ (x ∈ N)) → (((x mod y) + (y ∗ (x ÷ y))) = x)

Theorem: remainder-x-x (x mod x) = 0

Theorem: remainder-plus ((j + x) mod j ) = (x mod j )

Theorem: remainder-plus-times ((x + (i ∗ j )) mod j ) = (x mod j )

Theorem: remainder-plus-times-commuted ((x + (j ∗ i)) mod j ) = (x mod j )

Theorem: remainder-times ((j ∗ i) mod j ) = 0

Theorem: quotient-plus-times ((x + (i ∗ j )) ÷ j ) = if j ≃ 0 then 0

else i + (x ÷ j ) endif

Theorem: quotient-plus-times-commuted ((x + (j ∗ i)) ÷ j ) = if j ≃ 0 then 0

else i + (x ÷ j ) endif Theorem: quotient-times ((j ∗ i) ÷ j ) = if j ≃ 0 then 0

else fix (i) endif

Event: Disable times.

Theorem: times-distributes-over-remainder ((x ∗ y) mod (x ∗ z)) = (x ∗ (y mod z))

Theorem: remainder-of-1 (1 mod x) = if x = 1 then 0

else 1 endif

Theorem: remainder-crock3 ((x + (y − z)) mod y) = if (x + (y − z)) < y then x + (y − z)

elseif y < z then x mod y else (x − z) mod y endif

Theorem: remainder-of-0 (0 mod x) = 0

Theorem: remainder-crock4 ((1 + (x + (y − z))) mod y) = if (1 + (x + (y − z))) < y then 1 + (x + (y − z))

elseif y < z then (1 + x) mod y

elseif z < (1 + x) then (1 + (x − z)) mod y else 0 endif

Definition: evenp (n) = if n ∈ N

then if n ≃ 0 then t elseif n = 1 then f else evenp ((n − 1) − 1) endif

else f endif

Theorem: evenp-add1 ((a ∈ N) ∧ evenp (a)) → (¬ evenp (1 + a))

Theorem: not-evenp-add1 ((a ∈ N) ∧ (¬ evenp (a))) → evenp (1 + a)

Definition: exor (a, b) = (((¬ a) ∧ b) ∨ (a ∧ (¬ b)))

Definition: boolp (b) = (truep (b) ∨ falsep (b))

Theorem: lessp-boolp boolp (a < b)

Theorem: truep-boolp boolp (a) → (truep (a) = a)

Event: Add the shell bitvec, with bottom object function symbol bv-nil, with recognizer function symbol bitvecp, and 2 accessors: bv-bit, with type restriction (one-of truep falsep) and default value false; bv-vec, with type restriction (one-of bitvecp) and default value bv-nil.

Theorem: boolp-bv-bit boolp (bv-bit (a))

Definition: carry (c) = if c then 1

else 0 endif

Definition: bv-3 (a) = bv-bit (a)

Definition: bv-2 (a) = bv-bit (bv-vec (a))

Definition: bv-1 (a) = bv-bit (bv-vec (bv-vec (a)))

Definition: bv-0 (a) = bv-bit (bv-vec (bv-vec (bv-vec (a))))

Definition: bv-size (a) = if bitvecp (a)

then if a = bv-nil then 0

else 1 + bv-size (bv-vec (a)) endif else 0 endif

Theorem: size-0 (bv-size (x) = 0) = ((x = bv-nil) ∨ (¬ bitvecp (x)))

Definition: controlep (c) = (bitvecp (c) ∧ (bv-size (c) = 4))

Definition: bv-invert-even (b) = if bitvecp (b)

then if b = bv-nil then bv-nil

else bitvec (if evenp (bv-size (b)) then ¬ bv-bit (b) else bv-bit (b) endif, bv-invert-even (bv-vec (b))) endif

else bv-nil endif

Definition: bv-not (a) = if bitvecp (a)

then if a = bv-nil then bv-nil

else bitvec (¬ bv-bit (a), bv-not (bv-vec (a))) endif else bv-nil endif

Definition: bv-exor (a, b) = if bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b))

then if a = bv-nil then bv-nil

else bitvec (exor (bv-bit (a), bv-bit (b)),

bv-exor (bv-vec (a), bv-vec (b))) endif

else bv-nil endif

Theorem: bv-exor-nil-a (a = bv-nil) → (bv-exor (a, b) = bv-nil)

Theorem: bv-exor-nil-b (b = bv-nil) → (bv-exor (a, b) = bv-nil)

Definition: zero-bitvec (n) = if n ∈ N

then if n ≃ 0 then bv-nil

else bitvec (f, zero-bitvec (n − 1)) endif else bv-nil endif

Definition: one-bitvec (n) = if n ∈ N

then if n ≃ 0 then bv-nil

else bitvec (t, one-bitvec (n − 1)) endif else bv-nil endif

Theorem: size-zerobv bv-size (zero-bitvec (bv-size (a))) = bv-size (a)

Theorem: size-onebv bv-size (one-bitvec (bv-size (a))) = bv-size (a)

Theorem: size-bvnot bv-size (bv-not (a)) = bv-size (a)

Theorem: size-bvexor (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b))) → (bv-size (bv-exor (a, b)) = bv-size (a))

Theorem: size-bvinv bv-size (bv-invert-even (a)) = bv-size (a)

Definition: bv-append (a, b) = if bitvecp (a) ∧ bitvecp (b)

then if a = bv-nil then b

else bitvec (bv-bit (a), bv-append (bv-vec (a), b)) endif else bv-nil endif

Event: Add the shell bitvec-carry-ovf , with bottom object function symbol bvco-nil, with recognizer function symbol bitvec-carry-ovfp, and 3 accessors: bvco-bitvec, with type restriction (one-of bitvecp) and default value bv-nil; bvcocarry, with type restriction (one-of truep falsep) and default value false; bvcoovf , with type restriction (one-of truep falsep) and default value false.

Theorem: boolp-bvco-carry boolp (bvco-carry (a))

Theorem: boolp-bvco-ovf boolp (bvco-ovf (a))

Event: Add the shell carry-sign-ovf-bitvec, with bottom object function symbol csobv-nil, with recognizer function symbol carry-sign-ovf-bitvecp, and 4 accessors: csobv-carry, with type restriction (one-of truep falsep) and default value false; csobv-sign, with type restriction (one-of truep falsep) and default value false; csobv-ovf , with type restriction (one-of truep falsep) and default value false; csobv-bitvec, with type restriction (one-of bitvecp) and default value bvnil.

Definition: tcp (x) = ((x ∈ N) ∨ (negativep (x) ∧ (negative-guts (x) ≄ 0)))

Definition: tc-in-rangep (x, n) = if n ≃ 0 then f

elseif negativep (x) then twoto (n − 1) ≮ negative-guts (x)

else x < twoto (n − 1) endif

Definition: add (a, b) = if negativep (a)

then if negativep (b) then − (negative-guts (a) + negative-guts (b)) elseif b < negative-guts (a) then − (negative-guts (a) − b) else b − negative-guts (a) endif

elseif negativep (b)

then if a < negative-guts (b) then − (negative-guts (b) − a)

else a − negative-guts (b) endif else a + b endif

Theorem: commutativity2-of-add add (x, add (y, z)) = add (y, add (x, z))

Theorem: commutativity-of-add add (x, y) = add (y, x)

Theorem: associativity-of-add add (add (x, y), z) = add (x, add (y, z))

Definition: bv-to-nat (a) = if bitvecp (a)

then if a = bv-nil then 0

else (if bv-bit (a) then 1 else 0 endif

∗ twoto (bv-size (a) − 1)) + bv-to-nat (bv-vec (a)) endif

else 0 endif

Definition: nat-to-bv (a, size) = if size ≃ 0 then bv-nil

else bitvec (if (a ÷ twoto (size − 1)) = 1 then t else f endif, nat-to-bv (a mod twoto (size − 1), size − 1)) endif

Definition: tc-to-integer (a)

= if bitvecp (a)

then if falsep (bv-bit (a)) then bv-to-nat (a)

else add (bv-to-nat (a), − twoto (bv-size (a))) endif else 0 endif

Definition: nat-to-integer (n, size) = if n < twoto (size − 1) then n

else − (twoto (size) − n) endif

Definition: integer-to-nat (n, size) = if negativep (n) then twoto (size) − negative-guts (n)

else n endif

Theorem: upper-bound-on-bv-to-nat bv-to-nat (a) < twoto (bv-size (a))

Theorem: bv-to-nat-to-integer-lemma2 bv-bit (a) = if bv-size (a) ≃ 0 then f

else bv-to-nat (a) ≮ twoto (bv-size (a) − 1) endif

Theorem: nat-to-bv-of-trunc (bitvecp (a) ∧ boolp (b)) → (bv-to-nat (a) = (bv-to-nat (bitvec (b, a)) mod twoto (bv-size (a))))

Theorem: tcp-tc-to-integer tcp (tc-to-integer (n))

Theorem: upper-bound-on-non-negative-bv-to-nat (bitvecp (a) ∧ (a ≠ bv-nil) ∧ (¬ bv-bit (a))) → (bv-to-nat (a) < twoto (bv-size (a) − 1))

Theorem: lower-bound-on-negative-bv-to-nat (bitvecp (a) ∧ (a ≠ bv-nil) ∧ bv-bit (a)) → (bv-to-nat (a) ≮ twoto (bv-size (a) − 1))

Theorem: integer-in-rangep-of-tc-to-integer (n = bv-size (a)) → (tc-in-rangep (tc-to-integer (a), n) = (bitvecp (a) ∧ (a ≠ bv-nil)))

Theorem: plus-to-add (tcp (x) ∧ tcp (y) ∧ tc-in-rangep (x, n) ∧ tc-in-rangep (y, n)) → (nat-to-integer ((carry (c)

+ integer-to-nat (x, n)

+ integer-to-nat (y, n)) mod twoto (n), n)

= if tc-in-rangep (add (x, add (y, carry (c))), n) then add (x, add (y, carry (c))) elseif negativep (add (x, add (y, carry (c)))) then add (x, add (y, add (carry (c), twoto (n)))) else add (x, add (y, add (carry (c), − twoto (n)))) endif)

Theorem: times-2-twoto (a ∈ N) → ((2 ∗ twoto (a)) = twoto (1 + a))

Event: Disable times-2-twoto.

Theorem: bv-to-nat-to-integer tc-to-integer (a) = nat-to-integer (bv-to-nat (a), bv-size (a))

Event: Disable bv-to-nat-to-integer.

Theorem: tc-to-integer-to-nat (n = bv-size (a)) → (bv-to-nat (a) = integer-to-nat (tc-to-integer (a), n))

Event: Disable tc-to-integer-to-nat.

Theorem: bit-on-implies-non-0 bv-bit (a) → (bv-to-nat (a) ≠ 0)

Definition: bv-adder (a, b, cin) = if bitvecp (a)

∧ bitvecp (b)

∧ (bv-size (a) = bv-size (b))

∧ boolp (cin) then if a = bv-nil then bitvec-carry-ovf (bv-nil, cin, f)

else bitvec-carry-ovf (bitvec (exor (exor (bv-bit (a), bv-bit (b)),

bvco-carry (bv-adder (bv-vec (a), bv-vec (b), cin))),

bvco-bitvec (bv-adder (bv-vec (a), bv-vec (b), cin))),

(bv-bit (a) ∧ bv-bit (b))

∨ (bv-bit (a)

∧ bvco-carry (bv-adder (bv-vec (a), bv-vec (b), cin)))

∨ (bv-bit (b)

∧ bvco-carry (bv-adder (bv-vec (a), bv-vec (b), cin))),

bvco-carry (bv-adder (bv-vec (a), bv-vec (b), cin))) endif

else bvco-nil endif

Theorem: size-bv-adder (bitvecp (a) ∧ bitvecp (b) ∧ boolp (cin) ∧ (bv-size (a) = bv-size (b))) → (bv-size (bvco-bitvec (bv-adder (a, b, cin))) = bv-size (a))

Theorem: bv-adder-plusses (bitvecp (a) ∧ bitvecp (b) ∧ boolp (cin) ∧ (bv-size (a) = bv-size (b))) → (bv-to-nat (bitvec (bvco-carry (bv-adder (a, b, cin)),

bvco-bitvec (bv-adder (a, b, cin))))

= (bv-to-nat (a) + bv-to-nat (b) + carry (cin)))

Theorem: bv-adder-non-nil (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b)) ∧ boolp (cin) ∧ (a ≠ bv-nil) ∧ (b ≠ bv-nil)) → ((bvco-bitvec (bv-adder (a, b, cin)) = bv-nil) = f)

Theorem: nat-interpretation-of-bv-adder-output (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b)) ∧ boolp (cin)) → (bv-to-nat (bvco-bitvec (bv-adder (a, b, cin)))

= ((bv-to-nat (a) + bv-to-nat (b) + carry (cin))

mod twoto (bv-size (a))))

Event: Disable nat-interpretation-of-bv-adder-output.

Theorem: integer-interpretation-of-bv-adder-output-lemma1 (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b)) ∧ boolp (cin)) → (tc-to-integer (bvco-bitvec (bv-adder (a, b, cin)))

= nat-to-integer ((bv-to-nat (a) + bv-to-nat (b) + carry (cin)) mod twoto (bv-size (a)), bv-size (a)))

Theorem: integer-interpretation-of-bv-adder-output (bitvecp (a) ∧ bitvecp (b) ∧ (a ≠ bv-nil) ∧ boolp (cin) ∧ (b ≠ bv-nil) ∧ (bv-size (a) = bv-size (b))) → (tc-to-integer (bvco-bitvec (bv-adder (a, b, cin)))

= if tc-in-rangep (add (tc-to-integer (a),

add (tc-to-integer (b), carry (cin))), bv-size (a))

then add (tc-to-integer (a), add (tc-to-integer (b), carry (cin))) elseif negativep (add (tc-to-integer (a),

add (tc-to-integer (b), carry (cin))))

then add (tc-to-integer (a),

add (tc-to-integer (b),

add (carry (cin), twoto (bv-size (a)))))

else add (tc-to-integer (a),

add (tc-to-integer (b), add (carry (cin), − twoto (bv-size (a))))) endif)

Event: Disable integer-interpretation-of-bv-adder-output-lemma1.

Event: Disable integer-interpretation-of-bv-adder-output.

Definition: alucod-fc (ik, ip, cc) = ((ik ∧ (¬ ip)) ∨ (ip ∧ (¬ cc)))

Theorem: boolp-alucod-fc boolp (alucod-fc (k, p, c))

Definition: alucev-fc (ik, ip, cc) = (((¬ ik) ∧ (¬ ip)) ∨ (ip ∧ (¬ cc)))

Theorem: boolp-alucev-fc boolp (alucev-fc (k, p, c))

Definition: addbyp-fcout (cinshot, prop1 , prop2 , prop3 , prop4 , cinnorm) = if prop1 ∧ prop2 ∧ prop3 ∧ prop4 then cinshot

else cinnorm endif

Definition: c4 (cp1 , cp2 , cp3 , cp4 , ck1 , ck2 , ck3 , ck4 , cin)

= if boolp (cp1 )

∧ boolp (cp2 ) ∧ boolp (cp3 ) ∧ boolp (cp4 ) ∧ boolp (ck1 ) ∧ boolp (ck2 ) ∧ boolp (ck3 ) ∧ boolp (ck4 ) ∧ boolp (cin)

then bitvec-carry-ovf (bitvec (alucod-fc (ck2 , cp2 , alucev-fc (ck3 ,

cp3 ,

alucod-fc (ck4 , cp4 , cin))),

bitvec (alucev-fc (ck3 , cp3 , alucod-fc (ck4 , cp4 , cin)),

bitvec (alucod-fc (ck4 , cp4 , cin), bitvec (cin, bv-nil)))),

alucev-fc (ck1 , cp1 , alucod-fc (ck2 ,

cp2 ,

alucev-fc (ck3 , cp3 , alucod-fc (ck4 ,

cp4 , cin)))),

alucod-fc (ck2 , cp2 , alucev-fc (ck3 ,

cp3 ,

alucod-fc (ck4 , cp4 , cin))))

else bvco-nil endif

Definition: c4byp (cp1 , cp2 , cp3 , cp4 , ck1 , ck2 , ck3 , ck4 , cin) = if boolp (cp1 )

∧ boolp (cp2 ) ∧ boolp (cp3 ) ∧ boolp (cp4 ) ∧ boolp (ck1 )

∧ boolp (ck2 ) ∧ boolp (ck3 ) ∧ boolp (ck4 ) ∧ boolp (cin)

then bitvec-carry-ovf (bitvec (alucod-fc (ck2 , cp2 , alucev-fc (ck3 ,

cp3 ,

alucod-fc (ck4 , cp4 , cin))),

bitvec (alucev-fc (ck3 , cp3 , alucod-fc (ck4 , cp4 , cin)),

bitvec (alucod-fc (ck4 , cp4 , cin),

bitvec (cin, bv-nil)))),

addbyp-fcout (cin, cp4 , cp3 , cp2 , cp1 , alucev-fc (ck1 ,

cp1 ,

alucod-fc (ck2 , cp2 , alucev-fc (ck3 ,

cp3 ,

alucod-fc (ck4 , cp4 , cin))))),

alucod-fc (ck2 , cp2 , alucev-fc (ck3 ,

cp3 ,

alucod-fc (ck4 , cp4 , cin))))

else bvco-nil endif

Theorem: c4-c4byp-help (boolp (ck1 ) ∧ boolp (ck2 ) ∧ boolp (ck3 ) ∧ boolp (ck4 ) ∧ boolp (cp1 ) ∧ boolp (cp2 )

∧ boolp (cp3 ) ∧ boolp (cp4 ) ∧ boolp (cin)) → (addbyp-fcout (cin,

cp4 , cp3 , cp2 , cp1 , alucev-fc (ck1 ,

cp1 ,

alucod-fc (ck2 , cp2 , alucev-fc (ck3 ,

cp3 ,

alucod-fc (ck4 , cp4 , cin)))))

= alucev-fc (ck1 , cp1 , alucod-fc (ck2 ,

cp2 ,

alucev-fc (ck3 , cp3 , alucod-fc (ck4 , cp4 , cin)))))

Theorem: c4-c4byp-relate (boolp (p1 ) ∧ boolp (p2 ) ∧ boolp (p3 ) ∧ boolp (p4 ) ∧ boolp (k1 ) ∧ boolp (k2 ) ∧ boolp (k3 ) ∧ boolp (k4 ) ∧ boolp (cin)) → (c4byp (p1 , p2 , p3 , p4 , k1 , k2 , k3 , k4 , cin)

= c4 (p1 , p2 , p3 , p4 , k1 , k2 , k3 , k4 , cin))

Event: Disable c4.

Event: Disable c4byp.

Event: Disable c4-c4byp-help.

Definition: carry-col (ik, ip, ccin) = if bitvecp (ik)

∧ bitvecp (ip) ∧ boolp (ccin) ∧ (bv-size (ik) = bv-size (ip))

then if ik = bv-nil then bitvec-carry-ovf (bv-nil, ccin, f)

else bitvec-carry-ovf (bitvec (bvco-carry (carry-col (bv-vec (ik), bv-vec (ip), ccin)),

bvco-bitvec (carry-col (bv-vec (ik), bv-vec (ip), ccin))),

if evenp (bv-size (ik))

then alucev-fc (bv-bit (ik), bv-bit (ip), bvco-carry (carry-col (bv-vec (ik),

bv-vec (ip), ccin)))

else alucod-fc (bv-bit (ik), bv-bit (ip), bvco-carry (carry-col (bv-vec (ik),

bv-vec (ip), ccin))) endif,

bvco-carry (carry-col (bv-vec (ik), bv-vec (ip), ccin))) endif

else bvco-nil endif

Theorem: size-carry-col (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b)) ∧ boolp (ccin)) → (bv-size (bvco-bitvec (carry-col (a, b, ccin))) = bv-size (a))

Definition: up (nb) = ((4 ∗ ((nb − 10) ÷ 4)) + 9)

Definition: carry-col2 (ik, ip, ccin, nb) = if bitvecp (ik)

∧ bitvecp (ip) ∧ boolp (ccin) ∧ (bv-size (ik) = bv-size (ip)) ∧ evenp (nb)

then if ik = bv-nil then bitvec-carry-ovf (bv-nil, ccin, f)

elseif (bv-size (ik) < up (nb))

∧ (11 < nb)

∧ (4 < bv-size (ik)) ∧ evenp (bv-size (ik))

then bitvec-carry-ovf (bv-append (bvco-bitvec (c4 (bv-bit (ip), bv-bit (bv-vec (ip)), bv-bit (bv-vec (bv-vec (ip))), bv-bit (bv-vec (bv-vec (bv-vec (ip)))), bv-bit (ik), bv-bit (bv-vec (ik)), bv-bit (bv-vec (bv-vec (ik))), bv-bit (bv-vec (bv-vec (bv-vec (ik)))), bvco-carry (carry-col2 (bv-vec (bv-vec (bv-vec (bv-vec (ik)))),

bv-vec (bv-vec (bv-vec (bv-vec (ip)))), ccin, nb)))),

bvco-bitvec (carry-col2 (bv-vec (bv-vec (bv-vec (bv-vec (ik)))), bv-vec (bv-vec (bv-vec (bv-vec (ip)))), ccin, nb))),

bvco-carry (c4 (bv-bit (ip), bv-bit (bv-vec (ip)), bv-bit (bv-vec (bv-vec (ip))), bv-bit (bv-vec (bv-vec (bv-vec (ip)))), bv-bit (ik), bv-bit (bv-vec (ik)), bv-bit (bv-vec (bv-vec (ik))), bv-bit (bv-vec (bv-vec (bv-vec (ik)))), bvco-carry (carry-col2 (bv-vec (bv-vec (bv-vec (bv-vec (ik)))),

bv-vec (bv-vec (bv-vec (bv-vec (ip)))), ccin, nb)))),

bvco-carry (carry-col2 (bv-vec (ik), bv-vec (ip), ccin, nb)))

else bitvec-carry-ovf (bitvec (bvco-carry (carry-col2 (bv-vec (ik), bv-vec (ip), ccin, nb)),

bvco-bitvec (carry-col2 (bv-vec (ik), bv-vec (ip), ccin, nb))),

if evenp (bv-size (ik)) then alucev-fc (bv-bit (ik),

bv-bit (ip), bvco-carry (carry-col2 (bv-vec (ik),

bv-vec (ip), ccin, nb)))

else alucod-fc (bv-bit (ik), bv-bit (ip), bvco-carry (carry-col2 (bv-vec (ik),

bv-vec (ip), ccin, nb))) endif,

bvco-carry (carry-col2 (bv-vec (ik), bv-vec (ip), ccin, nb))) endif

else bvco-nil endif

Theorem: app-c4-carry1 (bitvecp (ik) ∧ bitvecp (ip) ∧ boolp (ccin) ∧ evenp (bv-size (ik)) ∧ (bv-size (ik) = bv-size (ip)) ∧ (4 < bv-size (ik))) → (bv-append (bvco-bitvec (c4 (bv-bit (ip),

bv-bit (bv-vec (ip)),

bv-bit (bv-vec (bv-vec (ip))),

bv-bit (bv-vec (bv-vec (bv-vec (ip)))),

bv-bit (ik),

bv-bit (bv-vec (ik)),

bv-bit (bv-vec (bv-vec (ik))),

bv-bit (bv-vec (bv-vec (bv-vec (ik)))),

bvco-carry (carry-col (bv-vec (bv-vec (bv-vec (bv-vec (ik)))), bv-vec (bv-vec (bv-vec (bv-vec (ip)))), ccin)))),

bvco-bitvec (carry-col (bv-vec (bv-vec (bv-vec (bv-vec (ik)))), bv-vec (bv-vec (bv-vec (bv-vec (ip)))), ccin)))

= bitvec (bvco-carry (carry-col (bv-vec (ik), bv-vec (ip), ccin)), bvco-bitvec (carry-col (bv-vec (ik), bv-vec (ip), ccin))))

Theorem: app-c4-carry2 (bitvecp (ik) ∧ bitvecp (ip) ∧ boolp (ccin) ∧ evenp (bv-size (ik)) ∧ (bv-size (ik) = bv-size (ip))

∧ (4 < bv-size (ik))) → (bvco-carry (c4 (bv-bit (ip),

bv-bit (bv-vec (ip)), bv-bit (bv-vec (bv-vec (ip))), bv-bit (bv-vec (bv-vec (bv-vec (ip)))), bv-bit (ik), bv-bit (bv-vec (ik)), bv-bit (bv-vec (bv-vec (ik))), bv-bit (bv-vec (bv-vec (bv-vec (ik)))), bvco-carry (carry-col (bv-vec (bv-vec (bv-vec (bv-vec (ik)))),

bv-vec (bv-vec (bv-vec (bv-vec (ip)))), ccin))))

= if evenp (bv-size (ik))

then alucev-fc (bv-bit (ik), bv-bit (ip), bvco-carry (carry-col (bv-vec (ik),

bv-vec (ip), ccin)))

else alucod-fc (bv-bit (ik), bv-bit (ip), bvco-carry (carry-col (bv-vec (ik),

bv-vec (ip), ccin))) endif)

Definition: induct-carry-col2 (ik, ip, ccin, nb) = if bitvecp (ik)

∧ bitvecp (ip) ∧ boolp (ccin) ∧ (bv-size (ik) = bv-size (ip)) ∧ evenp (nb)

then if ik = bv-nil then t

elseif (bv-size (ik) < up (nb))

∧ (11 < nb) ∧ (4 < bv-size (ik)) ∧ evenp (bv-size (ik))

then induct-carry-col2 (bv-vec (bv-vec (bv-vec (bv-vec (ik)))), bv-vec (bv-vec (bv-vec (bv-vec (ip)))), ccin, nb)

∧ induct-carry-col2 (bv-vec (ik), bv-vec (ip), ccin, nb) else induct-carry-col2 (bv-vec (ik), bv-vec (ip), ccin, nb) endif

else t endif

Theorem: carry2-carry-relate evenp (nb) → (carry-col2 (ik, ip, ccin, nb) = carry-col (ik, ip, ccin))

Definition: cbyp-col (ik, ip, ccin, nb) = if bitvecp (ik)

∧ bitvecp (ip) ∧ boolp (ccin) ∧ (bv-size (ik) = bv-size (ip)) ∧ evenp (nb)

then if ik = bv-nil then bitvec-carry-ovf (bv-nil, ccin, f)

elseif (bv-size (ik) < up (nb))

∧ (11 < nb) ∧ (4 < bv-size (ik)) ∧ evenp (bv-size (ik))

then bitvec-carry-ovf (bv-append (bvco-bitvec (c4byp (bv-bit (ip), bv-bit (bv-vec (ip)), bv-bit (bv-vec (bv-vec (ip))), bv-bit (bv-vec (bv-vec (bv-vec (ip)))), bv-bit (ik), bv-bit (bv-vec (ik)), bv-bit (bv-vec (bv-vec (ik))), bv-bit (bv-vec (bv-vec (bv-vec (ik)))), bvco-carry (cbyp-col (bv-vec (bv-vec (bv-vec (bv-vec (ik)))),

bv-vec (bv-vec (bv-vec (bv-vec (ip)))), ccin, nb)))),

bvco-bitvec (cbyp-col (bv-vec (bv-vec (bv-vec (bv-vec (ik)))), bv-vec (bv-vec (bv-vec (bv-vec (ip)))), ccin, nb))),

bvco-carry (c4byp (bv-bit (ip), bv-bit (bv-vec (ip)), bv-bit (bv-vec (bv-vec (ip))), bv-bit (bv-vec (bv-vec (bv-vec (ip)))), bv-bit (ik), bv-bit (bv-vec (ik)), bv-bit (bv-vec (bv-vec (ik))), bv-bit (bv-vec (bv-vec (bv-vec (ik)))), bvco-carry (cbyp-col (bv-vec (bv-vec (bv-vec (bv-vec (ik)))),

bv-vec (bv-vec (bv-vec (bv-vec (ip)))), ccin, nb)))),

bvco-carry (cbyp-col (bv-vec (ik), bv-vec (ip), ccin, nb)))

else bitvec-carry-ovf (bitvec (bvco-carry (cbyp-col (bv-vec (ik), bv-vec (ip), ccin, nb)),

bvco-bitvec (cbyp-col (bv-vec (ik), bv-vec (ip), ccin, nb))),

if evenp (bv-size (ik))

then alucev-fc (bv-bit (ik), bv-bit (ip), bvco-carry (cbyp-col (bv-vec (ik),

bv-vec (ip), ccin, nb)))

else alucod-fc (bv-bit (ik), bv-bit (ip), bvco-carry (cbyp-col (bv-vec (ik),

bv-vec (ip), ccin, nb))) endif,

bvco-carry (cbyp-col (bv-vec (ik), bv-vec (ip), ccin, nb))) endif

else bvco-nil endif

Theorem: cbyp-carry2-relate cbyp-col (ik, ip, ccin, nb) = carry-col2 (ik, ip, ccin, nb)

Theorem: cbyp-carry-relate evenp (nb) → (cbyp-col (k, p, cin, nb) = carry-col (k, p, cin))

Event: Disable cbyp-carry2-relate.

Event: Disable carry2-carry-relate.

Definition: alugen-o (ct3 , ct2 , ct1 , ct0 , ia, ib) = if falsep (ia)

then if falsep (ib) then ¬ ct2 else ¬ ct3 endif elseif falsep (ib) then ¬ ct1 else ¬ ct0 endif

Definition: alugenod-o (ct3 , ct2 , ct1 , ct0 , ia, ib) = if falsep (ia)

then if falsep (ib) then ¬ ct3

else ¬ ct2 endif elseif falsep (ib) then ¬ ct0 else ¬ ct1 endif

Theorem: alugen-alugenod-relate alugen-o (ct3 , ct2 , ct1 , ct0 , a, b) = alugenod-o (ct3 , ct2 , ct1 , ct0 , a, ¬ b)

Theorem: alugenodo-func (boolp (a) ∧ boolp (b)) → ((alugenod-o (t, t, t, t, a, b) = f)

∧ (alugenod-o (t, t, t, f, a, b) = (a ∧ (¬ b))) ∧ (alugenod-o (t, t, f, t, a, b) = (a ∧ b)) ∧ (alugenod-o (t, t, f, f, a, b) = a) ∧ (alugenod-o (t, f, t, t, a, b) = ((¬ a) ∧ b)) ∧ (alugenod-o (t, f, t, f, a, b) = exor (a, b)) ∧ (alugenod-o (t, f, f, t, a, b) = b) ∧ (alugenod-o (t, f, f, f, a, b) = (a ∨ b)) ∧ (alugenod-o (f, t, t, t, a, b) = (¬ (a ∨ b))) ∧ (alugenod-o (f, t, t, f, a, b) = (¬ b)) ∧ (alugenod-o (f, t, f, t, a, b) = (¬ exor (a, b))) ∧ (alugenod-o (f, t, f, f, a, b) = (a ∨ (¬ b))) ∧ (alugenod-o (f, f, t, t, a, b) = (¬ a)) ∧ (alugenod-o (f, f, t, f, a, b) = (¬ (a ∧ b))) ∧ (alugenod-o (f, f, f, t, a, b) = ((¬ a) ∨ b)) ∧ (alugenod-o (f, f, f, f, a, b) = t))

Definition: cscbi11 (input) = (¬ input)

Definition: cscbo11 (input) = (¬ input)

Definition: prop-col (ina, inb, cp) = if bitvecp (ina)

∧ bitvecp (inb) ∧ controlep (cp) ∧ (bv-size (ina) = bv-size (inb))

then if ina = bv-nil then bv-nil else bitvec (alugen-o (cscbi11 (bv-3 (cp)), cscbi11 (bv-2 (cp)), cscbi11 (bv-1 (cp)), cscbi11 (bv-0 (cp)), bv-bit (ina), bv-bit (inb)),

prop-col (bv-vec (ina), bv-vec (inb), cp)) endif

else bv-nil endif

Theorem: size-prop-col (controlep (cp) ∧ bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b))) → (bv-size (prop-col (a, b, cp)) = bv-size (a))

Theorem: prop-col-5 (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b))) → (prop-col (a, b, nat-to-bv (5, 4)) = bv-not (bv-exor (a, b)))

Theorem: prop-col-10 (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b))) → (prop-col (a, b, nat-to-bv (10, 4)) = bv-exor (a, b))

Theorem: prop-col-12 (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b))) → (prop-col (a, b, nat-to-bv (12, 4)) = bv-not (a))

Definition: kill-col (ina, inb, ck) = if bitvecp (ina)

∧ bitvecp (inb) ∧ controlep (ck) ∧ (bv-size (ina) = bv-size (inb))

then if ina = bv-nil then bv-nil

else bitvec (alugen-o (cscbi11 (bv-3 (ck)), cscbi11 (bv-2 (ck)), cscbi11 (bv-1 (ck)), cscbi11 (bv-0 (ck)), bv-bit (ina), bv-bit (inb)),

kill-col (bv-vec (ina), bv-vec (inb), ck)) endif

else bv-nil endif

Theorem: prop-kill-relate kill-col (a, b, control) = prop-col (a, b, control)

Theorem: size-kill-col (controlep (ck) ∧ bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b))) → (bv-size (kill-col (a, b, ck)) = bv-size (a))

Theorem: kill-col-12 (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b))) → (kill-col (a, b, nat-to-bv (12, 4)) = bv-not (a))

Event: Disable prop-kill-relate.

Definition: res-col (ina, inb, cr) = if bitvecp (ina)

∧ bitvecp (inb) ∧ controlep (cr) ∧ (bv-size (ina) = bv-size (inb)) then if ina = bv-nil then bv-nil

else bitvec (if evenp (bv-size (ina))

then alugenod-o (cscbi11 (bv-3 (cr)), cscbi11 (bv-2 (cr)), cscbi11 (bv-1 (cr)), cscbi11 (bv-0 (cr)), bv-bit (ina), bv-bit (inb))

else alugen-o (cscbi11 (bv-3 (cr)), cscbi11 (bv-2 (cr)), cscbi11 (bv-1 (cr)), cscbi11 (bv-0 (cr)), bv-bit (ina), bv-bit (inb)) endif, res-col (bv-vec (ina), bv-vec (inb), cr)) endif

else bv-nil endif

Theorem: size-res-col (controlep (cr) ∧ bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b))) → (bv-size (res-col (a, b, cr)) = bv-size (a))

Theorem: res-col-10 (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b))) → (res-col (a, b, nat-to-bv (10, 4)) = bv-exor (a, bv-invert-even (b)))

Theorem: lemma1 (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b)) ∧ controlep (cp) ∧ controlep (ck) ∧ boolp (ccin))

→ (bv-size (bvco-bitvec (carry-col (kill-col (a, b, ck), prop-col (a, b, cp), ccin))) = bv-size (prop-col (a, b, cp)))

Definition: rec-mcalu-imp (nb, byp, ina, inb, ck, cp, cr, ccin) = if evenp (nb)

∧ bitvecp (ina) ∧ bitvecp (inb) ∧ boolp (ccin) ∧ boolp (byp) ∧ (bv-size (ina) = bv-size (inb))

then if truep (byp)

then bitvec-carry-ovf (res-col (prop-col (ina, inb, cp),

bvco-bitvec (cbyp-col (kill-col (ina, inb, ck),

prop-col (ina, inb, cp),

ccin, nb)),

cr), bvco-carry (cbyp-col (kill-col (ina, inb, ck),

prop-col (ina, inb, cp), ccin, nb)),

bvco-ovf (cbyp-col (kill-col (ina, inb, ck), prop-col (ina, inb, cp), ccin, nb)))

else bitvec-carry-ovf (res-col (prop-col (ina, inb, cp),

bvco-bitvec (carry-col (kill-col (ina, inb, ck),

prop-col (ina, inb, cp),

ccin)),

cr), bvco-carry (carry-col (kill-col (ina,

inb, ck),

prop-col (ina, inb,

cp),

ccin)),

bvco-ovf (carry-col (kill-col (ina, inb, ck),

prop-col (ina, inb, cp),

ccin))) endif

else bvco-nil endif

Definition: csexor (a, b) = exor (a, b)

Definition: mcalu (nb, byp, ina, inb, ck, cp, cr, ccin) = if evenp (nb)

∧ bitvecp (ina) ∧ bitvecp (inb) ∧ boolp (ccin) ∧ boolp (byp) ∧ controlep (ck) ∧ controlep (cp) ∧ controlep (cr) ∧ (bv-size (ina) = bv-size (inb))

then carry-sign-ovf-bitvec (cscbo11 (bvco-carry (rec-mcalu-imp (nb, byp ∧ (11 < nb), ina, inb, ck, cp, cr, cscbi11 (ccin)))),

cscbo11 (bv-bit (bvco-bitvec (rec-mcalu-imp (nb, byp ∧ (11 < nb), ina, inb, ck, cp, cr, cscbi11 (ccin))))),

csexor (bvco-carry (rec-mcalu-imp (nb, byp ∧ (11 < nb), ina, inb, ck, cp, cr, cscbi11 (ccin))),

bvco-ovf (rec-mcalu-imp (nb, byp ∧ (11 < nb), ina, inb, ck, cp, cr, cscbi11 (ccin)))),

bvco-bitvec (rec-mcalu-imp (nb, byp ∧ (11 < nb), ina, inb, ck, cp, cr, cscbi11 (ccin))))

else csobv-nil endif

Definition: induct-vec-vec-evenp-f (a, b, c) = if bitvecp (a)

∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b)) ∧ boolp (c)

then if a = bv-nil then t elseif evenp (bv-size (a)) then induct-vec-vec-evenp-f (bv-vec (a), bv-vec (b), c) else induct-vec-vec-evenp-f (bv-vec (a), bv-vec (b), c) endif

else t endif

Theorem: the-proof (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b)) ∧ boolp (cin)) → (bvco-carry (carry-col (bv-not (a), bv-exor (a, b), cin))

= if evenp (bv-size (a)) then bvco-carry (bv-adder (a, b, cin)) else ¬ bvco-carry (bv-adder (a, b, cin)) endif)

Theorem: the-proof-part2 (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b)) ∧ boolp (cin)) → (bv-exor (bv-exor (a, b),

bv-invert-even (bvco-bitvec (carry-col (bv-not (a), bv-exor (a, b),

cin))))

= bvco-bitvec (bv-adder (a, b, cin)))

Theorem: the-proof-part3 (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b)) ∧ boolp (cin)) → (bvco-ovf (carry-col (bv-not (a), bv-exor (a, b), cin))

= if evenp (bv-size (a))

then if a = bv-nil then f

else ¬ bvco-ovf (bv-adder (a, b, cin)) endif else bvco-ovf (bv-adder (a, b, cin)) endif)

Theorem: rec-mcalu-imp-bv-adder-relate (bitvecp (a) ∧ bitvecp (b) ∧ boolp (cin) ∧ boolp (byp) ∧ (bv-size (a) = bv-size (b)) ∧ evenp (nb) ∧ (bv-size (a) = nb)) → (bvco-bitvec (rec-mcalu-imp (nb,

byp, a, b, nat-to-bv (12, 4), nat-to-bv (10, 4), nat-to-bv (10, 4), cin))

= bvco-bitvec (bv-adder (a, b, cin)))

Theorem: mcalu-imp-bv-adder-relate (bitvecp (a) ∧ bitvecp (b) ∧ boolp (cin) ∧ boolp (byp) ∧ (bv-size (a) = bv-size (b)) ∧ evenp (nb) ∧ (bv-size (a) = nb)) → (csobv-bitvec (mcalu (nb,

byp, a, b, nat-to-bv (12, 4), nat-to-bv (10, 4), nat-to-bv (10, 4), cin))

= bvco-bitvec (bv-adder (a, b, ¬ cin)))

Theorem: boolp-not boolp (¬ a)

Theorem: tc-interpretation-of-mcalu-output (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b)) ∧ boolp (cin) ∧ boolp (byp) ∧ evenp (nb) ∧ (bv-size (a) = nb) ∧ (a ≠ bv-nil) ∧ (b ≠ bv-nil)) → (tc-to-integer (csobv-bitvec (mcalu (nb,

byp, a, b, nat-to-bv (12, 4), nat-to-bv (10, 4), nat-to-bv (10, 4), cin)))

= if tc-in-rangep (add (tc-to-integer (a),

add (tc-to-integer (b), carry (¬ cin))), bv-size (a))

then add (tc-to-integer (a),

add (tc-to-integer (b), carry (¬ cin)))

elseif negativep (add (tc-to-integer (a),

add (tc-to-integer (b), carry (¬ cin))))

then add (tc-to-integer (a),

add (tc-to-integer (b),

add (carry (¬ cin), twoto (bv-size (a)))))

else add (tc-to-integer (a),

add (tc-to-integer (b), add (carry (¬ cin), − twoto (bv-size (a))))) endif)

Theorem: bv-to-nat-of-bv-not bv-to-nat (bv-not (a)) = ((twoto (bv-size (a)) − 1) − bv-to-nat (a))

Definition: tc-minus (a) = if negativep (a) then negative-guts (a)

elseif a ≃ 0 then 0 else − a endif Theorem: bit-of-bv-not (bitvecp (a) ∧ (a ≠ bv-nil)) → (bv-bit (bv-not (a)) = (¬ bv-bit (a)))

Theorem: equal-difference-0 ((x − y) = 0) = (y ≮ x)

Theorem: top-bit-off-implies-smaller (bitvecp (a) ∧ (a ≠ bv-nil) ∧ (¬ bv-bit (a))) → (bv-to-nat (a) < (twoto (bv-size (a)) − 1))

Theorem: tc-minus-tc-to-integer (bitvecp (a) ∧ (a ≠ bv-nil)) → (tc-minus (tc-to-integer (a))

= if tc-to-integer (a) = 0 then 0 else add (1, tc-to-integer (bv-not (a))) endif)

Definition: tc-fix (x) = if tcp (x) then x

else 0 endif

Theorem: tcp-add (tcp (x) → tcp (add (x, y))) ∧ (tcp (y) → tcp (add (x, y)))

Theorem: add-0 add (0, x) = tc-fix (x)

Theorem: add-1-1 add (1, add (-1, x)) = tc-fix (x)

Theorem: tc-to-integer-0 (bitvecp (a) ∧ (a ≠ bv-nil) ∧ (tc-to-integer (a) = 0)) → (tc-to-integer (bv-not (a)) = -1)

Theorem: bv-not-bv-exor-right bv-not (bv-exor (a, b)) = bv-exor (a, bv-not (b))

Theorem: bv-not-nil (bitvecp (a) ∧ (a ≠ bv-nil)) → (bv-not (a) ≠ bv-nil)

Theorem: tc-to-integer-bv-not (bitvecp (b) ∧ (b ≠ bv-nil)) → (tc-to-integer (bv-not (b)) = add (tc-minus (tc-to-integer (b)), -1))

Theorem: carry-not carry (¬ a) = add (1, tc-minus (carry (a)))

Theorem: tcp-tc-minus tcp (tc-minus (a))

Theorem: mcalu-12-5-10-mcalu-12-10-10-relate (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b)) ∧ evenp (nb) ∧ boolp (byp) ∧ boolp (cin)) → (mcalu (nb,

byp, a, b, nat-to-bv (12, 4), nat-to-bv (5, 4), nat-to-bv (10, 4), cin) = mcalu (nb,

byp, a, bv-not (b), nat-to-bv (12, 4), nat-to-bv (10, 4), nat-to-bv (10, 4), cin))

Theorem: tcp-twoto tcp (twoto (a))

Theorem: tcp-minus-twoto (a ∈ N) → tcp (− twoto (a))

Theorem: tc-interpretation-of-mcalu-imp-add (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b)) ∧ (a ≠ bv-nil) ∧ (b ≠ bv-nil) ∧ boolp (byp) ∧ evenp (nb) ∧ (bv-size (a) = nb)) → (tc-to-integer (csobv-bitvec (mcalu (nb,

byp, a, b, nat-to-bv (12, 4), nat-to-bv (10, 4), nat-to-bv (10, 4), t)))

= if tc-in-rangep (add (tc-to-integer (a), tc-to-integer (b)),

bv-size (a))

then add (tc-to-integer (a), tc-to-integer (b)) elseif negativep (add (tc-to-integer (a), tc-to-integer (b))) then add (tc-to-integer (a),

add (tc-to-integer (b), twoto (bv-size (a))))

else add (tc-to-integer (a), add (tc-to-integer (b), − twoto (bv-size (a)))) endif)

Theorem: tc-interpretation-of-mcalu-imp-xsub (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b)) ∧ (a ≠ bv-nil) ∧ (b ≠ bv-nil) ∧ boolp (cin) ∧ boolp (byp) ∧ evenp (nb) ∧ (bv-size (a) = nb)) → (tc-to-integer (csobv-bitvec (mcalu (nb,

byp, a, b, nat-to-bv (12, 4), nat-to-bv (5, 4), nat-to-bv (10, 4), cin)))

= if tc-in-rangep (add (tc-to-integer (a),

add (tc-minus (tc-to-integer (b)),

tc-minus (carry (cin)))),

bv-size (a))

then add (tc-to-integer (a),

add (tc-minus (tc-to-integer (b)), tc-minus (carry (cin))))

elseif negativep (add (tc-to-integer (a),

add (tc-minus (tc-to-integer (b)),

tc-minus (carry (cin)))))

then add (tc-to-integer (a),

add (tc-minus (tc-to-integer (b)), add (tc-minus (carry (cin)), twoto (bv-size (a))))) else add (tc-to-integer (a),

add (tc-minus (tc-to-integer (b)), add (tc-minus (carry (cin)),

− twoto (bv-size (a))))) endif)

Theorem: tc-interpretation-of-mcalu-imp-sub (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b)) ∧ (a ≠ bv-nil) ∧ (b ≠ bv-nil) ∧ boolp (byp) ∧ evenp (nb) ∧ (bv-size (a) = nb)) → (tc-to-integer (csobv-bitvec (mcalu (nb,

byp, a, b, nat-to-bv (12, 4), nat-to-bv (5, 4), nat-to-bv (10, 4), f)))

= if tc-in-rangep (add (tc-to-integer (a),

tc-minus (tc-to-integer (b))), bv-size (a))

then add (tc-to-integer (a), tc-minus (tc-to-integer (b))) elseif negativep (add (tc-to-integer (a),

tc-minus (tc-to-integer (b))))

then add (tc-to-integer (a),

add (tc-minus (tc-to-integer (b)), twoto (bv-size (a))))

else add (tc-to-integer (a),

add (tc-minus (tc-to-integer (b)), − twoto (bv-size (a)))) endif)

Theorem: bv-adder-non-nil2 (bitvecp (a) ∧ bitvecp (b) ∧ (bv-size (a) = bv-size (b)) ∧ boolp (cin) ∧ (a ≠ bv-nil)) → ((bvco-bitvec (bv-adder (a, b, cin)) = bv-nil) = f)

Definition: last (it) = if bitvecp (it) ∧ (it ≠ bv-nil) then if bv-vec (it) = bv-nil then bv-bit (it)

else last (bv-vec (it)) endif else f endif

Definition: butlast (it) = if bitvecp (it) ∧ (it ≠ bv-nil)

then if bv-vec (it) = bv-nil then bv-nil

else bitvec (bv-bit (it), butlast (bv-vec (it))) endif else bv-nil endif

Definition: do-shift-1 (it, shiftin) = if bitvecp (it) ∧ (it ≠ bv-nil) ∧ boolp (shiftin)

then bitvec (shiftin, butlast (it))

else bv-nil endif

Definition: up-shift-1 (it, shiftin) = if bitvecp (it) ∧ (it ≠ bv-nil) ∧ boolp (shiftin)

then bv-append (bv-vec (it), bitvec (shiftin, bv-nil)) else bv-nil endif

Definition: do-shift-n (n, it, shiftin) = if (n ∈ N) ∧ bitvecp (it) ∧ boolp (shiftin)

then if n ≃ 0 then it

else do-shift-1 (do-shift-n (n − 1, it, shiftin), shiftin) endif else bv-nil endif

Definition: up-shift-n (n, it, shiftin) = if (n ∈ N) ∧ bitvecp (it) ∧ boolp (shiftin)

then if n ≃ 0 then it

else up-shift-1 (up-shift-n (n − 1, it, shiftin), shiftin) endif else bv-nil endif

Theorem: size-bv-append (bitvecp (a) ∧ bitvecp (b)) → (bv-size (bv-append (a, b)) = (bv-size (a) + bv-size (b)))

Theorem: append-not-nil (bitvecp (a) ∧ bitvecp (b) ∧ (a ≠ bv-nil)) → ((bv-append (a, b) = bv-nil) = f)

Theorem: vec-append ((a ≠ bv-nil) ∧ bitvecp (a) ∧ bitvecp (b)) → (bv-vec (bv-append (a, b)) = bv-append (bv-vec (a), b))

Theorem: size-up-shift-1 boolp (shiftin) → (bv-size (up-shift-1 (it, shiftin)) = bv-size (it))

Theorem: size-up-shift-n (boolp (shiftin) ∧ (n ∈ N)) → (bv-size (up-shift-n (n, it, shiftin)) = bv-size (it))

Theorem: size-do-shift-n (boolp (shiftin) ∧ (n ∈ N)) → (bv-size (do-shift-n (n, it, shiftin)) = bv-size (it))

Theorem: bv-append-not-not (bitvecp (a) ∧ bitvecp (b)) → (bv-not (bv-append (a, b)) = bv-append (bv-not (a), bv-not (b)))

Theorem: up-shift-0 (bitvecp (it) ∧ boolp (sin)) → (up-shift-n (0, it, sin) = it)

Theorem: hack2 ((b ∈ N) ∧ (a ∈ N)) → ((a + (0 ∗ b)) = a)

Theorem: evenp-twoto (a ≄ 0) → evenp (twoto (a))

Theorem: evenp-plus ((a ∈ N) ∧ (b ∈ N) ∧ evenp (a) ∧ evenp (b)) → evenp (a + b)

Theorem: evenp-plus-extended ((a ∈ N) ∧ (b ∈ N)) → (evenp (a + b)

= if evenp (a) then evenp (b) else ¬ evenp (b) endif)

Theorem: do-shift-strict do-shift-n (n, bv-nil, sin) = bv-nil

Theorem: do-shift-0 (bitvecp (it) ∧ boolp (sin)) → (do-shift-n (0, it, sin) = it)

Definition: mult (a, b) = if negativep (a)

then if negativep (b) then negative-guts (a) ∗ negative-guts (b)

else tc-minus (negative-guts (a) ∗ b) endif elseif negativep (b) then tc-minus (a ∗ negative-guts (b)) else a ∗ b endif Theorem: tcp-mult tcp (mult (a, b))

Theorem: commutativity2-of-mult mult (x, mult (y, z)) = mult (y, mult (x, z))

Theorem: commutativity-of-mult mult (x, y) = mult (y, x)

Theorem: associativity-of-mult mult (mult (x, y), z) = mult (x, mult (y, z))

Theorem: bv-to-nat-bv-append (bitvecp (a) ∧ bitvecp (b)) → (bv-to-nat (bv-append (a, b))

= ((bv-to-nat (a) ∗ twoto (bv-size (b))) + bv-to-nat (b)))

Theorem: bv-to-nat-of-vec bv-to-nat (bv-vec (a)) = if bv-bit (a) then add (bv-to-nat (a), − twoto (bv-size (bv-vec (a))))

else bv-to-nat (a) endif

Theorem: times-difference (a ∗ (x − y)) = ((a ∗ x) − (a ∗ y))

Theorem: not-bit-implies-in-range-times-2 (¬ bv-bit (a)) → ((2 ∗ bv-to-nat (a)) < twoto (bv-size (a)))

Theorem: remainder-natural-interpretation-of-up-shift-1 bv-to-nat (up-shift-1 (it, f)) = ((bv-to-nat (it) ∗ 2) mod twoto (bv-size (it)))

Theorem: remainder-remainder ((e mod b) mod b) = (e mod b)

Theorem: remainder-diff (a ≮ b) → (((a − b) mod b) = (a mod b))

Theorem: remainder-diff-times (x ≮ (n ∗ b)) → (((x − (n ∗ b)) mod b) = (x mod b))

Definition: abs (a) = if a ∈ N then a

elseif negativep (a) then negative-guts (a)

else 0 endif Definition: divide (a, b) = if negativep (a)

then if negativep (b) then negative-guts (a) ÷ negative-guts (b)

else tc-minus (negative-guts (a) ÷ b) endif elseif negativep (b) then tc-minus (a ÷ negative-guts (b)) else a ÷ b endif

Theorem: tcp-divide tcp (divide (a, b))

Theorem: hackxaux ((w ∈ N) ∧ (w < b) ∧ (z ∈ N) ∧ (z < c) ∧ (c ∈ N) ∧ (c ≠ 0) ∧ (b ≠ 0) ∧ (b ∈ N)) → ((z + (c ∗ w)) < (b ∗ c))

Theorem: times-to-mult-1 (tcp (x) ∧ tc-in-rangep (x, z)) → (nat-to-integer ((2 ∗ integer-to-nat (x, z)) mod twoto (z), z)

= if tc-in-rangep (mult (2, x), z) then mult (2, x) elseif negativep (mult (2, x)) then add (mult (2, x), twoto (z)) else add (mult (2, x), − twoto (z)) endif)

Theorem: integer-interpretation-of-up-shift-1 (bitvecp (it) ∧ (it ≠ bv-nil)) → (tc-to-integer (up-shift-1 (it, f))

= if tc-in-rangep (mult (tc-to-integer (it), 2), bv-size (it)) then mult (tc-to-integer (it), 2) elseif negativep (mult (tc-to-integer (it), 2)) then add (mult (tc-to-integer (it), 2), twoto (bv-size (it))) else add (mult (tc-to-integer (it), 2),

− twoto (bv-size (it))) endif)

Theorem: lessp-plus-1 ((a + c) < (b + c)) = (a < b)

Theorem: lessp-plus-1-commuted ((a + c) < (c + b)) = (a < b)

Theorem: lessp-plus-2 (b < c) → ((a < (c − b)) = ((a + b) < c))

Theorem: equal-diff-twoto (twoto (a) − (twoto (a − 1) + b)) = ((twoto (a) ÷ 2) − b)

Theorem: evenp-times-even (evenp (a) ∨ evenp (b)) → evenp (a ∗ b)

Theorem: real-hack-1 ((z < 2) ∧ evenp (z + (2 ∗ a))) → ((z + (2 ∗ a)) = (2 ∗ a))

Theorem: real-hack-6 ((w < 2) ∧ (¬ evenp (w))) → ((w − 1) = 0)

Theorem: not-even-add1-commuted ((a ∈ N) ∧ (¬ evenp (1 + a))) → evenp (a)

Theorem: evenp-add1-commuted evenp (1 + a) → (¬ evenp (a))

Definition: multiplep (a, n) = ((a mod n) ≃ 0)

Theorem: negative-guts-tc-minus (a ∈ N) → (negative-guts (tc-minus (a)) = a)

Definition: invert-lsb (it) = bv-append (butlast (it), bitvec (¬ last (it), bv-nil))

Theorem: lsb-implies-odd last (it) = (¬ evenp (bv-to-nat (it)))

Theorem: bv-bit-of-bv-append (bitvecp (a) ∧ (a ≠ bv-nil) ∧ bitvecp (b)) → (bv-bit (bv-append (a, b)) = bv-bit (a))

Theorem: butlast-bv-append (bitvecp (b) ∧ (b ≠ bv-nil)) → (butlast (bv-append (a, b)) = bv-append (a, butlast (b)))

Theorem: bv-append-of-bv-nil bitvecp (a) → (bv-append (a, bv-nil) = a)

Theorem: up-shift-1-invert-lsb (bitvecp (it) ∧ (it ≠ bv-nil)) → (up-shift-1 (it, t) = invert-lsb (up-shift-1 (it, f)))

Theorem: last-of-bv-append (bitvecp (a) ∧ bitvecp (b) ∧ (b ≠ bv-nil)) → (last (bv-append (a, b)) = last (b))

Theorem: quotient-diff-times ((x − (i ∗ j )) ÷ j ) = if j ≃ 0 then 0

else (x ÷ j ) − i endif

Theorem: times-quotient-lessp-relate (a < (b ∗ c)) → ((a ÷ b) < c)

Definition: induct-quot-quot (x, y, b) = if b ≃ 0 then t

elseif x < b then t

else induct-quot-quot (x − b, y − b, b) endif

Theorem: quotient-lessp ((x ∈ N) ∧ (y ∈ N) ∧ (x ≮ y)) → ((x ÷ b) ≮ (y ÷ b))

Theorem: times-quotient-lessp-relate-dual ((a ∈ N) ∧ (b ∈ N) ∧ (c ∈ N) ∧ (b ≠ 0) ∧ (a ≮ (b ∗ c))) → ((a ÷ b) ≮ c)

Definition: new-r (i, r, noem) = if (noem ∈ N) = (r ∈ N)

then add (r, tc-minus (mult (noem, twoto (i − 1)))) else add (r, mult (noem, twoto (i − 1))) endif

Definition: anrd (i, r, noem) = if i ≃ 0 then bv-nil

else bitvec ((noem ∈ N) = (new-r (i, r, noem) ∈ N), anrd (i − 1, new-r (i, r, noem), noem)) endif

Theorem: tcp-new-r tcp (new-r (i, r, noem))

Theorem: size-anrd-bv bv-size (anrd (i, r, noem)) = fix (i)

Theorem: anrd-i-0 (i ≃ 0) → (tc-to-integer (anrd (i, tel, noem)) = 0)

Theorem: quotient-times-lessp ((a ∈ N) ∧ (b ∈ N) ∧ (c ∈ N) ∧ (b ≠ 0)) → ((a < (b ∗ c)) = ((a ÷ b) < c))

Theorem: quotient-times-commuted ((j ∗ i) ÷ i) = if i ≃ 0 then 0

else fix (j ) endif

Theorem: multiplep-diff ((a ≮ j ) ∧ multiplep (a, j )) → multiplep (a − j , j )

Theorem: q-d-t-lemma1 ((a ∈ N) ∧ (a ≠ 0)) → (((a − 1) ÷ j )

= if multiplep (a, j ) then (a ÷ j ) − 1 else a ÷ j endif)

Theorem: q-d-t-lemma2 ((i ∈ N) ∧ (j ∈ N) ∧ (j ≠ 0)) → ((((i ∗ j ) − 1) ÷ j ) = (i − 1))

Theorem: q-d-t-lemma3 ((j ∈ N) ∧ (j ≠ 0) ∧ (x ∈ N) ∧ (x ≠ 0) ∧ (x < j )) → ((((i ∗ j ) − x) ÷ j ) = (i − 1))

Theorem: quotient-diff-times-commuted (((i ∗ j ) − x) ÷ j ) = if j ≃ 0 then 0

elseif multiplep (x, j ) then i − (x ÷ j )

else (i − (x ÷ j )) − 1 endif

Definition: imultiplep (a, b) = if a ∈ N

then if b ∈ N then multiplep (a, b)

else multiplep (a, negative-guts (b)) endif elseif b ∈ N then multiplep (negative-guts (a), b) else multiplep (negative-guts (a), negative-guts (b)) endif

Theorem: imultiplep-add (tcp (a) ∧ tcp (b) ∧ (x ∈ N) ∧ imultiplep (a, b)) → imultiplep (add (a, mult (b, twoto (x))), b)

Theorem: tc-minus-mult tc-minus (mult (a, b)) = mult (tc-minus (a), b)

Theorem: multiplep-tc-minus imultiplep (a, tc-minus (b)) = imultiplep (a, b)

Theorem: imultiplep-new-r (tcp (r) ∧ tcp (n) ∧ (i ∈ N) ∧ imultiplep (r, n)) → imultiplep (new-r (i, r, n), n)

Theorem: remainder-diff-times-commuted ((a ∈ N) ∧ (x ∈ N) ∧ (b ∈ N) ∧ (x < b) ∧ ((a ∗ b) ≮ x)) → ((((a ∗ b) − x) mod b)

= if x = 0 then 0 else b − x endif)

Definition: times-times-induct (a, b, c) = if b ≃ 0 then t

else times-times-induct (a, b − 1, c − 1) endif

Theorem: not-equal-times-0 ((a ∈ N) ∧ (b ∈ N) ∧ (a ≠ 0) ∧ (b ≠ 0)) → ((0 ∗ a) ≠ (a ∗ b))

Theorem: equal-times-times ((a ∈ N) ∧ (b ∈ N) ∧ (c ∈ N) ∧ (a ≠ 0)) → (((a ∗ b) = (a ∗ c)) = (b = c))

Theorem: hack-around-next-lemma ((w ∈ N) ∧ (z ∈ N) ∧ (z < b) ∧ (v ∈ N) ∧ (b ≠ 0) ∧ (b ∈ N) ∧ (w ≠ 0) ∧ (z ≠ 0) ∧ ((b + (b ∗ w)) ≮ (z + (b ∗ v))) ∧ ((b ∗ w) < (z + (b ∗ v)))) → (((1 + v) − 1) = w)

Theorem: lower-upper-determines ((a ∈ N) ∧ (b ∈ N) ∧ (a ≠ 0) ∧ (a ≠ 1) ∧ (x ∈ N)

∧ (x ≠ 0) ∧ ((x mod b) ≠ 0) ∧ ((a ∗ b) ≮ x) ∧ (((a − 1) ∗ b) < x)) → ((1 + (x ÷ b)) = a)

Theorem: remainder-diff-times-commuted-2 ((a ∈ N) ∧ (x ∈ N) ∧ (b ∈ N) ∧ (x ≮ b) ∧ ((a ∗ b) ≮ x)) → ((((a ∗ b) − x) mod b)

= if (x mod b) = 0 then 0 else b − (x mod b) endif)

Theorem: not-imultiplep-add (tcp (a) ∧ tcp (b) ∧ (x ∈ N) ∧ (¬ imultiplep (a, b))) → (¬ imultiplep (add (a, mult (b, twoto (x))), b))

Theorem: not-imultiplep-new-r (tcp (n) ∧ tcp (r) ∧ (i ∈ N) ∧ (¬ imultiplep (r, n))) → (¬ imultiplep (new-r (i, r, n), n))

Theorem: unfold-positive-tc-to-integer ((tc-to-integer (a) = b) ∧ (b ∈ N)) → (tc-to-integer (a) = bv-to-nat (a))

Theorem: unfold-negative-tc-to-integer ((tc-to-integer (a) = b) ∧ negativep (b)) → (tc-to-integer (a) = add (tc-minus (twoto (bv-size (a))), bv-to-nat (a)))

Definition: div-in-rangep (tel, noem, i) = if tel ∈ N

then if noem ∈ N then tel < (twoto (i − 1) ∗ noem)

else tel < (twoto (i − 1) ∗ negative-guts (noem)) endif elseif noem ∈ N then (twoto (i − 1) ∗ noem) ≮ negative-guts (tel) else (twoto (i − 1) ∗ negative-guts (noem))

≮ negative-guts (tel) endif

Theorem: div-in-rangep-new-r-sign-1 (div-in-rangep (tel, noem, i) ∧ (tel ∈ N) ∧ (noem ∈ N)) → negativep (add (tel, tc-minus (mult (noem, twoto (i − 1)))))

Theorem: div-in-rangep-new-r-sign-2 (div-in-rangep (tel, noem, i) ∧ (tel ∈ N) ∧ negativep (noem)) → negativep (add (tel, mult (noem, twoto (i − 1))))

Theorem: div-in-rangep-new-r-sign-3 (div-in-rangep (tel, noem, i) ∧ negativep (tel) ∧ (noem ∈ N)) → (add (tel, mult (noem, twoto (i − 1))) ∈ N)

Theorem: div-in-rangep-new-r-sign-4 (div-in-rangep (tel, noem, i) ∧ negativep (tel) ∧ negativep (noem)) → (add (tel, tc-minus (mult (noem, twoto (i − 1)))) ∈ N)

Theorem: quotient-diff-times-dual ((x − (j ∗ i)) ÷ j ) = if j ≃ 0 then 0

else (x ÷ j ) − i endif

Theorem: quotient-diff-times-commuted-dual (((j ∗ i) − x) ÷ j ) = if j ≃ 0 then 0

elseif multiplep (x, j ) then i − (x ÷ j )

else (i − (x ÷ j )) − 1 endif

Theorem: sub1-difference ((a − b) − 1) = ((a − 1) − b)

Theorem: quotient-times-lessp-refrased ((a ∈ N) ∧ (b ∈ N) ∧ (c ∈ N) ∧ (b ≠ 0)) → (((a ÷ b) < c) = (a < (b ∗ c)))

Event: Disable quotient-times-lessp.

Theorem: difference-1 (x − 1) = (x − 1)

Theorem: may-be-baby ((x ∈ N) ∧ (y ∈ N) ∧ (z ∈ N) ∧ (y ≠ 0) ∧ (x < (z ∗ y))) → ((z − 1) ≮ (x ÷ y))

Theorem: may-be-baby-2 ((x ∈ N) ∧ (y ∈ N) ∧ (z ∈ N) ∧ (y ≠ 0) ∧ ((y ∗ z) ≮ x)) → (z ≮ (x ÷ y))

Theorem: may-be-baby-3 (negativep (x) ∧ (negative-guts (x) ≠ 0) ∧ (y ∈ N) ∧ (z ∈ N) ∧ (y ≠ 0)

∧ ((negative-guts (x) mod y) ≠ 0) ∧ ((y ∗ z) ≮ negative-guts (x)) ∧ ((negative-guts (x) ÷ y) = 0) ∧ (z < 1)) → (divide ((y ∗ z) − negative-guts (x), y) = add (− (1 − z), 0))

Theorem: may-be-baby-4 ((x ∈ N) ∧ (y ∈ N) ∧ (z ∈ N) ∧ (z ≮ 1) ∧ (x ≠ 0) ∧ (y ≠ 0) ∧ ((y ∗ z) ≮ x) ∧ ((x mod y) ≠ 0)) → ((z − 1) ≮ (x ÷ y))

Theorem: may-be-baby-5 ((x ∈ N) ∧ (x ≠ 0) ∧ (y ∈ N) ∧ (y ≠ 0) ∧ (y ≮ x) ∧ ((x mod y) ≠ 0)) → ((x ÷ y) = 0)

Theorem: may-be-baby-6 (negativep (x) ∧ (negative-guts (x) ≠ 0) ∧ negativep (y) ∧ (negative-guts (y) ≠ 0) ∧ negativep (z) ∧ (negative-guts (z) ≠ 0) ∧ ((negative-guts (x) mod negative-guts (y)) ≠ 0) ∧ ((negative-guts (y) ∗ negative-guts (z)) ≮ negative-guts (x)) ∧ (1 < negative-guts (z))) → (divide ((negative-guts (y) ∗ negative-guts (z)) − negative-guts (x),

y) = add (negative-guts (x) ÷ negative-guts (y), − (negative-guts (z) − 1)))

Theorem: equal-times-times-commuted ((a ∈ N) ∧ (b ∈ N) ∧ (c ∈ N) ∧ (a ≠ 0)) → (((a ∗ b) = (c ∗ a)) = (b = c))

Theorem: divide-add-mult (tcp (x) ∧ tcp (y) ∧ tcp (z)) → (divide (add (x, mult (y, z)), y)

= if y = 0 then 0 elseif imultiplep (x, y) then add (divide (x, y), z) elseif x ∈ N then if add (x, mult (y, z)) ∈ N then add (divide (x, y), z) elseif y ∈ N then add (divide (x, y), add (z, 1)) else add (divide (x, y), add (z, -1)) endif

elseif negativep (add (x, mult (y, z))) then add (divide (x, y), z) elseif y ∈ N then add (divide (x, y), add (z, -1)) else add (divide (x, y), add (z, 1)) endif)

Theorem: div-in-range-sign-new-r-1 ((tel ∈ N) ∧ (noem ∈ N) ∧ div-in-rangep (tel, noem, i)) → negativep (new-r (i, tel, noem))

Theorem: div-in-range-sign-new-r-2 ((tel ∈ N) ∧ negativep (noem) ∧ div-in-rangep (tel, noem, i)) → negativep (new-r (i, tel, noem))

Theorem: div-in-range-sign-new-r-3 (negativep (tel) ∧ (noem ∈ N) ∧ div-in-rangep (tel, noem, i)) → (new-r (i, tel, noem) ∈ N)

Theorem: div-in-range-sign-new-r-4 (negativep (tel) ∧ negativep (noem) ∧ div-in-rangep (tel, noem, i)) → (new-r (i, tel, noem) ∈ N)

Theorem: elim-hyp-1a-3aa (tcp (x) ∧ negativep (x) ∧ (y ∈ N) ∧ (y ≠ 0) ∧ imultiplep (x, y)) → negativep (divide (x, y))

Theorem: elim-hyp-1a-3ab (negativep (x) ∧ (y ∈ N)) → negativep (add (-1, divide (x, y)))

Theorem: transfer-add (tcp (b) ∧ tcp (c)) → ((add (a, b) = c) = (b = add (c, tc-minus (a))))

Theorem: equal-multiplep-r-new-r (tcp (r) ∧ tcp (n) ∧ (i ∈ N)) → (imultiplep (new-r (i, r, n), n) = imultiplep (r, n))

Theorem: add-a-minus-a add (a, tc-minus (a)) = 0 Theorem: tc-minus-tc-minus-a tc-minus (tc-minus (a)) = tc-fix (a)

Theorem: elim-hyp-1a-3ba (negativep (x) ∧ (n ∈ N) ∧ (n ≠ 0) ∧ (i ∈ N) ∧ ((n ∗ twoto (i − 1)) ≮ negative-guts (x))) → (add (divide (x, n), twoto (i − 1)) ∈ N)

Theorem: elim-hyp-1a-3bb (negativep (x) ∧ (n ∈ N) ∧ (n ≠ 0) ∧ (i ∈ N) ∧ ((n ∗ twoto (i − 1)) ≮ negative-guts (x)) ∧ (¬ imultiplep (x, n))) → (add (divide (x, n), add (-1, twoto (i − 1))) ∈ N)

Theorem: elim-hyp-1a-3c ((r ∈ N) ∧ (n ∈ N) ∧ (i ∈ N) ∧ (n ≠ 0) ∧ div-in-rangep (r, n, i)) → ((n ∗ twoto (i − 1)) ≮ negative-guts (new-r (i, r, n)))

Theorem: div-not-in-range-sign-new-r-1 ((r ∈ N) ∧ (n ∈ N) ∧ (i ∈ N) ∧ (n ≠ 0) ∧ (¬ div-in-rangep (r, n, i))) → (new-r (i, r, n) ∈ N)

Theorem: elim-hyp-1b-1a ((x ∈ N) ∧ (y ∈ N)) → (divide (x, y) ∈ N)

Theorem: elim-hyp-1b-1b ((x ∈ N) ∧ (n ∈ N) ∧ (x < (n ∗ twoto (i − 1)))) → negativep (add (divide (x, n), tc-minus (twoto (i − 1))))

Theorem: elim-hyp-1b-1c ((r ∈ N) ∧ (n ∈ N) ∧ (i ∈ N) ∧ (n ≠ 0) ∧ (r < (n ∗ twoto (i)))) → (new-r (i, r, n) < (n ∗ twoto (i − 1)))

Theorem: elim-hyp-1c ((r ∈ N)

∧ (n ∈ N) ∧ (i ∈ N) ∧ (n ≠ 0) ∧ (i ≠ 0) ∧ (r ≮ (n ∗ twoto (i)))) → (new-r (i, r, n) ≮ (n ∗ twoto (i − 1)))

Theorem: elim-hyp-2a-4aa ((r ∈ N) ∧ tcp (n) ∧ negativep (n) ∧ div-in-rangep (r, n, i) ∧ imultiplep (new-r (i, r, n), n)) → (add (divide (new-r (i, r, n), n), -1) ∈ N)

Theorem: elim-hyp-2a-4ab ((r ∈ N) ∧ tcp (n) ∧ negativep (n) ∧ div-in-rangep (r, n, i)) → (divide (new-r (i, r, n), n) ∈ N)

Theorem: remainder-0-implies ((a ∈ N) ∧ (b ∈ N) ∧ (c ∈ N) ∧ (a ≠ 0) ∧ ((c mod a) = 0) ∧ ((a ∗ b) = c)) → ((c ÷ a) = b)

Theorem: elim-hyp-2a-4ba (negativep (x) ∧ tcp (n) ∧ negativep (n) ∧ imultiplep (x, n) ∧ ((negative-guts (n) ∗ twoto (i − 1)) ≮ negative-guts (x))) → negativep (add (divide (x, n), add (-1, tc-minus (twoto (i − 1)))))

Theorem: equal-times-ab-c-equal-rem-ca-0 ((a ∈ N) ∧ (b ∈ N) ∧ (c ∈ N) ∧ (a ≠ 0) ∧ ((a ∗ b) = c)) → ((c mod a) = 0)

Theorem: elim-hyp-2a-4bb (negativep (x) ∧ tcp (n) ∧ negativep (n) ∧ (¬ imultiplep (x, n)) ∧ ((negative-guts (n) ∗ twoto (i − 1)) ≮ negative-guts (x))) → negativep (add (divide (x, n), tc-minus (twoto (i − 1))))

Theorem: elim-hyp-2a-4c ((r ∈ N) ∧ tcp (n) ∧ negativep (n) ∧ div-in-rangep (r, n, i)) → ((negative-guts (n) ∗ twoto (i − 1)) ≮ negative-guts (new-r (i, r, n)))

Theorem: div-not-in-range-sign-new-r-2 ((r ∈ N) ∧ tcp (n) ∧ negativep (n) ∧ (i ∈ N) ∧ (¬ div-in-rangep (r, n, i))) → (new-r (i, r, n) ∈ N)

Theorem: elim-hyp-2b-2a ((x ∈ N) ∧ negativep (n)) → negativep (add (-1, divide (x, n)))

Theorem: elim-hyp-2b-2b ((x ∈ N) ∧ negativep (n) ∧ (i ∈ N) ∧ (x < (twoto (i − 1) ∗ negative-guts (n)))) → (add (divide (x, n), add (-1, twoto (i − 1))) ∈ N)

Theorem: elim-hyp-3aab-1c (tcp (r) ∧ negativep (r) ∧ (n ∈ N) ∧ (n ≠ 0) ∧ div-in-rangep (r, n, i) ∧ (i ∈ N)) → (new-r (i, r, n) < (twoto (i − 1) ∗ n))

Theorem: div-not-in-range-sign-new-r-3 (tcp (r) ∧ negativep (r) ∧ (n ∈ N) ∧ (i ∈ N) ∧ (n ≠ 0) ∧ (¬ div-in-rangep (r, n, i))) → negativep (new-r (i, r, n))

Theorem: elim-hyp-3ba-3c (tcp (r) ∧ negativep (r) ∧ (n ∈ N) ∧ (n ≠ 0)

∧ (i ∈ N) ∧ ((twoto (i) ∗ n) ≮ negative-guts (r))) → ((twoto (i − 1) ∗ n) ≮ negative-guts (new-r (i, r, n)))

Theorem: elim-hyp-3c-3c (tcp (r) ∧ negativep (r) ∧ (n ∈ N) ∧ (n ≠ 0) ∧ (i ∈ N) ∧ ((n ∗ twoto (i)) < negative-guts (r)) ∧ (i ≠ 0)) → ((n ∗ twoto (i − 1)) < negative-guts (new-r (i, r, n)))

Theorem: elim-hyp-4aa-2c (tcp (r) ∧ negativep (r) ∧ tcp (n) ∧ negativep (n) ∧ div-in-rangep (r, n, i) ∧ (i ∈ N)) → (new-r (i, r, n) < (twoto (i − 1) ∗ negative-guts (n)))

Theorem: div-not-in-range-sign-new-r-4 (tcp (r) ∧ negativep (r) ∧ tcp (n) ∧ negativep (n) ∧ (i ∈ N) ∧ (¬ div-in-rangep (r, n, i))) → negativep (new-r (i, r, n))

Theorem: elim-hyp-4ba-4c (tcp (r) ∧ negativep (r) ∧ tcp (n) ∧ negativep (n) ∧ (i ∈ N) ∧ ((twoto (i) ∗ negative-guts (n)) ≮ negative-guts (r))) → ((twoto (i − 1) ∗ negative-guts (n)) ≮ negative-guts (new-r (i, r, n)))

Theorem: elim-hyp-4c-4c (tcp (r) ∧ negativep (r) ∧ tcp (n)

∧ negativep (n) ∧ (i ∈ N) ∧ (i ≠ 0) ∧ ((twoto (i) ∗ negative-guts (n)) < negative-guts (r))) → ((twoto (i − 1) ∗ negative-guts (n)) < negative-guts (new-r (i, r, n)))

Theorem: r-lessp-2n-quotient-1 ((n ≠ 0) ∧ (r ≮ n) ∧ (r < (2 ∗ n))) → ((r ÷ n) = 1)

Theorem: r-lessp-equal-2n-quotient-2-aux ((n ∈ N) ∧ (n ≠ 0) ∧ (n < r) ∧ ((2 ∗ n) ≮ r) ∧ ((r mod n) = 0)) → ((2 ∗ n) = r)

Theorem: r-lessp-equal-2n-quotient-2 ((n ∈ N) ∧ (n ≠ 0) ∧ (n < r) ∧ ((2 ∗ n) ≮ r) ∧ ((r mod n) = 0)) → ((r ÷ n) = 2)

Theorem: not-lessp-x-n-equal-quotient-1 ((x ∈ N) ∧ (x ≠ 0) ∧ (n ∈ N) ∧ (n ≠ 0) ∧ (n ≮ x) ∧ ((x mod n) = 0)) → ((x ÷ n) = 1)

Theorem: remainder-times-commuted ((j ∗ i) mod i) = 0

Theorem: anrd-integer-ok-i-1 (tcp (r) ∧ tcp (n) ∧ (n ≠ 0) ∧ (i = 1)) → (tc-to-integer (anrd (i, r, n))

= if i = 0 then 0 elseif r ∈ N then if n ∈ N

then if div-in-rangep (r, n, i) then divide (r, n) elseif r < (n ∗ twoto (i)) then add (divide (r, n), tc-minus (twoto (i))) else -1 endif

elseif div-in-rangep (r, n, i) then add (divide (r, n), -1) elseif r < (negative-guts (n) ∗ twoto (i)) then add (divide (r, n), add (twoto (i), -1)) else 0 endif

elseif n ∈ N then if div-in-rangep (r, n, i)

then if imultiplep (r, n) then divide (r, n)

else add (divide (r, n), -1) endif elseif (n ∗ twoto (i)) ≮ negative-guts (r) then if imultiplep (r, n) then add (divide (r, n), twoto (i))

else add (divide (r, n), add (twoto (i), -1)) endif else 0 endif

elseif div-in-rangep (r, n, i) then if imultiplep (r, n) then add (divide (r, n), -1)

else divide (r, n) endif elseif (negative-guts (n) ∗ twoto (i)) ≮ negative-guts (r) then if imultiplep (r, n)

then add (divide (r, n), add (tc-minus (twoto (i)), -1)) else add (divide (r, n), tc-minus (twoto (i))) endif

else -1 endif)

Theorem: elim-hyp-2b-2c-corr ((r ∈ N) ∧ tcp (n) ∧ negativep (n) ∧ (r < (twoto (i) ∗ negative-guts (n)))) → (new-r (i, r, n) < (twoto (i − 1) ∗ negative-guts (n)))

Theorem: elim-hyp-2c-2c-corr ((r ∈ N) ∧ tcp (n) ∧ negativep (n) ∧ (i ∈ N) ∧ (i ≠ 0) ∧ (r ≮ (twoto (i) ∗ negative-guts (n)))) → (new-r (i, r, n) ≮ (twoto (i − 1) ∗ negative-guts (n)))

Theorem: lessp-twoto-sub1 ((i ∈ N) ∧ ((n ∗ twoto (i)) < x)) → ((n ∗ twoto (i − 1)) < x)

Theorem: elim-hyp-4ba-4aa-corr-aux ((r ∈ N) ∧ (n ∈ N)

∧ (n ≠ 0) ∧ (r ≠ 0) ∧ ((r mod n) = 0) ∧ ((n ∗ i) < r) ∧ (i ≠ 0) ∧ (i ∈ N)) → (((r ÷ n) − i) ≮ 1)

Theorem: elim-hyp-4ba-4aa-corr (tcp (r) ∧ negativep (r) ∧ tcp (n) ∧ negativep (n) ∧ imultiplep (r, n) ∧ (¬ div-in-rangep (r, n, i))) → (add (divide (new-r (i, r, n), n), -1) ∈ N)

Theorem: elim-hyp-4bb-4ab-corr (tcp (r) ∧ negativep (r) ∧ tcp (n) ∧ negativep (n) ∧ (¬ div-in-rangep (r, n, i))) → (divide (new-r (i, r, n), n) ∈ N)

Theorem: anrd-integer-ok (tcp (r) ∧ tcp (n) ∧ (n ≠ 0) ∧ (i ∈ N)) → (tc-to-integer (anrd (i, r, n))

= if i = 0 then 0 elseif r ∈ N then if n ∈ N

then if div-in-rangep (r, n, i) then divide (r, n)

elseif r < (n ∗ twoto (i))

then add (divide (r, n), tc-minus (twoto (i))) else -1 endif

elseif div-in-rangep (r, n, i) then add (divide (r, n), -1) elseif r < (negative-guts (n) ∗ twoto (i)) then add (divide (r, n), add (twoto (i), -1)) else 0 endif

elseif n ∈ N

then if div-in-rangep (r, n, i)

then if imultiplep (r, n) then divide (r, n) else add (divide (r, n), -1) endif elseif (n ∗ twoto (i)) ≮ negative-guts (r) then if imultiplep (r, n) then add (divide (r, n), twoto (i))

else add (divide (r, n), add (twoto (i), -1)) endif else 0 endif elseif div-in-rangep (r, n, i) then if imultiplep (r, n) then add (divide (r, n), -1)

else divide (r, n) endif elseif (negative-guts (n) ∗ twoto (i)) ≮ negative-guts (r) then if imultiplep (r, n)

then add (divide (r, n), add (tc-minus (twoto (i)), -1)) else add (divide (r, n), tc-minus (twoto (i))) endif

else -1 endif)

Definition: long-new-r (r, noem) = if (noem ∈ N) = (r ∈ N) then add (r, tc-minus (noem))

else add (r, noem) endif

Theorem: tcp-long-new-r (tcp (tel) ∧ tcp (noem)) → tcp (long-new-r (tel, noem))

Definition: long-nrd (i, r, noem) = if i ≃ 0 then bv-nil

else bitvec ((noem ∈ N) = (long-new-r (r, noem) ∈ N), long-nrd (i − 1, mult (2, long-new-r (r, noem)), noem)) endif

Definition: alt-long-new-r (r, noem) = if (r ∈ N) = (noem ∈ N) then add (mult (2, r), tc-minus (noem))

else add (mult (2, r), noem) endif

Definition: alt-long-nrd (i, r, noem) = if i ≃ 0 then bv-nil

else bitvec ((noem ∈ N) = (alt-long-new-r (r, noem) ∈ N), alt-long-nrd (i − 1, alt-long-new-r (r, noem), noem)) endif

Theorem: alt-long-new-r-long-new-r-relate tcp (r) → (alt-long-new-r (r, n) = long-new-r (mult (2, r), n))

Definition: induct-fn (i, r, n) = if i ≃ 0 then t

else induct-fn (i − 1, long-new-r (mult (2, r), n), n) endif

Theorem: alt-long-nrd-long-nrd-relate (tcp (r) ∧ tcp (n)) → (alt-long-nrd (i, r, n) = long-nrd (i, mult (2, r), n))

Definition: bv-long-new-r (r, noem, prev) = if bv-bit (noem) = prev

then csobv-bitvec (mcalu (bv-size (r), f, r, noem, nat-to-bv (12, 4), nat-to-bv (5, 4), nat-to-bv (10, 4), f))

else csobv-bitvec (mcalu (bv-size (r), f, r, noem, nat-to-bv (12, 4), nat-to-bv (10, 4), nat-to-bv (10, 4), t)) endif

Definition: bv-long-nrd (i, r, noem, prev) = if i ≃ 0 then bv-nil

else bitvec (bv-bit (noem)

= bv-bit (bv-long-new-r (r, noem, prev)), bv-long-nrd (i − 1,

up-shift-1 (bv-long-new-r (r, noem, prev), f), noem, bv-bit (bv-long-new-r (r, noem, prev)))) endif

Definition: alt-bv-long-new-r (r, noem) = if bv-bit (noem) = bv-bit (r)

then csobv-bitvec (mcalu (bv-size (r), f, up-shift-1 (r, f), noem, nat-to-bv (12, 4), nat-to-bv (5, 4), nat-to-bv (10, 4), f))

else csobv-bitvec (mcalu (bv-size (r), f, up-shift-1 (r, f), noem, nat-to-bv (12, 4), nat-to-bv (10, 4), nat-to-bv (10, 4), t)) endif

Theorem: bv-size-alt-long-new-r (bitvecp (r) ∧ bitvecp (noem) ∧ (bv-size (r) = bv-size (noem)) ∧ evenp (bv-size (r)) ∧ (noem ≠ bv-nil)) → (bv-size (alt-bv-long-new-r (r, noem)) = bv-size (r))

Definition: alt-bv-long-nrd (i, r, noem) = if i ≃ 0 then bv-nil

else bitvec (bv-bit (noem) = bv-bit (alt-bv-long-new-r (r, noem)),

alt-bv-long-nrd (i − 1, alt-bv-long-new-r (r, noem), noem)) endif

Theorem: alt-bv-long-new-r-bv-long-new-r-relate alt-bv-long-new-r (r, n) = bv-long-new-r (up-shift-1 (r, f), n, bv-bit (r))

Theorem: alt-bv-long-nrd-bv-long-nrd-relate alt-bv-long-nrd (i, r, n) = bv-long-nrd (i, up-shift-1 (r, f), n, bv-bit (r))

Theorem: equal-bit-implies-equal-numberp ((tc-to-integer (a) ∈ N) = (tc-to-integer (b) ∈ N)) = (bv-bit (a) = bv-bit (b))

Theorem: equal-numberp-implies-tc-in-range-sub (((a ∈ N) = (b ∈ N)) ∧ tcp (a) ∧ tc-in-rangep (a, n) ∧ tcp (b) ∧ tc-in-rangep (b, n)) → tc-in-rangep (add (a, tc-minus (b)), n)

Theorem: not-equal-numberp-implies-tc-in-range-add (((a ∈ N) ≠ (b ∈ N)) ∧ tcp (a) ∧ tc-in-rangep (a, n) ∧ tcp (b) ∧ tc-in-rangep (b, n)) → tc-in-rangep (add (a, b), n)

Theorem: size-mcalu (bitvecp (a) ∧ bitvecp (b) ∧ boolp (byp) ∧ boolp (ccin) ∧ controlep (cr) ∧ (bv-size (a) = bv-size (b)) ∧ evenp (bv-size (a)) ∧ (b ≠ bv-nil) ∧ controlep (cp) ∧ controlep (ck)) → (bv-size (csobv-bitvec (mcalu (bv-size (a), byp, a, b, cp, ck, cr, ccin)))

= bv-size (a))

Theorem: tc-in-range-mult-2-tc-to-int-1 (tc-to-integer (tel) ∈ N) → ((2 ∗ tc-to-integer (tel)) < twoto (bv-size (tel)))

Theorem: special-francky-third-1 ((abs (tc-to-integer (noem)) ≮ abs (tc-to-integer (tel))) ∧ (¬ tc-in-rangep (mult (2, tc-to-integer (tel)), bv-size (tel))) ∧ (tc-to-integer (noem) ∈ N) ∧ (tc-to-integer (tel) ∈ N)) → (¬ tc-in-rangep (add (add (mult (2, tc-to-integer (tel)),

tc-minus (tc-to-integer (noem))), − twoto (bv-size (tel))),

bv-size (tel)))

Theorem: special-francky-third-1bis ((abs (tc-to-integer (noem)) ≮ abs (tc-to-integer (tel))) ∧ bitvecp (tel) ∧ bitvecp (noem) ∧ (¬ tc-in-rangep (mult (2, tc-to-integer (tel)), bv-size (tel))) ∧ (tc-to-integer (noem) ∈ N) ∧ (tc-to-integer (tel) ∈ N)) → negativep (add (add (mult (2, tc-to-integer (tel)),

tc-minus (tc-to-integer (noem))), − twoto (bv-size (tel))))

Theorem: special-francky-third-2 ((abs (tc-to-integer (noem)) ≮ abs (tc-to-integer (tel))) ∧ (¬ tc-in-rangep (mult (2, tc-to-integer (tel)), bv-size (tel))) ∧ negativep (tc-to-integer (noem)) ∧ (tc-to-integer (tel) ∈ N)) → (¬ tc-in-rangep (add (add (mult (2, tc-to-integer (tel)),

tc-to-integer (noem)), − twoto (bv-size (tel))),

bv-size (tel)))

Theorem: special-francky-third-2-bis ((abs (tc-to-integer (noem)) ≮ abs (tc-to-integer (tel))) ∧ bitvecp (tel) ∧ bitvecp (noem) ∧ (¬ tc-in-rangep (mult (2, tc-to-integer (tel)), bv-size (tel))) ∧ negativep (tc-to-integer (noem)) ∧ (tc-to-integer (tel) ∈ N)) → negativep (add (add (mult (2, tc-to-integer (tel)), tc-to-integer (noem)),

− twoto (bv-size (tel))))

Theorem: special-francky-third-3 ((abs (tc-to-integer (noem)) ≮ abs (tc-to-integer (tel))) ∧ (¬ tc-in-rangep (mult (2, tc-to-integer (tel)), bv-size (tel))) ∧ negativep (tc-to-integer (noem)) ∧ negativep (tc-to-integer (tel))) → (¬ tc-in-rangep (add (add (mult (2, tc-to-integer (tel)),

tc-minus (tc-to-integer (noem))), twoto (bv-size (tel))),

bv-size (tel)))

Theorem: special-francky-third-3-bis ((abs (tc-to-integer (noem)) ≮ abs (tc-to-integer (tel))) ∧ bitvecp (tel) ∧ bitvecp (noem) ∧ (¬ tc-in-rangep (mult (2, tc-to-integer (tel)), bv-size (tel))) ∧ negativep (tc-to-integer (noem)) ∧ negativep (tc-to-integer (tel))) → (add (add (mult (2, tc-to-integer (tel)), tc-minus (tc-to-integer (noem))),

twoto (bv-size (tel))) ∈ N)

Theorem: special-francky-third-4 ((abs (tc-to-integer (noem)) ≮ abs (tc-to-integer (tel))) ∧ (¬ tc-in-rangep (mult (2, tc-to-integer (tel)), bv-size (tel))) ∧ (tc-to-integer (noem) ∈ N) ∧ negativep (tc-to-integer (tel))) → (¬ tc-in-rangep (add (add (mult (2, tc-to-integer (tel)),

tc-to-integer (noem)), twoto (bv-size (tel))),

bv-size (tel)))

Theorem: special-francky-third-4-bis ((abs (tc-to-integer (noem)) ≮ abs (tc-to-integer (tel))) ∧ bitvecp (tel) ∧ bitvecp (noem) ∧ (¬ tc-in-rangep (mult (2, tc-to-integer (tel)), bv-size (tel))) ∧ (tc-to-integer (noem) ∈ N) ∧ negativep (tc-to-integer (tel))) → (add (add (mult (2, tc-to-integer (tel)), tc-to-integer (noem)),

twoto (bv-size (tel))) ∈ N)

Theorem: append-not-nil-2 bitvecp (a) → (bv-append (a, bitvec (x, bv-nil)) ≠ bv-nil)

Theorem: negativep-mult (tcp (x) ∧ negativep (x)) → negativep (mult (2, x))

Theorem: alt-bv-long-new-r-alt-long-new-r-relate (bitvecp (tel) ∧ bitvecp (noem) ∧ (bv-size (tel) = bv-size (noem)) ∧ (noem ≠ bv-nil) ∧ evenp (bv-size (tel)) ∧ (abs (tc-to-integer (noem)) ≮ abs (tc-to-integer (tel)))) → (tc-to-integer (alt-bv-long-new-r (tel, noem))

= alt-long-new-r (tc-to-integer (tel), tc-to-integer (noem)))

Theorem: special-francky-first-leq (tcp (tel) ∧ tcp (noem) ∧ (abs (noem) ≮ abs (tel))) → (abs (noem) ≮ abs (alt-long-new-r (tel, noem)))

Theorem: alt-bv-long-nrd-alt-long-nrd-relate (bitvecp (tel) ∧ bitvecp (n) ∧ (bv-size (tel) = bv-size (n)) ∧ (n ≠ bv-nil) ∧ evenp (bv-size (tel)) ∧ (abs (tc-to-integer (n)) ≮ abs (tc-to-integer (tel)))) → (alt-bv-long-nrd (i, tel, n)

= alt-long-nrd (i, tc-to-integer (tel), tc-to-integer (n)))

Definition: new-q (prev, noem) = (prev = bv-bit (noem))

Definition: new-z (z, noem, prev) = if prev = bv-bit (noem)

then csobv-bitvec (mcalu (bv-size (z), f, z, noem, nat-to-bv (12, 4), nat-to-bv (5, 4), nat-to-bv (10, 4), f))

else csobv-bitvec (mcalu (bv-size (z), f, z, noem, nat-to-bv (12, 4), nat-to-bv (10, 4), nat-to-bv (10, 4), t)) endif

Theorem: size-new-z (bitvecp (z) ∧ bitvecp (noem) ∧ (bv-size (noem) = bv-size (z)) ∧ evenp (bv-size (z)) ∧ (noem ≠ bv-nil)) → (bv-size (new-z (z, noem, prev)) = bv-size (z))

Definition: hard-anrd-it (i, noem, ps, z, prev) = if bitvecp (noem)

∧ bitvecp (ps) ∧ bitvecp (z) ∧ (bv-size (noem) = bv-size (ps)) ∧ (bv-size (noem) = bv-size (z)) ∧ boolp (prev) ∧ (i ∈ N)

then if i = 0 then bv-nil

else bitvec (new-q (bv-bit (new-z (z, noem, prev)), noem),

hard-anrd-it (i − 1, noem, up-shift-1 (ps, f), up-shift-1 (new-z (z, noem, prev), bv-bit (ps)), bv-bit (new-z (z, noem, prev)))) endif

else bv-nil endif

Definition: hard-anrd-init (i, l, tel, noem)

= hard-anrd-it (i, noem, up-shift-n (l, tel, f), do-shift-n (bv-size (tel) − l, tel, bv-bit (tel)), bv-bit (tel))

Theorem: hack-implies-sprop (t → (a = b)) = (a = b)

Theorem: adder-with-zero-bv bitvecp (x) → (bvco-bitvec (bv-adder (x, zero-bitvec (bv-size (x)), f)) = x)

Theorem: bv-append-bitvec (bitvecp (y) ∧ bitvecp (z)) → (bv-append (bitvec (x, y), z) = bitvec (x, bv-append (y, z)))

Theorem: carry-adder-with-zero-bv bitvecp (x) → (¬ bvco-carry (bv-adder (x, zero-bitvec (bv-size (x)), f)))

Theorem: bvco-carry-bit-adders-double-size (bitvecp (a) ∧ bitvecp (b) ∧ bitvecp (x) ∧ (bv-size (a) = bv-size (b))) → (bvco-carry (bv-adder (bv-append (a, x),

bv-append (b, zero-bitvec (bv-size (x))), f))

= bvco-carry (bv-adder (a, b, f)))

Theorem: bvco-bitvec-bit-adders-double-size (bitvecp (a) ∧ bitvecp (b) ∧ bitvecp (x) ∧ (bv-size (a) = bv-size (b))) → (bvco-bitvec (bv-adder (bv-append (a, x),

bv-append (b, zero-bitvec (bv-size (x))), f)) = bv-append (bvco-bitvec (bv-adder (a, b, f)), x))

Theorem: carry-adder-with-one-bv bitvecp (x) → bvco-carry (bv-adder (x, one-bitvec (bv-size (x)), t))

Theorem: adder-with-one-bv bitvecp (x) → (bvco-bitvec (bv-adder (x, one-bitvec (bv-size (x)), t)) = x)

Theorem: bvco-carry-bit-adders-double-size-t (bitvecp (a) ∧ bitvecp (b) ∧ bitvecp (x) ∧ (bv-size (a) = bv-size (b))) → (bvco-carry (bv-adder (bv-append (a, x),

bv-append (b, one-bitvec (bv-size (x))), t))

= bvco-carry (bv-adder (a, b, t)))

Theorem: bvco-bitvec-bit-adders-double-size-t (bitvecp (a) ∧ bitvecp (b) ∧ bitvecp (x) ∧ (bv-size (a) = bv-size (b))) → (bvco-bitvec (bv-adder (bv-append (a, x),

bv-append (b, one-bitvec (bv-size (x))), t)) = bv-append (bvco-bitvec (bv-adder (a, b, t)), x))

Theorem: not-zero-bv bv-not (zero-bitvec (nb)) = one-bitvec (nb)

Theorem: haiblnr-1 (bitvecp (ps) ∧ bitvecp (z) ∧ bitvecp (n) ∧ (bv-size (n) = bv-size (z)) ∧ (bv-size (ps) = bv-size (z)) ∧ (n ≠ bv-nil) ∧ evenp (bv-size (z))) → (bv-bit (new-z (z, n, prev))

= bv-bit (bv-long-new-r (bv-append (z, ps), bv-append (n, zero-bitvec (bv-size (z))), prev)))

Theorem: append-distributes (bitvecp (a) ∧ bitvecp (b) ∧ bitvecp (c)) → (bv-append (bv-append (a, b), c) = bv-append (a, bv-append (b, c)))

Theorem: haiblnr-2 (bitvecp (z) ∧ bitvecp (n) ∧ bitvecp (ps) ∧ boolp (prev) ∧ (bv-size (z) = bv-size (n)) ∧ (bv-size (z) = bv-size (ps)) ∧ (n ≠ bv-nil) ∧ evenp (bv-size (z))) → (bv-append (up-shift-1 (new-z (z, n, prev), bv-bit (ps)), up-shift-1 (ps, f))

= up-shift-1 (bv-long-new-r (bv-append (z, ps), bv-append (n, zero-bitvec (bv-size (z))), prev),

f))

Theorem: hard-anrd-it-bv-long-nrd-relate (bitvecp (ps) ∧ bitvecp (z)

∧ bitvecp (n) ∧ (bv-size (n) = bv-size (z)) ∧ (bv-size (ps) = bv-size (z)) ∧ (n ≠ bv-nil) ∧ evenp (bv-size (z)) ∧ boolp (prev) ∧ (i ∈ N)) → (hard-anrd-it (i, n, ps, z, prev)

= bv-long-nrd (i, bv-append (z, ps), bv-append (n, zero-bitvec (bv-size (z))), prev))

Theorem: numberp-mult (tcp (a) ∧ (b ∈ N) ∧ (b ≠ 0)) → ((mult (a, b) ∈ N) = (a ∈ N))

Theorem: long-new-r-new-r-relate ((i ∈ N) ∧ tcp (r) ∧ tcp (noem)) → (long-new-r (r, mult (noem, twoto (i − 1))) = new-r (i, r, noem))

Theorem: not-lessp-not-lessp-times ((x ∈ N) ∧ (x ≠ 0) ∧ (y ≮ z)) → ((x ∗ y) ≮ (x ∗ z))

Theorem: lessp-not-lessp-times (y < w) → ((v ∗ w) ≮ (v ∗ y))

Theorem: mult-add-distributes (tcp (x) ∧ tcp (y) ∧ tcp (z)) → (mult (x, add (y, z)) = add (mult (x, y), mult (x, z)))

Theorem: long-new-r-mult-2 (tcp (r) ∧ tcp (n)) → (long-new-r (mult (2, r), mult (2, n)) = mult (2, long-new-r (r, n)))

Theorem: long-nrd-mult-2 (tcp (r) ∧ tcp (n)) → (long-nrd (i, mult (2, r), mult (2, n)) = long-nrd (i, r, n))

Theorem: long-nrd-anrd-relate (tcp (tel) ∧ tcp (noem)) → (anrd (i, tel, noem) = long-nrd (i, mult (2, tel), mult (noem, twoto (i))))

Definition: simple-induct (x) = if x ≃ 0 then t

else simple-induct (x − 1) endif Theorem: up-shift-1-append (bitvecp (x) ∧ bitvecp (y) ∧ (y ≠ bv-nil) ∧ boolp (sin)) → (up-shift-1 (bv-append (x, y), sin)

= bv-append (up-shift-1 (x, bv-bit (y)), up-shift-1 (y, sin)))

Theorem: append-butlast-last (bitvecp (y) ∧ (y ≠ bv-nil)) → (bv-append (butlast (y), bitvec (last (y), bv-nil)) = y)

Theorem: us1-dos-1 (bitvecp (y) ∧ boolp (dsin)) → (up-shift-1 (do-shift-1 (y, dsin), last (y)) = y)

Definition: id-bitvec (size, bit) = if size ∈ N

then if size ≃ 0 then bv-nil

else bitvec (bit, id-bitvec (size − 1, bit)) endif else bv-nil endif

Theorem: size-id-bitvec bv-size (id-bitvec (size, bit)) = fix (size)

Definition: first (i, x) = if i ≃ 0 then bv-nil

else bitvec (bv-bit (x), first (i − 1, bv-vec (x))) endif

Theorem: first-size-x bitvecp (x) → (first (bv-size (x), x) = x)

Theorem: append-not-nil-3 bitvecp (a) → (bv-append (a, bitvec (x, b)) ≠ bv-nil)

Theorem: butlast-bitvec (bitvecp (rest) ∧ (rest ≠ bv-nil)) → (butlast (bitvec (bit, rest)) = bitvec (bit, butlast (rest)))

Theorem: butlast-first (bitvecp (x) ∧ (n ∈ N)) → (butlast (first (n, x)) = first (n − 1, x))

Theorem: do-shift-n-first-append-relate (bitvecp (x) ∧ (bv-size (x) ≮ i) ∧ (i ∈ N) ∧ boolp (bit)) → (do-shift-n (i, x, bit)

= bv-append (id-bitvec (i, bit), first (bv-size (x) − i, x)))

Theorem: full-down-shift boolp (bit) → (do-shift-n (bv-size (x), x, bit) = id-bitvec (bv-size (x), bit))

Theorem: up-shift-strict (x = bv-nil) → (up-shift-n (m, x, sin) = bv-nil)

Theorem: up-shift-1-bv-vec bv-vec (up-shift-n (n, x, sin)) = up-shift-n (n, bv-vec (x), sin)

Theorem: first-strict (first (n, x) = bv-nil) = (n ≃ 0)

Theorem: up-shift-strict-2 (up-shift-n (n, x, sin) = bv-nil) = ((¬ boolp (sin)) ∨ (¬ bitvecp (x)) ∨ (n ∉ N) ∨ (x = bv-nil))

Theorem: last-first (boolp (sin) ∧ (m ∈ N) ∧ (m ≠ 0) ∧ bitvecp (x) ∧ (bv-size (x) ≮ m)) → (last (first (m, x)) = bv-bit (up-shift-n (m − 1, x, sin)))

Theorem: last-id-bitvec (boolp (bit) ∧ (n ≄ 0)) → (last (id-bitvec (n, bit)) = bit)

Theorem: bit-us-last-dos (bitvecp (x) ∧ (m ∈ N) ∧ (bv-size (x) ≮ m)) → (last (do-shift-n (bv-size (x) − m, x, bv-bit (x)))

= bv-bit (up-shift-n (m − 1, x, f)))

Theorem: append-of-up-shift (bitvecp (x) ∧ (l ∈ N) ∧ (bv-size (x) = nb) ∧ (nb ≮ l)) → (bv-append (do-shift-n (nb − l, x, bv-bit (x)), up-shift-n (l, x, f))

= up-shift-n (l, bv-append (id-bitvec (nb, bv-bit (x)), x), f))

Theorem: id-bitvec-strict (id-bitvec (n, bit) = bv-nil) = (n ≃ 0)

Theorem: tc-to-int-simple-sign-extension tc-to-integer (bitvec (bv-bit (x), x)) = tc-to-integer (x)

Theorem: tc-to-int-sign-extension tc-to-integer (bv-append (id-bitvec (n, bv-bit (x)), x)) = tc-to-integer (x)

Theorem: mult-1 tcp (x) → (mult (1, x) = x)

Theorem: zero-bitvec-extension bitvec (f, zero-bitvec (n)) = bv-append (zero-bitvec (n), bitvec (f, bv-nil))

Theorem: tc-to-int-append-simple-zero-bitvec tc-to-integer (bv-append (x, bitvec (f, bv-nil))) = mult (2, tc-to-integer (x))

Theorem: tc-to-int-append-zero-bv (n ∈ N) → (tc-to-integer (bv-append (x, zero-bitvec (n)))

= mult (twoto (n), tc-to-integer (x)))

Theorem: times-conserves-lessp ((a ∈ N) ∧ (b ∈ N) ∧ (c ∈ N) ∧ (b ≄ 0) ∧ (c ≮ a)) → ((b ∗ c) ≮ a)

Theorem: times-conserves-lessp-dual ((a ∈ N) ∧ (b ∈ N) ∧ (c ∈ N) ∧ (c ≄ 0) ∧ (b ≮ a)) → ((b ∗ c) ≮ a)

Theorem: lessp-abs-max-upshift (tcp (a) ∧ tcp (b) ∧ tcp (c) ∧ (abs (b) ≮ abs (a)) ∧ (c ≠ 0)) → (abs (mult (b, c)) ≮ abs (a))

Theorem: abs-upper-bound-tc-to-int twoto (bv-size (x)) ≮ abs (tc-to-integer (x))

Theorem: hard-anrd-anrd-relate-1 (bitvecp (tel) ∧ bitvecp (noem) ∧ (bv-size (tel) = bv-size (noem)) ∧ (bv-size (tel) = nb) ∧ evenp (bv-size (tel)) ∧ (noem ≠ bv-nil) ∧ (tc-to-integer (noem) ≠ 0) ∧ (nb ≮ i) ∧ (i ∈ N)) → (hard-anrd-init (i, 1, tel, noem)

= anrd (i, tc-to-integer (tel), mult (tc-to-integer (noem), twoto (nb − i))))

Theorem: times-conserves-lessp-real ((a ∈ N) ∧ (b ∈ N) ∧ (c ∈ N) ∧ (b ≄ 0) ∧ (a < c)) → (a < (b ∗ c))

Theorem: times-conserves-lessp-dual-real ((a ∈ N) ∧ (b ∈ N) ∧ (c ∈ N) ∧ (b ≄ 0) ∧ (a < c)) → (a < (c ∗ b))

Theorem: neg-guts-tc-to-integer-0 (negative-guts (tc-to-integer (a)) = 0) = (tc-to-integer (a) ∈ N)

Theorem: div-in-rangep-tc-to-ints (bitvecp (tel) ∧ bitvecp (noem) ∧ (bv-size (tel) = bv-size (noem)) ∧ (tc-to-integer (noem) ≠ 0)) → div-in-rangep (tc-to-integer (tel), tc-to-integer (noem), bv-size (tel))

Theorem: hard-anrd-init-divides (bitvecp (tel) ∧ bitvecp (noem) ∧ (bv-size (tel) = bv-size (noem)) ∧ (bv-size (tel) = nb) ∧ evenp (bv-size (tel)) ∧ (noem ≠ bv-nil) ∧ (tc-to-integer (noem) ≠ 0)) → (tc-to-integer (hard-anrd-init (nb, 1, tel, noem))

= if tc-to-integer (tel) ∈ N

then if tc-to-integer (noem) ∈ N then divide (tc-to-integer (tel), tc-to-integer (noem)) else add (divide (tc-to-integer (tel),

tc-to-integer (noem)), -1) endif

elseif tc-to-integer (noem) ∈ N

then if imultiplep (tc-to-integer (tel), tc-to-integer (noem)) then divide (tc-to-integer (tel), tc-to-integer (noem)) else add (divide (tc-to-integer (tel),

tc-to-integer (noem)), -1) endif

elseif imultiplep (tc-to-integer (tel), tc-to-integer (noem)) then add (divide (tc-to-integer (tel), tc-to-integer (noem)), -1) else divide (tc-to-integer (tel), tc-to-integer (noem)) endif)

;; ))

Index

abs, 37, 57–59, 66 abs-upper-bound-tc-to-int, 66 add, 9–11, 13, 30, 31, 33, 34, 37, 38,

40, 41, 43–49, 52–54, 56– 59, 63, 67

add-0, 31 add-1-1, 31 add-a-minus-a, 46 addbyp-fcout, 13, 15, 16 adder-with-one-bv, 61 adder-with-zero-bv, 61 alt-bv-long-new-r, 55, 56, 59 alt-bv-long-new-r-alt-long-new-

r-relate, 59 alt-bv-long-new-r-bv-long-new-r

-relate, 56 alt-bv-long-nrd, 56, 59 alt-bv-long-nrd-alt-long-nrd-re

late, 59 alt-bv-long-nrd-bv-long-nrd-rel

ate, 56 alt-long-new-r, 54, 59 alt-long-new-r-long-new-r-relate, 54 alt-long-nrd, 54, 59 alt-long-nrd-long-nrd-relate, 54 alucev-fc, 13–17, 19, 20, 22 alucod-fc, 13–17, 19, 20, 22 alugen-alugenod-relate, 23 alugen-o, 22–25 alugenod-o, 23, 25 alugenodo-func, 23 anrd, 40, 51, 53, 63, 66 anrd-i-0, 40 anrd-integer-ok, 53 anrd-integer-ok-i-1, 51 app-c4-carry1, 19 app-c4-carry2, 19 append-butlast-last, 64 append-distributes, 62 append-not-nil, 35 append-not-nil-2, 59 append-not-nil-3, 64 append-of-up-shift, 65 associativity-of-add, 9 associativity-of-mult, 37 associativity-of-plus, 2 associativity-of-times, 2

bit-of-bv-not, 31

bit-on-implies-non-0, 11

bit-us-last-dos, 65

bitvec, 6–12, 14, 15, 17–19, 22, 24, 25, 35, 39, 40, 54–56, 59– 61, 64–66

bitvec-carry-ovf, 8, 11, 12, 14, 15, 17–19, 21, 22, 26, 27 bitvecp, 6–13, 16, 17, 19–21, 23–40,

56–67 boolp, 6, 8, 10–17, 19–21, 23, 25–30, 32–36, 57, 60, 62–65

boolp-alucev-fc, 13 boolp-alucod-fc, 13 boolp-bv-bit, 6 boolp-bvco-carry, 8 boolp-bvco-ovf, 8 boolp-not, 30 butlast, 35, 39, 64 butlast-bitvec, 64 butlast-bv-append, 39 butlast-first, 64 bv-0, 6, 24, 25 bv-1, 6, 24, 25 bv-2, 6, 24, 25 bv-3, 6, 23–25 bv-adder, 11–13, 28–30, 34, 61, 62 bv-adder-non-nil, 12 bv-adder-non-nil2, 34 bv-adder-plusses, 12 bv-append, 8, 18, 19, 21, 35–37, 39, 40, 59, 61–66

bv-append-bitvec, 61 bv-append-not-not, 36 bv-append-of-bv-nil, 39 bv-bit, 6–12, 17–22, 24, 25, 27, 31,

35, 37, 39, 55, 56, 59–62, 64, 65

bv-bit-of-bv-append, 39 bv-exor, 7, 8, 24, 25, 28, 29, 31 bv-exor-nil-a, 7 bv-exor-nil-b, 7 bv-invert-even, 7, 8, 25, 29 bv-long-new-r, 55, 56, 62 bv-long-nrd, 55, 56, 63 bv-nil, 6–15, 17, 20, 21, 23–25, 28–

36, 38–40, 54–57, 59, 60, 62–67

bv-not, 7, 8, 24, 25, 28–32, 36, 62 bv-not-bv-exor-right, 31 bv-not-nil, 31 bv-size, 6–13, 17–38, 40, 43, 55–67 bv-size-alt-long-new-r, 56 bv-to-nat, 9–12, 30, 31, 37, 39, 43 bv-to-nat-bv-append, 37 bv-to-nat-of-bv-not, 30 bv-to-nat-of-vec, 37 bv-to-nat-to-integer, 11 bv-to-nat-to-integer-lemma2, 10 bv-vec, 6–9, 11, 12, 17–22, 24, 25,

28, 35–37, 64, 65 bvco-bitvec, 11–13, 17–19, 21, 22,

26–30, 34, 61, 62 bvco-bitvec-bit-adders-double-si

ze, 61 ze-t, 62

bvco-carry, 8, 11, 12, 17–22, 26–28,

61 bvco-carry-bit-adders-double-si

ze, 61 ze-t, 61

bvco-nil, 12, 14, 15, 17, 19, 22, 27 bvco-ovf, 8, 26–29

c4, 13, 16, 18–20 c4-c4byp-help, 15 c4-c4byp-relate, 16 c4byp, 14, 16, 21 carry, 6, 10–13, 30, 31, 33, 34 carry-adder-with-one-bv, 61 carry-adder-with-zero-bv, 61 carry-col, 16, 17, 19–22, 26–29 carry-col2, 17–19, 21, 22 carry-not, 31 carry-sign-ovf-bitvec, 8, 28 carry2-carry-relate, 21 cbyp-carry-relate, 22 cbyp-carry2-relate, 22 cbyp-col, 21, 22, 26 commutativity-of-add, 9 commutativity-of-mult, 37 commutativity-of-plus, 2 commutativity-of-times, 2 commutativity2-of-add, 9 commutativity2-of-mult, 37 commutativity2-of-plus, 2 commutativity2-of-times, 2 controlep, 6, 23–25, 27, 57 cscbi11, 23–25, 27, 28 cscbo11, 23, 27 csexor, 27, 28 csobv-bitvec, 29, 30, 33, 34, 55–57,

60 csobv-nil, 28

difference-1, 44 difference-2, 3 difference-add1, 4 difference-crock1, 3 difference-difference, 3 difference-elim, 3 difference-plus, 3 difference-plus-cancellation, 3 difference-x-x, 3 distributivity-of-times-over-pl

us, 2 div-in-range-sign-new-r-1, 46 div-in-range-sign-new-r-2, 46 div-in-range-sign-new-r-3, 46 div-in-range-sign-new-r-4, 46 div-in-rangep, 43, 44, 46–54, 67 div-in-rangep-new-r-sign-1, 43 div-in-rangep-new-r-sign-2, 43 div-in-rangep-new-r-sign-3, 44 div-in-rangep-new-r-sign-4, 44 div-in-rangep-tc-to-ints, 67 div-not-in-range-sign-new-r-1, 47 div-not-in-range-sign-new-r-2, 49 div-not-in-range-sign-new-r-3, 49 div-not-in-range-sign-new-r-4, 50 divide, 38, 45–49, 51–54, 67 divide-add-mult, 46 do-shift-0, 36 do-shift-1, 35, 64 do-shift-n, 35, 36, 61, 64, 65 do-shift-n-first-append-relate, 64 do-shift-strict, 36

elim-hyp-1a-3aa, 46 elim-hyp-1a-3ab, 46 elim-hyp-1a-3ba, 47 elim-hyp-1a-3bb, 47 elim-hyp-1a-3c, 47 elim-hyp-1b-1a, 47 elim-hyp-1b-1b, 47 elim-hyp-1b-1c, 47 elim-hyp-1c, 47 elim-hyp-2a-4aa, 48 elim-hyp-2a-4ab, 48 elim-hyp-2a-4ba, 48 elim-hyp-2a-4bb, 48 elim-hyp-2a-4c, 49 elim-hyp-2b-2a, 49 elim-hyp-2b-2b, 49 elim-hyp-2b-2c-corr, 52 elim-hyp-2c-2c-corr, 52 elim-hyp-3aab-1c, 49 elim-hyp-3ba-3c, 49 elim-hyp-3c-3c, 50 elim-hyp-4aa-2c, 50 elim-hyp-4ba-4aa-corr, 53 elim-hyp-4ba-4aa-corr-aux, 52 elim-hyp-4ba-4c, 50 elim-hyp-4bb-4ab-corr, 53 elim-hyp-4c-4c, 50 equal-bit-implies-equal-numberp, 56 equal-bools, 2 equal-diff-twoto, 39 equal-difference-0, 31 equal-multiplep-r-new-r, 46 equal-numberp-implies-tc-in-ran

ge-sub, 56 equal-times-0, 2 equal-times-ab-c-equal-rem-ca-0, 48 equal-times-times, 42 equal-times-times-commuted, 45 evenp, 5, 7, 17–22, 25–30, 32–34, 36,

39, 56, 57, 59, 60, 62, 63, 66, 67

evenp-add1, 5

evenp-add1-commuted, 39

evenp-plus, 36

evenp-plus-extended, 36 evenp-times-even, 39 evenp-twoto, 36 exor, 6, 7, 11, 23, 27

first, 64, 65 first-size-x, 64 first-strict, 65 full-down-shift, 65

hack-around-next-lemma, 42

hack-implies-sprop, 61

hack2, 36 hackxaux, 38 haiblnr-1, 62 haiblnr-2, 62 hard-anrd-anrd-relate-1, 66 hard-anrd-init, 60, 66, 67 hard-anrd-init-divides, 67 hard-anrd-it, 60, 61, 63 hard-anrd-it-bv-long-nrd-relate, 62

id-bitvec, 64, 65 id-bitvec-strict, 65 imultiplep, 41–43, 46–48, 52–54, 67 imultiplep-add, 41 imultiplep-new-r, 42 induct-carry-col2, 20 induct-fn, 54 induct-quot-quot, 40 induct-vec-vec-evenp-f, 28 integer-in-rangep-of-tc-to-inte

ger, 10 integer-interpretation-of-bv-ad

der-output, 13

der-output-lemma1, 12 integer-interpretation-of-up-shi

ft-1, 38 integer-to-nat, 10, 11, 38 invert-lsb, 39

kill-col, 24–27 kill-col-12, 25

last, 34, 35, 39, 40, 64, 65 last-first, 65 last-id-bitvec, 65 last-of-bv-append, 40 lemma1, 25 lessp-abs-max-upshift, 66 lessp-boolp, 6 lessp-difference, 4 lessp-not-lessp-times, 63 lessp-plus-1, 38 lessp-plus-1-commuted, 38 lessp-plus-2, 39 lessp-remainder, 4 lessp-times, 3 lessp-twoto-sub1, 52 long-new-r, 54, 63 long-new-r-mult-2, 63 long-new-r-new-r-relate, 63 long-nrd, 54, 63 long-nrd-anrd-relate, 63 long-nrd-mult-2, 63 lower-bound-on-negative-bv-to-n

at, 10 lower-upper-determines, 42 lsb-implies-odd, 39

may-be-baby, 44 may-be-baby-2, 44 may-be-baby-3, 44 may-be-baby-4, 45 may-be-baby-5, 45 may-be-baby-6, 45 mcalu, 27, 29, 30, 32–34, 55–57, 60 mcalu-12-5-10-mcalu-12-10-10-re

late, 32 mcalu-imp-bv-adder-relate, 29 mult, 36–38, 40, 41, 43, 44, 46, 54, 57–59, 63, 65, 66

mult-1, 65

mult-add-distributes, 63 multiplep, 39, 41, 44 multiplep-diff, 41 multiplep-tc-minus, 42

nat-interpretation-of-bv-adder-

output, 12 nat-to-bv, 9, 24, 25, 29, 30, 32–34,

55, 56, 60 nat-to-bv-of-trunc, 10 nat-to-integer, 10–12, 38 neg-guts-tc-to-integer-0, 67 negative-guts-tc-minus, 39 negativep-mult, 59 new-q, 59, 60 new-r, 40, 42, 43, 46–53, 63 new-z, 59, 60, 62 not-bit-implies-in-range-times-

2, 37 not-equal-numberp-implies-tc-in

-range-add, 56 not-equal-times-0, 42 not-even-add1-commuted, 39 not-evenp-add1, 5 not-imultiplep-add, 43 not-imultiplep-new-r, 43 not-lessp-not-lessp-times, 63 not-lessp-x-n-equal-quotient-1, 51 not-zero-bv, 62 numberp-mult, 63

one-bitvec, 7, 8, 61, 62

pathological-difference, 3 plus-1, 1 plus-add1, 1 plus-cancellation, 2 plus-equal-0, 2 plus-right-id, 1 plus-to-add, 10 prop-col, 23, 24, 26, 27 prop-col-10, 24 prop-col-12, 24 prop-col-5, 24 prop-kill-relate, 24

q-d-t-lemma1, 41 q-d-t-lemma2, 41 q-d-t-lemma3, 41 quotient-diff-times, 40 quotient-diff-times-commuted, 41 quotient-diff-times-commuted-du

al, 44 quotient-diff-times-dual, 44 quotient-lessp, 40 quotient-plus-times, 4 quotient-plus-times-commuted, 4 quotient-times, 5 quotient-times-commuted, 41 quotient-times-lessp, 41 quotient-times-lessp-refrased, 44

r-lessp-2n-quotient-1, 51 r-lessp-equal-2n-quotient-2, 51 r-lessp-equal-2n-quotient-2-aux, 51 real-hack-1, 39 real-hack-6, 39 rec-mcalu-imp, 26–29 rec-mcalu-imp-bv-adder-relate, 29 remainder-0-implies, 48 remainder-by-nonnumber, 4 remainder-crock3, 5 remainder-crock4, 5 remainder-diff, 37 remainder-diff-times, 37 remainder-diff-times-commuted, 42 remainder-diff-times-commuted-2, 43 remainder-natural-interpretatio

n-of-up-shift-1, 37 remainder-of-0, 5 remainder-of-1, 5 remainder-plus, 4 remainder-plus-times, 4 remainder-plus-times-commuted, 4 remainder-quotient, 4 remainder-quotient-elim, 4 remainder-remainder, 37 remainder-times, 4 remainder-times-commuted, 51 remainder-x-x, 4 res-col, 25, 26 res-col-10, 25

simple-induct, 63 size-0, 6 size-anrd-bv, 40 size-bv-adder, 12 size-bv-append, 35 size-bvexor, 8 size-bvinv, 8 size-bvnot, 8 size-carry-col, 17 size-do-shift-n, 36 size-id-bitvec, 64 size-kill-col, 24 size-mcalu, 57 size-new-z, 60 size-onebv, 8 size-prop-col, 24 size-res-col, 25 size-up-shift-1, 36 size-up-shift-n, 36 size-zerobv, 7 special-francky-first-leq, 59 special-francky-third-1, 57 special-francky-third-1bis, 57 special-francky-third-2, 57 special-francky-third-2-bis, 58 special-francky-third-3, 58 special-francky-third-3-bis, 58 special-francky-third-4, 58 special-francky-third-4-bis, 59 sub1-difference, 44

tc-fix, 31, 47 tc-in-range-mult-2-tc-to-int-1, 57 tc-in-rangep, 9–11, 13, 30, 33, 34,

38, 56–59 tc-interpretation-of-mcalu-imp-

add, 32 sub, 34 xsub, 33

tc-interpretation-of-mcalu-outp

ut, 30 tc-minus, 30–34, 36, 38–44, 46–48,

52–54, 56–58 tc-minus-mult, 41 tc-minus-tc-minus-a, 47 tc-minus-tc-to-integer, 31 tc-to-int-append-simple-zero-bitve

c, 66 tc-to-int-append-zero-bv, 66 tc-to-int-sign-extension, 65 tc-to-int-simple-sign-extension, 65 tc-to-integer, 9–13, 30, 31, 33, 34,

38, 40, 43, 51, 53, 56–59, 65–67

tc-to-integer-0, 31 tc-to-integer-bv-not, 31 tc-to-integer-to-nat, 11 tcp, 8, 10, 31, 32, 37, 38, 40–43, 46,

48–54, 56, 59, 63, 65, 66 tcp-add, 31 tcp-divide, 38 tcp-long-new-r, 54 tcp-minus-twoto, 32 tcp-mult, 37 tcp-new-r, 40 tcp-tc-minus, 32 tcp-tc-to-integer, 10 tcp-twoto, 32 the-proof, 28 the-proof-part2, 28 the-proof-part3, 29 times-1, 2 times-2-not-1, 3 times-2-twoto, 11 times-add1, 2 times-conserves-lessp, 66 times-conserves-lessp-dual, 66 times-conserves-lessp-dual-real, 66 times-conserves-lessp-real, 66 times-difference, 37 times-distributes-over-remainde

r, 5 times-quotient-lessp-relate, 40 times-quotient-lessp-relate-dua

l, 40 times-times-induct, 42 times-to-mult-1, 38 times-zero2, 2 top-bit-off-implies-smaller, 31 transfer-add, 46 truep-boolp, 6 twoto, 3, 9–13, 30–34, 36–41, 43, 44,

47–54, 57–59, 63, 66 twoto-by-0, 3 twoto-never-0, 3 twoto-plus, 3

unfold-negative-tc-to-integer, 43 unfold-positive-tc-to-integer, 43 up, 17, 20, 21 up-shift-0, 36 up-shift-1, 35–39, 55, 56, 60, 62, 64 up-shift-1-append, 64 up-shift-1-bv-vec, 65 up-shift-1-invert-lsb, 39 up-shift-n, 35, 36, 61, 65 up-shift-strict, 65 up-shift-strict-2, 65 upper-bound-on-bv-to-nat, 10 upper-bound-on-non-negative-bv-t

o-nat, 10 us1-dos-1, 64

vec-append, 36

zero-bitvec, 7, 61–63, 65, 66 zero-bitvec-extension, 65