		Search-engine friendly clone of the ACL2 documentation.

Evaluation

Stepn

Perform at most a given number of evaluation steps.

Signature
(stepn estate n program) → new-estate
Arguments: estate — Guard (eval-state-p estate).; n — Guard (natp n).; program — Guard (programp program).
Returns: new-estate — Type (eval-state-p new-estate).

We repeatedly call step until either we reach a final or error state (from where no further evaluation step may take place) or we exhaust the given (maximum) number of steps.

Definitions and Theorems

Function: stepn

(defun stepn (estate n program)
  (declare (xargs :guard (and (eval-state-p estate)
                              (natp n)
                              (programp program))))
  (let ((__function__ 'stepn))
    (declare (ignorable __function__))
    (b* (((when (zp n)) (eval-state-fix estate))
         ((when (member-eq (eval-state-kind estate)
                           '(:final :error)))
          (eval-state-fix estate))
         (estate (step estate program)))
      (stepn estate (1- n) program))))

Theorem: eval-state-p-of-stepn

(defthm eval-state-p-of-stepn
  (b* ((new-estate (stepn estate n program)))
    (eval-state-p new-estate))
  :rule-classes :rewrite)

Theorem: stepn-of-eval-state-fix-estate

(defthm stepn-of-eval-state-fix-estate
  (equal (stepn (eval-state-fix estate)
                n program)
         (stepn estate n program)))

Theorem: stepn-eval-state-equiv-congruence-on-estate

(defthm stepn-eval-state-equiv-congruence-on-estate
  (implies (eval-state-equiv estate estate-equiv)
           (equal (stepn estate n program)
                  (stepn estate-equiv n program)))
  :rule-classes :congruence)

Theorem: stepn-of-nfix-n

(defthm stepn-of-nfix-n
  (equal (stepn estate (nfix n) program)
         (stepn estate n program)))

Theorem: stepn-nat-equiv-congruence-on-n

(defthm stepn-nat-equiv-congruence-on-n
  (implies (acl2::nat-equiv n n-equiv)
           (equal (stepn estate n program)
                  (stepn estate n-equiv program)))
  :rule-classes :congruence)

Theorem: stepn-of-program-fix-program

(defthm stepn-of-program-fix-program
  (equal (stepn estate n (program-fix program))
         (stepn estate n program)))

Theorem: stepn-program-equiv-congruence-on-program

(defthm stepn-program-equiv-congruence-on-program
  (implies (program-equiv program program-equiv)
           (equal (stepn estate n program)
                  (stepn estate n program-equiv)))
  :rule-classes :congruence)