		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)))))