Check if a translation unit ensemble has formal dynamic semantics.
(transunit-ensemble-formalp tunits) → yes/no
As in ldm-transunit-ensemble, there must be a single translation unit, and in addition it must have formal dynamic semantics.
Function:
(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->unwrap tunits))) (and (= (omap::size map) 1) (transunit-formalp (omap::head-val map))))))
Theorem:
(defthm booleanp-of-transunit-ensemble-formalp (b* ((yes/no (transunit-ensemble-formalp tunits))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm transunit-ensemble-formalp-of-transunit-ensemble-fix-tunits (equal (transunit-ensemble-formalp (transunit-ensemble-fix tunits)) (transunit-ensemble-formalp tunits)))
Theorem:
(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)