		Search-engine friendly clone of the ACL2 documentation.

Static-soundness

Static-soundness-of-variable-reading

Theorems about the static soundness of variable reading.

If check-var and check-var-list succeed, also read-var-value and read-vars-values do.

Definitions and Theorems

Theorem: read-var-value-when-check-var

(defthm read-var-value-when-check-var
        (implies (check-var var (cstate-to-vars cstate))
                 (not (reserrp (read-var-value var cstate)))))

Theorem: read-vars-values-when-check-var-list

(defthm read-vars-values-when-check-var-list
        (implies (check-var-list vars (cstate-to-vars cstate))
                 (not (reserrp (read-vars-values vars cstate)))))