Lines Matching defs:keys
16 rewrite rules) as alists where the keys (cars) are ordered using
80 (defun keys-aux (x)
84 (keys-aux (cdr x))))))
86 (defun keys (x)
87 (keys-aux (acl2->rcd x)))
161 (defthm g-keys-aux-relationship
163 (iff (memberp a (keys-aux r))
167 (defthm s-keys-aux-reduction
169 (equal (keys-aux (s-aux a v r))
171 (insert a (keys-aux r))
172 (drop a (keys-aux r)))))))
175 (defthm keys-aux-are-ordered
177 (orderedp (keys-aux r)))))
245 (defthm g-keys-relationship
246 (iff (memberp a (keys r))
249 (defthm s-keys-reduction
250 (equal (keys (s a v r))
252 (insert a (keys r))
253 (drop a (keys r)))))
255 (defthm keys-are-ordered
256 (orderedp (keys r)))
281 (in-theory (disable s g keys))