Lines Matching defs:p1
367 (defmacro p1 ()
377 ;; reduce the double word number hi*2**64 + lo (mod p1)
378 (defun simple-mod-reduce-p1 (hi lo)
394 (defthmd congruence-p1-aux
396 (+ (* (p1) hi)
419 (defthmd simple-mod-reduce-p1-congruent
422 (equal (mod (simple-mod-reduce-p1 hi lo) (p1))
423 (mod (join hi lo) (p1))))
424 :hints (("Goal''" :use ((:instance congruence-p1-aux)
426 (m (p1))
428 (y (* (p1) hi)))))))
456 ; For p1, two modular reductions are sufficient, for p2 and p3 three.
459 ;; p1: the first reduction is less than 2**96
460 (defthmd simple-mod-reduce-p1-<-2**96
464 (< (simple-mod-reduce-p1 hi lo)
467 ;; p1: the second reduction is less than 2*p1
468 (defthmd simple-mod-reduce-p1-<-2*p1
473 (< (simple-mod-reduce-p1 hi lo)
474 (* 2 (p1)))))
535 (defun mod-reduce-p1 (hi lo)
616 (defthm mod-reduce-p1==simple-mod-reduce-p1
620 (equal (mod-reduce-p1 hi lo)
621 (simple-mod-reduce-p1 hi lo)))