		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)