		Search-engine friendly clone of the ACL2 documentation.

Boolean-assert-true

Boolean-assert-true-lifting

Lifting of the circuit to a predicate.

Definitions and Theorems

Function: boolean-assert-true-pred

(defun boolean-assert-true-pred (x prime)
  (and (equal (pfield::mul x (mod 1 prime) prime)
              (mod 1 prime))))

Theorem: definition-satp-to-boolean-assert-true-pred

(defthm definition-satp-to-boolean-assert-true-pred
 (implies
  (and
   (equal
    (pfcs::lookup-definition '(:simple "boolean_assert_true")
                             pfcs::defs)
    '(:definition
          (name :simple "boolean_assert_true")
          (pfcs::para (:simple "x"))
          (pfcs::body (:equal (:mul (:var (:simple "x")) (:const 1))
                              (:const 1)))))
   (pfield::fep x prime)
   (primep prime))
  (equal (pfcs::definition-satp '(:simple "boolean_assert_true")
                                pfcs::defs (list x)
                                prime)
         (boolean-assert-true-pred x prime))))