Refine error to use the stobj states.
Function:
(defun error1 (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 'error1 (list stat feat)) (let ((change-stat stat) (stat->error t)) (if (acl2::mbt$ (stat1p change-stat)) (let ((change-stat (stat-from-stat1 change-stat))) (stat (stat->xregs change-stat) (stat->pc change-stat) (stat->memory change-stat) stat->error)) 0))))
Theorem:
(defthm error1-to-error (implies (stat1p stat) (equal (error1 stat feat) (error (stat-from-stat1 stat) feat))) :rule-classes :rewrite)
Theorem:
(defthm error-to-error1 (implies (statp stat) (equal (error stat feat) (error1 (stat1-from-stat stat) feat))) :rule-classes :rewrite)