Rodin Handbook


3.2.2 Substitutions

We use the notation $P[E/x]$ for a substitution of all free occurrences of the variable $x$ in $P$ by the expression $E$. Several substitutions can be performed simultaneously with $P(E_1/x_1,\ldots ,E_ n/x_ n)$. In particular, we use the syntax $P[\mathbf{x}’/\mathbf{x}]$ to denote the substitution of each identifier $x$ in the sequence $\mathbf{x}$ by $x’$. For more information on free identifiers, see Section


  • $(x>y)[5+2/y]$ corresponds to the predicate $(x>5+2)$.

  • $(x>y)[2\cdot y/x,5+2/y]$ corresponds to the predicate $(2\cdot y>5+2)$.

  • $(\exists x \mathord {\mkern 1mu\cdot \mkern 1mu}x\in S \land x>y)[2\cdot y/x,5+2/y]$ corresponds to the predicate $(\exists x \mathord {\mkern 1mu\cdot \mkern 1mu}x\in S \land x>5+2)$, because the $x$ is a quantified variable (i.e. it is not a free variable).

  • For a sequence $\mathbf{v}=v_1,v_2,v_3$ the predicate $(v_1\subseteq v_2\land v_3\in v_1)[\mathbf{v}’/\mathbf{v}]$ corresponds to $(v_1’\subseteq v_2’\land v_3’\in v_1’)$.