		Search-engine friendly clone of the ACL2 documentation.

Expdata-event-generation

Expdata-gen-forth-image-instances-to-mv-nth

Generate m lemma instances such that the j-th instance is of theorem forth_rj-image and instantiates the formal parameter of forth_rj with (mv-nth j-1 ...) applied to a given term term.

Signature
(expdata-gen-forth-image-instances-to-mv-nth term res-surjmaps wrld) → lemma-instances
Arguments: term — Guard (pseudo-termp term).; res-surjmaps — Guard (expdata-pos-surjmap-alistp res-surjmaps).; wrld — Guard (plist-worldp wrld).
Returns: lemma-instances — Type (true-list-listp lemma-instances).

Definitions and Theorems

Function: expdata-gen-forth-image-instances-to-mv-nth

(defun expdata-gen-forth-image-instances-to-mv-nth
       (term res-surjmaps wrld)
 (declare
      (xargs :guard (and (pseudo-termp term)
                         (expdata-pos-surjmap-alistp res-surjmaps)
                         (plist-worldp wrld))))
 (let ((__function__ 'expdata-gen-forth-image-instances-to-mv-nth))
  (declare (ignorable __function__))
  (b*
   (((when (endp res-surjmaps)) nil)
    (j (caar res-surjmaps))
    (surjmap (cdar res-surjmaps))
    (forth-image (expdata-surjmap->forth-image surjmap))
    (var (expdata-formal-of-forth surjmap wrld))
    (mv-nth-of-term (fcons-term* 'mv-nth (1- j) term))
    (instance
       (cons ':instance
             (cons forth-image
                   (cons ':extra-bindings-ok
                         (cons (cons var (cons mv-nth-of-term 'nil))
                               'nil)))))
    (instances (expdata-gen-forth-image-instances-to-mv-nth
                    term (cdr res-surjmaps)
                    wrld)))
   (cons instance instances))))

Theorem: true-list-listp-of-expdata-gen-forth-image-instances-to-mv-nth

(defthm
     true-list-listp-of-expdata-gen-forth-image-instances-to-mv-nth
  (b* ((lemma-instances (expdata-gen-forth-image-instances-to-mv-nth
                             term res-surjmaps wrld)))
    (true-list-listp lemma-instances))
  :rule-classes :rewrite)