(fraig-core strict-count aignet aignet2 config output-ranges state) → (mv new-aignet2 new-output-ranges new-state)
Function:
(defun fraig-core (strict-count aignet aignet2 config output-ranges state) (declare (xargs :stobjs (aignet aignet2 state))) (declare (xargs :guard (and (acl2::maybe-natp strict-count) (fraig-config-p config) (aignet-output-range-map-p output-ranges)))) (declare (xargs :guard (or (not strict-count) (<= strict-count (num-outs aignet))))) (let ((__function__ 'fraig-core)) (declare (ignorable __function__)) (b* (((local-stobjs copy strash classes s32v mark) (mv aignet2 copy strash classes s32v mark output-ranges state))) (fraig-core-aux strict-count aignet aignet2 config output-ranges copy strash classes s32v mark state))))
Theorem:
(defthm aignet-output-range-map-p-of-fraig-core.new-output-ranges (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig-core strict-count aignet aignet2 config output-ranges state))) (aignet-output-range-map-p new-output-ranges)) :rule-classes :rewrite)
Theorem:
(defthm num-ins-of-fraig-core (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig-core strict-count aignet aignet2 config output-ranges state))) (equal (stype-count :pi new-aignet2) (stype-count :pi aignet))))
Theorem:
(defthm num-regs-of-fraig-core (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig-core strict-count aignet aignet2 config output-ranges state))) (equal (stype-count :reg new-aignet2) (stype-count :reg aignet))))
Theorem:
(defthm output-range-map-length-of-fraig-core (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig-core strict-count aignet aignet2 config output-ranges state))) (equal (aignet-output-range-map-length new-output-ranges) (stype-count :po new-aignet2))))
Theorem:
(defthm num-outs-of-fraig-core (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig-core strict-count aignet aignet2 config output-ranges state))) (implies (not strict-count) (equal (stype-count :po new-aignet2) (stype-count :po aignet)))))
Theorem:
(defthm num-outs-lower-bound-of-fraig-core-nonstrict (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig-core strict-count aignet aignet2 config output-ranges state))) (implies strict-count (<= (nfix strict-count) (stype-count :po new-aignet2)))) :rule-classes :linear)
Theorem:
(defthm fraig-core-comb-equivalent (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig-core strict-count aignet aignet2 config output-ranges state))) (implies (not strict-count) (comb-equiv new-aignet2 aignet))))
Theorem:
(defthm output-eval-of-fraig-core-when-nonstrict (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig-core strict-count aignet aignet2 config output-ranges state))) (implies (and strict-count (< (nfix i) (nfix strict-count))) (equal (output-eval i invals regvals new-aignet2) (output-eval i invals regvals aignet)))))
Theorem:
(defthm normalize-input-of-fraig-core (implies (syntaxp (not (equal aignet2 ''nil))) (equal (fraig-core strict-count aignet aignet2 config output-ranges state) (fraig-core strict-count aignet nil config output-ranges state))))
Theorem:
(defthm w-state-of-fraig-core (b* (((mv ?new-aignet2 ?new-output-ranges ?new-state) (fraig-core strict-count aignet aignet2 config output-ranges state))) (equal (w new-state) (w state))))
Theorem:
(defthm fraig-core-of-maybe-natp-fix-strict-count (equal (fraig-core (acl2::maybe-natp-fix strict-count) aignet aignet2 config output-ranges state) (fraig-core strict-count aignet aignet2 config output-ranges state)))
Theorem:
(defthm fraig-core-maybe-nat-equiv-congruence-on-strict-count (implies (acl2::maybe-nat-equiv strict-count strict-count-equiv) (equal (fraig-core strict-count aignet aignet2 config output-ranges state) (fraig-core strict-count-equiv aignet aignet2 config output-ranges state))) :rule-classes :congruence)
Theorem:
(defthm fraig-core-of-fraig-config-fix-config (equal (fraig-core strict-count aignet aignet2 (fraig-config-fix config) output-ranges state) (fraig-core strict-count aignet aignet2 config output-ranges state)))
Theorem:
(defthm fraig-core-fraig-config-equiv-congruence-on-config (implies (fraig-config-equiv config config-equiv) (equal (fraig-core strict-count aignet aignet2 config output-ranges state) (fraig-core strict-count aignet aignet2 config-equiv output-ranges state))) :rule-classes :congruence)
Theorem:
(defthm fraig-core-of-aignet-output-range-map-fix-output-ranges (equal (fraig-core strict-count aignet aignet2 config (aignet-output-range-map-fix output-ranges) state) (fraig-core strict-count aignet aignet2 config output-ranges state)))
Theorem:
(defthm fraig-core-aignet-output-range-map-equiv-congruence-on-output-ranges (implies (aignet-output-range-map-equiv output-ranges output-ranges-equiv) (equal (fraig-core strict-count aignet aignet2 config output-ranges state) (fraig-core strict-count aignet aignet2 config output-ranges-equiv state))) :rule-classes :congruence)