Lines Matching refs:hi
253 (defun dw-reduce (hi lo m base)
254 (let* ((r1 (mod hi 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))))
294 (< hi base) (< lo base)
296 (natp hi) (natp lo)
297 (equal r1 (mod hi m)))
301 ("Subgoal 1''" :cases ((< (+ lo (* base (mod hi m))) (* base m))))
303 (x (mod hi 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))
378 (defun simple-mod-reduce-p1 (hi lo)
379 (+ (* (expt 2 32) hi) (- hi) lo))
382 (defun simple-mod-reduce-p2 (hi lo)
383 (+ (* (expt 2 34) hi) (- hi) lo))
386 (defun simple-mod-reduce-p3 (hi lo)
387 (+ (* (expt 2 40) hi) (- hi) lo))
395 (equal (* (expt 2 64) hi)
396 (+ (* (p1) hi)
397 (* (expt 2 32) hi)
398 (- hi))))
401 (equal (* (expt 2 64) hi)
402 (+ (* (p2) hi)
403 (* (expt 2 34) hi)
404 (- hi))))
407 (equal (* (expt 2 64) hi)
408 (+ (* (p3) hi)
409 (* (expt 2 40) hi)
410 (- hi))))
420 (implies (and (integerp hi)
422 (equal (mod (simple-mod-reduce-p1 hi lo) (p1))
423 (mod (join hi lo) (p1))))
427 (x (+ (- hi) lo (* (expt 2 32) hi)))
428 (y (* (p1) hi)))))))
431 (implies (and (integerp hi)
433 (equal (mod (simple-mod-reduce-p2 hi lo) (p2))
434 (mod (join hi lo) (p2))))
438 (x (+ (- hi) lo (* (expt 2 34) hi)))
439 (y (* (p2) hi)))))))
442 (implies (and (integerp hi)
444 (equal (mod (simple-mod-reduce-p3 hi lo) (p3))
445 (mod (join hi lo) (p3))))
449 (x (+ (- hi) lo (* (expt 2 40) hi)))
450 (y (* (p3) hi)))))))
461 (implies (and (< hi (expt 2 64))
463 (natp hi) (natp lo))
464 (< (simple-mod-reduce-p1 hi lo)
469 (implies (and (< hi (expt 2 64))
471 (< (join hi lo) (expt 2 96))
472 (natp hi) (natp lo))
473 (< (simple-mod-reduce-p1 hi lo)
479 (implies (and (< hi (expt 2 64))
481 (natp hi) (natp lo))
482 (< (simple-mod-reduce-p2 hi lo)
487 (implies (and (< hi (expt 2 64))
489 (< (join hi lo) (expt 2 98))
490 (natp hi) (natp lo))
491 (< (simple-mod-reduce-p2 hi lo)
496 (implies (and (< hi (expt 2 64))
498 (< (join hi lo) (expt 2 69))
499 (natp hi) (natp lo))
500 (< (simple-mod-reduce-p2 hi lo)
506 (implies (and (< hi (expt 2 64))
508 (natp hi) (natp lo))
509 (< (simple-mod-reduce-p3 hi lo)
514 (implies (and (< hi (expt 2 64))
516 (< (join hi lo) (expt 2 104))
517 (natp hi) (natp lo))
518 (< (simple-mod-reduce-p3 hi lo)
523 (implies (and (< hi (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)
536 (let* ((y hi)
538 (hi (>> hi 32))
540 (hi (if (> x lo) (+ hi -1) hi))
543 (hi (if (< lo y) (+ hi 1) hi)))
544 (+ (* hi (expt 2 64)) lo)))
546 (defun mod-reduce-p2 (hi lo)
547 (let* ((y hi)
549 (hi (>> hi 30))
551 (hi (if (> x lo) (+ hi -1) hi))
554 (hi (if (< lo y) (+ hi 1) hi)))
555 (+ (* hi (expt 2 64)) lo)))
557 (defun mod-reduce-p3 (hi lo)
558 (let* ((y hi)
560 (hi (>> hi 24))
562 (hi (if (> x lo) (+ hi -1) hi))
565 (hi (if (< lo y) (+ hi 1) hi)))
566 (+ (* hi (expt 2 64)) lo)))
617 (implies (and (< hi (expt 2 64))
619 (natp hi) (natp lo))
620 (equal (mod-reduce-p1 hi lo)
621 (simple-mod-reduce-p1 hi lo)))
623 :cases ((< 0 hi)))
627 (a (* (expt 2 32) hi)))))
631 (a (* (expt 2 32) hi)))))
635 (a (* (expt 2 32) hi)))))
639 (a (* (expt 2 32) hi)))))))
643 (implies (and (< hi (expt 2 64))
645 (natp hi) (natp lo))
646 (equal (mod-reduce-p2 hi lo)
647 (simple-mod-reduce-p2 hi lo)))
648 :hints (("Goal" :cases ((< 0 hi)))
652 (a (* (expt 2 34) hi)))))
656 (a (* (expt 2 34) hi)))))
660 (a (* (expt 2 34) hi)))))
664 (a (* (expt 2 34) hi)))))))
668 (implies (and (< hi (expt 2 64))
670 (natp hi) (natp lo))
671 (equal (mod-reduce-p3 hi lo)
672 (simple-mod-reduce-p3 hi lo)))
673 :hints (("Goal" :cases ((< 0 hi)))
677 (a (* (expt 2 40) hi)))))
681 (a (* (expt 2 40) hi)))))
685 (a (* (expt 2 40) hi)))))
689 (a (* (expt 2 40) hi)))))))