Theorems about the static soundness of variable writing.

If `check-safe-path` and `check-safe-path-list` succeeds,
also `write-var-value` and `write-vars-values` do.
These are proved by showing that path checking
ensures the success of `path-to-var` and `paths-to-vars`,
and also the success of `check-var` and `check-var-list`.
Then we show that `check-var` and `check-var-list`
ensure that `write-var-value` and `write-vars-values` succeed,
and finally we put things together.

**Theorem: **

(defthm path-to-var-when-check-safe-path (implies (not (reserrp (check-safe-path path varset))) (not (reserrp (path-to-var path)))))

**Theorem: **

(defthm check-var-when-check-safe-path (implies (not (reserrp (check-safe-path path varset))) (check-var (path-to-var path) varset)))

**Theorem: **

(defthm paths-to-vars-when-check-safe-path-list (implies (not (reserrp (check-safe-path-list paths varset))) (not (reserrp (paths-to-vars paths)))))

**Theorem: **

(defthm check-var-list-when-check-safe-path-list (implies (not (reserrp (check-safe-path-list paths varset))) (check-var-list (paths-to-vars paths) varset)))

**Theorem: **

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

**Theorem: **

(defthm write-var-value-when-check-safe-path (implies (not (reserrp (check-safe-path path (cstate-to-vars cstate)))) (not (reserrp (write-var-value (path-to-var path) val cstate)))))

**Theorem: **

(defthm write-vars-values-when-check-var-list (implies (and (check-var-list vars (cstate-to-vars cstate)) (equal (len vals) (len vars))) (not (reserrp (write-vars-values vars vals cstate)))))

**Theorem: **

(defthm write-vars-values-when-check-safe-path-list (implies (and (not (reserrp (check-safe-path-list paths (cstate-to-vars cstate)))) (equal (len vals) (len paths))) (not (reserrp (write-vars-values (paths-to-vars paths) vals cstate)))))