(vl-evatomlist-has-edge x) → *
Function:
(defun vl-evatomlist-has-edge (x) (declare (xargs :guard (vl-evatomlist-p x))) (let ((__function__ 'vl-evatomlist-has-edge)) (declare (ignorable __function__)) (if (atom x) nil (or (not (eq (vl-evatom->type (car x)) :vl-noedge)) (vl-evatomlist-has-edge (cdr x))))))
Theorem:
(defthm vl-evatomlist-has-edge-of-vl-evatomlist-fix-x (equal (vl-evatomlist-has-edge (vl-evatomlist-fix x)) (vl-evatomlist-has-edge x)))
Theorem:
(defthm vl-evatomlist-has-edge-vl-evatomlist-equiv-congruence-on-x (implies (vl-evatomlist-equiv x x-equiv) (equal (vl-evatomlist-has-edge x) (vl-evatomlist-has-edge x-equiv))) :rule-classes :congruence)