		Search-engine friendly clone of the ACL2 documentation.

Lifting

Lift-thm-asgfree-pairs

Calculate a list of pairs for constructing a witness assignment to quantified variables.

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

These are used in the hints for the `if' direction of the lifting theorem, when there are free PFCS variables, which become quantified variables in ACL2.

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)

Function: lift-thm-asgfree-pairs

(defun lift-thm-asgfree-pairs (quant witness)
  (declare (xargs :guard (symbol-listp quant)))
  (let ((__function__ 'lift-thm-asgfree-pairs))
    (declare (ignorable __function__))
    (cond ((endp quant) (raise "Error."))
          ((endp (cdr quant)) (list witness))
          (t (lift-thm-asgfree-pairs-aux quant 0 witness)))))

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

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