		Search-engine friendly clone of the ACL2 documentation.

Stv-debug

Stv-combine-into-snapshots

Signature
(stv-combine-into-snapshots in-alists out-alists int-alists) → snapshots
Arguments: in-alists — Guard (true-list-listp in-alists).; out-alists — Guard (true-list-listp out-alists).; int-alists — Guard (true-list-listp int-alists).
Returns: snapshots — Type (cons-list-listp snapshots), given (and (cons-list-listp in-alists) (cons-list-listp out-alists) (cons-list-listp int-alists)) .

Definitions and Theorems

Function: stv-combine-into-snapshots

(defun
  stv-combine-into-snapshots
  (in-alists out-alists int-alists)
  (declare (xargs :guard (and (true-list-listp in-alists)
                              (true-list-listp out-alists)
                              (true-list-listp int-alists))))
  (declare (xargs :guard (and (same-lengthp in-alists out-alists)
                              (same-lengthp in-alists int-alists))))
  (let ((__function__ 'stv-combine-into-snapshots))
       (declare (ignorable __function__))
       (b* (((when (atom in-alists)) nil)
            (snapshot1 (append (car in-alists)
                               (car out-alists)
                               (car int-alists))))
           (cons snapshot1
                 (stv-combine-into-snapshots (cdr in-alists)
                                             (cdr out-alists)
                                             (cdr int-alists))))))

Theorem: cons-list-listp-of-stv-combine-into-snapshots

(defthm
 cons-list-listp-of-stv-combine-into-snapshots
 (implies
  (and (cons-list-listp in-alists)
       (cons-list-listp out-alists)
       (cons-list-listp int-alists))
  (b*
   ((snapshots
      (stv-combine-into-snapshots in-alists out-alists int-alists)))
   (cons-list-listp snapshots)))
 :rule-classes :rewrite)