Generate the applicability condition
(casesplit-gen-appcond-new-guard k old$ conditions$ news state) → appcond
Recall that
Function:
(defun casesplit-gen-appcond-new-guard (k old$ conditions$ news state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (natp k) (symbolp old$) (pseudo-term-listp conditions$) (pseudo-term-listp news)))) (declare (xargs :guard (and (= (len news) (1+ (len conditions$))) (<= k (len conditions$))))) (let ((__function__ 'casesplit-gen-appcond-new-guard)) (declare (ignorable __function__)) (b* ((wrld (w state)) (name (casesplit-gen-appcond-new-guard-name k)) (old-guard (uguard old$ wrld)) (antecedent-conjuncts (if (= k 0) (cons old-guard (negate-terms conditions$)) (append (list old-guard) (negate-terms (take (1- k) conditions$)) (list (nth (1- k) conditions$))))) (antecedent (conjoin antecedent-conjuncts)) (new (if (= k 0) (car (last news)) (nth (1- k) news))) (consequent (term-guard-obligation new :limited state)) (formula (implicate antecedent consequent))) (make-evmac-appcond :name name :formula formula))))