		Search-engine friendly clone of the ACL2 documentation.

Computation-states

Compustate-frames-number

Number of frames in the call stack of a computation state.

Signature
(compustate-frames-number compst) → n
Arguments: compst — Guard (compustatep compst).
Returns: n — Type (natp n).

The theorem compustate-frames-number-of-compustate-same-frames is useful to show that change-compustate for a component other than :frames preserves the number of frames.

Definitions and Theorems

Function: compustate-frames-number

(defun compustate-frames-number (compst)
  (declare (xargs :guard (compustatep compst)))
  (let ((__function__ 'compustate-frames-number))
    (declare (ignorable __function__))
    (len (compustate->frames compst))))

Theorem: natp-of-compustate-frames-number

(defthm natp-of-compustate-frames-number
  (b* ((n (compustate-frames-number compst)))
    (natp n))
  :rule-classes :rewrite)

Theorem: compustate-frames-number-of-compustate-same-frames

(defthm compustate-frames-number-of-compustate-same-frames
  (equal (compustate-frames-number
              (compustate static (compustate->frames compst)
                          heap))
         (compustate-frames-number compst)))

Theorem: compustate-frames-number-of-compustate-fix-compst

(defthm compustate-frames-number-of-compustate-fix-compst
  (equal (compustate-frames-number (compustate-fix compst))
         (compustate-frames-number compst)))

Theorem: compustate-frames-number-compustate-equiv-congruence-on-compst

(defthm
     compustate-frames-number-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (compustate-frames-number compst)
                  (compustate-frames-number compst-equiv)))
  :rule-classes :congruence)