Generate the consequent of
the
(restrict-gen-restriction-of-rec-calls-consequent-term old rec-calls-with-tests restriction stub? wrld) → consequent
This is the term
(and (implies context1<x1,...,xn,?f> restriction<update1-x1<x1,...,xn,?f>, ..., update1-xn<x1,...,xn,?f>>) ... (implies contextm<x1,...,xn> restriction<updatem-x1<x1,...,xn,?f>, ..., updatem-xn<x1,...,xn,?f>>))
If the function is reflexive (i.e. if
Function:
(defun restrict-gen-restriction-of-rec-calls-consequent-term-aux (old rec-calls-with-tests restriction stub? rev-conjuncts wrld) (declare (xargs :guard (and (symbolp old) (pseudo-tests-and-call-listp rec-calls-with-tests) (pseudo-termp restriction) (symbolp stub?) (pseudo-term-listp rev-conjuncts) (plist-worldp wrld)))) (let ((__function__ 'restrict-gen-restriction-of-rec-calls-consequent-term-aux)) (declare (ignorable __function__)) (if (endp rec-calls-with-tests) (reverse rev-conjuncts) (b* ((tests-and-call (car rec-calls-with-tests)) (tests (access tests-and-call tests-and-call :tests)) (call (access tests-and-call tests-and-call :call)) (context (conjoin tests)) (context (if stub? (sublis-fn-simple (acons old stub? nil) context) context)) (restriction-of-update (subcor-var (formals old wrld) (fargs call) restriction)) (restriction-of-update (if stub? (sublis-fn-simple (acons old stub? nil) restriction-of-update) restriction-of-update))) (restrict-gen-restriction-of-rec-calls-consequent-term-aux old (cdr rec-calls-with-tests) restriction stub? (cons (implicate context restriction-of-update) rev-conjuncts) wrld)))))
Function:
(defun restrict-gen-restriction-of-rec-calls-consequent-term (old rec-calls-with-tests restriction stub? wrld) (declare (xargs :guard (and (symbolp old) (pseudo-tests-and-call-listp rec-calls-with-tests) (pseudo-termp restriction) (symbolp stub?) (plist-worldp wrld)))) (let ((__function__ 'restrict-gen-restriction-of-rec-calls-consequent-term)) (declare (ignorable __function__)) (conjoin (restrict-gen-restriction-of-rec-calls-consequent-term-aux old rec-calls-with-tests restriction stub? nil wrld))))