Check if a list of paths is safe.
(check-safe-path-list paths varset) → _
Function:
(defun check-safe-path-list (paths varset) (declare (xargs :guard (and (path-listp paths) (identifier-setp varset)))) (let ((__function__ 'check-safe-path-list)) (declare (ignorable __function__)) (b* (((when (endp paths)) nil) ((okf &) (check-safe-path (car paths) varset))) (check-safe-path-list (cdr paths) varset))))
Theorem:
(defthm reserr-optionp-of-check-safe-path-list (b* ((_ (check-safe-path-list paths varset))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm check-safe-path-list-of-path-list-fix-paths (equal (check-safe-path-list (path-list-fix paths) varset) (check-safe-path-list paths varset)))
Theorem:
(defthm check-safe-path-list-path-list-equiv-congruence-on-paths (implies (path-list-equiv paths paths-equiv) (equal (check-safe-path-list paths varset) (check-safe-path-list paths-equiv varset))) :rule-classes :congruence)
Theorem:
(defthm check-safe-path-list-of-identifier-set-fix-varset (equal (check-safe-path-list paths (identifier-set-fix varset)) (check-safe-path-list paths varset)))
Theorem:
(defthm check-safe-path-list-identifier-set-equiv-congruence-on-varset (implies (identifier-set-equiv varset varset-equiv) (equal (check-safe-path-list paths varset) (check-safe-path-list paths varset-equiv))) :rule-classes :congruence)