Lines Matching defs:mod
32 (include-book "arithmetic-2/floor-mod/floor-mod" :dir :system)
45 (defthm elim-mod-m<x<2*m
49 (equal (mod x m)
55 (equal (mod (- x) m)
61 (equal (mod x m)
69 (equal (mod x m)
75 (< (mod (+ b x) m) b))
76 (equal (mod (+ (- m) b x) m)
77 (+ (- m) b (mod x m)))))
82 (< (mod (+ b x) m) b))
83 (equal (mod (+ b x) m)
84 (+ (- m) b (mod x m))))
87 (defthm linear-mod-1
91 (equal (< x (mod (+ (- b) x) m))
96 (defthm linear-mod-2
100 (equal (< (mod x m)
101 (mod (+ (- b) x) m))
102 (< (mod x m) b))))
104 (defthm linear-mod-3
108 (equal (<= b (mod (+ b x) m))
110 :hints (("Goal" :use ((:instance elim-mod-m<x<2*m
116 (<= b (mod (+ b x) m)))
117 (equal (mod (+ b x) m)
118 (+ b (mod x m))))
119 :hints (("Subgoal *1/8''" :use (linear-mod-3))))
124 (<= x (mod (+ b x) m))
126 (equal (+ (- m) (mod (+ b x) m))
132 (defthm mod-m-b
136 (equal (mod (+ (mod (- x) m) b) m)
137 (mod (- x) b))))
145 (let* ((s (mod (+ a b) base))
146 (s (if (< s a) (mod (- s m) base) s))
147 (s (if (>= s m) (mod (- s m) base) s)))
156 (mod (+ a b) m)))
158 ("Subgoal 2.1'" :use ((:instance elim-mod-m<x<2*m
162 (let* ((d (mod (- a b) base))
163 (d (if (< a d) (mod (+ d m) base) d)))
167 (implies (and (< a (mod (+ a (- b)) base))
174 (implies (and (<= (mod (+ a (- b)) base) a)
186 (mod (- a b) m)))
197 (let* ((d (mod (- a b) base))
198 (d (if (< a b) (mod (+ d m) base) d)))
207 (mod (- a b) m)))
220 (d (mod (- a b) base))
221 (d (if (< a b) (mod (+ d m) base) d)))
226 (let* ((a (mod a m))
227 (b (mod b m))
228 (d (mod (- a b) base))
229 (d (if (< a b) (mod (+ d m) base) d)))
246 (mod (- a b) m))))
254 (let* ((r1 (mod hi m))
255 (r2 (mod (+ (* r1 base) lo) m)))
264 (mod (+ (* hi base) lo) m))))
297 (equal r1 (mod hi m)))
301 ("Subgoal 1''" :cases ((< (+ lo (* base (mod hi m))) (* base m))))
303 (x (mod hi m)))))))
312 (d (mod (- a r) base))
313 (d (if (< a r) (mod (+ d m) base) d)))
318 (natp x) (equal r (mod x m)))
319 (equal (mod (- a x) m)
320 (mod (- a r) m))))
329 (mod (- a (+ (* base hi) lo)) m)))
342 (mod (+ a b)
346 (mod (- a b)
350 (mod (* w (expt 2 n))
377 ;; reduce the double word number hi*2**64 + lo (mod p1)
378 (defun simple-mod-reduce-p1 (hi lo)
381 ;; reduce the double word number hi*2**64 + lo (mod p2)
382 (defun simple-mod-reduce-p2 (hi lo)
385 ;; reduce the double word number hi*2**64 + lo (mod p3)
386 (defun simple-mod-reduce-p3 (hi lo)
412 (defthmd mod-augment
416 (equal (mod (+ x y) m)
417 (mod (+ x (mod y m)) m))))
419 (defthmd simple-mod-reduce-p1-congruent
422 (equal (mod (simple-mod-reduce-p1 hi lo) (p1))
423 (mod (join hi lo) (p1))))
425 (:instance mod-augment
430 (defthmd simple-mod-reduce-p2-congruent
433 (equal (mod (simple-mod-reduce-p2 hi lo) (p2))
434 (mod (join hi lo) (p2))))
436 (:instance mod-augment
441 (defthmd simple-mod-reduce-p3-congruent
444 (equal (mod (simple-mod-reduce-p3 hi lo) (p3))
445 (mod (join hi lo) (p3))))
447 (:instance mod-augment
455 ; elim-mod-m<x<2*m for the final reduction.
460 (defthmd simple-mod-reduce-p1-<-2**96
464 (< (simple-mod-reduce-p1 hi lo)
468 (defthmd simple-mod-reduce-p1-<-2*p1
473 (< (simple-mod-reduce-p1 hi lo)
478 (defthmd simple-mod-reduce-p2-<-2**98
482 (< (simple-mod-reduce-p2 hi lo)
486 (defthmd simple-mod-reduce-p2-<-2*69
491 (< (simple-mod-reduce-p2 hi lo)
495 (defthmd simple-mod-reduce-p2-<-2*p2
500 (< (simple-mod-reduce-p2 hi lo)
505 (defthmd simple-mod-reduce-p3-<-2**104
509 (< (simple-mod-reduce-p3 hi lo)
513 (defthmd simple-mod-reduce-p3-<-2**81
518 (< (simple-mod-reduce-p3 hi lo)
522 (defthmd simple-mod-reduce-p3-<-2*p3
527 (< (simple-mod-reduce-p3 hi lo)
535 (defun mod-reduce-p1 (hi lo)
546 (defun mod-reduce-p2 (hi lo)
557 (defun mod-reduce-p3 (hi lo)
573 (defthm mod-reduce-aux1
577 (< (mod (+ b a) m)
578 (mod a m)))
579 (equal (mod (+ b a) m)
580 (+ b (mod a m))))
584 (defthm mod-reduce-aux2
587 (< (mod (+ b a) m)
588 (mod a m)))
589 (equal (+ m (mod (+ b a) m))
590 (+ b (mod a m)))))
593 (defthm mod-reduce-aux3
597 (<= (mod a m)
598 (mod (+ b a) m)))
599 (equal (+ (- m) (mod (+ b a) m))
600 (+ b (mod a m))))
607 (defthm mod-reduce-aux4
610 (<= (mod a m)
611 (mod (+ b a) m)))
612 (equal (mod (+ b a) m)
613 (+ b (mod a m)))))
616 (defthm mod-reduce-p1==simple-mod-reduce-p1
620 (equal (mod-reduce-p1 hi lo)
621 (simple-mod-reduce-p1 hi lo)))
624 ("Subgoal 1.2.2'" :use ((:instance mod-reduce-aux1
628 ("Subgoal 1.2.1'" :use ((:instance mod-reduce-aux3
632 ("Subgoal 1.1.2'" :use ((:instance mod-reduce-aux2
636 ("Subgoal 1.1.1'" :use ((:instance mod-reduce-aux4
642 (defthm mod-reduce-p2==simple-mod-reduce-p2
646 (equal (mod-reduce-p2 hi lo)
647 (simple-mod-reduce-p2 hi lo)))
649 ("Subgoal 1.2.2'" :use ((:instance mod-reduce-aux1
653 ("Subgoal 1.2.1'" :use ((:instance mod-reduce-aux3
657 ("Subgoal 1.1.2'" :use ((:instance mod-reduce-aux2
661 ("Subgoal 1.1.1'" :use ((:instance mod-reduce-aux4
667 (defthm mod-reduce-p3==simple-mod-reduce-p3
671 (equal (mod-reduce-p3 hi lo)
672 (simple-mod-reduce-p3 hi lo)))
674 ("Subgoal 1.2.2'" :use ((:instance mod-reduce-aux1
678 ("Subgoal 1.2.1'" :use ((:instance mod-reduce-aux3
682 ("Subgoal 1.1.2'" :use ((:instance mod-reduce-aux2
686 ("Subgoal 1.1.1'" :use ((:instance mod-reduce-aux4