		Search-engine friendly clone of the ACL2 documentation.

Computation-states

Pop-frame

Pop a frame from a computation state's non-empty call stack.

Signature
(pop-frame compst) → new-compst
Arguments: compst — Guard (compustatep compst).
Returns: new-compst — Type (compustatep new-compst).

Definitions and Theorems

Function: pop-frame

(defun pop-frame (compst)
  (declare (xargs :guard (compustatep compst)))
  (declare (xargs :guard (> (compustate-frames-number compst)
                            0)))
  (let ((__function__ 'pop-frame))
    (declare (ignorable __function__))
    (b* ((stack (compustate->frames compst))
         (new-stack (cdr stack)))
      (change-compustate compst
                         :frames new-stack))))

Theorem: compustatep-of-pop-frame

(defthm compustatep-of-pop-frame
  (b* ((new-compst (pop-frame compst)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: compustate-frames-number-of-pop-frame

(defthm compustate-frames-number-of-pop-frame
  (implies (> (compustate-frames-number compst) 0)
           (b* ((?new-compst (pop-frame compst)))
             (equal (compustate-frames-number new-compst)
                    (1- (compustate-frames-number compst))))))

Theorem: pop-frame-of-push-frame

(defthm pop-frame-of-push-frame
  (equal (pop-frame (push-frame frame compst))
         (compustate-fix compst)))

Theorem: pop-frame-of-compustate-fix-compst

(defthm pop-frame-of-compustate-fix-compst
  (equal (pop-frame (compustate-fix compst))
         (pop-frame compst)))

Theorem: pop-frame-compustate-equiv-congruence-on-compst

(defthm pop-frame-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (pop-frame compst)
                  (pop-frame compst-equiv)))
  :rule-classes :congruence)