(vl-parse-op-alist-p arity x) → *
Function:
(defun vl-parse-op-alist-p (arity x) (declare (xargs :guard (maybe-natp arity))) (let ((__function__ 'vl-parse-op-alist-p)) (declare (ignorable __function__)) (if (atom x) (not x) (and (consp (car x)) (symbolp (caar x)) (vl-op-p (cdar x)) (eql arity (vl-op-arity (cdar x))) (vl-parse-op-alist-p arity (cdr x))))))
Theorem:
(defthm vl-parse-op-alist-p-when-atom (implies (atom x) (equal (vl-parse-op-alist-p arity x) (not x))))
Theorem:
(defthm vl-parse-op-alist-p-of-cons (equal (vl-parse-op-alist-p arity (cons a x)) (and (consp a) (symbolp (car a)) (vl-op-p (cdr a)) (eql arity (vl-op-arity (cdr a))) (vl-parse-op-alist-p arity x))))