		Search-engine friendly clone of the ACL2 documentation.

Output-execution

Eval-output-section

Evaluate an output section.

Signature
(eval-output-section outsec curve) → val
Arguments: outsec — Guard (output-sectionp outsec).; curve — Guard (curvep curve).
Returns: val — Type (value-resultp val).

Definitions and Theorems

Function: eval-output-section

(defun eval-output-section (outsec curve)
  (declare (xargs :guard (and (output-sectionp outsec)
                              (curvep curve))))
  (let ((__function__ 'eval-output-section))
    (declare (ignorable __function__))
    (eval-output-item (output-section->item outsec)
                      curve)))

Theorem: value-resultp-of-eval-output-section

(defthm value-resultp-of-eval-output-section
  (b* ((val (eval-output-section outsec curve)))
    (value-resultp val))
  :rule-classes :rewrite)

Theorem: eval-output-section-of-output-section-fix-outsec

(defthm eval-output-section-of-output-section-fix-outsec
  (equal (eval-output-section (output-section-fix outsec)
                              curve)
         (eval-output-section outsec curve)))

Theorem: eval-output-section-output-section-equiv-congruence-on-outsec

(defthm
      eval-output-section-output-section-equiv-congruence-on-outsec
  (implies (output-section-equiv outsec outsec-equiv)
           (equal (eval-output-section outsec curve)
                  (eval-output-section outsec-equiv curve)))
  :rule-classes :congruence)

Theorem: eval-output-section-of-curve-fix-curve

(defthm eval-output-section-of-curve-fix-curve
  (equal (eval-output-section outsec (curve-fix curve))
         (eval-output-section outsec curve)))

Theorem: eval-output-section-curve-equiv-congruence-on-curve

(defthm eval-output-section-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (eval-output-section outsec curve)
                  (eval-output-section outsec curve-equiv)))
  :rule-classes :congruence)