Lift deftreeops-gen-conc-info to lists of concatenations, i.e. to alternations.
(deftreeops-gen-conc-info-list alt discriminant-terms-or-nils check-conc-fn alt-singletonp rulename-upstring prefix) → infos
Function:
(defun deftreeops-gen-conc-info-list-aux (alt i discriminant-terms-or-nils check-conc-fn alt-singletonp rulename-upstring prefix) (declare (xargs :guard (and (alternationp alt) (posp i) (common-lisp::symbolp check-conc-fn) (booleanp alt-singletonp) (common-lisp::stringp rulename-upstring) (common-lisp::symbolp prefix)))) (declare (xargs :guard (equal (len discriminant-terms-or-nils) (len alt)))) (let ((__function__ 'deftreeops-gen-conc-info-list-aux)) (declare (ignorable __function__)) (b* (((when (endp alt)) nil) (info (deftreeops-gen-conc-info (car alt) i (car discriminant-terms-or-nils) check-conc-fn alt-singletonp rulename-upstring prefix)) (more-info (deftreeops-gen-conc-info-list-aux (cdr alt) (1+ i) (cdr discriminant-terms-or-nils) check-conc-fn alt-singletonp rulename-upstring prefix))) (cons info more-info))))
Theorem:
(defthm deftreeops-conc-info-listp-of-deftreeops-gen-conc-info-list-aux (b* ((infos (deftreeops-gen-conc-info-list-aux alt i discriminant-terms-or-nils check-conc-fn alt-singletonp rulename-upstring prefix))) (deftreeops-conc-info-listp infos)) :rule-classes :rewrite)
Function:
(defun deftreeops-gen-conc-info-list (alt discriminant-terms-or-nils check-conc-fn alt-singletonp rulename-upstring prefix) (declare (xargs :guard (and (alternationp alt) (common-lisp::symbolp check-conc-fn) (booleanp alt-singletonp) (common-lisp::stringp rulename-upstring) (common-lisp::symbolp prefix)))) (declare (xargs :guard (equal (len discriminant-terms-or-nils) (len alt)))) (let ((__function__ 'deftreeops-gen-conc-info-list)) (declare (ignorable __function__)) (deftreeops-gen-conc-info-list-aux alt 1 discriminant-terms-or-nils check-conc-fn alt-singletonp rulename-upstring prefix)))
Theorem:
(defthm deftreeops-conc-info-listp-of-deftreeops-gen-conc-info-list (b* ((infos (deftreeops-gen-conc-info-list alt discriminant-terms-or-nils check-conc-fn alt-singletonp rulename-upstring prefix))) (deftreeops-conc-info-listp infos)) :rule-classes :rewrite)