Check if a translation unit ensemble is unambiguous.
(transunit-ensemble-unambp tunits) → yes/no
Function:
(defun transunit-ensemble-unambp-loop (map) (declare (xargs :guard (filepath-transunit-mapp map))) (let ((__function__ 'transunit-ensemble-unambp-loop)) (declare (ignorable __function__)) (or (omap::emptyp map) (and (transunit-unambp (omap::head-val map)) (transunit-ensemble-unambp-loop (omap::tail map))))))
Theorem:
(defthm booleanp-of-transunit-ensemble-unambp-loop (b* ((yes/no (transunit-ensemble-unambp-loop map))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm transunit-ensemble-unambp-loop-of-empty (implies (omap::emptyp tumap) (transunit-ensemble-unambp-loop tumap)))
Theorem:
(defthm transunit-ensemble-unambp-loop-of-update (implies (and (transunit-unambp tunit) (transunit-ensemble-unambp-loop tumap)) (transunit-ensemble-unambp-loop (omap::update path tunit tumap))))
Theorem:
(defthm transunit-unambp-of-head-when-transunit-ensemble-unambp-loop (implies (and (transunit-ensemble-unambp-loop tumap) (not (omap::emptyp tumap))) (transunit-unambp (mv-nth 1 (omap::head tumap)))))
Theorem:
(defthm transunit-ensemble-unambp-loop-of-tail (implies (transunit-ensemble-unambp-loop tumap) (transunit-ensemble-unambp-loop (omap::tail tumap))))
Function:
(defun transunit-ensemble-unambp (tunits) (declare (xargs :guard (transunit-ensemblep tunits))) (let ((__function__ 'transunit-ensemble-unambp)) (declare (ignorable __function__)) (transunit-ensemble-unambp-loop (transunit-ensemble->unwrap tunits))))
Theorem:
(defthm booleanp-of-transunit-ensemble-unambp (b* ((yes/no (transunit-ensemble-unambp tunits))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm transunit-ensemble-unambp-of-transunit-ensemble (equal (transunit-ensemble-unambp (transunit-ensemble tumap)) (transunit-ensemble-unambp-loop (filepath-transunit-map-fix tumap))))
Theorem:
(defthm transunit-ensemble-unambp-loop-of-transunit-ensemble->unwrap (implies (transunit-ensemble-unambp tunits) (transunit-ensemble-unambp-loop (transunit-ensemble->unwrap tunits))))
Theorem:
(defthm transunit-ensemble-unambp-of-transunit-ensemble-fix-tunits (equal (transunit-ensemble-unambp (transunit-ensemble-fix tunits)) (transunit-ensemble-unambp tunits)))
Theorem:
(defthm transunit-ensemble-unambp-transunit-ensemble-equiv-congruence-on-tunits (implies (transunit-ensemble-equiv tunits tunits-equiv) (equal (transunit-ensemble-unambp tunits) (transunit-ensemble-unambp tunits-equiv))) :rule-classes :congruence)