		Search-engine friendly clone of the ACL2 documentation.

Ipasir-formula

Ipasir-cancel-assumption

Identity function in execution; in the logic, ensures that the assumption field of the ipasir is empty, which it must be by the guard.

Signature
(ipasir-cancel-assumption ipasir) → new-ipasir

See ipasir-add-binary, particularly ipasir-add-binary-formula, for an example: if we didn't use this function at the beginning of ipasir-add-binary, then we'd need a hypothesis of (not (ipasir$a->assumption ipasir)) in ipasir-add-binary-formula.

Definitions and Theorems

Function: ipasir-cancel-assumption$inline

(defun ipasir-cancel-assumption$inline (ipasir)
  (declare (xargs :stobjs (ipasir)))
  (declare (xargs :guard (not (ipasir-get-assumption ipasir))))
  (let ((__function__ 'ipasir-cancel-assumption))
    (declare (ignorable __function__))
    (mbe :logic (non-exec (change-ipasir$a ipasir
                                           :assumption nil))
         :exec ipasir)))

Theorem: ipasir-cancel-assumption-status

(defthm ipasir-cancel-assumption-status
  (b* ((?new-ipasir (ipasir-cancel-assumption$inline ipasir)))
    (equal (ipasir$a->status new-ipasir)
           (ipasir$a->status ipasir))))

Theorem: ipasir-cancel-assumption-formula

(defthm ipasir-cancel-assumption-formula
  (b* ((?new-ipasir (ipasir-cancel-assumption$inline ipasir)))
    (equal (ipasir$a->formula new-ipasir)
           (ipasir$a->formula ipasir))))

Theorem: ipasir-cancel-assumption-assumption

(defthm ipasir-cancel-assumption-assumption
  (b* ((?new-ipasir (ipasir-cancel-assumption$inline ipasir)))
    (not (ipasir$a->assumption new-ipasir))))

Theorem: ipasir-cancel-assumption-new-clause

(defthm ipasir-cancel-assumption-new-clause
  (b* ((?new-ipasir (ipasir-cancel-assumption$inline ipasir)))
    (equal (ipasir$a->new-clause new-ipasir)
           (ipasir$a->new-clause ipasir))))