Apply function substitutions to terms.
See the discussion in fun-subst-function.
Function:
(defun fun-subst-term (fsbs term wrld) (declare (xargs :guard (and (fun-substp fsbs) (pseudo-termp term) (plist-worldp wrld)))) (let ((__function__ 'fun-subst-term)) (declare (ignorable __function__)) (if (or (variablep term) (quotep term)) term (let* ((fn (fn-symb term)) (new-fn (if (symbolp fn) (fun-subst-function fsbs fn wrld) (make-lambda (lambda-formals fn) (fun-subst-term fsbs (lambda-body fn) wrld)))) (new-args (fun-subst-terms fsbs (fargs term) wrld))) (cons new-fn new-args)))))
Function:
(defun fun-subst-terms (fsbs terms wrld) (declare (xargs :guard (and (fun-substp fsbs) (pseudo-term-listp terms) (plist-worldp wrld)))) (let ((__function__ 'fun-subst-terms)) (declare (ignorable __function__)) (if (endp terms) nil (cons (fun-subst-term fsbs (car terms) wrld) (fun-subst-terms fsbs (cdr terms) wrld)))))
Function:
(defun fun-subst-term (fsbs term wrld) (declare (xargs :guard (and (fun-substp fsbs) (pseudo-termp term) (plist-worldp wrld)))) (let ((__function__ 'fun-subst-term)) (declare (ignorable __function__)) (if (or (variablep term) (quotep term)) term (let* ((fn (fn-symb term)) (new-fn (if (symbolp fn) (fun-subst-function fsbs fn wrld) (make-lambda (lambda-formals fn) (fun-subst-term fsbs (lambda-body fn) wrld)))) (new-args (fun-subst-terms fsbs (fargs term) wrld))) (cons new-fn new-args)))))
Function:
(defun fun-subst-terms (fsbs terms wrld) (declare (xargs :guard (and (fun-substp fsbs) (pseudo-term-listp terms) (plist-worldp wrld)))) (let ((__function__ 'fun-subst-terms)) (declare (ignorable __function__)) (if (endp terms) nil (cons (fun-subst-term fsbs (car terms) wrld) (fun-subst-terms fsbs (cdr terms) wrld)))))