		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-gin-update

Update a simpadd0-gin with a simpadd0-gout.

Signature
(simpadd0-gin-update gin gout) → new-gin
Arguments: gin — Guard (simpadd0-ginp gin).; gout — Guard (simpadd0-goutp gout).
Returns: new-gin — Type (simpadd0-ginp new-gin).

Those two data structures include common components, whose values are threaded through the transformation functions.

Definitions and Theorems

Function: simpadd0-gin-update

(defun simpadd0-gin-update (gin gout)
  (declare (xargs :guard (and (simpadd0-ginp gin)
                              (simpadd0-goutp gout))))
  (let ((__function__ 'simpadd0-gin-update))
    (declare (ignorable __function__))
    (b* (((simpadd0-gout gout) gout))
      (change-simpadd0-gin gin
                           :thm-index gout.thm-index
                           :names-to-avoid gout.names-to-avoid))))

Theorem: simpadd0-ginp-of-simpadd0-gin-update

(defthm simpadd0-ginp-of-simpadd0-gin-update
  (b* ((new-gin (simpadd0-gin-update gin gout)))
    (simpadd0-ginp new-gin))
  :rule-classes :rewrite)

Theorem: simpadd0-gin-update-of-simpadd0-gin-fix-gin

(defthm simpadd0-gin-update-of-simpadd0-gin-fix-gin
  (equal (simpadd0-gin-update (simpadd0-gin-fix gin)
                              gout)
         (simpadd0-gin-update gin gout)))

Theorem: simpadd0-gin-update-simpadd0-gin-equiv-congruence-on-gin

(defthm simpadd0-gin-update-simpadd0-gin-equiv-congruence-on-gin
  (implies (simpadd0-gin-equiv gin gin-equiv)
           (equal (simpadd0-gin-update gin gout)
                  (simpadd0-gin-update gin-equiv gout)))
  :rule-classes :congruence)

Theorem: simpadd0-gin-update-of-simpadd0-gout-fix-gout

(defthm simpadd0-gin-update-of-simpadd0-gout-fix-gout
  (equal (simpadd0-gin-update gin (simpadd0-gout-fix gout))
         (simpadd0-gin-update gin gout)))

Theorem: simpadd0-gin-update-simpadd0-gout-equiv-congruence-on-gout

(defthm simpadd0-gin-update-simpadd0-gout-equiv-congruence-on-gout
  (implies (simpadd0-gout-equiv gout gout-equiv)
           (equal (simpadd0-gin-update gin gout)
                  (simpadd0-gin-update gin gout-equiv)))
  :rule-classes :congruence)