Lines Matching defs:del
86 (defun del (e x)
90 (cons (first x) (del e (rest x))))))
93 (defthm len-del-reduction-1
95 (equal (len (del e x))
103 (induction-hint-for-len-<= (cdr x) (del (car x) y))))
106 (defthm del-not-member-reduction
108 (equal (del e x) x)))
112 (defthm member-del-reduction
114 (equal (memberp v (del e y))
119 (defthm subset-del-member
122 (subset x (del e y))))
126 (defthm uniquep-del-reduction
128 (uniquep (del e x))))
165 (defthm del-e-to-cons-subset
166 (implies (subset (del e y) x)
190 :in-theory (disable del-e-to-cons-subset)
191 :use ((:instance del-e-to-cons-subset