diff options
Diffstat (limited to 'Modules/_decimal/libmpdec/literature/umodarith.lisp')
| -rw-r--r-- | Modules/_decimal/libmpdec/literature/umodarith.lisp | 692 |
1 files changed, 692 insertions, 0 deletions
diff --git a/Modules/_decimal/libmpdec/literature/umodarith.lisp b/Modules/_decimal/libmpdec/literature/umodarith.lisp new file mode 100644 index 0000000000..60a14a4e56 --- /dev/null +++ b/Modules/_decimal/libmpdec/literature/umodarith.lisp @@ -0,0 +1,692 @@ +; +; Copyright (c) 2008-2012 Stefan Krah. All rights reserved. +; +; Redistribution and use in source and binary forms, with or without +; modification, are permitted provided that the following conditions +; are met: +; +; 1. Redistributions of source code must retain the above copyright +; notice, this list of conditions and the following disclaimer. +; +; 2. Redistributions in binary form must reproduce the above copyright +; notice, this list of conditions and the following disclaimer in the +; documentation and/or other materials provided with the distribution. +; +; THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS "AS IS" AND +; ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +; IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE +; ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE +; FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +; DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS +; OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) +; HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +; LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY +; OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF +; SUCH DAMAGE. +; + + +(in-package "ACL2") + +(include-book "arithmetic/top-with-meta" :dir :system) +(include-book "arithmetic-2/floor-mod/floor-mod" :dir :system) + + +;; ===================================================================== +;; Proofs for several functions in umodarith.h +;; ===================================================================== + + + +;; ===================================================================== +;; Helper theorems +;; ===================================================================== + +(defthm elim-mod-m<x<2*m + (implies (and (<= m x) + (< x (* 2 m)) + (rationalp x) (rationalp m)) + (equal (mod x m) + (+ x (- m))))) + +(defthm modaux-1a + (implies (and (< x m) (< 0 x) (< 0 m) + (rationalp x) (rationalp m)) + (equal (mod (- x) m) + (+ (- x) m)))) + +(defthm modaux-1b + (implies (and (< (- x) m) (< x 0) (< 0 m) + (rationalp x) (rationalp m)) + (equal (mod x m) + (+ x m))) + :hints (("Goal" :use ((:instance modaux-1a + (x (- x))))))) + +(defthm modaux-1c + (implies (and (< x m) (< 0 x) (< 0 m) + (rationalp x) (rationalp m)) + (equal (mod x m) + x))) + +(defthm modaux-2a + (implies (and (< 0 b) (< b m) + (natp x) (natp b) (natp m) + (< (mod (+ b x) m) b)) + (equal (mod (+ (- m) b x) m) + (+ (- m) b (mod x m))))) + +(defthm modaux-2b + (implies (and (< 0 b) (< b m) + (natp x) (natp b) (natp m) + (< (mod (+ b x) m) b)) + (equal (mod (+ b x) m) + (+ (- m) b (mod x m)))) + :hints (("Goal" :use (modaux-2a)))) + +(defthm linear-mod-1 + (implies (and (< x m) (< b m) + (natp x) (natp b) + (rationalp m)) + (equal (< x (mod (+ (- b) x) m)) + (< x b))) + :hints (("Goal" :use ((:instance modaux-1a + (x (+ b (- x)))))))) + +(defthm linear-mod-2 + (implies (and (< 0 b) (< b m) + (natp x) (natp b) + (natp m)) + (equal (< (mod x m) + (mod (+ (- b) x) m)) + (< (mod x m) b)))) + +(defthm linear-mod-3 + (implies (and (< x m) (< b m) + (natp x) (natp b) + (rationalp m)) + (equal (<= b (mod (+ b x) m)) + (< (+ b x) m))) + :hints (("Goal" :use ((:instance elim-mod-m<x<2*m + (x (+ b x))))))) + +(defthm modaux-2c + (implies (and (< 0 b) (< b m) + (natp x) (natp b) (natp m) + (<= b (mod (+ b x) m))) + (equal (mod (+ b x) m) + (+ b (mod x m)))) + :hints (("Subgoal *1/8''" :use (linear-mod-3)))) + +(defthmd modaux-2d + (implies (and (< x m) (< 0 x) (< 0 m) + (< (- m) b) (< b 0) (rationalp m) + (<= x (mod (+ b x) m)) + (rationalp x) (rationalp b)) + (equal (+ (- m) (mod (+ b x) m)) + (+ b x))) + :hints (("Goal" :cases ((<= 0 (+ b x)))) + ("Subgoal 2'" :use ((:instance modaux-1b + (x (+ b x))))))) + +(defthm mod-m-b + (implies (and (< 0 x) (< 0 b) (< 0 m) + (< x b) (< b m) + (natp x) (natp b) (natp m)) + (equal (mod (+ (mod (- x) m) b) m) + (mod (- x) b)))) + + +;; ===================================================================== +;; addmod, submod +;; ===================================================================== + +(defun addmod (a b m base) + (let* ((s (mod (+ a b) base)) + (s (if (< s a) (mod (- s m) base) s)) + (s (if (>= s m) (mod (- s m) base) s))) + s)) + +(defthmd addmod-correct + (implies (and (< 0 m) (< m base) + (< a m) (<= b m) + (natp m) (natp base) + (natp a) (natp b)) + (equal (addmod a b m base) + (mod (+ a b) m))) + :hints (("Goal" :cases ((<= base (+ a b)))) + ("Subgoal 2.1'" :use ((:instance elim-mod-m<x<2*m + (x (+ a b))))))) + +(defun submod (a b m base) + (let* ((d (mod (- a b) base)) + (d (if (< a d) (mod (+ d m) base) d))) + d)) + +(defthmd submod-aux1 + (implies (and (< a (mod (+ a (- b)) base)) + (< 0 base) (< a base) (<= b base) + (natp base) (natp a) (natp b)) + (< a b)) + :rule-classes :forward-chaining) + +(defthmd submod-aux2 + (implies (and (<= (mod (+ a (- b)) base) a) + (< 0 base) (< a base) (< b base) + (natp base) (natp a) (natp b)) + (<= b a)) + :rule-classes :forward-chaining) + +(defthmd submod-correct + (implies (and (< 0 m) (< m base) + (< a m) (<= b m) + (natp m) (natp base) + (natp a) (natp b)) + (equal (submod a b m base) + (mod (- a b) m))) + :hints (("Goal" :cases ((<= base (+ a b)))) + ("Subgoal 2.2" :use ((:instance submod-aux1))) + ("Subgoal 2.2'''" :cases ((and (< 0 (+ a (- b) m)) + (< (+ a (- b) m) m)))) + ("Subgoal 2.1" :use ((:instance submod-aux2))) + ("Subgoal 1.2" :use ((:instance submod-aux1))) + ("Subgoal 1.1" :use ((:instance submod-aux2))))) + + +(defun submod-2 (a b m base) + (let* ((d (mod (- a b) base)) + (d (if (< a b) (mod (+ d m) base) d))) + d)) + +(defthm submod-2-correct + (implies (and (< 0 m) (< m base) + (< a m) (<= b m) + (natp m) (natp base) + (natp a) (natp b)) + (equal (submod-2 a b m base) + (mod (- a b) m))) + :hints (("Subgoal 2'" :cases ((and (< 0 (+ a (- b) m)) + (< (+ a (- b) m) m)))))) + + +;; ========================================================================= +;; ext-submod is correct +;; ========================================================================= + +; a < 2*m, b < 2*m +(defun ext-submod (a b m base) + (let* ((a (if (>= a m) (- a m) a)) + (b (if (>= b m) (- b m) b)) + (d (mod (- a b) base)) + (d (if (< a b) (mod (+ d m) base) d))) + d)) + +; a < 2*m, b < 2*m +(defun ext-submod-2 (a b m base) + (let* ((a (mod a m)) + (b (mod b m)) + (d (mod (- a b) base)) + (d (if (< a b) (mod (+ d m) base) d))) + d)) + +(defthmd ext-submod-ext-submod-2-equal + (implies (and (< 0 m) (< m base) + (< a (* 2 m)) (< b (* 2 m)) + (natp m) (natp base) + (natp a) (natp b)) + (equal (ext-submod a b m base) + (ext-submod-2 a b m base)))) + +(defthmd ext-submod-2-correct + (implies (and (< 0 m) (< m base) + (< a (* 2 m)) (< b (* 2 m)) + (natp m) (natp base) + (natp a) (natp b)) + (equal (ext-submod-2 a b m base) + (mod (- a b) m)))) + + +;; ========================================================================= +;; dw-reduce is correct +;; ========================================================================= + +(defun dw-reduce (hi lo m base) + (let* ((r1 (mod hi m)) + (r2 (mod (+ (* r1 base) lo) m))) + r2)) + +(defthmd dw-reduce-correct + (implies (and (< 0 m) (< m base) + (< hi base) (< lo base) + (natp m) (natp base) + (natp hi) (natp lo)) + (equal (dw-reduce hi lo m base) + (mod (+ (* hi base) lo) m)))) + +(defthmd <=-multiply-both-sides-by-z + (implies (and (rationalp x) (rationalp y) + (< 0 z) (rationalp z)) + (equal (<= x y) + (<= (* z x) (* z y))))) + +(defthmd dw-reduce-aux1 + (implies (and (< 0 m) (< m base) + (natp m) (natp base) + (< lo base) (natp lo) + (< x m) (natp x)) + (< (+ lo (* base x)) (* base m))) + :hints (("Goal" :cases ((<= (+ x 1) m))) + ("Subgoal 1''" :cases ((<= (* base (+ x 1)) (* base m)))) + ("subgoal 1.2" :use ((:instance <=-multiply-both-sides-by-z + (x (+ 1 x)) + (y m) + (z base)))))) + +(defthm dw-reduce-aux2 + (implies (and (< x (* base m)) + (< 0 m) (< m base) + (natp m) (natp base) (natp x)) + (< (floor x m) base))) + +;; This is the necessary condition for using _mpd_div_words(). +(defthmd dw-reduce-second-quotient-fits-in-single-word + (implies (and (< 0 m) (< m base) + (< hi base) (< lo base) + (natp m) (natp base) + (natp hi) (natp lo) + (equal r1 (mod hi m))) + (< (floor (+ (* r1 base) lo) m) + base)) + :hints (("Goal" :cases ((< r1 m))) + ("Subgoal 1''" :cases ((< (+ lo (* base (mod hi m))) (* base m)))) + ("Subgoal 1.2" :use ((:instance dw-reduce-aux1 + (x (mod hi m))))))) + + +;; ========================================================================= +;; dw-submod is correct +;; ========================================================================= + +(defun dw-submod (a hi lo m base) + (let* ((r (dw-reduce hi lo m base)) + (d (mod (- a r) base)) + (d (if (< a r) (mod (+ d m) base) d))) + d)) + +(defthmd dw-submod-aux1 + (implies (and (natp a) (< 0 m) (natp m) + (natp x) (equal r (mod x m))) + (equal (mod (- a x) m) + (mod (- a r) m)))) + +(defthmd dw-submod-correct + (implies (and (< 0 m) (< m base) + (natp a) (< a m) + (< hi base) (< lo base) + (natp m) (natp base) + (natp hi) (natp lo)) + (equal (dw-submod a hi lo m base) + (mod (- a (+ (* base hi) lo)) m))) + :hints (("Goal" :in-theory (disable dw-reduce) + :use ((:instance dw-submod-aux1 + (x (+ lo (* base hi))) + (r (dw-reduce hi lo m base))) + (:instance dw-reduce-correct))))) + + +;; ========================================================================= +;; ANSI C arithmetic for uint64_t +;; ========================================================================= + +(defun add (a b) + (mod (+ a b) + (expt 2 64))) + +(defun sub (a b) + (mod (- a b) + (expt 2 64))) + +(defun << (w n) + (mod (* w (expt 2 n)) + (expt 2 64))) + +(defun >> (w n) + (floor w (expt 2 n))) + +;; join upper and lower half of a double word, yielding a 128 bit number +(defun join (hi lo) + (+ (* (expt 2 64) hi) lo)) + + +;; ============================================================================= +;; Fast modular reduction +;; ============================================================================= + +;; These are the three primes used in the Number Theoretic Transform. +;; A fast modular reduction scheme exists for all of them. +(defmacro p1 () + (+ (expt 2 64) (- (expt 2 32)) 1)) + +(defmacro p2 () + (+ (expt 2 64) (- (expt 2 34)) 1)) + +(defmacro p3 () + (+ (expt 2 64) (- (expt 2 40)) 1)) + + +;; reduce the double word number hi*2**64 + lo (mod p1) +(defun simple-mod-reduce-p1 (hi lo) + (+ (* (expt 2 32) hi) (- hi) lo)) + +;; reduce the double word number hi*2**64 + lo (mod p2) +(defun simple-mod-reduce-p2 (hi lo) + (+ (* (expt 2 34) hi) (- hi) lo)) + +;; reduce the double word number hi*2**64 + lo (mod p3) +(defun simple-mod-reduce-p3 (hi lo) + (+ (* (expt 2 40) hi) (- hi) lo)) + + +; ---------------------------------------------------------- +; The modular reductions given above are correct +; ---------------------------------------------------------- + +(defthmd congruence-p1-aux + (equal (* (expt 2 64) hi) + (+ (* (p1) hi) + (* (expt 2 32) hi) + (- hi)))) + +(defthmd congruence-p2-aux + (equal (* (expt 2 64) hi) + (+ (* (p2) hi) + (* (expt 2 34) hi) + (- hi)))) + +(defthmd congruence-p3-aux + (equal (* (expt 2 64) hi) + (+ (* (p3) hi) + (* (expt 2 40) hi) + (- hi)))) + +(defthmd mod-augment + (implies (and (rationalp x) + (rationalp y) + (rationalp m)) + (equal (mod (+ x y) m) + (mod (+ x (mod y m)) m)))) + +(defthmd simple-mod-reduce-p1-congruent + (implies (and (integerp hi) + (integerp lo)) + (equal (mod (simple-mod-reduce-p1 hi lo) (p1)) + (mod (join hi lo) (p1)))) + :hints (("Goal''" :use ((:instance congruence-p1-aux) + (:instance mod-augment + (m (p1)) + (x (+ (- hi) lo (* (expt 2 32) hi))) + (y (* (p1) hi))))))) + +(defthmd simple-mod-reduce-p2-congruent + (implies (and (integerp hi) + (integerp lo)) + (equal (mod (simple-mod-reduce-p2 hi lo) (p2)) + (mod (join hi lo) (p2)))) + :hints (("Goal''" :use ((:instance congruence-p2-aux) + (:instance mod-augment + (m (p2)) + (x (+ (- hi) lo (* (expt 2 34) hi))) + (y (* (p2) hi))))))) + +(defthmd simple-mod-reduce-p3-congruent + (implies (and (integerp hi) + (integerp lo)) + (equal (mod (simple-mod-reduce-p3 hi lo) (p3)) + (mod (join hi lo) (p3)))) + :hints (("Goal''" :use ((:instance congruence-p3-aux) + (:instance mod-augment + (m (p3)) + (x (+ (- hi) lo (* (expt 2 40) hi))) + (y (* (p3) hi))))))) + + +; --------------------------------------------------------------------- +; We need a number less than 2*p, so that we can use the trick from +; elim-mod-m<x<2*m for the final reduction. +; For p1, two modular reductions are sufficient, for p2 and p3 three. +; --------------------------------------------------------------------- + +;; p1: the first reduction is less than 2**96 +(defthmd simple-mod-reduce-p1-<-2**96 + (implies (and (< hi (expt 2 64)) + (< lo (expt 2 64)) + (natp hi) (natp lo)) + (< (simple-mod-reduce-p1 hi lo) + (expt 2 96)))) + +;; p1: the second reduction is less than 2*p1 +(defthmd simple-mod-reduce-p1-<-2*p1 + (implies (and (< hi (expt 2 64)) + (< lo (expt 2 64)) + (< (join hi lo) (expt 2 96)) + (natp hi) (natp lo)) + (< (simple-mod-reduce-p1 hi lo) + (* 2 (p1))))) + + +;; p2: the first reduction is less than 2**98 +(defthmd simple-mod-reduce-p2-<-2**98 + (implies (and (< hi (expt 2 64)) + (< lo (expt 2 64)) + (natp hi) (natp lo)) + (< (simple-mod-reduce-p2 hi lo) + (expt 2 98)))) + +;; p2: the second reduction is less than 2**69 +(defthmd simple-mod-reduce-p2-<-2*69 + (implies (and (< hi (expt 2 64)) + (< lo (expt 2 64)) + (< (join hi lo) (expt 2 98)) + (natp hi) (natp lo)) + (< (simple-mod-reduce-p2 hi lo) + (expt 2 69)))) + +;; p3: the third reduction is less than 2*p2 +(defthmd simple-mod-reduce-p2-<-2*p2 + (implies (and (< hi (expt 2 64)) + (< lo (expt 2 64)) + (< (join hi lo) (expt 2 69)) + (natp hi) (natp lo)) + (< (simple-mod-reduce-p2 hi lo) + (* 2 (p2))))) + + +;; p3: the first reduction is less than 2**104 +(defthmd simple-mod-reduce-p3-<-2**104 + (implies (and (< hi (expt 2 64)) + (< lo (expt 2 64)) + (natp hi) (natp lo)) + (< (simple-mod-reduce-p3 hi lo) + (expt 2 104)))) + +;; p3: the second reduction is less than 2**81 +(defthmd simple-mod-reduce-p3-<-2**81 + (implies (and (< hi (expt 2 64)) + (< lo (expt 2 64)) + (< (join hi lo) (expt 2 104)) + (natp hi) (natp lo)) + (< (simple-mod-reduce-p3 hi lo) + (expt 2 81)))) + +;; p3: the third reduction is less than 2*p3 +(defthmd simple-mod-reduce-p3-<-2*p3 + (implies (and (< hi (expt 2 64)) + (< lo (expt 2 64)) + (< (join hi lo) (expt 2 81)) + (natp hi) (natp lo)) + (< (simple-mod-reduce-p3 hi lo) + (* 2 (p3))))) + + +; ------------------------------------------------------------------------- +; The simple modular reductions, adapted for compiler friendly C +; ------------------------------------------------------------------------- + +(defun mod-reduce-p1 (hi lo) + (let* ((y hi) + (x y) + (hi (>> hi 32)) + (x (sub lo x)) + (hi (if (> x lo) (+ hi -1) hi)) + (y (<< y 32)) + (lo (add y x)) + (hi (if (< lo y) (+ hi 1) hi))) + (+ (* hi (expt 2 64)) lo))) + +(defun mod-reduce-p2 (hi lo) + (let* ((y hi) + (x y) + (hi (>> hi 30)) + (x (sub lo x)) + (hi (if (> x lo) (+ hi -1) hi)) + (y (<< y 34)) + (lo (add y x)) + (hi (if (< lo y) (+ hi 1) hi))) + (+ (* hi (expt 2 64)) lo))) + +(defun mod-reduce-p3 (hi lo) + (let* ((y hi) + (x y) + (hi (>> hi 24)) + (x (sub lo x)) + (hi (if (> x lo) (+ hi -1) hi)) + (y (<< y 40)) + (lo (add y x)) + (hi (if (< lo y) (+ hi 1) hi))) + (+ (* hi (expt 2 64)) lo))) + + +; ------------------------------------------------------------------------- +; The compiler friendly versions are equal to the simple versions +; ------------------------------------------------------------------------- + +(defthm mod-reduce-aux1 + (implies (and (<= 0 a) (natp a) (natp m) + (< (- m) b) (<= b 0) + (integerp b) + (< (mod (+ b a) m) + (mod a m))) + (equal (mod (+ b a) m) + (+ b (mod a m)))) + :hints (("Subgoal 2" :use ((:instance modaux-1b + (x (+ a b))))))) + +(defthm mod-reduce-aux2 + (implies (and (<= 0 a) (natp a) (natp m) + (< b m) (natp b) + (< (mod (+ b a) m) + (mod a m))) + (equal (+ m (mod (+ b a) m)) + (+ b (mod a m))))) + + +(defthm mod-reduce-aux3 + (implies (and (< 0 a) (natp a) (natp m) + (< (- m) b) (< b 0) + (integerp b) + (<= (mod a m) + (mod (+ b a) m))) + (equal (+ (- m) (mod (+ b a) m)) + (+ b (mod a m)))) + :hints (("Subgoal 1.2'" :use ((:instance modaux-1b + (x b)))) + ("Subgoal 1''" :use ((:instance modaux-2d + (x I)))))) + + +(defthm mod-reduce-aux4 + (implies (and (< 0 a) (natp a) (natp m) + (< b m) (natp b) + (<= (mod a m) + (mod (+ b a) m))) + (equal (mod (+ b a) m) + (+ b (mod a m))))) + + +(defthm mod-reduce-p1==simple-mod-reduce-p1 + (implies (and (< hi (expt 2 64)) + (< lo (expt 2 64)) + (natp hi) (natp lo)) + (equal (mod-reduce-p1 hi lo) + (simple-mod-reduce-p1 hi lo))) + :hints (("Goal" :in-theory (disable expt) + :cases ((< 0 hi))) + ("Subgoal 1.2.2'" :use ((:instance mod-reduce-aux1 + (m (expt 2 64)) + (b (+ (- HI) LO)) + (a (* (expt 2 32) hi))))) + ("Subgoal 1.2.1'" :use ((:instance mod-reduce-aux3 + (m (expt 2 64)) + (b (+ (- HI) LO)) + (a (* (expt 2 32) hi))))) + ("Subgoal 1.1.2'" :use ((:instance mod-reduce-aux2 + (m (expt 2 64)) + (b (+ (- HI) LO)) + (a (* (expt 2 32) hi))))) + ("Subgoal 1.1.1'" :use ((:instance mod-reduce-aux4 + (m (expt 2 64)) + (b (+ (- HI) LO)) + (a (* (expt 2 32) hi))))))) + + +(defthm mod-reduce-p2==simple-mod-reduce-p2 + (implies (and (< hi (expt 2 64)) + (< lo (expt 2 64)) + (natp hi) (natp lo)) + (equal (mod-reduce-p2 hi lo) + (simple-mod-reduce-p2 hi lo))) + :hints (("Goal" :cases ((< 0 hi))) + ("Subgoal 1.2.2'" :use ((:instance mod-reduce-aux1 + (m (expt 2 64)) + (b (+ (- HI) LO)) + (a (* (expt 2 34) hi))))) + ("Subgoal 1.2.1'" :use ((:instance mod-reduce-aux3 + (m (expt 2 64)) + (b (+ (- HI) LO)) + (a (* (expt 2 34) hi))))) + ("Subgoal 1.1.2'" :use ((:instance mod-reduce-aux2 + (m (expt 2 64)) + (b (+ (- HI) LO)) + (a (* (expt 2 34) hi))))) + ("Subgoal 1.1.1'" :use ((:instance mod-reduce-aux4 + (m (expt 2 64)) + (b (+ (- HI) LO)) + (a (* (expt 2 34) hi))))))) + + +(defthm mod-reduce-p3==simple-mod-reduce-p3 + (implies (and (< hi (expt 2 64)) + (< lo (expt 2 64)) + (natp hi) (natp lo)) + (equal (mod-reduce-p3 hi lo) + (simple-mod-reduce-p3 hi lo))) + :hints (("Goal" :cases ((< 0 hi))) + ("Subgoal 1.2.2'" :use ((:instance mod-reduce-aux1 + (m (expt 2 64)) + (b (+ (- HI) LO)) + (a (* (expt 2 40) hi))))) + ("Subgoal 1.2.1'" :use ((:instance mod-reduce-aux3 + (m (expt 2 64)) + (b (+ (- HI) LO)) + (a (* (expt 2 40) hi))))) + ("Subgoal 1.1.2'" :use ((:instance mod-reduce-aux2 + (m (expt 2 64)) + (b (+ (- HI) LO)) + (a (* (expt 2 40) hi))))) + ("Subgoal 1.1.1'" :use ((:instance mod-reduce-aux4 + (m (expt 2 64)) + (b (+ (- HI) LO)) + (a (* (expt 2 40) hi))))))) + + + |