		Search-engine friendly clone of the ACL2 documentation.

Deffixequiv-sk-implementation

Deffixequiv-sk-lemma-inst-subst

Generate instantiations for the bound variables.

Signature
(deffixequiv-sk-lemma-inst-subst bvars index call) → instantiations
Arguments: bvars — Guard (symbol-listp bvars).; index — Guard (natp index).; call — Guard (pseudo-termp call).
Returns: instantiations — Type (true-list-listp instantiations).

If bvars consists of the variables b1, ... , bn, we generate the list of doublets ((b1 (mv-nth index call)) ... (bn (mv-nth index+n-1 call))), which is then used to create some lemma instances. The index is initially 0.

Definitions and Theorems

Function: deffixequiv-sk-lemma-inst-subst

(defun deffixequiv-sk-lemma-inst-subst (bvars index call)
  (declare (xargs :guard (and (symbol-listp bvars)
                              (natp index)
                              (pseudo-termp call))))
  (let ((__function__ 'deffixequiv-sk-lemma-inst-subst))
    (declare (ignorable __function__))
    (cond ((endp bvars) nil)
          (t (cons (cons (car bvars)
                         (cons (cons 'mv-nth
                                     (cons index (cons call 'nil)))
                               'nil))
                   (deffixequiv-sk-lemma-inst-subst (cdr bvars)
                                                    (1+ index)
                                                    call))))))

Theorem: true-list-listp-of-deffixequiv-sk-lemma-inst-subst

(defthm true-list-listp-of-deffixequiv-sk-lemma-inst-subst
  (b* ((instantiations
            (deffixequiv-sk-lemma-inst-subst bvars index call)))
    (true-list-listp instantiations))
  :rule-classes :rewrite)