(fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2) → (mv new-output-ranges new-aignet2)
Function:
(defun fraig-finish-copy-nonstrict (strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2) (declare (xargs :stobjs (classes aignet copy aignet2))) (declare (xargs :guard (and (acl2::maybe-natp strict-count) (aignet-output-range-map-p output-ranges) (symbolp save-candidate-equivs-as) (symbolp remove-candidate-equivs)))) (declare (xargs :guard (and (<= (num-fanins aignet) (lits-length copy)) (<= (num-regs aignet) (num-regs aignet2)) (or (not strict-count) (<= strict-count (num-outs aignet))) (aignet-copies-in-bounds copy aignet2) (equal (aignet-output-range-map-length output-ranges) (num-outs aignet)) (classes-wellformed classes) (equal (classes-size classes) (num-fanins aignet))))) (let ((__function__ 'fraig-finish-copy-nonstrict)) (declare (ignorable __function__)) (b* ((save-candidate-equivs-as (mbe :logic (acl2::symbol-fix save-candidate-equivs-as) :exec save-candidate-equivs-as)) (remove-candidate-equivs (mbe :logic (acl2::symbol-fix remove-candidate-equivs) :exec remove-candidate-equivs)) (output-ranges (aignet-output-range-map-fix output-ranges)) ((when (not strict-count)) (b* ((aignet2 (finish-copy-comb aignet copy aignet2))) (mv output-ranges aignet2))) ((mv first-ranges rest-ranges) (split-output-ranges strict-count output-ranges)) (first-ranges-length (aignet-output-range-map-length first-ranges)) (initial-segment (mbe :logic (max (nfix strict-count) first-ranges-length) :exec first-ranges-length)) (aignet2 (aignet-copy-outs-range 0 initial-segment aignet copy aignet2)) ((mv new-rest-ranges aignet2) (fraig-finish-copy-outs initial-segment rest-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2)) (aignet2 (aignet-copy-nxsts aignet copy aignet2))) (mv (append first-ranges new-rest-ranges) aignet2))))
Theorem:
(defthm aignet-output-range-map-p-of-fraig-finish-copy-nonstrict.new-output-ranges (b* (((mv ?new-output-ranges ?new-aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2))) (aignet-output-range-map-p new-output-ranges)) :rule-classes :rewrite)
Theorem:
(defthm aignet-extension-p-of-fraig-finish-copy-nonstrict (b* (((mv ?new-output-ranges ?new-aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2))) (aignet-extension-p new-aignet2 aignet2)))
Theorem:
(defthm output-range-length-of-fraig-finish-copy-nonstrict (b* (((mv ?new-output-ranges ?new-aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2))) (implies strict-count (equal (aignet-output-range-map-length new-output-ranges) (- (stype-count :po new-aignet2) (stype-count :po aignet2))))))
Theorem:
(defthm stype-count-of-fraig-finish-copy-nonstrict (b* (((mv ?new-output-ranges ?new-aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2))) (implies (and (not (equal (stype-fix stype) :po)) (not (equal (stype-fix stype) :nxst))) (equal (stype-count stype new-aignet2) (stype-count stype aignet2)))))
Theorem:
(defthm num-outs-of-fraig-finish-copy-nonstrict (b* (((mv ?new-output-ranges ?new-aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2))) (implies (not strict-count) (equal (stype-count :po new-aignet2) (+ (stype-count :po aignet2) (stype-count :po aignet))))))
Theorem:
(defthm num-outs-lower-bound-of-fraig-finish-copy-nonstrict-nonstrict (b* (((mv ?new-output-ranges ?new-aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2))) (implies strict-count (<= (nfix strict-count) (stype-count :po new-aignet2)))) :rule-classes :linear)
Theorem:
(defthm nxst-eval-of-fraig-finish-copy-nonstrict (b* (((mv ?new-output-ranges ?new-aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2))) (implies (and (aignet-copies-in-bounds copy aignet2) (equal (stype-count :reg aignet2) (stype-count :reg aignet)) (equal (stype-count :nxst aignet2) 0) (equal (lit-copy 0 copy) 0) (aignet-copy-is-comb-equivalent (+ 1 (fanin-count aignet)) aignet copy aignet2)) (equal (nxst-eval n invals regvals new-aignet2) (nxst-eval n invals regvals aignet)))))
Theorem:
(defthm output-eval-of-fraig-finish-copy-nonstrict (b* (((mv ?new-output-ranges ?new-aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2))) (implies (and (aignet-copies-in-bounds copy aignet2) (equal (stype-count :po aignet2) 0) (equal (lit-copy 0 copy) 0) (or (not strict-count) (and (< (nfix n) (nfix strict-count)))) (aignet-copy-is-comb-equivalent (+ 1 (fanin-count aignet)) aignet copy aignet2)) (equal (output-eval n invals regvals new-aignet2) (output-eval n invals regvals aignet)))))
Theorem:
(defthm comb-equiv-when-strict-of-fraig-finish-copy-nonstrict (b* (((mv ?new-output-ranges ?new-aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2))) (implies (and (not strict-count) (output-fanins-comb-equiv aignet copy aignet2) (nxst-fanins-comb-equiv aignet copy aignet2) (aignet-copies-in-bounds copy aignet2) (equal (stype-count :po aignet2) 0) (equal (stype-count :nxst aignet2) 0) (equal (stype-count :reg aignet) (stype-count :reg aignet2))) (comb-equiv new-aignet2 aignet))))
Theorem:
(defthm fraig-finish-copy-nonstrict-when-strict (b* (((mv ?new-output-ranges ?new-aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2))) (implies (not strict-count) (and (equal new-aignet2 (finish-copy-comb aignet copy aignet2)) (equal new-output-ranges (aignet-output-range-map-fix output-ranges))))))
Theorem:
(defthm fraig-finish-copy-nonstrict-of-maybe-natp-fix-strict-count (equal (fraig-finish-copy-nonstrict (acl2::maybe-natp-fix strict-count) output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2)))
Theorem:
(defthm fraig-finish-copy-nonstrict-maybe-nat-equiv-congruence-on-strict-count (implies (acl2::maybe-nat-equiv strict-count strict-count-equiv) (equal (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2) (fraig-finish-copy-nonstrict strict-count-equiv output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2))) :rule-classes :congruence)
Theorem:
(defthm fraig-finish-copy-nonstrict-of-aignet-output-range-map-fix-output-ranges (equal (fraig-finish-copy-nonstrict strict-count (aignet-output-range-map-fix output-ranges) save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2)))
Theorem:
(defthm fraig-finish-copy-nonstrict-aignet-output-range-map-equiv-congruence-on-output-ranges (implies (aignet-output-range-map-equiv output-ranges output-ranges-equiv) (equal (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges-equiv save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2))) :rule-classes :congruence)
Theorem:
(defthm fraig-finish-copy-nonstrict-of-symbol-fix-save-candidate-equivs-as (equal (fraig-finish-copy-nonstrict strict-count output-ranges (acl2::symbol-fix save-candidate-equivs-as) remove-candidate-equivs classes aignet copy aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2)))
Theorem:
(defthm fraig-finish-copy-nonstrict-symbol-equiv-congruence-on-save-candidate-equivs-as (implies (acl2::symbol-equiv save-candidate-equivs-as save-candidate-equivs-as-equiv) (equal (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as-equiv remove-candidate-equivs classes aignet copy aignet2))) :rule-classes :congruence)
Theorem:
(defthm fraig-finish-copy-nonstrict-of-symbol-fix-remove-candidate-equivs (equal (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as (acl2::symbol-fix remove-candidate-equivs) classes aignet copy aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2)))
Theorem:
(defthm fraig-finish-copy-nonstrict-symbol-equiv-congruence-on-remove-candidate-equivs (implies (acl2::symbol-equiv remove-candidate-equivs remove-candidate-equivs-equiv) (equal (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs classes aignet copy aignet2) (fraig-finish-copy-nonstrict strict-count output-ranges save-candidate-equivs-as remove-candidate-equivs-equiv classes aignet copy aignet2))) :rule-classes :congruence)