		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Inc41-pc

Refine inc4-pc to use the stobj states.

Definitions and Theorems

Function: inc41-pc

(defun inc41-pc (stat feat)
 (declare (xargs :non-executable t))
 (declare
    (xargs :guard (non-exec (and (stat1p stat)
                                 (statp (stat-from-stat1 stat))
                                 (featp feat)
                                 (stat-validp (stat-from-stat1 stat)
                                              feat)))))
 (prog2$ (acl2::throw-nonexec-error 'inc41-pc
                                    (list stat feat))
         (if (acl2::mbt$ (stat1p stat))
             (write-pc (+ (read-pc (stat-from-stat1 stat) feat)
                          4)
                       (stat-from-stat1 stat)
                       feat)
           0)))

Theorem: inc41-pc-to-inc4-pc

(defthm inc41-pc-to-inc4-pc
  (implies (stat1p stat)
           (equal (inc41-pc stat feat)
                  (inc4-pc (stat-from-stat1 stat) feat)))
  :rule-classes :rewrite)

Theorem: inc4-pc-to-inc41-pc

(defthm inc4-pc-to-inc41-pc
  (implies (statp stat)
           (equal (inc4-pc stat feat)
                  (inc41-pc (stat1-from-stat stat) feat)))
  :rule-classes :rewrite)