Push a scope onto the validation table.
(valid-push-scope table) → new-table
The newly pushed scope is always empty.
Function:
(defun valid-push-scope (table) (declare (xargs :guard (valid-tablep table))) (let ((__function__ 'valid-push-scope)) (declare (ignorable __function__)) (b* ((scopes (valid-table->scopes table)) (new-scopes (cons (valid-empty-scope) scopes))) (change-valid-table table :scopes new-scopes))))
Theorem:
(defthm valid-tablep-of-valid-push-scope (b* ((new-table (valid-push-scope table))) (valid-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm valid-table-num-scopes-of-valid-push-scope (b* ((?new-table (valid-push-scope table))) (equal (valid-table-num-scopes new-table) (1+ (valid-table-num-scopes table)))))
Theorem:
(defthm valid-push-scope-of-valid-table-fix-table (equal (valid-push-scope (valid-table-fix table)) (valid-push-scope table)))
Theorem:
(defthm valid-push-scope-valid-table-equiv-congruence-on-table (implies (valid-table-equiv table table-equiv) (equal (valid-push-scope table) (valid-push-scope table-equiv))) :rule-classes :congruence)