		Search-engine friendly clone of the ACL2 documentation.

Isodata-input-processing

Isodata-process-isomaps-ress

Signature
(isodata-process-isomaps-ress j m res-isomaps isomap-id) → new-res-isomaps
Arguments: j — Guard (posp j).; m — Guard (posp m).; res-isomaps — Guard (isodata-pos-isomap-alistp res-isomaps).; isomap-id — Guard (isodata-isomapp isomap-id).
Returns: new-res-isomaps — Type (isodata-pos-isomap-alistp new-res-isomaps), given the guard.

Definitions and Theorems

Function: isodata-process-isomaps-ress

(defun isodata-process-isomaps-ress (j m res-isomaps isomap-id)
 (declare (xargs :guard (and (posp j)
                             (posp m)
                             (isodata-pos-isomap-alistp res-isomaps)
                             (isodata-isomapp isomap-id))))
 (let ((__function__ 'isodata-process-isomaps-ress))
  (declare (ignorable __function__))
  (b* (((unless (mbt (and (posp j) (posp m))))
        nil)
       ((when (> j m)) nil)
       (pair (assoc j res-isomaps)))
   (if (consp pair)
       (cons pair
             (isodata-process-isomaps-ress (1+ j)
                                           m res-isomaps isomap-id))
    (acons
         j isomap-id
         (isodata-process-isomaps-ress (1+ j)
                                       m res-isomaps isomap-id))))))

Theorem: isodata-pos-isomap-alistp-of-isodata-process-isomaps-ress

(defthm isodata-pos-isomap-alistp-of-isodata-process-isomaps-ress
 (implies
   (and (posp j)
        (posp m)
        (isodata-pos-isomap-alistp res-isomaps)
        (isodata-isomapp isomap-id))
   (b*
    ((new-res-isomaps
          (isodata-process-isomaps-ress j m res-isomaps isomap-id)))
    (isodata-pos-isomap-alistp new-res-isomaps)))
 :rule-classes :rewrite)