Tietze transformations: dictionary generators, redundant relators, renaming, and their inverses

Let $\mathcal{P}=⟨X\mid R⟩$ be a formal presentation. A Tietze transformation in the reversible three-type package is one of the following moves.

1. A dictionary-generator move chooses a symbol $y\mathrm{\notin }X$ and a word $w\in F(X)$ and replaces $\mathcal{P}$ by $⟨X\cup \{y\}\mid R\cup \{y^{-1}w\}⟩$. Its inverse may delete $y$ and the relator $y^{-1}w$ only when $w$ contains no $y$ and $y$ occurs in no other remaining relator.
2. A redundant-relator move chooses $r\in ⟨\text{\hspace{0.17em}⁣}⟨R⟩\text{\hspace{0.17em}⁣}{⟩}_{F(X)}$ (The normal closure of a subset of a group) and replaces $R$ by $R\cup \{r\}$. Its inverse may delete a relator $r$ only when $r\in ⟨\text{\hspace{0.17em}⁣}⟨R\setminus \{r\}⟩\text{\hspace{0.17em}⁣}{⟩}_{F(X)}$, so it is already a consequence of the relators that remain.
3. A renaming move chooses a bijection $\alpha :X\to Y$ and replaces every letter $x^{\pm 1}$ in every relator by $\alpha (x{)}^{\pm 1}$. Its inverse is legal precisely because ${\alpha }^{-1}:Y\to X$ is a bijection.

For finite presentations this package has exactly the same reachability as the classical four moves: add or delete a generator with a dictionary relation, and add or delete a consequence relator. The first two types and their stated inverses are those four moves. Conversely, consider first a renaming bijection $\alpha :X\to Y$ with $X\cap Y=\mathrm{\varnothing }$. For each $x\in X$, put $y=\alpha (x)$ and add the fresh generator $y$ with dictionary relator $y^{-1}x$. These dictionaries make $r$ and its renamed word $\alpha (r)$ equal in the presented group for every $r\in R$. Hence each $\alpha (r)$ may be added as a consequence relator; once every renamed relator has been added, each old relator $r$ is a consequence of the renamed relators and the dictionaries and may be deleted. Finally, for each pair $(x,y)$, add $x^{-1}y$, delete its inverse $y^{-1}x$, and then delete $x$ using the dictionary $x^{-1}y$. At that point $x$ occurs in no other relator, so every inverse move is legal. The result is $⟨Y\mid \alpha (R)⟩$.

For a general bijection, choose a finite set $Z$ disjoint from $X\cup Y$ and factor the renaming as $X\to Z\to Y$. The preceding construction simulates both factors. Thus including renaming as a single move changes the packaging, but not finite-presentation reachability.