Lines Matching defs:dw
250 ;; dw-reduce is correct
253 (defun dw-reduce (hi lo m base)
258 (defthmd dw-reduce-correct
263 (equal (dw-reduce hi lo m base)
272 (defthmd dw-reduce-aux1
285 (defthm dw-reduce-aux2
292 (defthmd dw-reduce-second-quotient-fits-in-single-word
302 ("Subgoal 1.2" :use ((:instance dw-reduce-aux1
307 ;; dw-submod is correct
310 (defun dw-submod (a hi lo m base)
311 (let* ((r (dw-reduce hi lo m base))
316 (defthmd dw-submod-aux1
322 (defthmd dw-submod-correct
328 (equal (dw-submod a hi lo m base)
330 :hints (("Goal" :in-theory (disable dw-reduce)
331 :use ((:instance dw-submod-aux1
333 (r (dw-reduce hi lo m base)))
334 (:instance dw-reduce-correct)))))