		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)