		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-transunit-ensemble

Transform a translation unit ensemble.

Signature
(simpadd0-transunit-ensemble tunits) → (mv new-tunits events)
Arguments: tunits — Guard (transunit-ensemblep tunits).
Returns: new-tunits — Type (transunit-ensemblep new-tunits).; events — Type (pseudo-event-form-listp events).

Definitions and Theorems

Function: simpadd0-transunit-ensemble

(defun simpadd0-transunit-ensemble (tunits)
  (declare (xargs :guard (transunit-ensemblep tunits)))
  (declare (xargs :guard (transunit-ensemble-unambp tunits)))
  (let ((__function__ 'simpadd0-transunit-ensemble))
    (declare (ignorable __function__))
    (b* (((transunit-ensemble tunits) tunits)
         ((mv new-map events-map)
          (simpadd0-filepath-transunit-map tunits.unwrap)))
      (mv (transunit-ensemble new-map)
          events-map))))

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

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

Theorem: pseudo-event-form-listp-of-simpadd0-transunit-ensemble.events

(defthm
      pseudo-event-form-listp-of-simpadd0-transunit-ensemble.events
  (b* (((mv ?new-tunits ?events)
        (simpadd0-transunit-ensemble tunits)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)

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

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

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))
   (simpadd0-transunit-ensemble tunits)))

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