		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-code-ensemble

Transform a code ensemble.

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

Definitions and Theorems

Function: simpadd0-code-ensemble

(defun simpadd0-code-ensemble (code gin)
  (declare (xargs :guard (and (code-ensemblep code) (ginp gin))))
  (declare (xargs :guard (and (code-ensemble-unambp code)
                              (code-ensemble-annop code))))
  (let ((__function__ 'simpadd0-code-ensemble))
    (declare (ignorable __function__))
    (b* (((code-ensemble code) code)
         ((mv tunits-new (gout gout))
          (simpadd0-transunit-ensemble code.transunits gin)))
      (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)))
    (code-ensemblep new-code))
  :rule-classes :rewrite)

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

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

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

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

Theorem: code-ensemble-annop-of-simpadd0-code-ensemble

(defthm code-ensemble-annop-of-simpadd0-code-ensemble
  (implies (and (code-ensemble-unambp code)
                (code-ensemble-annop code))
           (b* (((mv ?new-code ?gout)
                 (simpadd0-code-ensemble code gin)))
             (code-ensemble-annop new-code))))

Theorem: code-ensemble-aidentp-of-simpadd0-code-ensemble

(defthm code-ensemble-aidentp-of-simpadd0-code-ensemble
  (implies (and (code-ensemble-unambp code)
                (code-ensemble-aidentp code))
           (b* (((mv ?new-code ?gout)
                 (simpadd0-code-ensemble code gin)))
             (code-ensemble-aidentp 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)
         (simpadd0-code-ensemble code gin)))

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)
                  (simpadd0-code-ensemble code-equiv gin)))
  :rule-classes :congruence)

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

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

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

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