		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Svtv-allphases-inputs

Signature
(svtv-allphases-inputs phase nphases ins overrides in-vars) → ins
Arguments: phase — Guard (natp phase).; nphases — Guard (posp nphases).; ins — Guard (svtv-lines-p ins).; overrides — Guard (svtv-overridelines-p overrides).; in-vars — Guard (svarlist-p in-vars).
Returns: ins — Type (svex-alistlist-p ins).

Definitions and Theorems

Function: svtv-allphases-inputs

(defun svtv-allphases-inputs (phase nphases ins overrides in-vars)
 (declare (xargs :guard (and (natp phase)
                             (posp nphases)
                             (svtv-lines-p ins)
                             (svtv-overridelines-p overrides)
                             (svarlist-p in-vars))))
 (declare (xargs :guard (<= phase nphases)))
 (let ((__function__ 'svtv-allphases-inputs))
   (declare (ignorable __function__))
   (b*
     (((when (mbe :logic (zp (- (pos-fix nphases) (nfix phase)))
                  :exec (eql nphases phase)))
       nil)
      (input-alist (svtv-phase-inputs phase ins overrides in-vars)))
     (cons (make-fast-alist input-alist)
           (svtv-allphases-inputs (1+ (lnfix phase))
                                  nphases ins overrides in-vars)))))

Theorem: svex-alistlist-p-of-svtv-allphases-inputs

(defthm svex-alistlist-p-of-svtv-allphases-inputs
 (b*
  ((ins
       (svtv-allphases-inputs phase nphases ins overrides in-vars)))
  (svex-alistlist-p ins))
 :rule-classes :rewrite)

Theorem: svtv-allphases-inputs-of-nfix-phase

(defthm svtv-allphases-inputs-of-nfix-phase
  (equal
       (svtv-allphases-inputs (nfix phase)
                              nphases ins overrides in-vars)
       (svtv-allphases-inputs phase nphases ins overrides in-vars)))

Theorem: svtv-allphases-inputs-nat-equiv-congruence-on-phase

(defthm svtv-allphases-inputs-nat-equiv-congruence-on-phase
 (implies
  (nat-equiv phase phase-equiv)
  (equal (svtv-allphases-inputs phase nphases ins overrides in-vars)
         (svtv-allphases-inputs phase-equiv
                                nphases ins overrides in-vars)))
 :rule-classes :congruence)

Theorem: svtv-allphases-inputs-of-pos-fix-nphases

(defthm svtv-allphases-inputs-of-pos-fix-nphases
  (equal
       (svtv-allphases-inputs phase (pos-fix nphases)
                              ins overrides in-vars)
       (svtv-allphases-inputs phase nphases ins overrides in-vars)))

Theorem: svtv-allphases-inputs-pos-equiv-congruence-on-nphases

(defthm svtv-allphases-inputs-pos-equiv-congruence-on-nphases
 (implies
  (pos-equiv nphases nphases-equiv)
  (equal
       (svtv-allphases-inputs phase nphases ins overrides in-vars)
       (svtv-allphases-inputs phase
                              nphases-equiv ins overrides in-vars)))
 :rule-classes :congruence)

Theorem: svtv-allphases-inputs-of-svtv-lines-fix-ins

(defthm svtv-allphases-inputs-of-svtv-lines-fix-ins
  (equal
       (svtv-allphases-inputs phase nphases (svtv-lines-fix ins)
                              overrides in-vars)
       (svtv-allphases-inputs phase nphases ins overrides in-vars)))

Theorem: svtv-allphases-inputs-svtv-lines-equiv-congruence-on-ins

(defthm svtv-allphases-inputs-svtv-lines-equiv-congruence-on-ins
 (implies
  (svtv-lines-equiv ins ins-equiv)
  (equal
       (svtv-allphases-inputs phase nphases ins overrides in-vars)
       (svtv-allphases-inputs phase
                              nphases ins-equiv overrides in-vars)))
 :rule-classes :congruence)

Theorem: svtv-allphases-inputs-of-svtv-overridelines-fix-overrides

(defthm svtv-allphases-inputs-of-svtv-overridelines-fix-overrides
  (equal
       (svtv-allphases-inputs phase nphases
                              ins (svtv-overridelines-fix overrides)
                              in-vars)
       (svtv-allphases-inputs phase nphases ins overrides in-vars)))

Theorem: svtv-allphases-inputs-svtv-overridelines-equiv-congruence-on-overrides

(defthm
 svtv-allphases-inputs-svtv-overridelines-equiv-congruence-on-overrides
 (implies
  (svtv-overridelines-equiv overrides overrides-equiv)
  (equal
       (svtv-allphases-inputs phase nphases ins overrides in-vars)
       (svtv-allphases-inputs phase
                              nphases ins overrides-equiv in-vars)))
 :rule-classes :congruence)

Theorem: svtv-allphases-inputs-of-svarlist-fix-in-vars

(defthm svtv-allphases-inputs-of-svarlist-fix-in-vars
  (equal
       (svtv-allphases-inputs phase nphases
                              ins overrides (svarlist-fix in-vars))
       (svtv-allphases-inputs phase nphases ins overrides in-vars)))

Theorem: svtv-allphases-inputs-svarlist-equiv-congruence-on-in-vars

(defthm svtv-allphases-inputs-svarlist-equiv-congruence-on-in-vars
 (implies
  (svarlist-equiv in-vars in-vars-equiv)
  (equal
       (svtv-allphases-inputs phase nphases ins overrides in-vars)
       (svtv-allphases-inputs phase
                              nphases ins overrides in-vars-equiv)))
 :rule-classes :congruence)