Lines Matching defs:abs
195 (defun abs-only-all-truths-p (states label vars)
198 (abs-only-all-truths-p (rest states) label vars))))
202 (defthm abs-concrete-only-all-truthsp-reduction
204 (abs-only-all-truths-p states (label-fn m) vars))
209 ;; And now let us just prove abs-all-truthsp-label for the label-fn
227 (defthm label-fn-is-abs-only--all-truthsp
228 (abs-only-all-truths-p states (create-label-fn states vars label) vars)
241 (in-theory (disable abs-concrete-only-all-truthsp-reduction))
245 (defun abs-label-subset-vars (states label vars)
248 (abs-label-subset-vars (rest states) label vars))))
252 (defthm abs-label-subset-vars-is-same-as-concrete
254 (abs-label-subset-vars states (label-fn m) vars))
260 (defthm create-label-fn-is-abs-label-subset-vars
261 (abs-label-subset-vars states (create-label-fn states vars label) vars)
274 (in-theory (disable abs-label-subset-vars-is-same-as-concrete))
278 (defun abs-only-truth-p (states label)
281 (abs-only-truth-p (rest states) label))))
285 (defthm only-truth-p-abs-reduction
287 (abs-only-truth-p states (label-fn m)))
293 (defthm label-fn-is-abs-only-truth-p
294 (abs-only-truth-p states (create-label-fn states vars label))
305 (in-theory (disable only-truth-p-abs-reduction))