		Search-engine friendly clone of the ACL2 documentation.

Random$

Random$-lemmas

Lemmas about random$ available in the system/random book.

Definitions and Theorems

Theorem: natp-random$-better

(defthm natp-random$-better
  (natp (mv-nth 0 (random$ limit state)))
  :rule-classes :type-prescription)

Theorem: random$-linear-better

(defthm random$-linear-better
  (and (<= 0 (mv-nth 0 (random$ n state)))
       (implies (posp n)
                (< (mv-nth 0 (random$ n state)) n))))

Theorem: state-p1-of-random

(defthm state-p1-of-random
  (implies (force (state-p1 state))
           (state-p1 (mv-nth 1 (random$ limit state)))))