Below we define mc(s,n) to be the function that single-steps n
times from a given starting state, s. In Common Lisp, ``mc(s,n)'' is
written (mc s n).
(defun mc (s n) ; To step s n times:
(if (zp n) ; If n is 0
s ; then return s
(mc (single-step s) (- n 1)))) ; else step single-step(s)
n-1 times.
This is an example of a formal model in ACL2.
