Defmapping-differentiate-a/b-vars
Ensure that the variables
a1, ..., an or b1, ..., bm
do not overlap with
b1, ..., bm or a1, ..., an.
- Signature
(defmapping-differentiate-a/b-vars a1/b1...an/bm b1/a1...bm/an)
→
a1/b1...an/bm-differentiated
- Arguments
- a1/b1...an/bm — Guard (symbol-listp a1/b1...an/bm).
- b1/a1...bm/an — Guard (symbol-listp b1/a1...bm/an).
- Returns
- a1/b1...an/bm-differentiated — A symbol-listp.
In the formula of the :alpha-of-beta applicability condition,
in certain cases a1, ..., an are bound by mv-let,
and b1, ..., bm are used in the body of the mv-let:
if any bj were identical to any ai,
the formula would be incorrect in general.
A similar situation occurs
with the :beta-of-alpha applicability condition,
with the roles of a1, ..., an and b1, ..., bm swapped.
Thus, in these cases we may need to differentiate
a1, ..., an apart from b1, ..., bm or vice versa.
We do that here, using genvar.
Definitions and Theorems
Function: defmapping-differentiate-a/b-vars
(defun defmapping-differentiate-a/b-vars
(a1/b1...an/bm b1/a1...bm/an)
(declare (xargs :guard (and (symbol-listp a1/b1...an/bm)
(symbol-listp b1/a1...bm/an))))
(let ((__function__ 'defmapping-differentiate-a/b-vars))
(declare (ignorable __function__))
(cond
((endp a1/b1...an/bm) nil)
(t
(b* ((a2/b2...an/bm-differentiated
(defmapping-differentiate-a/b-vars (cdr a1/b1...an/bm)
b1/a1...bm/an))
(a1/b1 (car a1/b1...an/bm))
(a1/b1-differentiated
(genvar a1/b1 (symbol-name a1/b1)
nil
(append b1/a1...bm/an
a2/b2...an/bm-differentiated))))
(cons a1/b1-differentiated
a2/b2...an/bm-differentiated))))))
