		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-order-permutationp

Check if an order parameter is a valid permutation.

Signature
(defdefparse-order-permutationp order) → yes/no
Arguments: order — Guard (pos-listp order).
Returns: yes/no — Type (booleanp yes/no).

We check if a list of length n is a permutation of (1 ... n).

Definitions and Theorems

Function: defdefparse-order-permutationp-aux

(defun defdefparse-order-permutationp-aux (a b)
 (declare (xargs :guard (and (pos-listp a) (pos-listp b))))
 (let ((__function__ 'defdefparse-order-permutationp-aux))
  (declare (ignorable __function__))
  (cond
   ((endp a) (endp b))
   (t
    (and
       (member (car a) b)
       (defdefparse-order-permutationp-aux (cdr a)
                                           (remove1 (car a) b)))))))

Theorem: booleanp-of-defdefparse-order-permutationp-aux

(defthm booleanp-of-defdefparse-order-permutationp-aux
  (b* ((yes/no (defdefparse-order-permutationp-aux a b)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Function: defdefparse-order-permutationp

(defun defdefparse-order-permutationp (order)
  (declare (xargs :guard (pos-listp order)))
  (let ((__function__ 'defdefparse-order-permutationp))
    (declare (ignorable __function__))
    (defdefparse-order-permutationp-aux
         order
         (integers-from-to 1 (len order)))))

Theorem: booleanp-of-defdefparse-order-permutationp

(defthm booleanp-of-defdefparse-order-permutationp
  (b* ((yes/no (defdefparse-order-permutationp order)))
    (booleanp yes/no))
  :rule-classes :rewrite)