Function:
(defun fraig-level-limit-ok (node aignet-levels level-limit) (declare (xargs :stobjs (aignet-levels))) (declare (xargs :guard (and (natp node) (natp level-limit)))) (declare (xargs :guard (< node (u32-length aignet-levels)))) (let ((__function__ 'fraig-level-limit-ok)) (declare (ignorable __function__)) (if (zp level-limit) t (<= (get-u32 node aignet-levels) level-limit))))
Theorem:
(defthm fraig-level-limit-ok-of-nfix-node (equal (fraig-level-limit-ok (nfix node) aignet-levels level-limit) (fraig-level-limit-ok node aignet-levels level-limit)))
Theorem:
(defthm fraig-level-limit-ok-nat-equiv-congruence-on-node (implies (nat-equiv node node-equiv) (equal (fraig-level-limit-ok node aignet-levels level-limit) (fraig-level-limit-ok node-equiv aignet-levels level-limit))) :rule-classes :congruence)
Theorem:
(defthm fraig-level-limit-ok-of-nfix-level-limit (equal (fraig-level-limit-ok node aignet-levels (nfix level-limit)) (fraig-level-limit-ok node aignet-levels level-limit)))
Theorem:
(defthm fraig-level-limit-ok-nat-equiv-congruence-on-level-limit (implies (nat-equiv level-limit level-limit-equiv) (equal (fraig-level-limit-ok node aignet-levels level-limit) (fraig-level-limit-ok node aignet-levels level-limit-equiv))) :rule-classes :congruence)