		Search-engine friendly clone of the ACL2 documentation.

Ipasir

Ipasir-assume$c

Signature
(ipasir-assume$c ipasir$c lit) → ipasir$c
Arguments: lit — Guard (litp lit).

Definitions and Theorems

Function: ipasir-assume$c

(defun ipasir-assume$c (ipasir$c lit)
 (declare (xargs :stobjs (ipasir$c)))
 (declare (xargs :guard (litp lit)))
 (declare
     (xargs :guard (not (eq (ipasir$a->status (ipasir-get ipasir$c))
                            :undef))))
 (let ((__function__ 'ipasir-assume$c))
   (declare (ignorable __function__))
   (ipasir-set (ipasir-assume$a (ipasir-get ipasir$c)
                                lit)
               ipasir$c)))

Theorem: ipasir-assume$c-of-lit-fix-lit

(defthm ipasir-assume$c-of-lit-fix-lit
  (equal (ipasir-assume$c ipasir$c (lit-fix lit))
         (ipasir-assume$c ipasir$c lit)))

Theorem: ipasir-assume$c-lit-equiv-congruence-on-lit

(defthm ipasir-assume$c-lit-equiv-congruence-on-lit
  (implies (lit-equiv lit lit-equiv)
           (equal (ipasir-assume$c ipasir$c lit)
                  (ipasir-assume$c ipasir$c lit-equiv)))
  :rule-classes :congruence)