		Search-engine friendly clone of the ACL2 documentation.

Jubjub

Jubjub-r

The constant r_\mathbb{J} in [ZPS:5.4.9.3].

Signature
(jubjub-r) → r
Returns: r — Type (natp r).

Definitions and Theorems

Function: jubjub-r

(defun jubjub-r nil
  (declare (xargs :guard t))
  (let ((__function__ 'jubjub-r))
    (declare (ignorable __function__))
    (primes::jubjub-subgroup-prime)))

Theorem: natp-of-jubjub-r

(defthm natp-of-jubjub-r
  (b* ((r (jubjub-r))) (natp r))
  :rule-classes :rewrite)

Theorem: primep-of-jubjub-r

(defthm primep-of-jubjub-r
  (primep (jubjub-r)))