		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-code-ensemble

Transform a code ensemble.

Signature
(simpadd0-code-ensemble code gin state) → (mv new-code gout)
Arguments: code — Guard (code-ensemblep code).; gin — Guard (simpadd0-ginp gin).
Returns: new-code — Type (code-ensemblep new-code).; gout — Type (simpadd0-goutp gout).

Definitions and Theorems

Function: simpadd0-code-ensemble

(defun simpadd0-code-ensemble (code gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (code-ensemblep code)
                             (simpadd0-ginp gin))))
 (declare
  (xargs
      :guard
      (transunit-ensemble-unambp (code-ensemble->transunits code))))
 (let ((__function__ 'simpadd0-code-ensemble))
   (declare (ignorable __function__))
   (b* (((code-ensemble code) code)
        ((mv tunits-new (simpadd0-gout gout))
         (simpadd0-transunit-ensemble code.transunits gin state)))
     (mv (change-code-ensemble code
                               :transunits tunits-new)
         gout))))

Theorem: code-ensemblep-of-simpadd0-code-ensemble.new-code

(defthm code-ensemblep-of-simpadd0-code-ensemble.new-code
  (b* (((mv ?new-code ?gout)
        (simpadd0-code-ensemble code gin state)))
    (code-ensemblep new-code))
  :rule-classes :rewrite)

Theorem: simpadd0-goutp-of-simpadd0-code-ensemble.gout

(defthm simpadd0-goutp-of-simpadd0-code-ensemble.gout
  (b* (((mv ?new-code ?gout)
        (simpadd0-code-ensemble code gin state)))
    (simpadd0-goutp gout))
  :rule-classes :rewrite)

Theorem: transunit-ensemble-unambp-of-simpadd0-code-ensemble

(defthm transunit-ensemble-unambp-of-simpadd0-code-ensemble
 (b* (((mv ?new-code ?gout)
       (simpadd0-code-ensemble code gin state)))
  (transunit-ensemble-unambp (code-ensemble->transunits new-code))))

Theorem: simpadd0-code-ensemble-of-code-ensemble-fix-code

(defthm simpadd0-code-ensemble-of-code-ensemble-fix-code
  (equal (simpadd0-code-ensemble (c$::code-ensemble-fix code)
                                 gin state)
         (simpadd0-code-ensemble code gin state)))

Theorem: simpadd0-code-ensemble-code-ensemble-equiv-congruence-on-code

(defthm
      simpadd0-code-ensemble-code-ensemble-equiv-congruence-on-code
  (implies (c$::code-ensemble-equiv code code-equiv)
           (equal (simpadd0-code-ensemble code gin state)
                  (simpadd0-code-ensemble code-equiv gin state)))
  :rule-classes :congruence)

Theorem: simpadd0-code-ensemble-of-simpadd0-gin-fix-gin

(defthm simpadd0-code-ensemble-of-simpadd0-gin-fix-gin
  (equal (simpadd0-code-ensemble code (simpadd0-gin-fix gin)
                                 state)
         (simpadd0-code-ensemble code gin state)))

Theorem: simpadd0-code-ensemble-simpadd0-gin-equiv-congruence-on-gin

(defthm simpadd0-code-ensemble-simpadd0-gin-equiv-congruence-on-gin
  (implies (simpadd0-gin-equiv gin gin-equiv)
           (equal (simpadd0-code-ensemble code gin state)
                  (simpadd0-code-ensemble code gin-equiv state)))
  :rule-classes :congruence)