(aig-right-shift-ss place n shamt) → *
Function:
(defun aig-right-shift-ss (place n shamt) (declare (xargs :guard (and (posp place) (true-listp n) (true-listp shamt)))) (let ((__function__ 'aig-right-shift-ss)) (declare (ignorable __function__)) (b* (((mv shdig shrst shend) (gl::first/rest/end shamt)) (place (lposfix place)) ((when shend) (aig-logtail-ns 1 n)) (rst (aig-right-shift-ss (* 2 place) n shrst))) (aig-ite-bss shdig rst (aig-logtail-ns place rst)))))
Theorem:
(defthm aig-right-shift-ss-correct (implies (< (aig-list->s shamt env) 0) (equal (aig-list->s (aig-right-shift-ss place n shamt) env) (ash (aig-list->s n env) (+ -1 (pos-fix place) (* (pos-fix place) (aig-list->s shamt env)))))))
Theorem:
(defthm aig-right-shift-ss-of-pos-fix-place (equal (aig-right-shift-ss (pos-fix place) n shamt) (aig-right-shift-ss place n shamt)))
Theorem:
(defthm aig-right-shift-ss-pos-equiv-congruence-on-place (implies (pos-equiv place place-equiv) (equal (aig-right-shift-ss place n shamt) (aig-right-shift-ss place-equiv n shamt))) :rule-classes :congruence)
Theorem:
(defthm aig-right-shift-ss-of-list-fix-n (equal (aig-right-shift-ss place (list-fix n) shamt) (aig-right-shift-ss place n shamt)))
Theorem:
(defthm aig-right-shift-ss-list-equiv-congruence-on-n (implies (list-equiv n n-equiv) (equal (aig-right-shift-ss place n shamt) (aig-right-shift-ss place n-equiv shamt))) :rule-classes :congruence)
Theorem:
(defthm aig-right-shift-ss-of-list-fix-shamt (equal (aig-right-shift-ss place n (list-fix shamt)) (aig-right-shift-ss place n shamt)))
Theorem:
(defthm aig-right-shift-ss-list-equiv-congruence-on-shamt (implies (list-equiv shamt shamt-equiv) (equal (aig-right-shift-ss place n shamt) (aig-right-shift-ss place n shamt-equiv))) :rule-classes :congruence)