Using the stable-under-simplificationp flag  A problem with the
example in using-computed-hints-6 is that exactly one
simplification occurs between each (effective) firing of the
hint. Much more commonly we wish to fire a hint once a subgoal
has become stable under simplification.  A classic example of
this is when we are dealing with an interpreter for some state
machine. We typically do not want the ``step'' function to open
up on the symbolic representation of a state until that state
has been maximally simplified. We will illustrate with a simple
state machine.  Let us start by defining the step function, stp,
and the corresponding run function that applies it a given
number of times.  (defun stp (s)   (+ 1 s))  (defun run (s n)
(if (zp n) s (run (stp s) (- n 1))))  The step function here is
trivial: a state is just a number and the step function
increments it. In this example we will not be interested in the
theorems we prove but in how we prove them. The formula we will
focus on is (thm (equal (run s 7)