		Search-engine friendly clone of the ACL2 documentation.

Random$

Random-list-aux

Add random numbers onto an accumulator.

Definitions and Theorems

Function: random-list-aux

(defun random-list-aux (n limit acc state)
  (declare (xargs :guard (and (natp n)
                              (posp limit)
                              (true-listp acc))))
  (if (zp n)
      (mv (reverse acc) state)
    (b* (((mv x1 state) (random$ limit state)))
      (random-list-aux (- n 1)
                       limit (cons x1 acc)
                       state))))

Theorem: nat-listp-of-random-list-aux

(defthm nat-listp-of-random-list-aux
 (implies
   (nat-listp acc)
   (equal (nat-listp (mv-nth 0 (random-list-aux n limit acc state)))
          (nat-listp acc))))

Theorem: state-p1-of-random-list-aux

(defthm state-p1-of-random-list-aux
  (implies (force (state-p1 state))
           (state-p1 (mv-nth 1
                             (random-list-aux n limit acc state)))))