		Search-engine friendly clone of the ACL2 documentation.

Semantics

Terminatingp

Check if a configuration is terminating.

If we try to exhaustively apply the step function to an initial configuration, either we will reach a final configuration with no commands, or we will keep stepping forever. This function recognizes which situation we are in: it is a property of the initial configuration.

This function is not executable. It uses an (unbounded) existential quantifier. The configuration is terminating if there is a number of steps after which the final configuration has no commands.

Definitions and Theorems

Theorem: terminatingp-suff

(defthm terminatingp-suff
  (implies (and (natp n)
                (not (consp (config->comms (stepn cfg n)))))
           (terminatingp cfg)))

Theorem: booleanp-of-terminatingp

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

Theorem: terminatingp-of-config-fix-cfg

(defthm terminatingp-of-config-fix-cfg
  (equal (terminatingp (config-fix cfg))
         (terminatingp cfg)))

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

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

Theorem: natp-of-terminatingp-witness

(defthm natp-of-terminatingp-witness
  (implies (terminatingp cfg)
           (natp (terminatingp-witness cfg)))
  :rule-classes :type-prescription)