		Search-engine friendly clone of the ACL2 documentation.

Formalized-subset

Transunit-ensemble-formalp

Check if a translation unit ensemble has formal dynamic semantics.

Signature
(transunit-ensemble-formalp tunits) → yes/no
Arguments: tunits — Guard (transunit-ensemblep tunits).
Returns: yes/no — Type (booleanp yes/no).

As in ldm-transunit-ensemble, there must be a single translation unit, and in addition it must have formal dynamic semantics.

Definitions and Theorems

Function: transunit-ensemble-formalp

(defun transunit-ensemble-formalp (tunits)
  (declare (xargs :guard (transunit-ensemblep tunits)))
  (declare (xargs :guard (transunit-ensemble-unambp tunits)))
  (let ((__function__ 'transunit-ensemble-formalp))
    (declare (ignorable __function__))
    (b* ((map (transunit-ensemble->units tunits)))
      (and (= (omap::size map) 1)
           (transunit-formalp (omap::head-val map))))))

Theorem: booleanp-of-transunit-ensemble-formalp

(defthm booleanp-of-transunit-ensemble-formalp
  (b* ((yes/no (transunit-ensemble-formalp tunits)))
    (booleanp yes/no))
  :rule-classes :rewrite)

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

(defthm transunit-ensemble-formalp-of-transunit-ensemble-fix-tunits
 (equal (transunit-ensemble-formalp (transunit-ensemble-fix tunits))
        (transunit-ensemble-formalp tunits)))

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

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