		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-transunit-ensemble

Transform a translation unit ensemble.

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

Definitions and Theorems

Function: simpadd0-transunit-ensemble

(defun simpadd0-transunit-ensemble (tunits gin)
  (declare (xargs :guard (and (transunit-ensemblep tunits)
                              (ginp gin))))
  (declare (xargs :guard (and (transunit-ensemble-unambp tunits)
                              (transunit-ensemble-annop tunits))))
  (let ((__function__ 'simpadd0-transunit-ensemble))
    (declare (ignorable __function__))
    (b* (((transunit-ensemble tunits) tunits)
         ((mv new-map (gout gout-map))
          (simpadd0-filepath-transunit-map tunits.units gin))
         (gin (gin-update gin gout-map)))
      (mv (transunit-ensemble new-map)
          (gout-no-thm gin)))))

Theorem: transunit-ensemblep-of-simpadd0-transunit-ensemble.new-tunits

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

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

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

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

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

Theorem: transunit-ensemble-annop-of-simpadd0-transunit-ensemble

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

Theorem: transunit-ensemble-aidentp-of-simpadd0-transunit-ensemble

(defthm transunit-ensemble-aidentp-of-simpadd0-transunit-ensemble
  (implies (and (transunit-ensemble-unambp tunits)
                (transunit-ensemble-aidentp tunits gcc))
           (b* (((mv ?new-tunits ?gout)
                 (simpadd0-transunit-ensemble tunits gin)))
             (transunit-ensemble-aidentp new-tunits gcc))))

Theorem: simpadd0-transunit-ensemble-of-transunit-ensemble-fix-tunits

(defthm simpadd0-transunit-ensemble-of-transunit-ensemble-fix-tunits
 (equal
    (simpadd0-transunit-ensemble (c$::transunit-ensemble-fix tunits)
                                 gin)
    (simpadd0-transunit-ensemble tunits gin)))

Theorem: simpadd0-transunit-ensemble-transunit-ensemble-equiv-congruence-on-tunits

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

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

(defthm simpadd0-transunit-ensemble-of-gin-fix-gin
  (equal (simpadd0-transunit-ensemble tunits (gin-fix gin))
         (simpadd0-transunit-ensemble tunits gin)))

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

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