		Search-engine friendly clone of the ACL2 documentation.

Ipasir

Ipasir-set$a

Signature
(ipasir-set$a val ipasir$a) → new-ipasir$a
Arguments: val — Guard (ipasir$a-p val).; ipasir$a — Guard (ipasir$a-p ipasir$a).
Returns: new-ipasir$a — Type (ipasir$a-p new-ipasir$a).

Definitions and Theorems

Function: ipasir-set$a

(defun ipasir-set$a (val ipasir$a)
       (declare (xargs :guard (and (ipasir$a-p val)
                                   (ipasir$a-p ipasir$a))))
       (declare (ignore ipasir$a))
       (let ((__function__ 'ipasir-set$a))
            (declare (ignorable __function__))
            (ipasir$a-fix val)))

Theorem: ipasir$a-p-of-ipasir-set$a

(defthm ipasir$a-p-of-ipasir-set$a
        (b* ((new-ipasir$a (ipasir-set$a val ipasir$a)))
            (ipasir$a-p new-ipasir$a))
        :rule-classes :rewrite)

Theorem: ipasir-set$a-of-ipasir$a-fix-val

(defthm ipasir-set$a-of-ipasir$a-fix-val
        (equal (ipasir-set$a (ipasir$a-fix val)
                             ipasir$a)
               (ipasir-set$a val ipasir$a)))

Theorem: ipasir-set$a-ipasir$a-equiv-congruence-on-val

(defthm ipasir-set$a-ipasir$a-equiv-congruence-on-val
        (implies (ipasir$a-equiv val val-equiv)
                 (equal (ipasir-set$a val ipasir$a)
                        (ipasir-set$a val-equiv ipasir$a)))
        :rule-classes :congruence)

Theorem: ipasir-set$a-of-ipasir$a-fix-ipasir$a

(defthm ipasir-set$a-of-ipasir$a-fix-ipasir$a
        (equal (ipasir-set$a val (ipasir$a-fix ipasir$a))
               (ipasir-set$a val ipasir$a)))

Theorem: ipasir-set$a-ipasir$a-equiv-congruence-on-ipasir$a

(defthm ipasir-set$a-ipasir$a-equiv-congruence-on-ipasir$a
        (implies (ipasir$a-equiv ipasir$a ipasir$a-equiv)
                 (equal (ipasir-set$a val ipasir$a)
                        (ipasir-set$a val ipasir$a-equiv)))
        :rule-classes :congruence)