		Search-engine friendly clone of the ACL2 documentation.

Casesplit-event-generation

Casesplit-gen-appconds-new-guard

Generate the applicability conditions new1-guard, ..., newp-guard, new0-guard, in that order.

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

Definitions and Theorems

Function: casesplit-gen-appconds-new-guard-aux

(defun casesplit-gen-appconds-new-guard-aux
       (k old$ conditions$ news state acc)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (natp k)
                              (symbolp old$)
                              (pseudo-term-listp conditions$)
                              (pseudo-term-listp news)
                              (symbol-alistp acc))))
  (declare (xargs :guard (and (= (len news) (1+ (len conditions$)))
                              (<= k (len conditions$)))))
  (let ((__function__ 'casesplit-gen-appconds-new-guard-aux))
    (declare (ignorable __function__))
    (b* (((when (zp k)) acc)
         (appcond (casesplit-gen-appcond-new-guard
                       k old$ conditions$ news state))
         (acc (cons appcond acc)))
      (casesplit-gen-appconds-new-guard-aux
           (1- k)
           old$ conditions$ news state acc))))

Function: casesplit-gen-appconds-new-guard

(defun casesplit-gen-appconds-new-guard
       (old$ conditions$ news state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (symbolp old$)
                              (pseudo-term-listp conditions$)
                              (pseudo-term-listp news))))
  (declare (xargs :guard (equal (len news)
                                (1+ (len conditions$)))))
  (let ((__function__ 'casesplit-gen-appconds-new-guard))
    (declare (ignorable __function__))
    (append (casesplit-gen-appconds-new-guard-aux
                 (len conditions$)
                 old$ conditions$ news state nil)
            (list (casesplit-gen-appcond-new-guard
                       0 old$ conditions$ news state)))))