(supergate-has-contradiction-top x) → *
Function:
(defun supergate-has-contradiction-top (x) (declare (xargs :guard (lit-listp x))) (let ((__function__ 'supergate-has-contradiction-top)) (declare (ignorable __function__)) (mbe :logic (supergate-has-contradiction x) :exec (and (consp x) (supergate-has-contradiction x)))))
Theorem:
(defthm supergate-has-contradiction-top-of-lit-list-fix-x (equal (supergate-has-contradiction-top (lit-list-fix x)) (supergate-has-contradiction-top x)))
Theorem:
(defthm supergate-has-contradiction-top-lit-list-equiv-congruence-on-x (implies (satlink::lit-list-equiv x x-equiv) (equal (supergate-has-contradiction-top x) (supergate-has-contradiction-top x-equiv))) :rule-classes :congruence)