		Search-engine friendly clone of the ACL2 documentation.

Evaluation

Terminatingp

Check if an evaluation state is terminating.

This is the case when a final or error state can be reached in a finite number of steps.

This is a non-executable predicate.

Definitions and Theorems

Theorem: terminatingp-suff

(defthm
 terminatingp-suff
 (implies (and (natp n)
               (member-eq (eval-state-kind (stepn estate n program))
                          '(:final :error))
               t)
          (terminatingp estate program)))

Theorem: booleanp-of-terminatingp

(defthm booleanp-of-terminatingp
        (b* ((yes/no (terminatingp estate program)))
            (booleanp yes/no))
        :rule-classes :rewrite)

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

(defthm terminatingp-of-eval-state-fix-estate
        (equal (terminatingp (eval-state-fix estate)
                             program)
               (terminatingp estate program)))

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

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

Theorem: terminatingp-of-program-fix-program

(defthm terminatingp-of-program-fix-program
        (equal (terminatingp estate (program-fix program))
               (terminatingp estate program)))

Theorem: terminatingp-program-equiv-congruence-on-program

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

Theorem: natp-of-terminatingp-witness-when-terminatingp

(defthm natp-of-terminatingp-witness-when-terminatingp
        (implies (terminatingp estate program)
                 (natp (terminatingp-witness estate program)))
        :rule-classes :type-prescription)

Theorem: terminating-state-is-final-or-error

(defthm
 terminating-state-is-final-or-error
 (implies
  (terminatingp estate program)
  (member-equal
       (eval-state-kind (stepn estate
                               (terminatingp-witness estate program)
                               program))
       '(:final :error)))
 :rule-classes nil)