Add a list of condition obligation-hypotheses to a context, in order.
(context-add-condition-list conds ctxt) → new-ctxt
Function:
(defun context-add-condition-list (conds ctxt) (declare (xargs :guard (and (expression-listp conds) (contextp ctxt)))) (let ((__function__ 'context-add-condition-list)) (declare (ignorable __function__)) (b* (((when (endp conds)) (context-fix ctxt)) (ctxt (context-add-condition (car conds) ctxt))) (context-add-condition-list (cdr conds) ctxt))))
Theorem:
(defthm contextp-of-context-add-condition-list (b* ((new-ctxt (context-add-condition-list conds ctxt))) (contextp new-ctxt)) :rule-classes :rewrite)
Theorem:
(defthm context-add-condition-list-of-expression-list-fix-conds (equal (context-add-condition-list (expression-list-fix conds) ctxt) (context-add-condition-list conds ctxt)))
Theorem:
(defthm context-add-condition-list-expression-list-equiv-congruence-on-conds (implies (expression-list-equiv conds conds-equiv) (equal (context-add-condition-list conds ctxt) (context-add-condition-list conds-equiv ctxt))) :rule-classes :congruence)
Theorem:
(defthm context-add-condition-list-of-context-fix-ctxt (equal (context-add-condition-list conds (context-fix ctxt)) (context-add-condition-list conds ctxt)))
Theorem:
(defthm context-add-condition-list-context-equiv-congruence-on-ctxt (implies (context-equiv ctxt ctxt-equiv) (equal (context-add-condition-list conds ctxt) (context-add-condition-list conds ctxt-equiv))) :rule-classes :congruence)