Generate the applicability condition
(casesplit-gen-appcond-thm-hyp k conditions$ hyps) → appcond
Recall that
Function:
(defun casesplit-gen-appcond-thm-hyp (k conditions$ hyps) (declare (xargs :guard (and (natp k) (pseudo-term-listp conditions$) (pseudo-term-listp hyps)))) (declare (xargs :guard (and (= (len hyps) (1+ (len conditions$))) (<= k (len conditions$))))) (let ((__function__ 'casesplit-gen-appcond-thm-hyp)) (declare (ignorable __function__)) (b* ((name (casesplit-gen-appcond-thm-hyp-name k)) (antecedent-conjuncts (if (= k 0) (negate-terms conditions$) (append (negate-terms (take (1- k) conditions$)) (list (nth (1- k) conditions$))))) (antecedent (conjoin antecedent-conjuncts)) (consequent (if (= k 0) (car (last hyps)) (nth (1- k) hyps))) (formula (implicate antecedent consequent))) (make-evmac-appcond :name name :formula formula))))