Lines Matching defs:all
87 ;; I think we can remove the all-evaluations-p from defun-sk to
90 (defun-sk all-evaluations-p (states vars)
115 (defun all-truthsp-label (label s vars)
119 (all-truthsp-label label s (rest vars)))))
121 (defthm all-truthsp-label-expanded
122 (implies (and (all-truthsp-label label s vars)
127 (defun only-all-truths-p (states m vars)
129 (and (all-truthsp-label (label-of (first states) m) (first states) vars)
130 (only-all-truths-p (rest states) m vars))))
183 (all-evaluations-p (states m) (variables m))
185 (only-all-truths-p (states m) m (variables m))
234 (defthm all-evaluations-considers-an-evaluation-a-member
236 (all-evaluations-p states vars))
239 :use all-evaluations-p-necc)))
241 (in-theory (disable all-evaluations-p all-evaluations-p-necc))
325 ;; And all truths are present in the label.
327 (defthm all-truths-p-from-only-all-truths-p
328 (implies (and (only-all-truths-p states m vars)
330 (all-truthsp-label (label-of s m) s vars)))
360 (all-truthsp-label label q variables))
368 (all-truthsp-label lq q variables))
378 (all-truthsp-label lq q variables))
394 (all-truthsp-label lq q variables))
508 all-evaluations-p
568 all-evaluations-p
630 all-evaluations-p