		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-unambp

Code-ensemble-unambp

Signature
(code-ensemble-unambp code-ensemble) → fty::result
Arguments: code-ensemble — Guard (code-ensemblep code-ensemble).
Returns: fty::result — Type (booleanp fty::result).

Definitions and Theorems

Function: code-ensemble-unambp

(defun code-ensemble-unambp (code-ensemble)
  (declare (xargs :guard (code-ensemblep code-ensemble)))
  (declare (ignorable code-ensemble))
  (let ((__function__ 'code-ensemble-unambp))
    (declare (ignorable __function__))
    (transunit-ensemble-unambp
         (code-ensemble->transunits code-ensemble))))

Theorem: booleanp-of-code-ensemble-unambp

(defthm booleanp-of-code-ensemble-unambp
  (b* ((fty::result (code-ensemble-unambp code-ensemble)))
    (booleanp fty::result))
  :rule-classes :rewrite)

Theorem: code-ensemble-unambp-of-code-ensemble-fix-code-ensemble

(defthm code-ensemble-unambp-of-code-ensemble-fix-code-ensemble
  (equal (code-ensemble-unambp (code-ensemble-fix code-ensemble))
         (code-ensemble-unambp code-ensemble)))

Theorem: code-ensemble-unambp-code-ensemble-equiv-congruence-on-code-ensemble

(defthm
 code-ensemble-unambp-code-ensemble-equiv-congruence-on-code-ensemble
 (implies (code-ensemble-equiv code-ensemble code-ensemble-equiv)
          (equal (code-ensemble-unambp code-ensemble)
                 (code-ensemble-unambp code-ensemble-equiv)))
 :rule-classes :congruence)