		Search-engine friendly clone of the ACL2 documentation.

Semantics

Stepn

Bounded repetition of Imp steps.

Signature
(stepn cfg n) → new-config
Arguments: cfg — Guard (configp cfg).; n — Guard (natp n).
Returns: new-config — Type (configp new-config).

This function repeats the step function at most n times. It stops when either n is 0 or the configuration has no commands.

This bounded-repetition-step function is executable.

Definitions and Theorems

Function: stepn

(defun stepn (cfg n)
  (declare (xargs :guard (and (configp cfg) (natp n))))
  (b* (((when (zp n)) (config-fix cfg))
       ((unless (consp (config->comms cfg)))
        (config-fix cfg)))
    (stepn (step cfg) (1- n))))

Theorem: configp-of-stepn

(defthm configp-of-stepn
  (b* ((new-config (stepn cfg n)))
    (configp new-config))
  :rule-classes :rewrite)

Theorem: stepn-of-config-fix-cfg

(defthm stepn-of-config-fix-cfg
  (equal (stepn (config-fix cfg) n)
         (stepn cfg n)))

Theorem: stepn-config-equiv-congruence-on-cfg

(defthm stepn-config-equiv-congruence-on-cfg
  (implies (config-equiv cfg cfg-equiv)
           (equal (stepn cfg n)
                  (stepn cfg-equiv n)))
  :rule-classes :congruence)

Theorem: stepn-of-nfix-n

(defthm stepn-of-nfix-n
  (equal (stepn cfg (nfix n))
         (stepn cfg n)))

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

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