Using robert (bob) harper

Given:

• A set of variables $𝒳$.

• A set of sorts $𝒮$.

• A sort-indexed family of ABTs $ℬ=\{{ℬ}_s\}$.

• An arity-indexed family of operators $𝒪$.

For a term $b$ and variable $x$, a variable substitution is a partial function $[b/x]$ such that:

• If $x\in 𝒳$ then $[b/x]x=b$.

• If $y\in 𝒳$ and $x\ne y$ then $[b/x]y=y$.

• If $o\in 𝒪$, if ${\overrightarrow{x}}_i\notin b$ then $[b/x]o({\overrightarrow{x}}_1.a_1;\dots ;{\overrightarrow{x}}_n.a_n)=o({\overrightarrow{x}}_1.a_1^{\prime };\dots ;{\overrightarrow{x}}_n.a_n^{\prime })$ such that $a_i^{\prime }=[b/x]a_i$ when $x\notin {\overrightarrow{x}}_i$, else $a_i^{\prime }=a_i$.