		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Elab-mod$a-ninsts

Signature
(elab-mod$a-ninsts elab-mod$a) → *
Arguments: elab-mod$a — Guard (elab-mod$ap elab-mod$a).

Definitions and Theorems

Function: elab-mod$a-ninsts

(defun elab-mod$a-ninsts (elab-mod$a)
  (declare (xargs :guard (elab-mod$ap elab-mod$a)))
  (let ((__function__ 'elab-mod$a-ninsts))
    (declare (ignorable __function__))
    (len (g :insts (elab-mod$a-fix elab-mod$a)))))

Theorem: elab-mod$a-ninsts-of-elab-mod$a-fix-elab-mod$a

(defthm elab-mod$a-ninsts-of-elab-mod$a-fix-elab-mod$a
  (equal (elab-mod$a-ninsts (elab-mod$a-fix elab-mod$a))
         (elab-mod$a-ninsts elab-mod$a)))

Theorem: elab-mod$a-ninsts-elab-mod$a-equiv-congruence-on-elab-mod$a

(defthm elab-mod$a-ninsts-elab-mod$a-equiv-congruence-on-elab-mod$a
  (implies (elab-mod$a-equiv elab-mod$a elab-mod$a-equiv)
           (equal (elab-mod$a-ninsts elab-mod$a)
                  (elab-mod$a-ninsts elab-mod$a-equiv)))
  :rule-classes :congruence)