Recognizer for m-assumption-n-output-comb-transform.
(m-assumption-n-output-comb-transform-p x) → *
Function:
(defun m-assumption-n-output-comb-transform-p (x) (declare (xargs :guard t)) (let ((__function__ 'm-assumption-n-output-comb-transform-p)) (declare (ignorable __function__)) (case (tag x) ((:balance-config :fraig-config :rewrite-config :abc-comb-simp-config :obs-constprop-config :observability-config :constprop-config :snapshot-config :prune-config :unreachability-config :dom-supergates-sweep-config) (comb-transform-p x)) ((:n-outputs-unreachability-config) (n-outputs-unreachability-config-p x)) ((:n-outputs-dom-supergates-sweep-config) (n-outputs-dom-supergates-sweep-config-p x)) ((:m-assum-n-output-observability-config) (m-assum-n-output-observability-config-p x)) (otherwise (parametrize-config-p x)))))
Theorem:
(defthm consp-when-m-assumption-n-output-comb-transform-p (implies (m-assumption-n-output-comb-transform-p x) (consp x)) :rule-classes :compound-recognizer)
Theorem:
(defthm m-assumption-n-output-comb-transform-p-when-comb-transform-p (implies (comb-transform-p x) (m-assumption-n-output-comb-transform-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm m-assumption-n-output-comb-transform-p-when-n-outputs-unreachability-config-p (implies (n-outputs-unreachability-config-p x) (m-assumption-n-output-comb-transform-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm m-assumption-n-output-comb-transform-p-when-n-outputs-dom-supergates-sweep-config-p (implies (n-outputs-dom-supergates-sweep-config-p x) (m-assumption-n-output-comb-transform-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm m-assumption-n-output-comb-transform-p-when-m-assum-n-output-observability-config-p (implies (m-assum-n-output-observability-config-p x) (m-assumption-n-output-comb-transform-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm m-assumption-n-output-comb-transform-p-when-parametrize-config-p (implies (parametrize-config-p x) (m-assumption-n-output-comb-transform-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm comb-transform-p-by-tag-when-m-assumption-n-output-comb-transform-p (implies (and (or (equal (tag x) :balance-config) (equal (tag x) :fraig-config) (equal (tag x) :rewrite-config) (equal (tag x) :abc-comb-simp-config) (equal (tag x) :obs-constprop-config) (equal (tag x) :observability-config) (equal (tag x) :constprop-config) (equal (tag x) :snapshot-config) (equal (tag x) :prune-config) (equal (tag x) :unreachability-config) (equal (tag x) :dom-supergates-sweep-config)) (m-assumption-n-output-comb-transform-p x)) (comb-transform-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm n-outputs-unreachability-config-p-by-tag-when-m-assumption-n-output-comb-transform-p (implies (and (or (equal (tag x) :n-outputs-unreachability-config)) (m-assumption-n-output-comb-transform-p x)) (n-outputs-unreachability-config-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm n-outputs-dom-supergates-sweep-config-p-by-tag-when-m-assumption-n-output-comb-transform-p (implies (and (or (equal (tag x) :n-outputs-dom-supergates-sweep-config)) (m-assumption-n-output-comb-transform-p x)) (n-outputs-dom-supergates-sweep-config-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm m-assum-n-output-observability-config-p-by-tag-when-m-assumption-n-output-comb-transform-p (implies (and (or (equal (tag x) :m-assum-n-output-observability-config)) (m-assumption-n-output-comb-transform-p x)) (m-assum-n-output-observability-config-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm parametrize-config-p-by-tag-when-m-assumption-n-output-comb-transform-p (implies (and (or (equal (tag x) :parametrize-config)) (m-assumption-n-output-comb-transform-p x)) (parametrize-config-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm m-assumption-n-output-comb-transform-p-when-invalid-tag (implies (and (not (equal (tag x) :balance-config)) (not (equal (tag x) :fraig-config)) (not (equal (tag x) :rewrite-config)) (not (equal (tag x) :abc-comb-simp-config)) (not (equal (tag x) :obs-constprop-config)) (not (equal (tag x) :observability-config)) (not (equal (tag x) :constprop-config)) (not (equal (tag x) :snapshot-config)) (not (equal (tag x) :prune-config)) (not (equal (tag x) :unreachability-config)) (not (equal (tag x) :dom-supergates-sweep-config)) (not (equal (tag x) :n-outputs-unreachability-config)) (not (equal (tag x) :n-outputs-dom-supergates-sweep-config)) (not (equal (tag x) :m-assum-n-output-observability-config)) (not (equal (tag x) :parametrize-config))) (not (m-assumption-n-output-comb-transform-p x))) :rule-classes ((:rewrite :backchain-limit-lst 0)))
Theorem:
(defthm tag-when-m-assumption-n-output-comb-transform-p-forward (implies (m-assumption-n-output-comb-transform-p x) (or (equal (tag x) :balance-config) (equal (tag x) :fraig-config) (equal (tag x) :rewrite-config) (equal (tag x) :abc-comb-simp-config) (equal (tag x) :obs-constprop-config) (equal (tag x) :observability-config) (equal (tag x) :constprop-config) (equal (tag x) :snapshot-config) (equal (tag x) :prune-config) (equal (tag x) :unreachability-config) (equal (tag x) :dom-supergates-sweep-config) (equal (tag x) :n-outputs-unreachability-config) (equal (tag x) :n-outputs-dom-supergates-sweep-config) (equal (tag x) :m-assum-n-output-observability-config) (equal (tag x) :parametrize-config))) :rule-classes ((:forward-chaining)))