		Search-engine friendly clone of the ACL2 documentation.

Atc-symbolic-computation-states

Atc-compustate-frames-number-rules

Rules about compustate-frames-number.

The first four theorems about compustate-frames-number serve to discharge the hypotheses about it being not 0 in some of the other theorems. These are all immediately discharged, because the functions used to represent the symbolic execution states satisfy that condition (by design, for add-var and update-var).

The last theorems serve to skip over update-object calls.

Definitions and Theorems

Theorem: compustate-frames-number-of-add-frame-not-zero

(defthm compustate-frames-number-of-add-frame-not-zero
  (> (compustate-frames-number (add-frame fun compst))
     0))

Theorem: compustate-frames-number-of-enter-scope-not-zero

(defthm compustate-frames-number-of-enter-scope-not-zero
  (> (compustate-frames-number (enter-scope compst))
     0))

Theorem: compustate-frames-number-of-add-var-not-zero

(defthm compustate-frames-number-of-add-var-not-zero
  (> (compustate-frames-number (add-var var val compst))
     0))

Theorem: compustate-frames-number-of-update-var

(defthm compustate-frames-number-of-update-var
  (equal (compustate-frames-number (update-var var val compst))
         (compustate-frames-number compst)))

Theorem: compustate-frames-number-of-update-static-var

(defthm compustate-frames-number-of-update-static-var
  (equal
       (compustate-frames-number (update-static-var var val compst))
       (compustate-frames-number compst)))

Theorem: compustate-frames-number-of-update-object

(defthm compustate-frames-number-of-update-object
 (equal (compustate-frames-number (update-object objdes obj compst))
        (compustate-frames-number compst)))