Lines Matching defs:submod
141 ;; addmod, submod
161 (defun submod (a b m base)
166 (defthmd submod-aux1
173 (defthmd submod-aux2
180 (defthmd submod-correct
185 (equal (submod a b m base)
188 ("Subgoal 2.2" :use ((:instance submod-aux1)))
191 ("Subgoal 2.1" :use ((:instance submod-aux2)))
192 ("Subgoal 1.2" :use ((:instance submod-aux1)))
193 ("Subgoal 1.1" :use ((:instance submod-aux2)))))
196 (defun submod-2 (a b m base)
201 (defthm submod-2-correct
206 (equal (submod-2 a b m base)
213 ;; ext-submod is correct
217 (defun ext-submod (a b m base)
225 (defun ext-submod-2 (a b m base)
232 (defthmd ext-submod-ext-submod-2-equal
237 (equal (ext-submod a b m base)
238 (ext-submod-2 a b m base))))
240 (defthmd ext-submod-2-correct
245 (equal (ext-submod-2 a b m base)
307 ;; dw-submod is correct
310 (defun dw-submod (a hi lo m base)
316 (defthmd dw-submod-aux1
322 (defthmd dw-submod-correct
328 (equal (dw-submod a hi lo m base)
331 :use ((:instance dw-submod-aux1