Modeling in ACL2

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.