		Search-engine friendly clone of the ACL2 documentation.

Casesplit-event-generation

Casesplit-gen-appconds-thm-hyp

Generate the applicability conditions thm1-hyp, ..., thmp-hyp, thm0-hyp, in that order.

Signature
(casesplit-gen-appconds-thm-hyp conditions$ hyps wrld) → appconds
Arguments: conditions$ — Guard (pseudo-term-listp conditions$).; hyps — Guard (pseudo-term-listp hyps).; wrld — Guard (plist-worldp wrld).
Returns: appconds — An evmac-appcond-listp.

Definitions and Theorems

Function: casesplit-gen-appconds-thm-hyp-aux

(defun casesplit-gen-appconds-thm-hyp-aux
       (k conditions$ hyps wrld acc)
 (declare (xargs :guard (and (natp k)
                             (pseudo-term-listp conditions$)
                             (pseudo-term-listp hyps)
                             (plist-worldp wrld)
                             (symbol-alistp acc))))
 (declare (xargs :guard (and (= (len hyps) (1+ (len conditions$)))
                             (<= k (len conditions$)))))
 (let ((__function__ 'casesplit-gen-appconds-thm-hyp-aux))
  (declare (ignorable __function__))
  (b* (((when (zp k)) acc)
       (appcond (casesplit-gen-appcond-thm-hyp k conditions$ hyps))
       (acc (cons appcond acc)))
   (casesplit-gen-appconds-thm-hyp-aux (1- k)
                                       conditions$ hyps wrld acc))))

Function: casesplit-gen-appconds-thm-hyp

(defun casesplit-gen-appconds-thm-hyp (conditions$ hyps wrld)
 (declare (xargs :guard (and (pseudo-term-listp conditions$)
                             (pseudo-term-listp hyps)
                             (plist-worldp wrld))))
 (declare (xargs :guard (= (len hyps) (1+ (len conditions$)))))
 (let ((__function__ 'casesplit-gen-appconds-thm-hyp))
  (declare (ignorable __function__))
  (append
      (casesplit-gen-appconds-thm-hyp-aux (len conditions$)
                                          conditions$ hyps wrld nil)
      (list (casesplit-gen-appcond-thm-hyp 0 conditions$ hyps)))))