Lines Matching refs:expt
343 (expt 2 64)))
347 (expt 2 64)))
350 (mod (* w (expt 2 n))
351 (expt 2 64)))
354 (floor w (expt 2 n)))
358 (+ (* (expt 2 64) hi) lo))
368 (+ (expt 2 64) (- (expt 2 32)) 1))
371 (+ (expt 2 64) (- (expt 2 34)) 1))
374 (+ (expt 2 64) (- (expt 2 40)) 1))
379 (+ (* (expt 2 32) hi) (- hi) lo))
383 (+ (* (expt 2 34) hi) (- hi) lo))
387 (+ (* (expt 2 40) hi) (- hi) lo))
395 (equal (* (expt 2 64) hi)
397 (* (expt 2 32) hi)
401 (equal (* (expt 2 64) hi)
403 (* (expt 2 34) hi)
407 (equal (* (expt 2 64) hi)
409 (* (expt 2 40) hi)
427 (x (+ (- hi) lo (* (expt 2 32) hi)))
438 (x (+ (- hi) lo (* (expt 2 34) hi)))
449 (x (+ (- hi) lo (* (expt 2 40) hi)))
461 (implies (and (< hi (expt 2 64))
462 (< lo (expt 2 64))
465 (expt 2 96))))
469 (implies (and (< hi (expt 2 64))
470 (< lo (expt 2 64))
471 (< (join hi lo) (expt 2 96))
479 (implies (and (< hi (expt 2 64))
480 (< lo (expt 2 64))
483 (expt 2 98))))
487 (implies (and (< hi (expt 2 64))
488 (< lo (expt 2 64))
489 (< (join hi lo) (expt 2 98))
492 (expt 2 69))))
496 (implies (and (< hi (expt 2 64))
497 (< lo (expt 2 64))
498 (< (join hi lo) (expt 2 69))
506 (implies (and (< hi (expt 2 64))
507 (< lo (expt 2 64))
510 (expt 2 104))))
514 (implies (and (< hi (expt 2 64))
515 (< lo (expt 2 64))
516 (< (join hi lo) (expt 2 104))
519 (expt 2 81))))
523 (implies (and (< hi (expt 2 64))
524 (< lo (expt 2 64))
525 (< (join hi lo) (expt 2 81))
544 (+ (* hi (expt 2 64)) lo)))
555 (+ (* hi (expt 2 64)) lo)))
566 (+ (* hi (expt 2 64)) lo)))
617 (implies (and (< hi (expt 2 64))
618 (< lo (expt 2 64))
622 :hints (("Goal" :in-theory (disable expt)
625 (m (expt 2 64))
627 (a (* (expt 2 32) hi)))))
629 (m (expt 2 64))
631 (a (* (expt 2 32) hi)))))
633 (m (expt 2 64))
635 (a (* (expt 2 32) hi)))))
637 (m (expt 2 64))
639 (a (* (expt 2 32) hi)))))))
643 (implies (and (< hi (expt 2 64))
644 (< lo (expt 2 64))
650 (m (expt 2 64))
652 (a (* (expt 2 34) hi)))))
654 (m (expt 2 64))
656 (a (* (expt 2 34) hi)))))
658 (m (expt 2 64))
660 (a (* (expt 2 34) hi)))))
662 (m (expt 2 64))
664 (a (* (expt 2 34) hi)))))))
668 (implies (and (< hi (expt 2 64))
669 (< lo (expt 2 64))
675 (m (expt 2 64))
677 (a (* (expt 2 40) hi)))))
679 (m (expt 2 64))
681 (a (* (expt 2 40) hi)))))
683 (m (expt 2 64))
685 (a (* (expt 2 40) hi)))))
687 (m (expt 2 64))
689 (a (* (expt 2 40) hi)))))))