		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables-execution

Reserr-limitp-theorems

Theorems about reserr-limitp.

These are mainly about certain dynamic semantic operations never returning limit errors. There is also one theorem to simplify reserr-limitp when applied to reserr. There is also a theorem to show that an error is not a limit error, based on looking at the keyword (assuming it is constant).

Definitions and Theorems

Theorem: reserr-limitp-of-reserr-of-info

(defthm reserr-limitp-of-reserr-of-info
 (implies
  (and (reserrp error)
       (error-info-wfp error))
  (equal
      (reserr-limitp (reserr (cons more (fty::reserr->info error))))
      (reserr-limitp error))))

Theorem: not-reserr-limitp-of-const

(defthm not-reserr-limitp-of-const
 (implies
   (and (syntaxp (quotep kwd))
        (not (equal kwd :limit)))
   (not (reserr-limitp (reserr (list (list fn (cons kwd more))))))))

Theorem: not-reserr-limitp-of-eval-literal

(defthm not-reserr-limitp-of-eval-literal
  (not (reserr-limitp (eval-literal lit))))

Theorem: not-reserr-limitp-of-soutcome

(defthm not-reserr-limitp-of-soutcome
  (not (reserr-limitp (soutcome cstate mode))))

Theorem: not-reserr-limitp-of-path-to-var

(defthm not-reserr-limitp-of-path-to-var
  (implies (reserrp (path-to-var path))
           (not (reserr-limitp (path-to-var path)))))

Theorem: not-reserr-limitp-of-paths-to-vars

(defthm not-reserr-limitp-of-paths-to-vars
  (implies (reserrp (paths-to-vars paths))
           (not (reserr-limitp (paths-to-vars paths)))))

Theorem: not-reserr-limitp-of-read-var-value

(defthm not-reserr-limitp-of-read-var-value
  (b* ((result (read-var-value var cstate)))
    (implies (reserrp result)
             (not (reserr-limitp result)))))

Theorem: not-reserr-limitp-of-read-vars-values

(defthm not-reserr-limitp-of-read-vars-values
  (b* ((result (read-vars-values vars cstate)))
    (implies (reserrp result)
             (not (reserr-limitp result)))))

Theorem: not-reserr-limitp-of-write-var-value

(defthm not-reserr-limitp-of-write-var-value
  (b* ((result (write-var-value var val cstate)))
    (implies (reserrp result)
             (not (reserr-limitp result)))))

Theorem: not-reserr-limitp-of-write-vars-values

(defthm not-reserr-limitp-of-write-vars-values
  (b* ((result (write-vars-values vars vals cstate)))
    (implies (reserrp result)
             (not (reserr-limitp result)))))

Theorem: not-reserr-limitp-of-add-var-value

(defthm not-reserr-limitp-of-add-var-value
  (b* ((result (add-var-value var val cstate)))
    (implies (reserrp result)
             (not (reserr-limitp result)))))

Theorem: not-reserr-limitp-of-add-vars-values

(defthm not-reserr-limitp-of-add-vars-values
  (b* ((result (add-vars-values vars vals cstate)))
    (implies (reserrp result)
             (not (reserr-limitp result)))))

Theorem: not-reserr-limitp-of-find-fun

(defthm not-reserr-limitp-of-find-fun
  (b* ((result (find-fun fun env)))
    (implies (reserrp result)
             (not (reserr-limitp result)))))

Theorem: not-reserr-limitp-of-init-local

(defthm not-reserr-limitp-of-init-local
  (b* ((result (init-local in-vars in-vals out-vars cstate)))
    (implies (reserrp result)
             (not (reserr-limitp result)))))