(aignet-build-wide-and lits gatesimp strash aignet) → (mv and-lit new-strash new-aignet)
Function:
(defun aignet-build-wide-and (lits gatesimp strash aignet) (declare (xargs :stobjs (strash aignet))) (declare (xargs :guard (and (lit-listp lits) (gatesimp-p gatesimp)))) (declare (xargs :guard (aignet-lit-listp lits aignet))) (let ((__function__ 'aignet-build-wide-and)) (declare (ignorable __function__)) (b* (((when (atom lits)) (b* ((aignet (aignet-fix aignet))) (mv 1 strash aignet))) ((mv rest strash aignet) (aignet-build-wide-and (cdr lits) gatesimp strash aignet))) (aignet-hash-and (car lits) rest gatesimp strash aignet))))
Theorem:
(defthm litp-of-aignet-build-wide-and.and-lit (b* (((mv ?and-lit ?new-strash ?new-aignet) (aignet-build-wide-and lits gatesimp strash aignet))) (litp and-lit)) :rule-classes :rewrite)
Theorem:
(defthm aignet-extension-p-of-aignet-build-wide-and (b* (((mv ?and-lit ?new-strash ?new-aignet) (aignet-build-wide-and lits gatesimp strash aignet))) (aignet-extension-p new-aignet aignet)))
Theorem:
(defthm aignet-litp-of-aignet-build-wide-and (b* (((mv ?and-lit ?new-strash ?new-aignet) (aignet-build-wide-and lits gatesimp strash aignet))) (implies (aignet-lit-listp lits aignet) (aignet-litp and-lit new-aignet))))
Theorem:
(defthm lit-eval-of-aignet-build-wide-and (b* (((mv ?and-lit ?new-strash ?new-aignet) (aignet-build-wide-and lits gatesimp strash aignet))) (implies (aignet-lit-listp lits aignet) (equal (lit-eval and-lit invals regvals new-aignet) (aignet-eval-conjunction lits invals regvals aignet)))))
Theorem:
(defthm stype-counts-of-aignet-build-wide-and (b* (((mv ?and-lit ?new-strash ?new-aignet) (aignet-build-wide-and lits gatesimp strash aignet))) (implies (and (not (equal (stype-fix stype) (and-stype))) (not (equal (stype-fix stype) (xor-stype)))) (equal (stype-count stype new-aignet) (stype-count stype aignet)))))
Theorem:
(defthm aignet-build-wide-and-of-lit-list-fix-lits (equal (aignet-build-wide-and (lit-list-fix lits) gatesimp strash aignet) (aignet-build-wide-and lits gatesimp strash aignet)))
Theorem:
(defthm aignet-build-wide-and-lit-list-equiv-congruence-on-lits (implies (satlink::lit-list-equiv lits lits-equiv) (equal (aignet-build-wide-and lits gatesimp strash aignet) (aignet-build-wide-and lits-equiv gatesimp strash aignet))) :rule-classes :congruence)
Theorem:
(defthm aignet-build-wide-and-of-gatesimp-fix-gatesimp (equal (aignet-build-wide-and lits (gatesimp-fix gatesimp) strash aignet) (aignet-build-wide-and lits gatesimp strash aignet)))
Theorem:
(defthm aignet-build-wide-and-gatesimp-equiv-congruence-on-gatesimp (implies (gatesimp-equiv gatesimp gatesimp-equiv) (equal (aignet-build-wide-and lits gatesimp strash aignet) (aignet-build-wide-and lits gatesimp-equiv strash aignet))) :rule-classes :congruence)
Theorem:
(defthm aignet-build-wide-and-of-node-list-fix-aignet (equal (aignet-build-wide-and lits gatesimp strash (node-list-fix aignet)) (aignet-build-wide-and lits gatesimp strash aignet)))
Theorem:
(defthm aignet-build-wide-and-node-list-equiv-congruence-on-aignet (implies (node-list-equiv aignet aignet-equiv) (equal (aignet-build-wide-and lits gatesimp strash aignet) (aignet-build-wide-and lits gatesimp strash aignet-equiv))) :rule-classes :congruence)