(fraig-core aignet aignet2 config state) → (mv new-aignet2 new-state)
Function:
(defun fraig-core (aignet aignet2 config state) (declare (xargs :stobjs (aignet aignet2 state))) (declare (xargs :guard (fraig-config-p config))) (let ((__function__ 'fraig-core)) (declare (ignorable __function__)) (b* (((local-stobjs copy strash classes s32v) (mv aignet2 copy strash classes s32v state))) (fraig-core-aux aignet aignet2 config copy strash classes s32v state))))
Theorem:
(defthm num-ins-of-fraig-core (b* (((mv ?new-aignet2 ?new-state) (fraig-core aignet aignet2 config state))) (equal (stype-count :pi new-aignet2) (stype-count :pi aignet))))
Theorem:
(defthm num-regs-of-fraig-core (b* (((mv ?new-aignet2 ?new-state) (fraig-core aignet aignet2 config state))) (equal (stype-count :reg new-aignet2) (stype-count :reg aignet))))
Theorem:
(defthm num-outs-of-fraig-core (b* (((mv ?new-aignet2 ?new-state) (fraig-core aignet aignet2 config state))) (equal (stype-count :po new-aignet2) (stype-count :po aignet))))
Theorem:
(defthm fraig-core-comb-equivalent (b* (((mv ?new-aignet2 ?new-state) (fraig-core aignet aignet2 config state))) (comb-equiv new-aignet2 aignet)))
Theorem:
(defthm normalize-input-of-fraig-core (implies (syntaxp (not (equal aignet2 ''nil))) (equal (fraig-core aignet aignet2 config state) (fraig-core aignet nil config state))))
Theorem:
(defthm w-state-of-fraig-core (b* (((mv ?new-aignet2 ?new-state) (fraig-core aignet aignet2 config state))) (equal (w new-state) (w state))))
Theorem:
(defthm fraig-core-of-fraig-config-fix-config (equal (fraig-core aignet aignet2 (fraig-config-fix config) state) (fraig-core aignet aignet2 config state)))
Theorem:
(defthm fraig-core-fraig-config-equiv-congruence-on-config (implies (fraig-config-equiv config config-equiv) (equal (fraig-core aignet aignet2 config state) (fraig-core aignet aignet2 config-equiv state))) :rule-classes :congruence)