		Search-engine friendly clone of the ACL2 documentation.

Static-soundness

Static-soundness-of-variable-addition

Theorems about the static soundness of variable addition.

If add-var and add-vars succeed, also add-var-value and add-vars-values do. Furthermore, the variable table for the resulting computation states is the same returned by the safety checks.

Definitions and Theorems

Theorem: add-var-value-when-add-var

(defthm add-var-value-when-add-var
        (b* ((varset1 (add-var var (cstate-to-vars cstate)))
             (cstate1 (add-var-value var val cstate)))
            (implies (not (reserrp varset1))
                     (and (not (reserrp cstate1))
                          (equal (cstate-to-vars cstate1)
                                 varset1)))))

Theorem: add-vars-values-when-add-vars

(defthm add-vars-values-when-add-vars
        (b* ((varset1 (add-vars vars (cstate-to-vars cstate)))
             (cstate1 (add-vars-values vars vals cstate)))
            (implies (and (not (reserrp varset1))
                          (equal (len vals) (len vars)))
                     (and (not (reserrp cstate1))
                          (equal (cstate-to-vars cstate1)
                                 varset1)))))