(transunit-ensemble-aidentp transunit-ensemble gcc) → fty::result
Function:
(defun transunit-ensemble-aidentp (transunit-ensemble gcc) (declare (xargs :guard (and (transunit-ensemblep transunit-ensemble) (booleanp gcc)))) (declare (ignorable transunit-ensemble)) (let ((__function__ 'transunit-ensemble-aidentp)) (declare (ignorable __function__)) (filepath-transunit-map-aidentp (transunit-ensemble->unwrap transunit-ensemble) gcc)))
Theorem:
(defthm booleanp-of-transunit-ensemble-aidentp (b* ((fty::result (transunit-ensemble-aidentp transunit-ensemble gcc))) (booleanp fty::result)) :rule-classes :rewrite)
Theorem:
(defthm transunit-ensemble-aidentp-of-transunit-ensemble-fix-transunit-ensemble (equal (transunit-ensemble-aidentp (transunit-ensemble-fix transunit-ensemble) gcc) (transunit-ensemble-aidentp transunit-ensemble gcc)))
Theorem:
(defthm transunit-ensemble-aidentp-transunit-ensemble-equiv-congruence-on-transunit-ensemble (implies (transunit-ensemble-equiv transunit-ensemble transunit-ensemble-equiv) (equal (transunit-ensemble-aidentp transunit-ensemble gcc) (transunit-ensemble-aidentp transunit-ensemble-equiv gcc))) :rule-classes :congruence)
Theorem:
(defthm transunit-ensemble-aidentp-of-bool-fix-gcc (equal (transunit-ensemble-aidentp transunit-ensemble (bool-fix gcc)) (transunit-ensemble-aidentp transunit-ensemble gcc)))
Theorem:
(defthm transunit-ensemble-aidentp-iff-congruence-on-gcc (implies (iff gcc gcc-equiv) (equal (transunit-ensemble-aidentp transunit-ensemble gcc) (transunit-ensemble-aidentp transunit-ensemble gcc-equiv))) :rule-classes :congruence)