Recognizer for fgl-sat-config.
(fgl-sat-config-p x) → *
Function:
(defun fgl-sat-config-p (x) (declare (xargs :guard t)) (let ((__function__ 'fgl-sat-config-p)) (declare (ignorable __function__)) (case (tag x) ((:fgl-satlink-config) (fgl-satlink-monolithic-sat-config-p x)) ((:fgl-ipasir-config) (fgl-ipasir-config-p x)) (otherwise (fgl-exhaustive-test-config-p x)))))
Theorem:
(defthm consp-when-fgl-sat-config-p (implies (fgl-sat-config-p x) (consp x)) :rule-classes :compound-recognizer)
Theorem:
(defthm fgl-sat-config-p-when-fgl-satlink-monolithic-sat-config-p (implies (fgl-satlink-monolithic-sat-config-p x) (fgl-sat-config-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm fgl-sat-config-p-when-fgl-ipasir-config-p (implies (fgl-ipasir-config-p x) (fgl-sat-config-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm fgl-sat-config-p-when-fgl-exhaustive-test-config-p (implies (fgl-exhaustive-test-config-p x) (fgl-sat-config-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm fgl-satlink-monolithic-sat-config-p-by-tag-when-fgl-sat-config-p (implies (and (or (equal (tag x) :fgl-satlink-config)) (fgl-sat-config-p x)) (fgl-satlink-monolithic-sat-config-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm fgl-ipasir-config-p-by-tag-when-fgl-sat-config-p (implies (and (or (equal (tag x) :fgl-ipasir-config)) (fgl-sat-config-p x)) (fgl-ipasir-config-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm fgl-exhaustive-test-config-p-by-tag-when-fgl-sat-config-p (implies (and (or (equal (tag x) :fgl-exhaustive-test-config)) (fgl-sat-config-p x)) (fgl-exhaustive-test-config-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm fgl-sat-config-p-when-invalid-tag (implies (and (not (equal (tag x) :fgl-satlink-config)) (not (equal (tag x) :fgl-ipasir-config)) (not (equal (tag x) :fgl-exhaustive-test-config))) (not (fgl-sat-config-p x))) :rule-classes ((:rewrite :backchain-limit-lst 0)))
Theorem:
(defthm tag-when-fgl-sat-config-p-forward (implies (fgl-sat-config-p x) (or (equal (tag x) :fgl-satlink-config) (equal (tag x) :fgl-ipasir-config) (equal (tag x) :fgl-exhaustive-test-config))) :rule-classes ((:forward-chaining)))