		Search-engine friendly clone of the ACL2 documentation.

Fraig

Fraig-total-checks

Signature
(fraig-total-checks fraig-stats) → checks
Returns: checks — Type (natp checks).

Definitions and Theorems

Function: fraig-total-checks

(defun fraig-total-checks (fraig-stats)
  (declare (xargs :stobjs (fraig-stats)))
  (declare (xargs :guard t))
  (let ((__function__ 'fraig-total-checks))
    (declare (ignorable __function__))
    (lnfix (+ (fraig-unsat-checks fraig-stats)
              (fraig-sat-checks fraig-stats)
              (fraig-failed-checks fraig-stats)))))

Theorem: natp-of-fraig-total-checks

(defthm natp-of-fraig-total-checks
  (b* ((checks (fraig-total-checks fraig-stats)))
    (natp checks))
  :rule-classes :type-prescription)