		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Stat1-validp{1}

Simplify stat1-validp{0} after the isomorphic state transformation.

stat1-validp{0} includes term of the form (stat->FIELD (stat-from-stat1 stat)). By enabling stat-from-stat1, those turn into (stat->FIELD (stat ... (stat1->FIELD <field>) ...)), which reduces to (stat1->FIELD <field>) as desired.

Definitions and Theorems

Function: stat1-validp{1}

(defun stat1-validp{1} (stat feat)
  (declare (xargs :non-executable t))
  (declare (xargs :guard (and (stat1p stat) (featp feat))))
  (prog2$ (acl2::throw-nonexec-error 'stat1-validp{1}
                                     (list stat feat))
          (and (mbt (stat1p stat))
               (let* ((stat.xregs (stat1->xregs stat))
                      (stat.pc (stat1->pc stat)))
                 (let nil
                   (let* ((xlen (feat->xlen feat))
                          (xnum (feat->xnum feat)))
                     (and (unsigned-byte-listp xlen stat.xregs)
                          (equal (len stat.xregs) (+ -1 xnum))
                          (unsigned-byte-p xlen stat.pc)
                          (equal (len (stat1->memory stat))
                                 (expt 2 xlen)))))))))

Theorem: stat1-validp{0}-becomes-stat1-validp{1}

(defthm stat1-validp{0}-becomes-stat1-validp{1}
  (equal (stat1-validp{0} stat feat)
         (stat1-validp{1} stat feat)))