		Search-engine friendly clone of the ACL2 documentation.

Input-execution

Eval-input-section-list

Evaluate a list of input sections.

Signature
(eval-input-section-list insecs curve) → funargs
Arguments: insecs — Guard (input-section-listp insecs).; curve — Guard (curvep curve).
Returns: funargs — Type (funarg-list-resultp funargs).

We evaluate them one after the other, concatenating the resulting function arguments.

Definitions and Theorems

Function: eval-input-section-list

(defun eval-input-section-list (insecs curve)
  (declare (xargs :guard (and (input-section-listp insecs)
                              (curvep curve))))
  (let ((__function__ 'eval-input-section-list))
    (declare (ignorable __function__))
    (b* (((when (endp insecs)) nil)
         ((okf funargs)
          (eval-input-section (car insecs) curve))
         ((okf more-funargs)
          (eval-input-section-list (cdr insecs)
                                   curve)))
      (append funargs more-funargs))))

Theorem: funarg-list-resultp-of-eval-input-section-list

(defthm funarg-list-resultp-of-eval-input-section-list
  (b* ((funargs (eval-input-section-list insecs curve)))
    (funarg-list-resultp funargs))
  :rule-classes :rewrite)

Theorem: eval-input-section-list-of-input-section-list-fix-insecs

(defthm eval-input-section-list-of-input-section-list-fix-insecs
  (equal (eval-input-section-list (input-section-list-fix insecs)
                                  curve)
         (eval-input-section-list insecs curve)))

Theorem: eval-input-section-list-input-section-list-equiv-congruence-on-insecs

(defthm
 eval-input-section-list-input-section-list-equiv-congruence-on-insecs
 (implies (input-section-list-equiv insecs insecs-equiv)
          (equal (eval-input-section-list insecs curve)
                 (eval-input-section-list insecs-equiv curve)))
 :rule-classes :congruence)

Theorem: eval-input-section-list-of-curve-fix-curve

(defthm eval-input-section-list-of-curve-fix-curve
  (equal (eval-input-section-list insecs (curve-fix curve))
         (eval-input-section-list insecs curve)))

Theorem: eval-input-section-list-curve-equiv-congruence-on-curve

(defthm eval-input-section-list-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (eval-input-section-list insecs curve)
                  (eval-input-section-list insecs curve-equiv)))
  :rule-classes :congruence)