		Search-engine friendly clone of the ACL2 documentation.

Casesplit-event-generation

Casesplit-gen-appcond-cond-guard

Generate the applicability condition condk-guard.

Signature
(casesplit-gen-appcond-cond-guard k old$ conditions$ state) → appcond
Arguments: k — Guard (posp k).; old$ — Guard (symbolp old$).; conditions$ — Guard (pseudo-term-listp conditions$).
Returns: appcond — An evmac-appcondp.

Definitions and Theorems

Function: casesplit-gen-appcond-cond-guard

(defun casesplit-gen-appcond-cond-guard (k old$ conditions$ state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (posp k)
                              (symbolp old$)
                              (pseudo-term-listp conditions$))))
  (declare (xargs :guard (<= k (len conditions$))))
  (let ((__function__ 'casesplit-gen-appcond-cond-guard))
    (declare (ignorable __function__))
    (b* ((wrld (w state))
         (name (casesplit-gen-appcond-cond-guard-name k))
         (old-guard (uguard old$ wrld))
         (antecedent-conjuncts
              (cons old-guard
                    (negate-terms (take (1- k) conditions$))))
         (antecedent (conjoin antecedent-conjuncts))
         (consequent (term-guard-obligation (nth (1- k) conditions$)
                                            :limited state))
         (formula (implicate antecedent consequent)))
      (make-evmac-appcond :name name
                          :formula formula))))