		Search-engine friendly clone of the ACL2 documentation.

State-stobj

Make-stat1

Signature
(make-stat1 xregs pc memory error) → stat1
Arguments: xregs — Guard (stat1-xregs-p xregs).; pc — Guard (stat1-pc-p pc).; memory — Guard (stat1-memory-p memory).; error — Guard (stat1-error-p error).
Returns: stat1 — Type (stat1p stat1), given the guard.

Definitions and Theorems

Function: make-stat1

(defun make-stat1 (xregs pc memory error)
  (declare (xargs :guard (and (stat1-xregs-p xregs)
                              (stat1-pc-p pc)
                              (stat1-memory-p memory)
                              (stat1-error-p error))))
  (list xregs pc memory error))

Theorem: stat1p-of-make-stat1

(defthm stat1p-of-make-stat1
  (implies (and (stat1-xregs-p xregs)
                (stat1-pc-p pc)
                (stat1-memory-p memory)
                (stat1-error-p error))
           (b* ((stat1 (make-stat1 xregs pc memory error)))
             (stat1p stat1)))
  :rule-classes :rewrite)