		Search-engine friendly clone of the ACL2 documentation.

Built-in-theorems

Built-in-theorems-about-random$

Built-in theorems about random$.

Theorem: natp-random$

(defthm natp-random$
        (natp (car (random$ n state)))
        :rule-classes :type-prescription)

Theorem: random$-linear

(defthm random$-linear
        (and (<= 0 (car (random$ n state)))
             (implies (posp n)
                      (< (car (random$ n state)) n)))
        :rule-classes :linear)