		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-thm-asgfree-pairs-aux

Signature
(lift-thm-asgfree-pairs-aux quant index witness) → terms
Arguments: quant — Guard (symbol-listp quant).; index — Guard (natp index).; witness — A term.
Returns: terms — Type (true-listp terms).

Definitions and Theorems

Function: lift-thm-asgfree-pairs-aux

(defun lift-thm-asgfree-pairs-aux (quant index witness)
  (declare (xargs :guard (and (symbol-listp quant)
                              (natp index))))
  (let ((__function__ 'lift-thm-asgfree-pairs-aux))
    (declare (ignorable __function__))
    (cond ((endp quant) nil)
          (t (cons (cons 'mv-nth
                         (cons index (cons witness 'nil)))
                   (lift-thm-asgfree-pairs-aux (cdr quant)
                                               (1+ index)
                                               witness))))))

Theorem: true-listp-of-lift-thm-asgfree-pairs-aux

(defthm true-listp-of-lift-thm-asgfree-pairs-aux
  (b* ((terms (lift-thm-asgfree-pairs-aux quant index witness)))
    (true-listp terms))
  :rule-classes :rewrite)