Lines Matching defs:p3
373 (defmacro p3 ()
385 ;; reduce the double word number hi*2**64 + lo (mod p3)
386 (defun simple-mod-reduce-p3 (hi lo)
406 (defthmd congruence-p3-aux
408 (+ (* (p3) hi)
441 (defthmd simple-mod-reduce-p3-congruent
444 (equal (mod (simple-mod-reduce-p3 hi lo) (p3))
445 (mod (join hi lo) (p3))))
446 :hints (("Goal''" :use ((:instance congruence-p3-aux)
448 (m (p3))
450 (y (* (p3) hi)))))))
456 ; For p1, two modular reductions are sufficient, for p2 and p3 three.
494 ;; p3: the third reduction is less than 2*p2
504 ;; p3: the first reduction is less than 2**104
505 (defthmd simple-mod-reduce-p3-<-2**104
509 (< (simple-mod-reduce-p3 hi lo)
512 ;; p3: the second reduction is less than 2**81
513 (defthmd simple-mod-reduce-p3-<-2**81
518 (< (simple-mod-reduce-p3 hi lo)
521 ;; p3: the third reduction is less than 2*p3
522 (defthmd simple-mod-reduce-p3-<-2*p3
527 (< (simple-mod-reduce-p3 hi lo)
528 (* 2 (p3)))))
557 (defun mod-reduce-p3 (hi lo)
667 (defthm mod-reduce-p3==simple-mod-reduce-p3
671 (equal (mod-reduce-p3 hi lo)
672 (simple-mod-reduce-p3 hi lo)))