(aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash) → (mv pairing remaining)
Function:
(defun aignet-balance-find-pairing-rec (first limit level-ref rest levels gatesimp aignet2 strash) (declare (xargs :stobjs (levels aignet2 strash))) (declare (type (unsigned-byte 30) first)) (declare (xargs :guard (and (litp first) (natp limit) (litp level-ref) (lit-listp rest) (gatesimp-p gatesimp)))) (declare (xargs :guard (and (fanin-litp first aignet2) (fanin-litp level-ref aignet2) (aignet-lit-listp rest aignet2) (<= (num-fanins aignet2) (u32-length levels))))) (let ((__function__ 'aignet-balance-find-pairing-rec)) (declare (ignorable __function__)) (b* ((rest (lit-list-fix rest)) ((when (or (atom rest) (zp limit) (and (not (lit-equiv 0 level-ref)) (levels-sort-< (lit-fix level-ref) (car rest) levels)))) (mv nil rest)) (candidate (lit-fix (car rest))) ((when (eql (lit-id candidate) (lit-id first))) (mv candidate (cdr rest))) ((mv existing & & &) (mbe :logic (aignet-and-gate-simp/strash first candidate gatesimp strash aignet2) :exec (if (<= (car rest) 536870911) (aignet-and-gate-simp/strash first candidate gatesimp strash aignet2) (ec-call (aignet-and-gate-simp/strash first candidate gatesimp strash aignet2))))) ((when existing) (mv candidate (cdr rest))) ((mv pairing remaining) (aignet-balance-find-pairing-rec first (1- limit) level-ref (cdr rest) levels gatesimp aignet2 strash)) ((when pairing) (mv pairing (cons candidate remaining)))) (mv nil rest))))
Theorem:
(defthm return-type-of-aignet-balance-find-pairing-rec.pairing (b* (((mv ?pairing ?remaining) (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash))) (iff (litp pairing) pairing)) :rule-classes :rewrite)
Theorem:
(defthm lit-listp-of-aignet-balance-find-pairing-rec.remaining (b* (((mv ?pairing ?remaining) (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash))) (lit-listp remaining)) :rule-classes :rewrite)
Theorem:
(defthm aignet-balance-find-pairing-rec-correct-when-found (b* (((mv ?pairing ?remaining) (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash))) (implies pairing (equal (b-and (lit-eval pairing invals regvals aignet2) (aignet-eval-conjunction remaining invals regvals aignet2)) (aignet-eval-conjunction rest invals regvals aignet2)))))
Theorem:
(defthm aignet-balance-find-pairing-rec-correct-when-found-rest (b* (((mv ?pairing ?remaining) (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash))) (implies pairing (equal (b-and (lit-eval pairing invals regvals aignet2) (b-and (aignet-eval-conjunction remaining invals regvals aignet2) c)) (b-and (aignet-eval-conjunction rest invals regvals aignet2) c)))))
Theorem:
(defthm aignet-balance-find-pairing-rec-when-not-found (b* (((mv ?pairing ?remaining) (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash))) (implies (not pairing) (equal remaining (lit-list-fix rest)))))
Theorem:
(defthm len-of-aignet-balance-find-pairing-rec (b* (((mv ?pairing ?remaining) (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash))) (equal (len remaining) (if pairing (1- (len rest)) (len rest)))))
Theorem:
(defthm aignet-lit-listp-of-aignet-balance-find-pairing-rec (b* (((mv ?pairing ?remaining) (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash))) (implies (aignet-lit-listp rest aignet) (aignet-lit-listp remaining aignet))))
Theorem:
(defthm aignet-litp-of-aignet-balance-find-pairing-rec (b* (((mv ?pairing ?remaining) (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash))) (implies (and (aignet-lit-listp rest aignet) pairing) (aignet-litp pairing aignet))))
Theorem:
(defthm aignet-balance-find-pairing-rec-of-lit-fix-first (equal (aignet-balance-find-pairing-rec (lit-fix first) limit level-ref rest levels gatesimp aignet2 strash) (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash)))
Theorem:
(defthm aignet-balance-find-pairing-rec-lit-equiv-congruence-on-first (implies (lit-equiv first first-equiv) (equal (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash) (aignet-balance-find-pairing-rec first-equiv limit level-ref rest levels gatesimp aignet2 strash))) :rule-classes :congruence)
Theorem:
(defthm aignet-balance-find-pairing-rec-of-nfix-limit (equal (aignet-balance-find-pairing-rec first (nfix limit) level-ref rest levels gatesimp aignet2 strash) (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash)))
Theorem:
(defthm aignet-balance-find-pairing-rec-nat-equiv-congruence-on-limit (implies (nat-equiv limit limit-equiv) (equal (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash) (aignet-balance-find-pairing-rec first limit-equiv level-ref rest levels gatesimp aignet2 strash))) :rule-classes :congruence)
Theorem:
(defthm aignet-balance-find-pairing-rec-of-lit-fix-level-ref (equal (aignet-balance-find-pairing-rec first limit (lit-fix level-ref) rest levels gatesimp aignet2 strash) (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash)))
Theorem:
(defthm aignet-balance-find-pairing-rec-lit-equiv-congruence-on-level-ref (implies (lit-equiv level-ref level-ref-equiv) (equal (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash) (aignet-balance-find-pairing-rec first limit level-ref-equiv rest levels gatesimp aignet2 strash))) :rule-classes :congruence)
Theorem:
(defthm aignet-balance-find-pairing-rec-of-lit-list-fix-rest (equal (aignet-balance-find-pairing-rec first limit level-ref (lit-list-fix rest) levels gatesimp aignet2 strash) (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash)))
Theorem:
(defthm aignet-balance-find-pairing-rec-lit-list-equiv-congruence-on-rest (implies (satlink::lit-list-equiv rest rest-equiv) (equal (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash) (aignet-balance-find-pairing-rec first limit level-ref rest-equiv levels gatesimp aignet2 strash))) :rule-classes :congruence)
Theorem:
(defthm aignet-balance-find-pairing-rec-of-gatesimp-fix-gatesimp (equal (aignet-balance-find-pairing-rec first limit level-ref rest levels (gatesimp-fix gatesimp) aignet2 strash) (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash)))
Theorem:
(defthm aignet-balance-find-pairing-rec-gatesimp-equiv-congruence-on-gatesimp (implies (gatesimp-equiv gatesimp gatesimp-equiv) (equal (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp aignet2 strash) (aignet-balance-find-pairing-rec first limit level-ref rest levels gatesimp-equiv aignet2 strash))) :rule-classes :congruence)