Lines Matching refs:lo
253 (defun dw-reduce (hi lo m base)
255 (r2 (mod (+ (* r1 base) lo) m)))
260 (< hi base) (< lo base)
262 (natp hi) (natp lo))
263 (equal (dw-reduce hi lo m base)
264 (mod (+ (* hi base) lo) m))))
275 (< lo base) (natp lo)
277 (< (+ lo (* base x)) (* base m)))
294 (< hi base) (< lo base)
296 (natp hi) (natp lo)
298 (< (floor (+ (* r1 base) lo) m)
301 ("Subgoal 1''" :cases ((< (+ lo (* base (mod hi m))) (* base m))))
310 (defun dw-submod (a hi lo m base)
311 (let* ((r (dw-reduce hi lo m base))
325 (< hi base) (< lo base)
327 (natp hi) (natp lo))
328 (equal (dw-submod a hi lo m base)
329 (mod (- a (+ (* base hi) lo)) m)))
332 (x (+ lo (* base hi)))
333 (r (dw-reduce hi lo m base)))
357 (defun join (hi lo)
358 (+ (* (expt 2 64) hi) lo))
377 ;; reduce the double word number hi*2**64 + lo (mod p1)
378 (defun simple-mod-reduce-p1 (hi lo)
379 (+ (* (expt 2 32) hi) (- hi) lo))
381 ;; reduce the double word number hi*2**64 + lo (mod p2)
382 (defun simple-mod-reduce-p2 (hi lo)
383 (+ (* (expt 2 34) hi) (- hi) lo))
385 ;; reduce the double word number hi*2**64 + lo (mod p3)
386 (defun simple-mod-reduce-p3 (hi lo)
387 (+ (* (expt 2 40) hi) (- hi) lo))
421 (integerp lo))
422 (equal (mod (simple-mod-reduce-p1 hi lo) (p1))
423 (mod (join hi lo) (p1))))
427 (x (+ (- hi) lo (* (expt 2 32) hi)))
432 (integerp lo))
433 (equal (mod (simple-mod-reduce-p2 hi lo) (p2))
434 (mod (join hi lo) (p2))))
438 (x (+ (- hi) lo (* (expt 2 34) hi)))
443 (integerp lo))
444 (equal (mod (simple-mod-reduce-p3 hi lo) (p3))
445 (mod (join hi lo) (p3))))
449 (x (+ (- hi) lo (* (expt 2 40) hi)))
462 (< lo (expt 2 64))
463 (natp hi) (natp lo))
464 (< (simple-mod-reduce-p1 hi lo)
470 (< lo (expt 2 64))
471 (< (join hi lo) (expt 2 96))
472 (natp hi) (natp lo))
473 (< (simple-mod-reduce-p1 hi lo)
480 (< lo (expt 2 64))
481 (natp hi) (natp lo))
482 (< (simple-mod-reduce-p2 hi lo)
488 (< lo (expt 2 64))
489 (< (join hi lo) (expt 2 98))
490 (natp hi) (natp lo))
491 (< (simple-mod-reduce-p2 hi lo)
497 (< lo (expt 2 64))
498 (< (join hi lo) (expt 2 69))
499 (natp hi) (natp lo))
500 (< (simple-mod-reduce-p2 hi lo)
507 (< lo (expt 2 64))
508 (natp hi) (natp lo))
509 (< (simple-mod-reduce-p3 hi lo)
515 (< lo (expt 2 64))
516 (< (join hi lo) (expt 2 104))
517 (natp hi) (natp lo))
518 (< (simple-mod-reduce-p3 hi lo)
524 (< lo (expt 2 64))
525 (< (join hi lo) (expt 2 81))
526 (natp hi) (natp lo))
527 (< (simple-mod-reduce-p3 hi lo)
535 (defun mod-reduce-p1 (hi lo)
539 (x (sub lo x))
540 (hi (if (> x lo) (+ hi -1) hi))
542 (lo (add y x))
543 (hi (if (< lo y) (+ hi 1) hi)))
544 (+ (* hi (expt 2 64)) lo)))
546 (defun mod-reduce-p2 (hi lo)
550 (x (sub lo x))
551 (hi (if (> x lo) (+ hi -1) hi))
553 (lo (add y x))
554 (hi (if (< lo y) (+ hi 1) hi)))
555 (+ (* hi (expt 2 64)) lo)))
557 (defun mod-reduce-p3 (hi lo)
561 (x (sub lo x))
562 (hi (if (> x lo) (+ hi -1) hi))
564 (lo (add y x))
565 (hi (if (< lo y) (+ hi 1) hi)))
566 (+ (* hi (expt 2 64)) lo)))
618 (< lo (expt 2 64))
619 (natp hi) (natp lo))
620 (equal (mod-reduce-p1 hi lo)
621 (simple-mod-reduce-p1 hi lo)))
644 (< lo (expt 2 64))
645 (natp hi) (natp lo))
646 (equal (mod-reduce-p2 hi lo)
647 (simple-mod-reduce-p2 hi lo)))
669 (< lo (expt 2 64))
670 (natp hi) (natp lo))
671 (equal (mod-reduce-p3 hi lo)
672 (simple-mod-reduce-p3 hi lo)))