Structural induction modulo fresh renaming

To show that $\begin{array}{l}\\ mathcalP[mathcalX](a)\end{array}$ holds for every $\begin{array}{l}a\\ in\\ mathcalB[mathcalX]\end{array}$, it is enough to show the following:

• Formulation

  Consider:

  • A set of sorts $𝒮$.

  • A set of variables $𝒳$.

  • A predicate $𝒫$ that is parameterized by $𝒳$ and $s$.

  • A set of Abstract binding tree (ABT) $ℬ$ with Free variables in $𝒳$.

    To show that $𝒫[𝒳](a)$ holds for every $a\in ℬ[𝒳]$, it is enough to show the following:

  1. If $x\in {𝒳}_s$, then $𝒫{[𝒳]}_s(x)$.

  2. For every $o$ of arity $({\overrightarrow{s}}_1.s_1;\dots ;{\overrightarrow{s}}_n.s_n).s$, if for each $1\le i\le n$, $𝒫{[𝒳,{\overrightarrow{x}}_i^{\prime }]}_{s_i}({\hat{\rho }}_i(a_i))$ for every ${\rho }_i:{\overrightarrow{x}}_i\leftrightarrow {\overrightarrow{x}}_i^{\prime }$ with ${\overrightarrow{x}}_i^{\prime }\notin 𝒳$, then $𝒫{[𝒳]}_s(o({\overrightarrow{x}}_1.a_1;\dots ;{\overrightarrow{x}}_n.a_n))$.