		Search-engine friendly clone of the ACL2 documentation.

Make-self-code-ensemble

Code-ensemble-make-self

Signature
(code-ensemble-make-self code-ensemble) → *
Arguments: code-ensemble — Guard (code-ensemblep code-ensemble).

Definitions and Theorems

Function: code-ensemble-make-self

(defun code-ensemble-make-self (code-ensemble)
  (declare (xargs :guard (code-ensemblep code-ensemble)))
  (let ((__function__ 'code-ensemble-make-self))
    (declare (ignorable __function__))
    (list 'code-ensemble
          (transunit-ensemble-make-self
               (code-ensemble->transunits code-ensemble))
          (ienv-make-self (code-ensemble->ienv code-ensemble)))))

Theorem: code-ensemble-make-self-of-code-ensemble-fix-code-ensemble

(defthm code-ensemble-make-self-of-code-ensemble-fix-code-ensemble
  (equal (code-ensemble-make-self (code-ensemble-fix code-ensemble))
         (code-ensemble-make-self code-ensemble)))

Theorem: code-ensemble-make-self-code-ensemble-equiv-congruence-on-code-ensemble

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