		Search-engine friendly clone of the ACL2 documentation.

Casesplit-event-generation

Casesplit-gen-appconds

Generate the applicability conditions that are present for the current call of the transformation, in the order given in the reference documentation.

Signature
(casesplit-gen-appconds old$ conditions$ hyps news verify-guards$ state) → appconds
Arguments: old$ — Guard (symbolp old$).; conditions$ — Guard (pseudo-term-listp conditions$).; hyps — Guard (pseudo-term-listp hyps).; news — Guard (pseudo-term-listp news).; verify-guards$ — Guard (booleanp verify-guards$).
Returns: appconds — An evmac-appcond-listp.

Definitions and Theorems

Function: casesplit-gen-appconds

(defun casesplit-gen-appconds (old$ conditions$
                                    hyps news verify-guards$ state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp old$)
                             (pseudo-term-listp conditions$)
                             (pseudo-term-listp hyps)
                             (pseudo-term-listp news)
                             (booleanp verify-guards$))))
 (declare
      (xargs :guard (and (= (len hyps) (1+ (len conditions$)))
                         (= (len news) (1+ (len conditions$))))))
 (let ((__function__ 'casesplit-gen-appconds))
  (declare (ignorable __function__))
  (if verify-guards$
   (append
     (casesplit-gen-appconds-thm-hyp conditions$ hyps (w state))
     (casesplit-gen-appconds-cond-guard old$ conditions$ state)
     (casesplit-gen-appconds-new-guard old$ conditions$ news state))
   (casesplit-gen-appconds-thm-hyp conditions$ hyps (w state)))))