		Search-engine friendly clone of the ACL2 documentation.

Unambiguity

Code-ensemble-unambp

Check if a code ensemble is unambiguous.

Signature
(code-ensemble-unambp code) → yes/no
Arguments: code — Guard (code-ensemblep code).
Returns: yes/no — Type (booleanp yes/no).

That is, check whether the translation unit ensemble is unambiguous. The implementation environment is ignored for this, but it is convenient to lift the unambiguity predicate from translation unit ensembles to code ensembles.

Definitions and Theorems

Function: code-ensemble-unambp

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

Theorem: booleanp-of-code-ensemble-unambp

(defthm booleanp-of-code-ensemble-unambp
  (b* ((yes/no (code-ensemble-unambp code)))
    (booleanp yes/no))
  :rule-classes :rewrite)

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

(defthm code-ensemble-unambp-of-code-ensemble
  (equal (code-ensemble-unambp (code-ensemble tunits ienv))
         (transunit-ensemble-unambp tunits)))

Theorem: transunit-ensemble-unambp-of-code-ensemble->transunits

(defthm transunit-ensemble-unambp-of-code-ensemble->transunits
 (implies
      (code-ensemble-unambp code)
      (transunit-ensemble-unambp (code-ensemble->transunits code))))

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

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

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

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