(casesplit-gen-appconds-new-guard-aux k old$ conditions$ news state acc) → appconds
Function:
(defun casesplit-gen-appconds-new-guard-aux (k old$ conditions$ news state acc) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (natp k) (symbolp old$) (pseudo-term-listp conditions$) (pseudo-term-listp news) (symbol-alistp acc)))) (declare (xargs :guard (and (= (len news) (1+ (len conditions$))) (<= k (len conditions$))))) (let ((__function__ 'casesplit-gen-appconds-new-guard-aux)) (declare (ignorable __function__)) (b* (((when (zp k)) acc) (appcond (casesplit-gen-appcond-new-guard k old$ conditions$ news state)) (acc (cons appcond acc))) (casesplit-gen-appconds-new-guard-aux (1- k) old$ conditions$ news state acc))))