# A Sound and Complete Equational Theory for 3-Qubit Toffoli-Hadamard Circuits

Matthew Amy Simon Fraser University
Burnaby, Canada<EMAIL_ADDRESS>Dalhousie University
Halifax, CanadaDalhousie University
Halifax, Canada Neil J. Ross Dalhousie University
Halifax, Canada<EMAIL_ADDRESS>Dalhousie University
Halifax, Canada Scott Wesley Dalhousie University
Halifax, Canada<EMAIL_ADDRESS>
###### Abstract

We give a sound and complete equational theory for $3$-qubit quantum circuits
over the Toffoli-Hadamard gate set $\\{X,CX,CCX,H\\}$. That is, we introduce a
collection of true equations among Toffoli-Hadamard circuits on three qubits
that is sufficient to derive any other true equation between such circuits. To
obtain this equational theory, we first consider circuits over the Toffoli-$K$
gate set $\\{X,CX,CCX,K\\}$, where $K=H\otimes H$. The Toffoli-Hadamard and
Toffoli-$K$ gate sets appear similar, but they are crucially different on
exactly three qubits. Indeed, in this case, the former generates an infinite
group of operators, while the latter generates the finite group of
automorphisms of the well-known $E_{8}$ lattice. We take advantage of this
fact, and of the theory of automorphism groups of lattices, to obtain a sound
and complete collection of equations for Toffoli-$K$ circuits. We then extend
this equational theory to one for Toffoli-Hadamard circuits by leveraging
prior work of Li et al. on Toffoli-Hadamard operators.

##  1 Introduction

The _Toffoli-Hadamard_ gate set is obtained by extending the classical
reversible gate set $\\{X,CX,CCX\\}$ with the Hadamard gate $H$. The addition
of the Hadamard gate promotes the gate set $\\{X,CX,CCX\\}$ from one that is
universal for classical reversible computation to one that is universal for
quantum computation [2, 24]. Because the Hadamard gate can introduce phases of
$(-1)$ and produce superpositions, one can think of the addition of the
Hadamard gate as a simple way to augment classical reversible computation with
these typically quantum features. In turn, this motivates the study of
Toffoli-Hadamard circuits [2, 5, 4, 11, 19, 24, 26, 27].

In recent years, an important effort has been made to understand quantum
circuits equationally. If $G$ is a set of quantum gates, an _equational
theory_ for $G$ is given by a set of _equations_ (or _relations_) among the
circuits over $G$. The equational theory is _sound_ if it only equates
circuits that correspond to the same operator, and _complete_ if it always
equates circuits that correspond to the same operator. Equational theories can
be used to optimize and verify quantum circuits in practice, but, more
fundamentally, they can illuminate the mathematical structure underlying the
gate set $G$. Sound and complete equational theories have been found for
several important gate sets [3, 8, 9, 12, 20, 23].

In this paper, we give a sound and complete equational theory for 3-qubit
Toffoli-Hadamard circuits. A presentation for the group of Toffoli-Hadamard
operators was given in [19], but the presentation uses 1-, 2-, and 4-level
operators as generators. While these operators can be represented by Toffoli-
Hadamard circuits, this leads to an unnatural presentation, from the
perspective of quantum circuits. What is more, the presentation of [19]
contains over 2000 relations, even when restricted to 3-qubit operators. Many
of these relations can be presented concisely as relation schemas in the
language of operators, but these relations need to be expanded to be stated in
the language of circuits. In contrast, our presentation contains only 65
relations, most of which are natural from the perspective of quantum circuits.

To obtain our presentation, we first consider circuits over the Toffoli-$K$
gate set $\\{X,CX,CCX,K\\}$, where $K=H\otimes H$. The Toffoli-Hadamard and
Toffoli-$K$ gate sets appear similar, but they are crucially different on
exactly three qubits. Indeed, in this case, the former generates an infinite
group of operators, while the latter generates the finite group of
automorphisms of the well-known $E_{8}$ lattice. The correspondence between
3-qubit Toffoli-$K$ circuits and the automorphisms of the $E_{8}$ lattice was
previously known (see [15, 22]). We take advantage of this correspondence, and
of the theory of automorphism groups of lattices, to obtain a sound and
complete collection of equations for Toffoli-$K$ circuits. The automorphism
group of the $E_{8}$ lattice admits a finite Coxeter presentation, which
enjoys many geometric and combinatorial properties, and we use _Tietze
transformations_ to turn the Coxeter presentation of the group of Toffoli-$K$
operators into a concise circuit presentation. We then extend this equational
theory to one for Toffoli-Hadamard circuits by building upon [19]. Our paper
therefore regards the group of $3$-qubit Toffoli-Hadamard circuits as an
extension of the automorphism group of the $E_{8}$ lattice in order to
elucidate its underlying mathematical structure.

The paper is organized as follows. In Section 2, we define three groups of
interest. In Section 3, we recall prior results on finite group presentations
and we review Tietze transformations. In Section 4, we use the theory of
Coxeter groups to obtain a presentation for the group of $3$-qubit Toffoli-K
circuits using a minimal number of generators. We moreover show that every
operator in this group can be represented by a circuit of Toffoli-count at
most $120$. In Sections 5 and 6, the results of Li _et al._ [19] are used to
extend this presentation to a presentation for $3$-qubit circuits over the
gate set $\\{X,CX,CCX,K,CCZ\\}$, and then to one for 3-qubit Toffoli-Hadamard
circuits. Our approach relies on a large number of derivations and intricate
rewriting proofs, which we relegate to several appendices and a supplement
[6].

##  2 Three Groups and Their Generators

Let $\mathbb{Z}$ denote the ring of integers. The _half-integers_
$\mathbb{Z}+1/2$ are defined as $\mathbb{Z}+1/2=\\{a+1/2\mid
a\in\mathbb{Z}\\}$ and the ring of _dyadic fractions_ $\mathbb{D}$ is defined
as $\mathbb{D}=\mathbb{Z}[1/2]=\\{a/2^{k}\mid a\in\mathbb{Z}\mbox{ and
}k\in\mathbb{N}\\}$. Equivalently, $\mathbb{D}$ is the smallest subring of
$\mathbb{Q}$ that contains both $\mathbb{Z}$ and $1/2$. The _$E_{8}$ lattice_
$\Gamma_{8}$ is the following collection of 8-dimensional vectors,

$\Gamma_{8}=\left\\{x\in\mathbb{Z}^{8}\cup(\mathbb{Z}+1/2)^{8}\;\middle|\;\sum
x_{i}\equiv 0\pmod{2}\right\\}.$

In other words, $\Gamma_{8}$ consists of the vectors in $\mathbb{R}^{8}$ whose
components sum to an even integer and are either all integers or all half-
integers. The $E_{8}$ lattice is well-studied because it enjoys many
remarkable properties [13]; in particular, it provides the densest sphere
packing in dimension 8 [25].

We now introduce the three groups that will be the focus of this paper. Let
$R$ be a ring. For each $n\in\mathbb{N}$, let $\mathrm{GL}(n,R)$ denote the
general linear group over $R$ in dimension $n$ and let $\mathrm{O}(n,R)$
denote the orthogonal group over $R$ in dimension $n$. Define $W(E_{8})$ to be
the subgroup of $\mathrm{O}(8,\mathbb{D})$ consisting of the elements of
$\mathrm{O}(8,\mathbb{D})$ that fix the $E_{8}$ lattice. Define
$\textsf{TofH}(n)$ to be the subgroup of
$\mathrm{O}(2^{n},\mathbb{Z}[1/\sqrt{2}])$ consisting of matrices
$M/\sqrt{2}{}^{k}$, where $M$ is an integer matrix and $k\in\mathbb{N}$. We
will be interested in the groups $W(E_{8})$, $\mathrm{O}(8,\mathbb{D})$, and
$\textsf{TofH}(3)$. Note that we have
$W(E_{8})\leq\mathrm{O}(8,\mathbb{D})\leq\textsf{TofH}(3)$.

The above three groups are generated by well-known quantum gates. Let $I$
denote the $2\times 2$ identity matrix and $\otimes$ denote the Kronecker
tensor product. Given a dimension $2$ matrix $M$, define ${M}_{0}=M\otimes
I\otimes I$, ${M}_{1}=I\otimes M\otimes I$, and ${M}_{2}=I\otimes I\otimes M$.
That is, ${M}_{j}$ applies operator $M$ to the $j$-th qubit. Furthermore,
define ${C{M}}_{{j},{k}}$ to be the operator that sends each standard basis
state $\ket{x_{0}x_{1}x_{2}}$ to $({M}_{k})^{x_{j}}\ket{x_{0}x_{1}x_{2}}$.
That is, ${C{M}}_{{j},{k}}$ applies operator $M$ to the $k$-th qubit whenever
the $j$-th qubit is in the basis state $\ket{1}$. Likewise, define
${CC{M}}_{{j},{k}}$ to be the operator that sends each standard basis state
$\ket{x_{0}x_{1}x_{2}}$ to $({M}_{l})^{x_{j}x_{k}}\ket{x_{0}x_{1}x_{2}}$ for
$l\in\\{1,2,3\\}\setminus\\{j,k\\}$. That is, ${CC{M}}_{{j},{k}}$ applies
operator $M$ to the $l$-th qubit whenever the $j$-th and $k$-th qubits are
both in the basis state $\ket{1}$. The operators ${C{M}}_{{j},{k}}$ and
${CC{M}}_{{j},{k}}$ denote the usual _controlled- $M$ gate_ and _doubly-
controlled- $M$ gate_, respectively. Now recall the _Pauli $X$_, _Pauli $Z$_,
_Hadamard_ , and $K$ matrices,

$X=\begin{bmatrix}0&1\\\ 1&0\end{bmatrix},\qquad Z=\begin{bmatrix}1&0\\\
0&-1\end{bmatrix},\qquad H=\frac{1}{\sqrt{2}}\begin{bmatrix}1&1\\\
1&-1\end{bmatrix},\qquad\mbox{and}\qquad K_{j,k}=H_{j}\circ H_{k},$

where $(\circ)$ denotes matrix multiplication. Then ${CC{X}}_{{j},{k}}$
denotes the _Toffoli_ gate. Note that the matrices of the form ${X}_{j}$,
${K}_{{j,k}}$, ${C{X}}_{{j},{k}}$, ${CC{X}}_{{j},{k}}$, and
${CC{Z}}_{{j},{k}}$ belong to $\mathrm{O}(8,\mathbb{D})$. It is known that
$\\{{X}_{j},{C{X}}_{{j},{k}},{CC{X}}_{{j},{k}},{K}_{{j,k}}\\}$ is a generating
set for $W(E_{8})$ [13]. Similarly it is known that
$\\{{X}_{j},{C{X}}_{{j},{k}},{CC{X}}_{{j},{k}},{K}_{{j,k}},{CC{Z}}_{{j},{k}}\\}$
and $\\{{X}_{j},{C{X}}_{{j},{k}},{CC{X}}_{{j},{k}},{H}_{j}\\}$ are generating
sets for $\mathrm{O}(8,\mathbb{D})$ and $\textsf{TofH}(3)$, respectively
[4]111The generator $CCZ_{j,k}$ is necessary to apply these results to the
ancilla-free three-qubit case..

##  3 Presentations and Tietze Transformations

We now recall key results from combinatorial group theory. In particular, we
discuss monoid presentations, as well as _Tietze transformations_ , which will
play an important role in the rest of the paper.

###  3.1 Presentations

Let $\Sigma$ be an alphabet (i.e., a set of symbols). Then $\Sigma^{*}$ is the
_free monoid on $\Sigma$_. The elements of $\Sigma^{*}$ are the words over
$\Sigma$, the monoid operation is string concatenation, which we denote by
$(\cdot)$, and the identity element in $\Sigma^{*}$ is the empty word, which
we denote by $\epsilon$.

If $G$ is a monoid and $Q$ is a quotient of $G$, then we write
$\pi_{Q}:G\twoheadrightarrow Q$ to denote the canonical projection of $G$ onto
$Q$. Given a subset $R$ of $\Sigma^{*}\times\Sigma^{*}$, we write
$Q=\langle\Sigma\mid R\rangle$ to denote the largest quotient of
$G=\Sigma^{*}$ such that $\pi_{Q}(q)=\pi_{Q}(r)$ for all $(q,r)\in R$. If
$M\cong\langle\Sigma\mid R\rangle$, then we say that $\langle\Sigma\mid
R\rangle$ is a _presentation of $M$_ and write $q\approx_{R}$ for each
$(q,r)\in R$. The elements of $\Sigma$ are called _generators_ and the
elements of $R$ are called _relations_. If, for each $x\in\Sigma$, there
exists a $w\in\Sigma^{*}$ such that $\pi_{Q}(x\cdot w)=\pi_{Q}(\epsilon)$,
then $M$ is a group and $\langle\Sigma\mid R\rangle$ is a _monoid presentation
for the group_ $M$. In either case, if $\Sigma$ and $R$ are finite, then
$\langle\Sigma\mid R\rangle$ is a _finite presentation_. We distinguish
between the presentations $\langle\Sigma\mid R\rangle$ and $\langle\Sigma\mid
R^{\prime}\rangle$ whenever $R\neq R^{\prime}$, even if $R$ and $R^{\prime}$
generate the same quotient.

Certain aspects of presentations can be conveniently expressed in the language
of string rewriting. Let $\Sigma$ be an alphabet and
$R\subseteq\Sigma^{*}\times\Sigma^{*}$. Fix some $u\in\Sigma^{*}$ and
$v\in\Sigma^{*}$. If there exists some $(q,r)\in R$ and $s,t\in\Sigma^{*}$
such that $u=s\cdot q\cdot t$ and $v=s\cdot r\cdot t$, then we write,

$u\xrightarrow{R}v.$

If either $u\xrightarrow{R}v$ or $u\xleftarrow{R}v$, then we write
$u\stackrel{{\scriptstyle R}}{{\leftrightarrow}}v$. We say that _$u$ rewrites
to $v$_, denoted $u\sim_{R}v$, if either $u=v$ or there exists a finite
sequence,

$u\stackrel{{\scriptstyle R}}{{\leftrightarrow}}w_{1}\stackrel{{\scriptstyle
R}}{{\leftrightarrow}}w_{2}\stackrel{{\scriptstyle
R}}{{\leftrightarrow}}\cdots\stackrel{{\scriptstyle
R}}{{\leftrightarrow}}w_{n}\stackrel{{\scriptstyle R}}{{\leftrightarrow}}v.$

That is, $(\sim_{R})$ is the symmetric, transitive and reflexive closure of
$\xrightarrow{R}$. Importantly, $\pi_{Q}(u)=\pi_{Q}(v)$ in
$Q=\langle\Sigma,R\rangle$ if and only if $u\sim_{R}v$ [10, Ch. 7]. That is,
two words $u$ and $v$ represent the same element in $G$ if and only if the
relations in $R$ suffice to rewrite $u$ into $v$. In this sense, the relations
in $R$ define a _complete equational theory_ for the monoid $Q$ with respect
to the generators $\Sigma$. For further information on presentations and on
rewriting, the reader is encouraged to consult [18] and [10], respectively.

###  3.2 Tietze Transformations

The transformations, which we state formally below, allow one to add a
generator, remove a generator, add a relation, and remove a relation. Let
$\Sigma$ be an alphabet, $R\subseteq\Sigma^{*}\times\Sigma^{*}$, and
$G=\langle\Sigma\mid R\rangle$ be a monoid.

  * –

Gen($+$). Let $x$ be a symbol. If $x\not\in\Sigma$ and $w\in\Sigma^{*}$, then
$G\cong\langle\Sigma\cup\\{x\\}\mid R\cup\\{x\approx w\\}\rangle$.

  * –

Gen($-$). Let $x\in\Sigma$, $x\approx_{R}w$, $\Pi=\Sigma\setminus\\{x\\}$, and
$Q=R\setminus\\{x\approx w\\}$. If $Q\subseteq\Pi^{*}\times\Pi^{*}$, then
$G\cong\langle\Pi\mid Q\rangle$.

  * –

Rel($+$). If $q\sim_{R}r$, then $G\cong\langle\Sigma\mid R\cup\\{q\approx
r\\}\rangle$.

  * –

Rel($-$). Let $q\approx_{R}r$ and $Q=R\setminus\\{q\approx r\\}$. If
$q\sim_{Q}r$, then $G\cong\langle\Sigma\mid Q\rangle$.

The Gen($+$) rule states that one can add a generator if one also adds a
relation defining it in terms of the other generators. The Gen($-$) rule
states that a generator can be removed if it is defined in terms of the other
generators, and does not appear in any of the other relations. The Rel($+$)
rule states that if a relation can be derived from the existing ones, then it
can be added to the set of relations. Finally, the Rel($-$) rule conversely
states that if a relation can be derived from other relations in the
presentation, it is redundant and can be removed.

Tietze transformations are sound and complete for the isomorphism of finite
monoid presentations. That is, two presentations $\langle\Sigma\mid R\rangle$
and $\langle\Pi\mid Q\rangle$ specify the same monoid if and only if
$\langle\Sigma\mid R\rangle$ can be obtained from $\langle\Pi\mid Q\rangle$
through a finite sequence of Tietze transformations [16, Section 1].

The goal of this paper is to find presentations for groups of quantum
operators in which each generator corresponds to a specific quantum gate. More
explicitly, given a group $G$, a generating set $\Sigma$, and a _semantic
interpretation_ $[\\![\cdot]\\!]_{\Sigma}:\Sigma\to G$, our goal is to find a
set of relations $R\subseteq\Sigma^{*}\times\Sigma^{*}$ such that
$[\\![\cdot]\\!]$ induces an isomorphism between $\langle\Sigma\mid R\rangle$
and $G$. In what follows, we start from a known presentation $\langle\Pi\mid
Q\rangle$ over different generators $\Pi$ with a semantic interpretation
$[\\![\cdot]\\!]_{\Pi}:\Pi\to G$, and obtain $\langle\Sigma\mid R\rangle$ via
a sequence of Tietze transformations. As these Tietze transformations act on
the abstract group $\langle\Pi\mid Q\rangle$, one must ensure that the
transformations respect the intended interpretation $[\\![\cdot]\\!]_{\Sigma}$
of the new generators in $\Sigma$, as discussed further in Appendix A.

##  4 From Coxeter to Circuit Presentations of $W(E_{8})$

A _Coxeter group_ is a group $G$ which admits a group presentation of the form
$\langle r_{1},\ldots,r_{n}\mid(r_{j}r_{k})^{N_{j,k}}\approx\epsilon\rangle$,
where $N$ is an $n\times n$ matrix over $\mathbb{N}\cup\\{\infty\\}$ such that
$N_{j,j}=1$ and $N_{j,k}>1$ for all $j\neq k$ [17]. The matrix $N$ is known as
the _Coxeter matrix_ of $G$. Note that since $\pi_{G}(r_{j}\cdot
r_{j})=\epsilon$ for each $r_{j}$, then every Coxeter presentation is
automatically a monoid presentation for a group. Coxeter groups are an
abstraction of reflection groups and, in particular, for every finite Coxeter
group $G$, there is a faithful group representation $G\to\mathrm{O}(n)$ that
maps each $r_{j}$ to a reflection in $\mathbb{R}^{n}$ [17]. Recall that a
_Householder transformation_ is a reflection about the hyperplane normal to
some vector $\alpha\in\mathbb{R}^{n}$ defined by $v\mapsto v-2\frac{\langle
v,\alpha\rangle}{\langle\alpha,\alpha\rangle}\alpha$ [17]. If $r$ is the
reflection about the hyperplane normal to $\alpha\in\mathbb{R}^{n}$ and
$M\in\mathrm{O}(n)$, then $M\circ r\circ M^{-1}$ is the reflection about the
hyperplane normal to $M\alpha$ [17, Prop. 1.2]. As a special case, $v$ and
$-v$ define the same reflection.

The goal of this section is to construct a presentation for the Weyl group of
the $E_{8}$ lattice in terms of Toffoli-K gates. Recall that the Weyl group
for any lattice $L\subseteq\mathbb{R}^{n}$ is the finite reflection group
generated by reflections about the roots of $L$ (see [17, Sec. 2.9]). That is,
given a root system $\Phi$ for $L$, the group $W(L)$ is generated by
$\\{r_{\alpha}:\alpha\in\Phi\\}$ where $r_{\alpha}$ is the reflection through
the hyperplane normal to $\alpha$. Consequently, $W(E_{8})$ is a Coxeter
group. A root system and the corresponding Coxeter matrix for $W(E_{8})$ are
given in Figure 1.

$\begin{bmatrix}1&0&0&0&0&0&0&-1/2\\\ -1&1&0&0&0&0&0&-1/2\\\
0&-1&1&0&0&0&0&-1/2\\\ 0&0&-1&1&0&0&0&-1/2\\\ 0&0&0&-1&1&0&0&-1/2\\\
0&0&0&0&-1&1&1&-1/2\\\ 0&0&0&0&0&-1&1&-1/2\\\ 0&0&0&0&0&0&0&-1/2\\\
\end{bmatrix}$

(a) $E_{8}$ Root System.

$\begin{bmatrix}1&3&2&2&2&2&2&2\\\ 3&1&3&2&2&2&2&2\\\ 2&3&1&3&2&2&2&2\\\
2&2&3&1&3&2&2&2\\\ 2&2&2&3&1&3&3&2\\\ 2&2&2&2&3&1&2&2\\\ 2&2&2&2&3&2&1&3\\\
2&2&2&2&2&2&3&1\\\ \end{bmatrix}$

(b) $W(E_{8})$ Coxeter Matrix.

Figure 1: The root system and Coxeter matrix for $W(E_{8})$. Note that the
root system consists of $8$ vectors and are presented as the columns of an
$8\times 8$ matrix. ${\langle\Sigma_{E8}\mid
R_{E8}\rangle}$${\langle\Sigma_{E8}\cup\Sigma_{D}\mid R_{E8}\cup
R_{D(E8)}\rangle}$${\langle\Sigma_{E8}\cup\Sigma_{D}\mid R_{E8}\cup
R_{D(E8)}\cup R_{E8(D)}\rangle}$${\langle\Sigma_{E8}\cup\Sigma_{D}\mid
R_{E8}\cup R_{D(E8)}\cup R_{E8(D)}\cup R_{D}\rangle}$${\langle\Sigma_{D}\mid
R_{D}\rangle}$${\langle\Sigma_{E8}\cup\Sigma_{D}\mid R_{E8(D)}\cup
R_{D}\rangle}$${\langle\Sigma_{E8}\cup\Sigma_{D}\mid R_{E8}\cup R_{E8(D)}\cup
R_{D}\rangle}$$\scriptstyle{\textbf{Gen(}+\textbf{)}}$$\scriptstyle{\cong}$$\scriptstyle{\textbf{Rel(}+\textbf{)}}$$\scriptstyle{\textbf{Rel(}+\textbf{)}}$$\scriptstyle{\textbf{Rel(}-\textbf{)}}$$\scriptstyle{\textbf{Gen(}-\textbf{)}}$$\scriptstyle{\textbf{Rel(}-\textbf{)}}$
Figure 2: A diagrammatic summary of the Tietze transformations used to obtain
a presentation for $W(E_{8})$. Note that in this diagram $\Sigma_{E8}$ denotes
the Coxeter generators, $\Sigma_{D}$ denotes the dyadic Toffoli-Hadamard
gates, $R_{D(E8)}$ expresses the $\Sigma_{D}$ in terms of $\Sigma_{E8}$, and
$R_{E8(D)}$ expresses $\Sigma_{E8}$ in terms of $\Sigma_{D}$.

To obtain a presentation in terms of Toffoli-K gates, we begin with the
Coxeter presentation of $W(E_{8})$. The desired presentation is then obtained
through a sequence of Tietze transformations. First, the Gen($+$) rule is used
to introduce the dyadic Toffoli-K gates with their intended semantics. Second,
the Rel($+$) rule is used to rewrite the Coxeter generators in terms of
Toffoli-K gates (call these relations $R_{E8(D)}$). Third, the Rel($+$) rule
is used to introduce well-known relations satisfied by the Toffoli-K gates
(see, e.g., [19, 20]). Given these new relations, the Rel($-$) rule is used to
eliminate all defining relations for the Toffoli-K gates. In a similar
fashion, the Rel($-$) rule is also used to eliminate the Coxeter relations of
$W(E_{8})$. At this point, the Coxeter generators only appear in $R_{E8(D)}$,
and can be eliminated using the Gen($-$) rule. What remains is a presentation
of $W(E_{8})$ in terms of Toffoli-K gates. All steps of this proof are
summarized in Figure 2.

Each step of this proof requires numerous applications of the corresponding
Tietze transformation. To establish that each Gen($+$) and Rel($+$)
transformation holds, an equation of $8\times 8$ matrices must be validated.
To establish that each Rel($-$) transformation holds, a derivational proof
must be validated. In both cases, the proof obligation is computational in
nature. The validity of our Tietze transformations have been machine-verified
by the software package Tietze 222Available at:
https://github.com/meamy/tietze..

###  4.1 Introducing the Toffoli-K Gates

The generators of $W(E_{8})$ can be written as follows.

$\displaystyle r_{1}$
$\displaystyle={X}_{0}\circ{X}_{1}\circ{CC{X}}_{{0},{1}}\circ{X}_{1}\circ{X}_{0}$
$\displaystyle r_{2}$
$\displaystyle={X}_{0}\circ{C{X}}_{{2},{1}}\circ{CC{X}}_{{0},{1}}\circ{C{X}}_{{2},{1}}\circ{X}_{0}$
$\displaystyle r_{3}$
$\displaystyle={X}_{0}\circ{CC{X}}_{{0},{1}}\circ{X}_{0}$ $\displaystyle
r_{4}$
$\displaystyle={C{X}}_{{0},{1}}\circ{C{X}}_{{0},{2}}\circ{CC{X}}_{{1},{2}}\circ{C{X}}_{{0},{2}}\circ{C{X}}_{{0},{1}}$
$\displaystyle r_{5}$
$\displaystyle={X}_{1}\circ{CC{X}}_{{0},{1}}\circ{X}_{1}$ $\displaystyle
r_{6}$
$\displaystyle={C{X}}_{{2},{1}}\circ{CC{X}}_{{0},{1}}\circ{C{X}}_{{2},{1}}$
$\displaystyle r_{7}$
$\displaystyle={C{Z}}_{{0},{1}}\circ{C{X}}_{{2},{1}}\circ{CC{X}}_{{0},{1}}\circ{C{X}}_{{2},{1}}\circ{C{Z}}_{{0},{1}}$
$\displaystyle r_{8}$
$\displaystyle=K_{1,2}\circ{X}_{1}\circ{X}_{2}\circ{C{Z}}_{{0},{2}}\circ{CC{X}}_{{1},{2}}\circ{C{Z}}_{{0},{2}}\circ{X}_{2}\circ{X}_{1}\circ
K_{1,2}$

These equations can be derived from the geometry of $\mathbb{R}^{8}$. First,
note that ${CC{X}}_{{0},{1}}$ is a reflection about the hyperplane normal to
$\ket{\widehat{b}}=\ket{1}\otimes\ket{1}\otimes\ket{-}$ where
$\ket{\pm}=(\ket{0}\pm\ket{1})/\sqrt{2}$. Then for each generator $r_{j}$ with
normal vector $\ket{b_{j}}$, it suffices to find an element $M\in W(E_{8})$
such that $M\ket{\widehat{b}}=\ket{b_{j}}$. The corresponding circuit would be
$M\circ{CC{X}}_{{1},{2}}\circ M^{-1}$. As an example of this technique,
consider the Coxeter generator $r_{3}$ defined by the normal vector
$\ket{b_{3}}=\ket{0}\otimes\ket{1}\otimes\ket{-}$. Since
$({X}_{0})\ket{\widehat{b}}=\ket{b_{3}}$ with ${X}_{0}$ self-inverse, then
$r_{3}={X}_{0}\circ{CC{X}}_{{0},{1}}\circ{X}_{0}$. The remaining cases are
established in Appendix C.

Next, the Toffoli-K gates are introduced. For simplicity of presentation, we
first introduce the swap matrices
$\sigma_{j,k}={C{X}}_{{j},{k}}\circ{C{X}}_{{k},{j}}\circ{C{X}}_{{j},{k}}$
where $\sigma_{j,k}$ permutes the $j$-th qubit with the $k$-th qubit. Recall
that the Toffoli-K gates correspond to the following matrices333For
simplicity, we assume that all $K$ gates are applied to adjacent qubits. This
is sufficient, since $K_{0,2}=K_{0,1}\circ K_{1,2}$.:

$\Sigma_{D}:=\left\\{{X}_{j},{C{X}}_{{k},{l}},{CC{X}}_{{j},{k}},{Z}_{j},{C{Z}}_{{j},{k}},K_{j,j+1},\sigma_{j,k}\mid
j,k,l\in\\{0,1,2\\},j<k,j\neq l\neq k\right\\}.$

It turns out that all Toffoli-K gates are generated by ${X}_{0}$,
${C{X}}_{{1},{0}}$, ${CC{X}}_{{1},{2}}$, and $K_{1,2}$. To derive these
primitive gates, it helps to first derive several diagonal matrices over $(\pm
1)$. These are then used to derive the ${CC{X}}_{{0},{1}}$ and ${X}_{0}$
gates. From this, the swap matrices can be derived, after which, it is
relatively straightforward to construct the ${X}_{0}$, ${K}_{1,2}$, and
${C{X}}_{{0},{1}}$ gates. This yields four words $w_{X}$, $w_{K}$, $w_{CX}$,
and $w_{CCX}$, such that $[\\![w_{X}]\\!]^{*}_{E8}={X}_{0}$,
$[\\![w_{CX}]\\!]^{*}_{E8}={C{X}}_{{1},{0}}$,
$[\\![w_{CCX}]\\!]^{*}_{E8}={CC{X}}_{{1},{2}}$, and
$[\\![w_{K}]\\!]^{*}_{E8}={K}_{1,2}$, as outlined in Appendix D.

The remaining Toffoli-K gates are derived in terms of $K_{1,2}$,
${CC{X}}_{{1},{2}}$, ${X}_{0}$, and ${C{X}}_{{0},{1}}$. To simplify this
process, we note that once a gate has been derived, it may then be used to
derive other gates. This is analogous to how the generator ${X}_{0}$ appears
in the defining relation for ${C{X}}_{{0},{1}}$. Given a set of defining
relations, if the dependencies between the generators defined by the relations
form an acyclic digraph, then the defining relations arise from a valid
sequence of Gen($+$) transformations (see Section B.2). Likewise, the derived
generators can be eliminated by a valid sequence of Tietze transformation. The
defining relations for the remaining $19$ gates are found in Section B.2.
Since the dependencies among these generators are acyclic, then they must
arise from $19$ valid applications of the Gen($+$) rules. Let $R_{D(E8)}$
denote all $23$ relations. Then
$W(E_{8})\cong\langle\Sigma_{E8}\cup\Sigma_{D}\mid R_{E8}\cup
R_{D(E8)}\rangle$.

###  4.2 Deriving the $W(E_{8})$ Coxeter Generators

Recall the circuit definitions for the $W(E_{8})$ generators from Section 4.1.
Let $R_{E8(D)}$ denote the set of corresponding relations. For example, the
relation corresponding to $r_{3}$ is
$r_{3}\approx{X}_{0}\cdot{CC{X}}_{{0},{1}}\cdot{X}_{0}$. Since these relations
hold by definition, then they may be introduced via $8$ applications of
Rel($+$) and consequently $W(E_{8})\cong\langle\Sigma_{E8}\cup\Sigma_{D}\mid
R_{E8}\cup R_{D(E8)}\cup R_{E8(D)}\rangle$.

###  4.3 Elimination of the Coxeter Generators

$\displaystyle\mathbf{r_{1}}\cdot r_{1}$
$\displaystyle\;\rightarrow\;{X}_{0}\cdot{X}_{1}\cdot{CC{X}}_{{0},{1}}\cdot{X}_{1}\cdot{X}_{0}\cdot\mathbf{r_{1}}$
$\displaystyle\;\rightarrow\;{X}_{0}\cdot{X}_{1}\cdot{CC{X}}_{{0},{1}}\cdot{X}_{1}\cdot\mathbf{{X}_{0}\cdot{X}_{0}}\cdot{X}_{1}\cdot{CC{X}}_{{0},{1}}\cdot{X}_{1}\cdot{X}_{0}$
$\displaystyle\;\rightarrow\;{X}_{0}\cdot{X}_{1}\cdot{CC{X}}_{{0},{1}}\cdot\mathbf{{X}_{1}\cdot{X}_{1}}\cdot{CC{X}}_{{0},{1}}\cdot{X}_{1}\cdot{X}_{0}$
$\displaystyle\;\rightarrow\;{X}_{0}\cdot{X}_{1}\cdot\mathbf{{CC{X}}_{{0},{1}}\cdot{CC{X}}_{{0},{1}}}\cdot{X}_{1}\cdot{X}_{0}$
$\displaystyle\;\rightarrow\;{X}_{0}\cdot\mathbf{{X}_{1}\cdot{X}_{1}}\cdot{X}_{0}$
$\displaystyle\;\rightarrow\;\mathbf{{X}_{0}\cdot{X}_{0}}$
$\displaystyle\;\rightarrow\;\epsilon$ (a) Deriving $\epsilon$ from
$r_{1}\cdot r_{1}$.

$\displaystyle\mathbf{{C{X}}_{{0},{1}}}\cdot{X}_{1}$
$\displaystyle\;\rightarrow\;\sigma_{0,1}\cdot{C{X}}_{{1},{0}}\cdot\sigma_{0,1}\cdot\mathbf{{X}_{1}}$
$\displaystyle\;\rightarrow\;\sigma_{0,1}\cdot{C{X}}_{{1},{0}}\cdot\mathbf{\sigma_{0,1}\cdot\sigma_{0,1}}\cdot{X}_{0}\sigma_{0,1}$
$\displaystyle\;\rightarrow\;\sigma_{0,1}\cdot\mathbf{{C{X}}_{{1},{0}}\cdot{X}_{0}}\cdot\sigma_{0,1}$
$\displaystyle\;\rightarrow\;\sigma_{0,1}\cdot{X}_{0}\mathbf{\cdot}{C{X}}_{{1},{0}}\sigma_{0,1}$
$\displaystyle\;\rightarrow\;\mathbf{\sigma_{0,1}\cdot{X}_{0}\cdot\sigma_{0,1}}\cdot\sigma_{0,1}\cdot{C{X}}_{{1},{0}}\cdot\sigma_{0,1}$
$\displaystyle\;\rightarrow\;{X}_{1}\cdot\mathbf{\sigma_{0,1}\cdot{C{X}}_{{1},{0}}\cdot\sigma_{0,1}}$
$\displaystyle\;\rightarrow\;{X}_{1}\cdot{C{X}}_{{0},{1}}$ (b) Deriving
${X}_{1}\cdot{C{X}}_{{0},{1}}$ from ${C{X}}_{{0},{1}}\cdot{X}_{1}$.

Figure 3: Examples of derivations proofs which appear in the proof that
$W(E_{8})\cong\langle\Sigma_{D}\mid R_{0}\rangle$.

In this section, the relations in $R_{E8}$ and $R_{D(E8)}$ are eliminated. To
do this, some additional $(\Sigma_{D})$-relations are required. For the
remainder of this section, let $M_{(x_{0},x_{1},\ldots,x_{k})}$ denote a gate
$M$ applied to the qubits $x_{0}$ through to $x_{k}$. For example, if $M$ is a
doubly-controlled $X$ gate, then $M_{(1,2,0)}$ would correspond to
${CC{X}}_{{1},{2}}$. Using this notation, we introduce the following families
of relations, denoted $R_{D}$.

  * –

Bifunctoriality. $M_{S}\cdot N_{T}=N_{T}\cdot M_{S}$, for all
$M_{S},N_{T}\in\Sigma_{D}$ with $S\cap T=\varnothing$.

  * –

Symmetry. $\sigma_{i,j}\cdot M_{S}\cdot\sigma_{i,j}=M_{\sigma_{i,j}(S)}$, for
all $M_{S}\in\Sigma_{D}$ and integers $0\leq i<j\leq 3$.

  * –

Order. $M\cdot M=\epsilon$, for all $M\in\Sigma_{D}$.

  * –

Commutators. $M_{S}\cdot N_{T}=N_{T}\cdot w$, for all
$M_{S},N_{T}\in\Sigma_{D}$ with $S\cap T\neq\varnothing$ and
$w\in(\Sigma_{D})^{*}$ minimal.

The relation $\sigma_{1,2}\,\approx\,{C{Z}}_{{1},{2}}\cdot
K_{1,2}\cdot{C{Z}}_{{1},{2}}\cdot K_{1,2}\cdot{C{Z}}_{{1},{2}}\cdot K_{1,2}$
from [8] is also included for simplicity. From these relations, all elements
of $R_{D(E8)}$ and $R_{E8}$ can be derived. Since all elements of
$\Sigma_{E8}$ are self-inverse, then it suffices to consider only the upper
half of the Coxeter matrix for $W(E_{8})$. As an example, consider the
relation $r_{1}\cdot r_{1}\approx\epsilon$ in $R_{E8}$. The proof proceeds as
in Figure 3(a). Then $\epsilon$ can be derived from $r_{1}\cdot r_{1}$ using
the relations in $R_{D}$. Similar methods can be used to eliminate the
remaining $(R_{E8})$-relations. All derivations, for both $R_{D(E8)}$ and
$R_{E8}$ can be found in the supplement to this paper [6].

######  Theorem 4.1.

$W(E_{8})\cong\langle\Sigma_{D}\mid R_{D}\rangle$

It follows immediately from Theorem 4.1 that given any circuit $C$ over
$\Sigma_{D}$, there exists a minimal word $w$ over the alphabet
$\\{r_{1},r_{2},\ldots,r_{8}\\}$ such
$[\\![C]\\!]_{D}^{*}=[\\![w]\\!]_{E8}^{*}$. Then by the decompositions of
Section 4.1, there exists a circuit $C^{\prime}$ over $\Sigma_{D}$ such that
$[\\![w]\\!]_{E8}^{*}=[\\![C^{\prime}]\\!]_{D}^{*}$ such that $C^{\prime}$
contains exactly $|w|$ Toffoli gates. By [17, Thm. 1.8], every minimal word in
$W(E_{8})$ has length at most $n$, where $n$ is the cardinality of the
positive root system associated with $W(E_{8})$. By [17], the positive root
system associated with $W(E_{8})$ has cardinality $120$. Therefore,
$C^{\prime}$ contains at most $120$ Toffoli gates. This provides an upper-
bound on the Toffoli count for circuits over $\Sigma_{D}$, which can be
thought of as a measure of computational complexity for these three-qubit
circuits.

######  Corollary 4.2.

If $C\in\Sigma_{D}^{*}$, then there exists $C^{\prime}\in\Sigma_{D}$ with
Toffoli count at most $120$ such that
$[\\![C]\\!]_{D}^{*}=[\\![C^{\prime}]\\!]_{D}^{*}$.

###  4.4 A Reduced Set of Relations for $W(E_{8})$

$\displaystyle{C{Z}}_{{0},{1}}$
$\displaystyle\,\approx\,K_{1,2}\cdot{C{X}}_{{0},{1}}\cdot K_{1,2}$ (1)
$\displaystyle{X}_{1}$
$\displaystyle\,\approx\,{C{X}}_{{0},{1}}\cdot{X}_{0}\cdot{C{X}}_{{0},{1}}\cdot{X}_{0}$
(2) $\displaystyle{Z}_{0}$
$\displaystyle\,\approx\,{C{Z}}_{{0},{1}}\cdot{C{X}}_{{0},{1}}\cdot{C{Z}}_{{0},{1}}\cdot{C{X}}_{{0},{1}}$
(3) $\displaystyle{Z}_{1}$ $\displaystyle\,\approx\,K_{1,2}\cdot{X}_{1}\cdot
K_{1,2}$ (4) $\displaystyle{C{X}}_{{2},{0}}$
$\displaystyle\,\approx\,{X}_{1}\cdot{CC{X}}_{{1},{2}}\cdot{X}_{1}\cdot{CC{X}}_{{1},{2}}$
(5) $\displaystyle{C{X}}_{{2},{1}}$
$\displaystyle\,\approx\,{C{X}}_{{2},{0}}\cdot{C{X}}_{{0},{1}}\cdot{C{X}}_{{2},{0}}\cdot{C{X}}_{{0},{1}}$
(6) $\displaystyle{C{X}}_{{1},{2}}$
$\displaystyle\,\approx\,K_{1,2}\cdot{C{X}}_{{2},{1}}\cdot K_{1,2}$ (7)
$\displaystyle\sigma_{1,2}$
$\displaystyle\,\approx\,{C{X}}_{{1},{2}}\cdot{C{X}}_{{2},{1}}\cdot{C{X}}_{{1},{2}}$
(8) $\displaystyle{C{X}}_{{0},{2}}$
$\displaystyle\,\approx\,\sigma_{1,2}\cdot{C{X}}_{{0},{1}}\cdot\sigma_{1,2}$
(9) $\displaystyle\sigma_{0,2}$
$\displaystyle\,\approx\,{C{X}}_{{0},{2}}\cdot{C{X}}_{{2},{0}}\cdot{C{X}}_{{0},{2}}$
(10) $\displaystyle K_{0,1}$ $\displaystyle\,\approx\,\sigma_{0,2}\cdot
K_{1,2}\cdot\sigma_{0,2}$ (11) $\displaystyle{C{X}}_{{1},{0}}$
$\displaystyle\,\approx\,K_{0,1}\cdot{C{X}}_{{0},{1}}\cdot K_{0,1}$ (12)
$\displaystyle\sigma_{0,1}$
$\displaystyle\,\approx\,{C{X}}_{{0},{1}}\cdot{C{X}}_{{1},{0}}\cdot{C{X}}_{{0},{1}}$
(13) $\displaystyle{CC{X}}_{{0},{2}}$
$\displaystyle\,\approx\,\sigma_{0,1}\cdot{CC{X}}_{{1},{2}}\cdot\sigma_{0,1}$
(14) $\displaystyle{X}_{2}$
$\displaystyle\,\approx\,\sigma_{0,2}\cdot{X}_{0}\cdot\sigma_{0,2}$ (15)
$\displaystyle{Z}_{2}$
$\displaystyle\,\approx\,\sigma_{0,2}\cdot{Z}_{0}\cdot\sigma_{0,2}$ (16)
$\displaystyle{CC{X}}_{{0},{1}}$
$\displaystyle\,\approx\,K_{1,2}\cdot{CC{X}}_{{0},{2}}\cdot K_{1,2}$ (17)
$\displaystyle{C{Z}}_{{0},{2}}$
$\displaystyle\,\approx\,\sigma_{1,2}\cdot{C{Z}}_{{0},{1}}\cdot\sigma_{1,2}$
(18) $\displaystyle{C{Z}}_{{1},{2}}$
$\displaystyle\,\approx\,\sigma_{0,1}\cdot{C{Z}}_{{0},{2}}\cdot\sigma_{0,1}$
(19) $\displaystyle\sigma_{1,2}$
$\displaystyle\,\approx\,{C{Z}}_{{1},{2}}\cdot
K_{1,2}\cdot{C{Z}}_{{1},{2}}\cdot K_{1,2}\cdot{C{Z}}_{{1},{2}}\cdot K_{1,2}$
(20) $\displaystyle{X}_{0}\cdot{X}_{0}$ $\displaystyle\,\approx\,\epsilon$
(21) $\displaystyle{C{X}}_{{0},{1}}\cdot{C{X}}_{{0},{1}}$
$\displaystyle\,\approx\,\epsilon$ (22) $\displaystyle K_{1,2}\cdot K_{1,2}$
$\displaystyle\,\approx\,\epsilon$ (23)

$\displaystyle{CC{X}}_{{1},{2}}\cdot{CC{X}}_{{1},{2}}$
$\displaystyle\,\approx\,\epsilon$ (24) $\displaystyle K_{0,1}\cdot K_{0,1}$
$\displaystyle\,\approx\,\epsilon$ (25)
$\displaystyle{C{X}}_{{1},{2}}\cdot{X}_{0}$
$\displaystyle\,\approx\,{X}_{0}\cdot{C{X}}_{{1},{2}}$ (26)
$\displaystyle{X}_{0}\cdot K_{1,2}$
$\displaystyle\,\approx\,K_{1,2}\cdot{X}_{0}$ (27) $\displaystyle{X}_{1}$
$\displaystyle\,\approx\,\sigma_{0,1}\cdot{X}_{0}\cdot\sigma_{0,1}$ (28)
$\displaystyle{C{X}}_{{2},{0}}$
$\displaystyle\,\approx\,\sigma_{0,2}\cdot{C{X}}_{{0},{2}}\cdot\sigma_{0,2}$
(29) $\displaystyle{C{X}}_{{1},{2}}$
$\displaystyle\,\approx\,\sigma_{0,1}\cdot{C{X}}_{{0},{2}}\cdot\sigma_{0,1}$
(30) $\displaystyle{C{X}}_{{2},{1}}$
$\displaystyle\,\approx\,\sigma_{0,1}\cdot{C{X}}_{{2},{0}}\cdot\sigma_{0,1}$
(31) $\displaystyle{CC{X}}_{{0},{1}}$
$\displaystyle\,\approx\,\sigma_{0,2}\cdot{CC{X}}_{{1},{2}}\cdot\sigma_{0,2}$
(32) $\displaystyle{CC{X}}_{{0},{1}}$
$\displaystyle\,\approx\,\sigma_{1,2}\cdot{CC{X}}_{{0},{2}}\cdot\sigma_{0,2}$
(33) $\displaystyle{Z}_{1}$
$\displaystyle\,\approx\,\sigma_{0,1}\cdot{Z}_{0}\cdot\sigma_{0,1}$ (34)
$\displaystyle K_{0,1}$ $\displaystyle\,\approx\,\sigma_{0,1}\cdot
K_{0,1}\cdot\sigma_{0,1}$ (35)
$\displaystyle{CC{X}}_{{1},{2}}\cdot{C{X}}_{{1},{0}}$
$\displaystyle\,\approx\,{C{X}}_{{1},{0}}\cdot{CC{X}}_{{1},{2}}$ (36)
$\displaystyle{X}_{0}\cdot{CC{X}}_{{1},{2}}$
$\displaystyle\,\approx\,{CC{X}}_{{1},{2}}\cdot{X}_{0}$ (37)
$\displaystyle{X}_{0}\cdot{C{X}}_{{1},{0}}$
$\displaystyle\,\approx\,{C{X}}_{{1},{0}}\cdot{X}_{0}$ (38) $\displaystyle
K_{0,1}\cdot K_{1,2}$ $\displaystyle\,\approx\,K_{1,2}\cdot K_{0,1}$ (39)
$\displaystyle{C{Z}}_{{0},{1}}\cdot{C{Z}}_{{1},{2}}$
$\displaystyle\,\approx\,{C{Z}}_{{1},{2}}\cdot{C{Z}}_{{0},{1}}$ (40)
$\displaystyle K_{0,1}\cdot{Z}_{0}$ $\displaystyle\,\approx\,{X}_{0}\cdot
K_{0,1}$ (41) $\displaystyle{X}_{0}\cdot{CC{X}}_{{0},{1}}$
$\displaystyle\,\approx\,{CC{X}}_{{0},{1}}\cdot{C{X}}_{{1},{2}}\cdot{X}_{0}$
(42) $\displaystyle{C{X}}_{{0},{1}}\cdot{C{Z}}_{{1},{2}}$
$\displaystyle\,\approx\,{C{Z}}_{{1},{2}}\cdot{C{Z}}_{{0},{2}}\cdot{C{X}}_{{0},{1}}$
(43) $\displaystyle{C{X}}_{{1},{2}}\cdot{CC{X}}_{{1},{2}}$
$\displaystyle\,\approx\,{CC{X}}_{{1},{2}}\cdot{C{X}}_{{1},{0}}\cdot{C{X}}_{{1},{2}}$
(44) $\displaystyle{CC{X}}_{{1},{2}}\cdot{C{X}}_{{0},{1}}$
$\displaystyle\,\approx\,{C{X}}_{{0},{1}}\cdot{CC{X}}_{{0},{2}}\cdot{CC{X}}_{{1},{2}}\cdot{CC{X}}_{{0},{2}}$
(45) $\displaystyle{CC{X}}_{{0},{1}}\cdot{CC{X}}_{{0},{2}}$
$\displaystyle\,\approx\,{CC{X}}_{{0},{2}}\cdot{CC{X}}_{{0},{1}}\cdot{CC{X}}_{{0},{2}}\cdot{CC{X}}_{{0},{1}}$
(46)

Figure 4: Relations for $W(E_{8})$, denoted $R_{0}$.

The relations $R_{D}$ from Section 4.3 are far from minimal. For example, the
family of commutator relations contains all relations of the form
${C{X}}_{{j},{k}}\cdot{X}_{k}\approx{X}_{k}\cdot{C{X}}_{{j},{k}}$. However,
given all symmetry relations, it suffices to include only
${C{X}}_{{1},{0}}\cdot{X}_{0}\approx{X}_{0}\cdot{C{X}}_{{1},{0}}$. The
remaining commutator relations can be derived, as illustrated in Figure 3(b).
Furthermore, many of the relations in $R_{D}$ do not appear in any derivations
of the supplement. For example, the relation
${C{X}}_{{2},{0}}\cdot{X}_{0}\approx{X}_{0}\cdot{C{X}}_{{2},{0}}$ does not
appear, and therefore Theorem 4.1 holds with respect to the relation set
$R_{D}\setminus\\{{C{X}}_{{2},{0}}\cdot{X}_{0}\approx{X}_{0}\cdot{C{X}}_{{2},{0}}\\}$.
Using both techniques, a new relation set $R_{0}$ is obtained, as illustrated
in Figure 4. All derivations can be found in the supplement to this paper [6].

######  Corollary 4.3.

$W(E_{8})\cong\langle\Sigma_{D}\mid R_{0}\rangle$

###  4.5 A Minimal Generating Set for $W(E_{8})$

Define
$\Sigma_{0}=\left\\{{X}_{0},{C{X}}_{{0},{1}},{CC{X}}_{{1},{2}},K_{1,2}\right\\}$.
From Section 4.1, it is clear that $\Sigma_{0}$ generates $W(E_{8})$. In fact,
$\Sigma_{0}$ is minimal in the sense that every proper subset of $\Sigma_{0}$
generates a proper subgroup of $W(E_{8})$. In other words, no proper subset of
$\Sigma_{0}$ generates $W(E_{8})$. To show that $\Sigma_{0}$ is a minimal
generating set for $W(E_{8})$, it suffices to show that for every maximal
proper subset $\Sigma^{\prime}$ of $\Sigma_{0}$, there exists some $8\times 8$
dyadic matrix $M$ such that $M$ commutes with the elements of
$\Sigma^{\prime}$ but does not commute with the elements of $\Sigma_{0}$.
Intuitively, the subgroup generated by $\Sigma^{\prime}$ commutes with $M$,
whereas the subgroup generated by $\Sigma_{0}$ does not commute with $M$. This
claim is proven in Appendix E, and the matrices are constructed.

######  Theorem 4.4.

$\Sigma_{0}$ is a minimal generating set for $W(E_{8})$.

##  5 Extending to a Presentation of $\mathrm{O}(8,\mathbb{D})$

$\displaystyle{X}{}_{[a,b]}{}^{2}$ $\displaystyle\,\approx\,\epsilon$ (47)
$\displaystyle{(-1)}{}_{[a]}{}^{2}$ $\displaystyle\,\approx\,\epsilon$ (48)
$\displaystyle{K}{}_{[a,b,c,d]}{}^{2}$ $\displaystyle\,\approx\,\epsilon$ (49)
$\displaystyle{X}{}_{[a,b]}\cdot{X}{}_{[c,d]}$
$\displaystyle\,\approx\,{X}{}_{[c,d]}\cdot{X}{}_{[a,b]}$ (50)
$\displaystyle{X}{}_{[a,b]}\cdot{(-1)}{}_{[c]}$
$\displaystyle\,\approx\,{(-1)}{}_{[c]}\cdot{X}{}_{[a,b]}$ (51)
$\displaystyle{X}{}_{[a,b]}\cdot{K}{}_{[c,d,e,f]}$
$\displaystyle\,\approx\,{K}{}_{[c,d,e,f]}\cdot{X}{}_{[a,b]}$ (52)
$\displaystyle{(-1)}{}_{[a]}\cdot{K}{}_{[b,c,d,e]}$
$\displaystyle\,\approx\,{K}{}_{[b,c,d,e]}\cdot{(-1)}{}_{[a]}$ (53)
$\displaystyle{(-1)}{}_{[a]}\cdot{(-1)}{}_{[b]}$
$\displaystyle\,\approx\,{(-1)}{}_{[b]}\cdot{(-1)}{}_{[a]}$ (54)
$\displaystyle{K}{}_{[a,b,c,d]}\cdot{K}{}_{[e,f,g,h]}$
$\displaystyle\,\approx\,{K}{}_{[e,f,g,h]}\cdot{K}{}_{[a,b,c,d]}$ (55)
$\displaystyle{X}{}_{[a,c]}\cdot{X}{}_{[a,b]}$
$\displaystyle\,\approx\,{X}{}_{[c,b]}\cdot{X}{}_{[a,c]}$ (56)

$\displaystyle{X}{}_{[b,c]}\cdot{X}{}_{[a,b]}$
$\displaystyle\,\approx\,{X}{}_{[a,c]}\cdot{X}{}_{[b,c]}$ (57)
$\displaystyle{X}{}_{[a,b]}\cdot{(-1)}{}_{[a]}$
$\displaystyle\,\approx\,{(-1)}{}_{[b]}\cdot{X}{}_{[a,b]}$ (58)
$\displaystyle{X}{}_{[a,e]}\cdot{K}{}_{[a,b,c,d]}$
$\displaystyle\,\approx\,{K}{}_{[e,b,c,d]}\cdot{X}{}_{[a,e]}$ (59)
$\displaystyle{X}{}_{[b,e]}\cdot{K}{}_{[a,b,c,d]}$
$\displaystyle\,\approx\,{K}{}_{[a,e,c,d]}\cdot{X}{}_{[b,e]}$ (60)
$\displaystyle{X}{}_{[c,e]}\cdot{K}{}_{[a,b,c,d]}$
$\displaystyle\,\approx\,{K}{}_{[a,b,e,d]}\cdot{X}{}_{[c,e]}$ (61)
$\displaystyle{X}{}_{[d,e]}\cdot{K}{}_{[a,b,c,d]}$
$\displaystyle\,\approx\,{K}{}_{[a,b,c,e]}\cdot{X}{}_{[d,e]}$ (62)
$\displaystyle{X}{}_{[a,b]}\cdot{K}{}_{[a,b,c,d]}$
$\displaystyle\,\approx\,{K}{}_{[a,b,c,d]}\cdot{X}{}_{[a,b]}\cdot{(-1)}{}_{[b]}\cdot{(-1)}{}_{[d]}$
(63) $\displaystyle{X}{}_{[b,c]}\cdot{K}{}_{[a,b,c,d]}$
$\displaystyle\,\approx\,{(-1)}{}_{[a]}\cdot{K}{}_{[a,b,c,d]}\cdot{(-1)}{}_{[a]}\cdot{K}{}_{[a,b,c,d]}\cdot{(-1)}{}_{[a]}$
(64) $\displaystyle{X}{}_{[c,d]}\cdot{K}{}_{[a,b,c,d]}$
$\displaystyle\,\approx\,{K}{}_{[a,b,c,d]}\cdot{X}{}_{[b,d]}$ (65)
$\displaystyle{K}{}_{[a,b,c,d]}\cdot{K}{}_{[b,d,e,f]}$
$\displaystyle\,\approx\,{K}{}_{[b,d,e,f]}\cdot{K}{}_{[a,b,c,d]}$ (66)
$\displaystyle{(-1)}{}_{[a]}\cdot{(-1)}{}_{[e]}\cdot{X}{}_{[a,e]}\cdot\rho_{a,b,c,d,e,f,g,h}$
$\displaystyle\,\approx\,\rho_{a,b,c,d,e,f,g,h}\cdot{X}{}_{[a,e]}\cdot{(-1)}{}_{[e]}\cdot{(-1)}{}_{[a]}$
(67)

Figure 5: The relations in $\mathcal{R}_{n}$ from [19], for all valid choices
of $a,b,c,d,e,f,g,h\in\mathbb{Z}$. We write $\rho_{a,b,c,d,e,f,g,h}$ for the
substring
${K}{}_{[e,f,g,h]}\cdot{K}{}_{[a,b,c,d]}\cdot{X}{}_{[d,e]}\cdot{K}{}_{[a,b,c,d]}\cdot{K}{}_{[e,f,g,h]}$.

Li et al. [19] introduced a presentation for $\mathrm{O}(8,\mathbb{D})$ using
$m$-level operators. Let $n>0$, $I$ be the $n\times n$ identity matrix, and
$[m]=\\{0,1,\ldots,m-1\\}$. Then given an $m\times m$ matrix $M$ with $m<n$,
and a strictly increasing sequence $(a_{0},\ldots,a_{m-1})$ over $[m]$, define
${M}{}_{[a_{0},\ldots,a_{m-1}]}$ to be the $n\times n$ matrix such that:

  1. 1.

For each pair of elements $(j,k)$ over $[m]$, the component $(a_{j},a_{k})$ of
${M}{}_{[a_{0},\ldots,a_{m-1}]}$ is equal to the component $(a_{j},a_{k})$ of
$M$;

  2. 2.

For each pair of elements $(j,k)$ over
$[n]\setminus\\{a_{0},a_{1},\ldots,a_{m}\\}$, the component $(j,k)$ of
${M}{}_{[a_{0},a_{1},\ldots,a_{m-1}]}$ is equal to the component
$(a_{j},a_{k})$ of $I$.

We say that ${M}{}_{[a_{0},\ldots,a_{m-1}]}$ is an _$m$ -level operator of
type $M$_. When $n=8$ for example, ${CC{X}}_{{0},{1}}={X}{}_{[6,7]}$,
${CC{Z}}_{{0},{1}}={(-1)}{}_{[7]}$, and ${K}{}_{[4,5,6,7]}$ is a controlled
$K$-gate. Define the following for $n>3$.

$\mathcal{G}_{n}=\left\\{{(-1)}{}_{[a]},{X}{}_{[a,b]},{K}{}_{[a,b,c,d]}\mid
a,b,c,d\in\mathbb{Z}\text{ and }0\leq a<b<c<d<n\right\\}$

It was shown in [19] that
$\mathrm{O}(n,\mathbb{D})\cong\langle\mathcal{G}_{n}\mid\mathcal{R}_{n}\rangle$,
where $\mathcal{R}_{n}$ is given in Figure 5. The goal of this section is to
construct a sequence of Tietze transformations, starting from
$\langle\mathcal{G}_{8}\mid\mathcal{R}_{8}\rangle$, such that the generators
and relations describing the subgroup $W(E_{8})$ are replaced by $\Sigma_{D}$
and $R_{0}$, respectively. This process follows similarly to Section 4.
However, one should note that $|\mathcal{R}_{8}|=2113$ (see Section F.1).
Inspection of $\mathcal{R}_{n}$ reveals that many of these relations are
either definitional, or obtained through permutations of indices. For this
reason, $\mathcal{R}_{n}$ is partially reduced before carrying out the
aforementioned Tietze transformations. First, the permutations are eliminated
via a sequence of Rel($-$) transformations to obtain $\mathcal{R}_{n}^{1}$.
Next, some redundant commutator relations are eliminated via a sequence of
Rel($-$) transformations to obtain $\mathcal{R}_{n}^{2}$. Finally, the derived
generators are eliminated to obtain $\mathcal{R}_{n}^{3}$. All proofs can be
found in Appendix F.

###  5.1 Permutation Groups and Reindexing

Let $[n]=\\{0,1,\ldots,n-1\\}$ and $\mathrm{S}(n)$ denote the group of
permutations on $[n]$. For $j,k\in[n]$, let $\tau_{j,k}$ denote the
permutation that swaps $j$ and $k$. For example, $\tau_{0,1}(0)=1$,
$\tau_{0,1}(1)=0$, and $\tau_{0,1}(2)=2$. The group $\mathrm{S}(n)$ is a
finite reflection group generated by the _transpositions_ $\\{\tau_{j,j+1}\mid
j\in[n]\\}$ (see [17]). The _braiding relations_ , which state that
$\tau_{j,j+1}\circ\tau_{j+1,j+2}\circ\tau_{j,j+1}=\tau_{j+1,j+2}\circ\tau_{j,j+1}\circ\tau_{j+1,j+2}$
for all $j\in[n-2]$, together with the order relations are sound and complete
for $\mathrm{S}(n)$ (see [18]). The standard representation of $\mathrm{S}(n)$
as a reflection group sends each $\tau_{j,k}$ to $X_{[j,k]}$. This means that
every two-level operator of type $X$ can be decomposed into sequence of
transpositions. Intuitively, each $X_{[j,k]}$ acts by permuting the standard
basis vectors $\ket{j}$ and $\ket{k}$, which can be achieved through a
sequence of transpositions of basis vectors. Clearly,
$\mathrm{S}(8)\hookrightarrow W(E_{8})\leq O(8,\mathbb{D})$.

Many relations in $\mathcal{R}_{n}$ are related via permutation of indices.
The _formal application of $\sigma$_ to a word over $\mathcal{G}_{n}$ is
defined inductively as follows.

$\displaystyle\sigma(\epsilon)$ $\displaystyle=\epsilon$
$\displaystyle\sigma({X}{}_{[a,b]}\cdot w)$
$\displaystyle={X}{}_{[\sigma(a),\sigma(b)]}\cdot\sigma(w)$
$\displaystyle\sigma({(-1)}{}_{[a]}\cdot w)$
$\displaystyle={(-1)}{}_{[\sigma(a)]}\cdot\sigma(w)$
$\displaystyle\sigma({K}{}_{[a,b,c,d]}\cdot w)$
$\displaystyle={K}{}_{[\sigma(a),\sigma(b),\sigma(c),\sigma(d)]}\cdot\sigma(w)$

Note that $\sigma(w)$ may yield $m$-level operators with invalid indices. For
example, $\tau_{1,2}({X}{}_{[1,2]})$ yields ${X}{}_{[2,1]}$, which is not a
valid two-level operator since $2>1$. The permutation $\sigma$ is a _valid
reindexing for $w$_ if all symbols in $\sigma(w)$ are well-formed multi-level
operators. If $\sigma$ is valid for $v$ and $w$, then $\sigma$ is valid for
$v\cdot w$. Conversely, if $\sigma$ is valid for $w$, then $\sigma$ is valid
for all subwords in $w$. Consider, for example, the word
$w={K}{}_{[2,3,4,5]}\cdot{K}{}_{[3,5,6,7]}$ which appears on the left-hand
side of an instance of Relation 55. Let $\sigma\in\mathrm{S}(8)$ be the cyclic
permutation $7\mapsto 5\mapsto 3\mapsto 1\mapsto 6\mapsto 4\mapsto 2\mapsto
0\mapsto 7$. Then $\sigma$ is a valid reindexing for $w$ since
$\sigma(w)={K}{}_{[0,1,2,5]}\cdot{K}{}_{[1,3,4,5]}$. In Section F.2, we show
that all valid reindexings are derivable using only the relations in
$\mathcal{R}_{\sigma}=\\{\text{\lx@cref{creftypeplural~refnum}{Eq:O8DRels:Orig:Perm1},
\lx@cref{refnum}{Eq:O8DRels:Orig:Perm3},
\lx@cref{refnum}{Eq:O8DRels:Orig:Perm4},
\lx@cref{refnum}{Eq:O8DRels:Orig:Perm5},
\lx@cref{refnum}{Eq:O8DRels:Orig:Perm6},
\lx@cref{refnum}{Eq:O8DRels:Orig:Perm7},
\lx@cref{refnum}{Eq:O8DRels:Orig:Perm8},
\lx@cref{refnum}{Eq:O8DRels:Orig:Perm9},
\lx@cref{refnum}{Eq:O8DRels:Orig:Perm10}
and~\lx@cref{refnum}{Eq:O8DRels:Orig:Perm11}}\\}$.

###  5.2 Selecting Representative Relations for $\mathrm{O}(n,\mathbb{D})$

As a consequence of Section 5.1, many relations in $\mathcal{R}_{n}$ can be
replaced by representative instances. For example, let $r$ denote instance
${(-1)}{}_{[6]}\cdot{(-1)}{}_{[7]}\approx{(-1)}{}_{[7]}\cdot{(-1)}{}_{[6]}$ of
Relation 54. Clearly $\sigma=\tau_{0,6}\circ\tau_{1,7}$ is a valid reindexing
for $r$, where $\sigma(r)$ is
${(-1)}{}_{[0]}\cdot{(-1)}{}_{[1]}\approx{(-1)}{}_{[1]}\cdot{(-1)}{}_{[0]}$
Then by Section F.2, it is possible to derive $\sigma(r)$ from $r$ using
$\mathcal{R}_{n}\setminus\\{\sigma(r)\\}$. Then
$\langle\mathcal{G}_{n}\mid\mathcal{R}_{n}\rangle\cong\langle\mathcal{G}_{n}\mid\mathcal{R}_{n}\setminus\\{\sigma(r)\\}\rangle$
by Rel($-$).

This process can be repeated, until all instances of Relation 54 have been
eliminated, except for the representative relation $r$. In a similar fashion,
Relations 48, 49, 53, 55, 63, 64, 65, 66 and 67 can be eliminated, since these
relations do not appear in $\mathcal{R}_{\sigma}$. Then
$\mathrm{O}(n,\mathbb{D})\cong\langle\mathcal{G}_{n}\mid\mathcal{R}_{n}^{1}\rangle$
where $\mathcal{R}_{n}^{1}$ is the set of representative relations (see
Section F.3).

###  5.3 Selecting Representative Generators for $\mathrm{O}(n,\mathbb{D})$

Define the new generator set,

$\mathcal{G}_{n}^{1}=\left\\{{X}{}_{[a,b]},\mid a,b,\in\mathbb{Z}\text{ and
}0\leq
a<b<n\right\\}\cup\left\\{{K}{}_{[0,1,2,3]}\right\\}\cup\left\\{{(-1)}{}_{[0]}\right\\}.$

Many of the generators in $\mathcal{G}_{n}$ are redundant in the sense that
they may be constructed using only the generators in $\mathcal{G}_{n}^{1}$.
This is because $\mathrm{S}(n)\hookrightarrow\mathcal{G}_{n}^{1}$, with
$\mathcal{G}_{n}^{1}\setminus\mathcal{G}_{n}$ consisting of valid indexings of
either ${K}{}_{[0,1,2,3]}$ or ${(-1)}{}_{[0]}$. Furthermore, these reindexings
follow from relations in $\mathcal{R}_{n}^{1}$. As an example, consider the
instance
${X}{}_{[0,7]}\cdot{(-1)}{}_{[0]}\approx{(-1)}{}_{[7]}\cdot{X}{}_{[0,7]}$ of
Relation 58. Using the order relation for ${X}{}_{[0,7]}$, the following
derivation holds.

${(-1)}{}_{[7]}\;\leftarrow\;{(-1)}{}_{[7]}\cdot{X}{}_{[0,7]}{}^{2}\;\leftarrow\;{X}{}_{[0,7]}\cdot{(-1)}{}_{[0]}\cdot{X}{}_{[0,7]}$

Similarly, the original relation can be obtained from this new relation using
the order relation for ${X}{}_{[0,7]}$. Then through a Rel($+$) transformation
followed by a Rel($-$) transformation, the commutator relation
${X}{}_{[0,7]}\cdot{(-1)}{}_{[0]}\approx{(-1)}{}_{[7]}\cdot{X}{}_{[0,7]}$ can
be replaced by the definitional relation
${(-1)}{}_{[7]}={X}{}_{[0,7]}\cdot{(-1)}{}_{[0]}\cdot{X}{}_{[0,7]}$. This
process can be repeated for all instances of Relation 58.

To derive the four-level operators of type $K$, it suffices to note that the
following family of relations are valid with respect to
$[\\![\cdot]\\!]_{O}^{*}$.

${K}{}_{[a,b,c,d]}\approx{X}{}_{[0,a]}\cdot{X}{}_{[1,b]}\cdot{X}{}_{[2,c]}\cdot{X}{}_{[3,d]}\cdot{K}{}_{[0,1,2,3]}\cdot{X}{}_{[3,d]}\cdot{X}{}_{[2,c]}\cdot{X}{}_{[1,b]}\cdot{X}{}_{[0,a]}$

The cases where $\\{a,b,c,d\\}\cap\\{0,1,2,3\\}\neq\varnothing$ can be handled
using the techniques of Section F.2. These relations are introduced using a
sequence of Rel($+$) relations to obtain a new relation set $R$. In this
relation set, all multi-level operators of type $(-1)$ and $K$ are defined in
terms of ${(-1)}{}_{[0]}$ and ${K}{}_{[0,1,2,3]}$, respectively. As outlined
in Section B.2, these defining relations can be used to eliminate all
generators in $\mathcal{G}_{n}^{1}\setminus\mathcal{R}_{n}^{0}$ via a finite
sequence of Tietze transformations.

The elimination process works as follows. Let
$M\in\mathcal{G}_{n}^{1}\setminus\mathcal{G}_{n}$. Then $M$ appears in some
defining relation $M\approx w$. If $M$ appears in some relation $r\in R$, then
every instance of $M$ will be replaced by $w$. For example, Relation 54 will
be replaced by the following relation.

${(-1)}{}_{[0]}\cdot{X}{}_{[0,5]}\cdot{(-1)}{}_{[0]}\cdot{X}{}_{[0,5]}\approx{X}{}_{[0,5]}\cdot{(-1)}{}_{[0]}\cdot{X}{}_{[0,5]}\cdot{(-1)}{}_{[0]}$

We introduce the following abbreviations for simplicity of presentation.

$\displaystyle{(-1)}{}_{[c]}$
$\displaystyle={X}{}_{[0,c]}\cdot{(-1)}{}_{[0]}\cdot{X}{}_{[0,c]}$
$\displaystyle{K}{}_{[0,1,2,d]}$
$\displaystyle={X}{}_{[3,d]}\cdot{K}{}_{[0,1,2,3]}\cdot{X}{}_{[3,d]}$
$\displaystyle{K}{}_{[0,1,c,d]}$
$\displaystyle={X}{}_{[2,c]}\cdot{K}{}_{[0,1,2,d]}\cdot{X}{}_{[2,c]}$
$\displaystyle{K}{}_{[0,b,c,d]}$
$\displaystyle={X}{}_{[1,b]}\cdot{K}{}_{[0,1,c,d]}\cdot{X}{}_{[1,b]}$
$\displaystyle{K}{}_{[a,b,c,d]}$
$\displaystyle={X}{}_{[0,a]}\cdot{K}{}_{[0,b,c,d]}\cdot{X}{}_{[0,a]}$

Denote this new set of relations $\mathcal{R}_{n}^{2}$. Then
$\mathrm{O}(n,\mathbb{D})\cong\langle\mathcal{G}_{n}^{1}\mid\mathcal{R}_{n}^{2}\rangle$.

###  5.4 Eliminating Redundant Relations

$\displaystyle{X}{}_{[a,a+1]}{}^{2}$ $\displaystyle\,\approx\,\epsilon$ (68)
$\displaystyle{(-1)}{}_{[0]}{}^{2}$ $\displaystyle\,\approx\,\epsilon$ (69)
$\displaystyle{K}{}_{[0,1,2,3]}{}^{2}$ $\displaystyle\,\approx\,\epsilon$ (70)
$\displaystyle{X}{}_{[b,b+1]}\cdot{(-1)}{}_{[0]}$
$\displaystyle\,\approx\,{(-1)}{}_{[0]}\cdot{X}{}_{[b,b+1]}$ (71)
$\displaystyle{X}{}_{[c,c+1]}\cdot{K}{}_{[0,1,2,3]}$
$\displaystyle\,\approx\,{K}{}_{[0,1,2,3]}\cdot{X}{}_{[c,c+1]}$ (72)
$\displaystyle{(-1)}{}_{[4]}\cdot{K}{}_{[0,1,2,3]}$
$\displaystyle\,\approx\,{K}{}_{[0,1,2,3]}\cdot{(-1)}{}_{[4]}$ (73)
$\displaystyle{(-1)}{}_{[0]}\cdot{(-1)}{}_{[4]}$
$\displaystyle\,\approx\,{(-1)}{}_{[4]}\cdot{(-1)}{}_{[0]}$ (74)

$\displaystyle{K}{}_{[0,1,2,3]}\cdot{K}{}_{[4,5,6,7]}$
$\displaystyle\,\approx\,{K}{}_{[4,5,6,7]}\cdot{K}{}_{[0,1,2,3]}$ (75)
$\displaystyle{X}{}_{[a,a+1]}\cdot{X}{}_{[a,a+2]}$
$\displaystyle\,\approx\,{X}{}_{[a+1,a+2]}\cdot{X}{}_{[a,a+1]}$ (76)
$\displaystyle{X}{}_{[a+1,b]}\cdot{X}{}_{[a,a+1]}$
$\displaystyle\,\approx\,{X}{}_{[a,b]}\cdot{X}{}_{[a+1,b]}$ (77)
$\displaystyle{X}{}_{[0,1]}\cdot{K}{}_{[0,1,2,3]}$
$\displaystyle\,\approx\,{K}{}_{[0,1,2,3]}\cdot{X}{}_{[0,1]}\cdot{(-1)}{}_{[1]}\cdot{(-1)}{}_{[3]}$
(78) $\displaystyle{X}{}_{[1,2]}\cdot{K}{}_{[0,1,2,3]}$
$\displaystyle\,\approx\,{(-1)}{}_{[0]}\cdot{K}{}_{[0,1,2,3]}\cdot{(-1)}{}_{[0]}\cdot{K}{}_{[0,1,2,3]}\cdot{(-1)}{}_{[0]}$
(79) $\displaystyle{X}{}_{[2,3]}\cdot{K}{}_{[0,1,2,3]}$
$\displaystyle\,\approx\,{K}{}_{[0,1,2,3]}\cdot{X}{}_{[1,3]}$ (80)
$\displaystyle{K}{}_{[0,1,2,3]}\cdot{K}{}_{[1,3,4,5]}$
$\displaystyle\,\approx\,{K}{}_{[1,3,4,5]}\cdot{K}{}_{[0,1,2,3]}$ (81)
$\displaystyle{(-1)}{}_{[0]}\cdot{(-1)}{}_{[4]}\cdot{X}{}_{[0,4]}\cdot\rho$
$\displaystyle\,\approx\,\rho\cdot{X}{}_{[0,4]}\cdot{(-1)}{}_{[4]}\cdot{(-1)}{}_{[0]}$
(82)

Figure 6: The reduced relations in $\mathcal{R}_{n}^{3}$, for all valid
choices of $a,b,c\in\mathbb{Z}$ where $b>0$ and $c>3$. We write $\rho$ for the
substring
${K}{}_{[4,5,6,7]}\cdot{K}{}_{[0,1,2,3]}\cdot{X}{}_{[3,4]}\cdot{K}{}_{[0,1,2,3]}\cdot{K}{}_{[4,5,6,7]}$.

It will now shown that many relations in $\mathcal{R}_{n}^{2}$ are redundant.
First, the braiding relations and order relations are used according to
Section F.2 to eliminate all other relations over the two-level operators of
type $X$. This reduced relation set is then used to show that all instances of
Relations 51 and 52 can be derived using transpositions in place of swaps.
Finally, it is shown that the relations Relations 59, 60, 61 and 62 are
entirely redundant. All derivations can be found in Section F.4. This new set
of relations is denoted $\mathcal{R}_{n}^{3}$, and can be found in Figure 6.
Then via a sequence of Rel($-$) transformations, the following presentation is
obtained.

######  Theorem 5.1.

$\mathrm{O}(n,\mathbb{D})\cong\langle\mathcal{G}_{n}^{1}\mid\mathcal{R}_{n}^{3}\rangle$.

###  5.5 Introducing the $W(E_{8})$ Generators

It this section, the circuit generators and relations for $W(E_{8})$ are
introduced. Since ${CC{X}}_{{1},{2}}={X}{}_{[6,7]}$, then without loss of
generality, every instance of ${X}{}_{[6,7]}$ in $\mathcal{R}_{8}^{3}$ can be
replaced by ${CC{X}}_{{1},{2}}$. Next, the generators ${X}_{0}$ and
${C{X}}_{{0},{1}}$ are introduced. This yields the following relations.

$\displaystyle(r_{X}):{X}_{0}$
$\displaystyle\approx{X}{}_{[0,4]}\cdot{X}{}_{[1,5]}\cdot{X}{}_{[2,6]}\cdot{X}{}_{[3,7]}$
$\displaystyle(r_{CX}):{C{X}}_{{0},{1}}$
$\displaystyle\approx{X}{}_{[2,6]}\cdot{X}{}_{[3,7]}$

It turns out that the ${K}_{1,2}$ gate decomposes into a word over ${X}_{0}$
and ${K}{}_{[0,1,2,3]}$. This is because ${K}{}_{[0,1,2,3]}$ is a ${K}_{1,2}$
gate which is applied when qubit $0$ is in state $\ket{1}$, and
${X}_{0}\circ{K}{}_{[0,1,2,3]}\circ{X}_{0}$ is a ${K}_{1,2}$ gate which is
applied when qubit $0$ is in state $\ket{0}$. Together, these two words
compose to a ${K}_{1,2}$ gate without any controls. This yields the following
relation.

$\displaystyle(r_{K}):{K}_{1,2}$
$\displaystyle\approx{K}{}_{[4,5,6,7]}\cdot{X}_{0}\cdot{K}{}_{[4,5,6,7]}\cdot{X}_{0}$

The relations $r_{X}$, $r_{CX}$, and $r_{K}$ can be validated with respect to
$[\\![\cdot]\\!]_{O}$. These relations do not depend on one-another, so the
generators in $\Sigma_{0}$ may be introduced via a sequence of Gen($+$)
transformations, as outlined in Section B.2. Likewise, the derived generators
in $\Sigma_{D}\setminus\Sigma_{0}$ may be introduced via a sequence of
Gen($+$) transformations, as outlined in Section B.2. Finally, the relations
in $R_{0}$ may be introduced, since Section 4.1 established the validity of
these relations in $W(E_{8})$, which is a subgroup of $O(8,\mathbb{D})$. This
sequence of transformations yields
$\mathrm{O}(8,\mathbb{D})\cong\left\langle\mathcal{G}_{8}^{1}\cup\Sigma_{D}\mid\mathcal{R}_{8}^{3}\cup
R_{0}\cup\\{r_{X},r_{CX},r_{K}\\}\right\rangle$.

###  5.6 Eliminating the Multi-Level Operators

Using the generators in $\Sigma_{D}$ and the relations in $R_{0}$, it is
possible to eliminate all two-level operators of type $X$. As a first step, it
must be shown that the two-level operators can be decomposed into circuits
over $\Sigma_{D}$. This follows from the fact that $\Sigma_{D}$ generates
$W(E_{8})$, and $\mathrm{S}(n)\hookrightarrow W(E_{8})$.

$\displaystyle{X}{}_{[0,1]}$
$\displaystyle={X}_{0}\circ{X}_{1}\circ{CC{X}}_{{0},{1}}\circ{X}_{1}\circ{X}_{0}$
$\displaystyle{X}{}_{[1,2]}$
$\displaystyle={X}_{0}\circ{CC{X}}_{{0},{1}}\circ{CC{X}}_{{0},{2}}\circ{CC{X}}_{{0},{1}}\circ{X}_{0}$
$\displaystyle{X}{}_{[2,3]}$
$\displaystyle={X}_{0}\circ{CC{X}}_{{0},{1}}\circ{X}_{0}$
$\displaystyle{X}{}_{[3,4]}$
$\displaystyle={X}_{0}\circ{X}_{2}\circ{CC{X}}_{{0},{1}}\circ{X}_{0}\circ{CC{X}}_{{1},{2}}\circ{CC{X}}_{{0},{2}}\circ{CC{X}}_{{1},{2}}\circ{X}_{0}\circ{CC{X}}_{{0},{1}}\circ{X}_{2}\circ{X}_{0}$
$\displaystyle{X}{}_{[4,5]}$
$\displaystyle={X}_{1}\circ{CC{X}}_{{0},{1}}\circ{X}_{1}$
$\displaystyle{X}{}_{[5,6]}$
$\displaystyle={CC{X}}_{{0},{1}}\circ{CC{X}}_{{0},{2}}\circ{CC{X}}_{{0},{1}}$

These relations can be validated with respect to $[\\![\cdot]\\!]_{O}$, and
consequently introduced via a sequence of Gen($+$) operations. These
definitional relations can then be used to eliminate the two-level operators
of type $X$, as outlined in Section B.2.

$\displaystyle{(-1)}{}_{[0]}{}^{2}$ $\displaystyle\,\approx\,\epsilon$ (83)
$\displaystyle{K}{}_{[0,1,2,3]}{}^{2}$ $\displaystyle\,\approx\,\epsilon$ (84)
$\displaystyle{X}{}_{[1,2]}\cdot{(-1)}{}_{[0]}$
$\displaystyle\,\approx\,{(-1)}{}_{[0]}\cdot{X}{}_{[1,2]}$ (85)
$\displaystyle{X}{}_{[2,3]}\cdot{(-1)}{}_{[0]}$
$\displaystyle\,\approx\,{(-1)}{}_{[0]}\cdot{X}{}_{[2,3]}$ (86)
$\displaystyle{X}{}_{[3,4]}\cdot{(-1)}{}_{[0]}$
$\displaystyle\,\approx\,{(-1)}{}_{[0]}\cdot{X}{}_{[3,4]}$ (87)
$\displaystyle{X}{}_{[4,5]}\cdot{(-1)}{}_{[0]}$
$\displaystyle\,\approx\,{(-1)}{}_{[0]}\cdot{X}{}_{[4,5]}$ (88)
$\displaystyle{X}{}_{[5,6]}\cdot{(-1)}{}_{[0]}$
$\displaystyle\,\approx\,{(-1)}{}_{[0]}\cdot{X}{}_{[5,6]}$ (89)
$\displaystyle{X}{}_{[6,7]}\cdot{(-1)}{}_{[0]}$
$\displaystyle\,\approx\,{(-1)}{}_{[0]}\cdot{X}{}_{[6,7]}$ (90)
$\displaystyle{X}{}_{[4,5]}\cdot{K}{}_{[0,1,2,3]}$
$\displaystyle\,\approx\,{K}{}_{[0,1,2,3]}\cdot{X}{}_{[4,5]}$ (91)

$\displaystyle{X}{}_{[5,6]}\cdot{K}{}_{[0,1,2,3]}$
$\displaystyle\,\approx\,{K}{}_{[0,1,2,3]}\cdot{X}{}_{[5,6]}$ (92)
$\displaystyle{X}{}_{[6,7]}\cdot{K}{}_{[0,1,2,3]}$
$\displaystyle\,\approx\,{K}{}_{[0,1,2,3]}\cdot{X}{}_{[6,7]}$ (93)
$\displaystyle{(-1)}{}_{[4]}\cdot{K}{}_{[0,1,2,3]}$
$\displaystyle\,\approx\,{K}{}_{[0,1,2,3]}\cdot{(-1)}{}_{[4]}$ (94)
$\displaystyle{(-1)}{}_{[0]}\cdot{(-1)}{}_{[4]}$
$\displaystyle\,\approx\,{(-1)}{}_{[4]}\cdot{(-1)}{}_{[0]}$ (95)
$\displaystyle{K}{}_{[0,1,2,3]}\cdot{K}{}_{[4,5,6,7]}$
$\displaystyle\,\approx\,{K}{}_{[4,5,6,7]}\cdot{K}{}_{[0,1,2,3]}$ (96)
$\displaystyle{X}{}_{[0,1]}\cdot{K}{}_{[0,1,2,3]}$
$\displaystyle\,\approx\,{K}{}_{[0,1,2,3]}\cdot{X}{}_{[0,1]}\cdot{(-1)}{}_{[1]}\cdot{(-1)}{}_{[3]}$
(97) $\displaystyle{X}{}_{[1,2]}\cdot{K}{}_{[0,1,2,3]}$
$\displaystyle\,\approx\,{(-1)}{}_{[0]}\cdot{K}{}_{[0,1,2,3]}\cdot{(-1)}{}_{[0]}\cdot{K}{}_{[0,1,2,3]}\cdot{(-1)}{}_{[0]}$
(98) $\displaystyle{X}{}_{[2,3]}\cdot{K}{}_{[0,1,2,3]}$
$\displaystyle\,\approx\,{K}{}_{[0,1,2,3]}\cdot{X}{}_{[1,3]}$ (99)
$\displaystyle{K}{}_{[0,1,2,3]}\cdot{K}{}_{[1,3,4,5]}$
$\displaystyle\,\approx\,{K}{}_{[1,3,4,5]}\cdot{K}{}_{[0,1,2,3]}$ (100)
$\displaystyle{(-1)}{}_{[0]}\cdot{(-1)}{}_{[4]}\cdot{X}{}_{[0,4]}\cdot\rho$
$\displaystyle\,\approx\,\rho\cdot{X}{}_{[0,4]}\cdot{(-1)}{}_{[4]}\cdot{(-1)}{}_{[0]}$
(101)

Figure 7: The relations in $\mathcal{R}_{8}^{4}$, sufficient to extend from
$W(E_{8})$ to $O(8,\mathbb{D})$.

In this new presentation, then relations Relations 47, 56 and 57 are replaced
by relations over $\Sigma_{D}$. Since $R_{0}$ is complete for $W(E_{8})$, then
these relations can be derived from $R_{0}$. Consequently, these relations can
be eliminated with a sequence of Rel($-$) transformations. This yields a new
set of relations, denoted $\mathcal{R}_{8}^{4}$, which can be found in Figure
7. For simplicity of presentation, we used ${X}{}_{[0,1]}$ through to
${X}{}_{[6,7]}$ as abbreviations for the circuits given above. Furthermore, we
take $CCZ={(-1)}{}_{[7]}$ to be a generator with ${(-1)}{}_{[0]}$ an alias for
${X}_{0}\cdot{X}_{1}\cdot CCZ\cdot{X}_{1}\cdot{X}_{0}$. Then define
$\Sigma_{1}=\Sigma_{D}\cup\\{{K}{}_{[0,1,2,3]},CCZ\\}$ and
$R_{1}=R_{0}\cup\mathcal{R}_{8}^{4}$, where ${K}{}_{[0,1,2,3]}$ corresponds to
a negatively controlled $K$ gate.

######  Theorem 5.2.

$\mathrm{O}(8,\mathbb{D})\cong\langle\Sigma_{1}\mid R_{1}\rangle$.

###  5.7 A Minimal Generating Set for $\mathrm{O}(8,\mathbb{D})$

It turns out that $CCZ$ and ${K}{}_{[0,1,2,3]}$ can be defined in terms of
one-another, given that generators in $\Sigma_{D}$. The decompositions are as
follows.

$\displaystyle CCZ$
$\displaystyle={K}_{1,2}\circ{C{Z}}_{{1},{2}}\circ{X}_{0}\circ{K}{}_{[0,1,2,3]}\circ{X}_{0}\circ{C{Z}}_{{1},{2}}\circ{K}{}_{[0,1,2,3]}\circ{X}{}_{[5,6]}$
$\displaystyle{K}{}_{[0,1,2,3]}$ $\displaystyle=({K}_{1,2}\circ
CCZ)^{3}\circ{X}{}_{[5,6]}$

Given this observation, it seems natural to eliminate the ${K}{}_{[0,1,2,3]}$,
given that it is not a common generator in quantum computation. However, the
set $\Sigma_{D}\cup\\{CCZ\\}$ is minimal, whereas the set
$\Sigma_{D}\cup\\{{K}{}_{[0,1,2,3]}\\}$ is not. In other words, choosing the
generator ${K}{}_{[0,1,2,3]}$ enables a smaller generating set, whereas
choosing the generator $CCZ$ allows for more conventional circuit
decompositions. For this reason, we choose to keep both ${K}{}_{[0,1,2,3]}$
and $CCZ$ in our presentation. The minimality of these generating sets are
proven in Appendix E, using the same techniques as in Section 4.5.

######  Theorem 5.3.

The following generating sets are minimal for $\mathrm{O}(8,\mathbb{D})$.

  1. 1.

$\Sigma_{K}=\left\\{{X}_{0},{C{X}}_{{0},{1}},{CC{X}}_{{1},{2}},{K}{}_{[0,1,2,3]}\right\\}$.

  2. 2.

$\Sigma_{Z}=\left\\{{X}_{0},{C{X}}_{{0},{1}},{CC{X}}_{{1},{2}},{K}_{1,2},CCZ\right\\}$

##  6 Extending to the 3-Qubit Toffoli-Hadamard Circuits

We now give a presentation of $\textsf{TofH}(3)$, by leveraging the
presentation of $\mathrm{O}(8,\mathbb{D})$ found in Section 5. The argument in
this section closely follows [19, Section 5]. From [4], it is known that
$\textsf{TofH}(3)$ is obtained by adding the generator ${H}_{2}$ to
$\mathrm{O}(8,\mathbb{D})$. Let $\Sigma_{2}=\Sigma_{1}\cup\\{{H}_{2}\\}$ and
$R_{2}$ extend the set $R_{1}$ with all relations found in Figure 8. Using the
relations in Figure 8, the generator ${H}_{2}$ can be moved from the left-hand
side to the right-hand side of any word over $\Sigma_{1}$. Since ${H}_{2}$ is
self-inverse, this is sufficient to decide equality in $\textsf{TofH}(3)$.

$\displaystyle{H}_{2}\cdot{X}_{0}$
$\displaystyle\,\approx\,{X}_{0}\cdot{H}_{2}$ (102)
$\displaystyle{H}_{2}\cdot{C{X}}_{{0},{1}}$
$\displaystyle\,\approx\,{C{X}}_{{0},{1}}\cdot{H}_{2}$ (103)
$\displaystyle{H}_{2}\cdot{CC{X}}_{{1},{2}}$
$\displaystyle\,\approx\,K_{0,1}\cdot K_{1,2}\cdot CCZ\cdot K_{1,2}\cdot
K_{0,1}\cdot{H}_{2}$ (104)

$\displaystyle{H}_{2}\cdot CCZ$
$\displaystyle\,\approx\,{CC{X}}_{{0},{1}}\cdot{H}_{2}$ (105)
$\displaystyle{H}_{2}\cdot K_{1,2}$
$\displaystyle\,\approx\,K_{1,2}\cdot{H}_{2}$ (106)
$\displaystyle{H}_{2}\cdot{K}{}_{[0,1,2,3]}$
$\displaystyle\,\approx\,{K}{}_{[0,1,2,3]}\cdot{H}_{2}$ (107)
$\displaystyle{H}_{2}\cdot{H}_{2}$ $\displaystyle\,\approx\,\epsilon$ (108)

Figure 8: Additional relations for $\textsf{TofH}(3)$.

The proof proceeds as follows. In Lemma 6.1, it is shown that ${H}_{2}$
commutes with every word in over $\Sigma_{1}$ using only the relations in
$R_{2}$. This is used in Lemma 6.2, to show that every word over $\Sigma_{2}$
can be rewritten as a word over $\Sigma_{1}$, followed by at most one
${H}_{2}$ gate. Since $R_{1}\subseteq R_{2}$ is a complete equational theory
for $\mathrm{O}(8,\mathbb{D})$ with every element of $\textsf{TofH}(3)$ of the
form described in Lemma 6.2, it follows that $R_{2}$ is a complete equational
theory for $\textsf{TofH}(3)$ (see Theorem 6.3).

######  Lemma 6.1.

If $w\in\Sigma_{1}^{*}$, then there exists a $w^{\prime}\in\Sigma_{1}^{*}$
such that ${H}_{2}\cdot w\,\sim_{R2}\,w^{\prime}\cdot{H}_{2}$.

###### Proof.

The proof follows by induction on $|w|$.

  1. –

Base Case. If $|w|=0$, then ${H}_{2}\cdot w=w\cdot{H}_{2}$. Then ${H}_{2}\cdot
w\,\sim_{R2}\,w\cdot{H}_{2}$ by the transitivity of $(\sim_{R2})$.

  2. –

Inductive Case. Assume that for some $k\in\mathbb{N}$, if $|w|=k$, then there
exists a $w^{\prime}\in\Sigma_{1}^{*}$ such that ${H}_{2}\cdot
w\,\sim_{R2}\,w^{\prime}\cdot{H}_{2}$.

  3. –

Inductive Step. Assume that $|w|=k+1$. Then there exists a
$u\in\Sigma_{1}^{*}$ and $x\in\Sigma_{1}$ such that $x\cdot u=w$. It follows
by one of Relations 102, 103, 104, 105, 106 and 107, that there exits a
$u^{\prime}\in\Sigma_{1}^{*}$ such that ${H}_{2}\cdot
w\,\sim_{R2}\,u^{\prime}\cdot{H}_{2}\cdot u$. Since $|u|=k$, then by the
inductive hypothesis, there exists a $w^{\prime}\in\Sigma_{1}^{*}$ such that
${H}_{2}\cdot u\,\sim_{R2}\,w^{\prime}\cdot{H}_{2}$. Then
$u^{\prime}\cdot{H}_{2}\cdot u\,\sim_{R2}\,u^{\prime}\cdot
w^{\prime}\cdot{H}_{2}$. Then ${H}_{2}\cdot u\,\sim_{R2}\,u^{\prime}\cdot
w^{\prime}\cdot{H}_{2}$ by the transitivity of $(\sim_{R2})$, and the
inductive case holds.

Then by the principle of induction, there exists a
$w^{\prime}\in\Sigma_{1}^{*}$ such that ${H}_{2}\cdot
w\,\sim_{R2}\,w^{\prime}\cdot{H}_{2}$. ∎

######  Lemma 6.2.

If $w\in\Sigma_{2}^{*}$, then there exists some $w^{\prime}\in\Sigma_{1}^{*}$
and $\ell\in\\{0,1\\}$ such that
$w\,\sim_{R_{2}}\,w^{\prime}\cdot{H}_{2}^{\ell}$.

###### Proof.

Let $f:\Sigma_{2}^{*}\to\mathbb{N}$ map each word $w\in\Sigma_{2}^{*}$ to the
number of ${H}_{2}$ symbols in $w$. The proof follows by induction on $f(w)$.

  1. –

Base Case. If $f(w)=0$, then $w\in\Sigma_{1}^{*}$. Then
$w\,\sim_{R2}\,w\cdot{H}_{2}^{0}$ by the reflexivity of $(\sim_{R2})$

  2. –

Inductive Hypothesis. Assume that for some $k\in\mathbb{N}$, if $f(w)=k$, then
there exists some $w^{\prime}\in\Sigma_{1}^{*}$ and $\ell\in\\{0,1\\}$ such
that $w\,\sim_{R2}\,w^{\prime}\cdot{H}_{2}^{\ell}$.

  3. –

Inductive Step. Assume that $f(w)=k+1$. Then there exists
$w_{1}\in\Sigma_{2}^{*}$ and $w_{2}\in\Sigma_{1}^{*}$ such that
$w=w_{1}\cdot{H}_{2}\cdot w_{2}$ with $f(w_{1})=f(w)-1$. Then by Lemma 6.1,
$w\,\sim_{R2}\,w_{1}\cdot w_{2}^{\prime}\cdot{H}_{2}$ for some
$w_{2}^{\prime}\in\Sigma_{1}^{*}$. Then $f(w_{1}\cdot
w_{2}^{\prime})=f(w_{1})=f(w)-1$. By the inductive hypothesis, there exists
some $w_{3}\in\Sigma_{1}^{*}$ and $\ell\in\\{0,1\\}$ such that $w_{1}\cdot
w_{2}^{\prime}\,\sim_{R2}\,w_{3}\cdot{H}_{2}^{\ell}$. Then
$w\,\sim_{R2}\,w_{3}\cdot{H}_{2}^{\ell+1}$. If $\ell=0$, then
$w\,\sim_{R2}\,w_{3}\cdot{H}_{2}$ and we are done. Otherwise, if $\ell=1$,
then $w\,\sim_{R2}\,w_{3}$ by Relation 108. In either case, there exists an
$\ell^{\prime}\in\\{0,1\\}$ such that
$w\,\sim_{R2}\,w_{3}\cdot{H}_{2}^{\ell^{\prime}}$ and the inductive step
holds.

Then by the principle of induction, there exists some
$w^{\prime}\in\Sigma_{1}^{*}$ and $\ell\in\\{0,1\\}$ such that
$w\,\sim_{R_{2}}\,w^{\prime}\cdot{H}_{2}^{\ell}$. ∎

######  Theorem 6.3.

For all $w_{1},w_{2}\in\Sigma_{2}^{*}$,
$[\\![w_{1}]\\!]_{H}^{*}=[\\![w_{2}]\\!]_{H}^{*}$ if and only if
$w_{1}\sim_{R2}w_{2}$.

###### Proof.

It follows by matrix multiplication that the relations in Figure 8 are sound.
It remains to be shown that the relations in Figure 8 are complete. Let
$w_{1}\in\Sigma_{2}^{*}$ and $w_{2}\in\Sigma_{2}^{*}$ such that
$[\\![w_{1}]\\!]_{H}^{*}=[\\![w_{2}]\\!]_{H}^{*}$. By Lemma 6.2, there exists
$\ell_{1},\ell_{2}\in\\{0,1\\}$ and
$w_{1}^{\prime},w_{2}^{\prime}\in\Sigma_{1}^{*}$ such that
$w_{1}\,\sim_{R2}\,w_{1}^{\prime}\cdot{H}_{2}^{\ell_{1}}$ and
$w_{2}\,\sim_{R2}\,w_{2}^{\prime}\cdot{H}_{2}^{\ell_{2}}$. Since
$[\\![w_{1}]\\!]_{H}^{*}\in\mathrm{O}(8,\mathbb{D})\cong\langle\Sigma_{1},R_{1}\rangle$
with $R_{1}\subseteq R_{2}$, then
$w_{1}^{\prime}\cdot{H}_{2}^{\ell_{1}}\,\sim_{R2}\,w_{2}^{\prime}\cdot{H}_{2}^{\ell_{1}}$.
Assume for the intent of contradiction that $\ell_{1}\neq\ell_{2}$. Then
$[\\![w_{1}^{\prime}]\\!]_{H}^{*}=[\\![w_{2}^{\prime}]\\!]_{H}^{*}\circ[\\![{H}_{2}]\\!]_{H}$.
Then
$[\\![w_{2}^{\prime}]\\!]_{H}^{*}\circ[\\![{H}_{2}]\\!]_{H}^{*}\in\mathrm{O}(8,\mathbb{D})$.
However, $[\\![w_{2}^{\prime}]\\!]_{H}^{*}\circ[\\![{H}_{2}]\\!]_{H}$ has a
denominator of the form $1/(2^{k}\sqrt{2})$, and therefore
$[\\![w_{2}^{\prime}]\\!]_{H}^{*}\circ[\\![{H}_{2}]\\!]_{H}\not\in\mathrm{O}(8,\mathbb{D})$.
By contradiction, $\ell_{1}=\ell_{2}$. Since $\ell_{1}=\ell_{2}$, then
$w_{1}\,\sim_{R2}\,w_{2}$ by the transitivity and symmetry of $(\sim_{R2})$.
Since $w_{1}$ and $w_{2}$ were arbitrary, then the relations in Figure 8 are
complete. ∎

##  7 Conclusion

We used the geometry of $W(E_{8})$ to obtain a circuit presentation for the
$3$-qubit Toffoli-K circuits, and then leveraged [19] to obtain a finite
presentation of $3$-qubit Toffoli-Hadamard circuits. Our presentation contains
65 relations, compared to the 2113 relations of [19]. There are several
directions for future work. We hope to simplify our presentation by further
reducing the number of relations. In addition, we plan to explore the
structural properties of the group of 3-qubit Toffoli-Hadamard circuits and of
its subgroups. In particular, it is known that the group
$\mathrm{O}(8,\mathbb{D})$ is generated by reflections, but it is not known
whether this group can be presented as an (infinite) Coexeter group. From an
applied perspective, we also hope to explore applications of these
presentations to circuit optimization and equivalence checking.

## References

  * [1]
  * [2] Dorit Aharonov (2003): _A simple proof that Toffoli and Hadamard are quantum universal_.  arXiv:quant-ph/0301040.
  * [3] Matthew Amy, Jianxin Chen & Neil J. Ross (2018): _A Finite Presentation of CNOT-Dihedral Operators_.  EPTCS 266, pp. 84–97, 10.4204/eptcs.266.5.
  * [4] Matthew Amy, Andrew Glaudell & Neil Ross (2020): _Number-Theoretic Characterizations of Some Restricted Clifford+T Circuits_.  Quantum 4, p. 252, 10.22331/q-2020-04-06-252.
  * [5] Matthew Amy, Andrew N. Glaudell, Sarah Meng Li & Neil J. Ross (2023): _Improved Synthesis of Toffoli-Hadamard Circuits_.  In: Reversible Computation, Springer-Verlag, pp. 169–209, 10.1007/978-3-031-38100-3_12.
  * [6] Matthew Amy, Neil J. Ross & Scott Wesley (2024): _Supplement: A Sound and Complete Equational Theory for 3-Qubit Toffoli-Hadamard Circuits_.  Available as an ancillary file from the arXiv page of this paper.
  * [7] Franz Baader & Tobias Nipkow (1998): _Term Rewriting and All That_.  Cambridge University Press, 10.1017/CBO9781139172752.
  * [8] Xiaoning Bian & Peter Selinger (2023): _Generators and relations for 2-qubit Clifford+ $T$ operators_.  EPTCS 394, pp. 13–28, 10.4204/eptcs.394.2.
  * [9] Xiaoning Bian & Peter Selinger (2023): _Generators and relations for 3-qubit Clifford+ $CS$ operators_.  EPTCS 384, pp. 114–126, 10.4204/eptcs.384.7.
  * [10] Ronald V. Book & Friedrich Otto (1993): _String-Rewriting Systems_.  Springer, 10.1007/978-1-4613-9771-7.
  * [11] Maria Luisa Dalla Chiara, Antonio Ledda, Giuseppe Sergioli & Roberto Giuntini (2013): _The Toffoli-Hadamard gate system: an algebraic approach_.  Journal of Philosophical Logic 42, pp. 467–481, 10.1007/s10992-013-9271-9.
  * [12] Alexandre Clément, Nicolas Heurtel, Shane Mansfield, Simon Perdrix & Benoît Valiron (2023): _A Complete Equational Theory for Quantum Circuits_.  In: LiCS, IEEE, pp. 1–13, 10.1109/LICS56636.2023.10175801.
  * [13] J. H. Conway & N. J. A. Sloane (1987): _Sphere-Packings, Lattices, and Groups_.  Springer-Verlag, 10.1007/978-1-4757-6568-7.
  * [14] Jörg Endrullis, Herman Geuvers, Jakob Grue Simonsen & Hans Zantema (2011): _Levels of undecidability in rewriting_.  Information and Computation 209(2), pp. 227–245, 10.1016/j.ic.2010.09.003.
  * [15] Adam P. Goucher (2020): _Minimalistic Quantum Computation_.  https://cp4space.hatsya.com/2020/05/10/minimalistic-quantum-computation/.  Accessed: 2023-11-26.
  * [16] Simon Henry & Samuel Mimram (2022): _Tietze Equivalences as Weak Equivalences_.  Applied Categorical Structures 30(3), pp. 453–483, 10.1007/s10485-021-09662-w.
  * [17] James E. Humphreys (1990): _Reflection Groups and Coxeter Groups_.  Cambridge Studies in Advanced Mathematics, Cambridge University Press, 10.1017/CBO9780511623646.
  * [18] D. L. Johnson (1990): _Presentations of Groups_.  Cambridge University Press, 10.1017/CBO9781139168410.
  * [19] Sarah Meng Li, Neil J. Ross & Peter Selinger (2021): _Generators and Relations for the Group $On(Z[1/2])$_.  EPTCS 343, pp. 210–264, 10.4204/eptcs.343.11.
  * [20] Justin Makary, Neil J. Ross & Peter Selinger (2021): _Generators and Relations for Real Stabilizer Operators_.  EPTCS 343, p. 14–36, 10.4204/eptcs.343.2.
  * [21] Leonardo de Moura & Nikolaj Bjørner (2008): _Z3: An Efficient SMT Solver_.  In: TACAS, Springer-Verlag, pp. 337–340, 10.5555/1792734.1792766.
  * [22] Michel Planat (2011): _Clifford group dipoles and the enactment of Weyl/Coxeter group $W(E8)$ by entangling gates_.  Gen. Math. Notes 2(1), pp. 96–113, 10.22331/q-2020-04-06-252.
  * [23] Peter Selinger (2015): _Generators and Relations for $n$-Qubit Clifford Operators_.  LMCS 11(2:10), pp. 1–17, 10.2168/LMCS-11(2:10)2015.
  * [24] Yaoyun Shi (2003): _Both Toffoli and controlled-NOT need little help to do universal quantum computing_.  Quantum Info. Comput. 3(1), pp. 84–92, 10.5555/2011508.2011515.
  * [25] Maryna S. Viazovska (2017): _The sphere packing problem in dimension 8_.  Annals of Mathematics 185(3), pp. 991–1015, 10.4007/annals.2017.185.3.7.
  * [26] Renaud Vilmart (2019): _A ZX-calculus with triangles for Toffoli-Hadamard, Clifford+ $T$, and beyond_.  EPTCS 287, pp. 313–344, 10.4204/eptcs.287.18.
  * [27] Renaud Vilmart (2023): _Completeness of sum-over-paths for Toffoli-Hadamard and the dyadic fragments of quantum computation_.  In: CSL, LIPIcs 252, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, pp. 36:1–36:17, 10.4230/LIPIcs.CSL.2023.36.

##  Appendix A Semantic Tietze Transformations

This section recalls what it means for a function to induce a monoid
homomorphism. This is then used to prove the soundness and completeness of
Tietze transformations with respect to semantic interpretations. The majority
of this section is dedicated to proving that all induced homomorphisms are
isomorphisms, and in the case of Gen($+$), the extension is unique. The
uniqueness of this extension is necessary to prove that each generator in
$\Sigma_{D}$ has the intended matrix semantics.

###  A.1 Induced Monoid Homomorphisms

Let $\Sigma$ be an alphabet and $M$ a monoid. For each function $f:\Sigma\to
M$, define the function $f^{*}:\Sigma^{*}\to M$ such that $f^{*}(x_{1}\cdot
x_{2}\cdots x_{n})=1_{M}\circ f(x_{1})\circ f(x_{2})\circ\cdots\circ f(x_{n})$
for all $x_{1}\cdot x_{2}\cdots x_{n}\in\Sigma^{*}$. It can then be shown that
$f^{*}$ is the unique monoid homomorphism such that $f^{*}(x)=f(x)$ for all
$x\in\Sigma$ [18]. Given a set of relations
$R\subseteq\Sigma^{*}\times\Sigma^{*}$, it can then be asked whether $f$
induces a monoid homomorphism between $G=\langle\Sigma\mid R\rangle$ and $M$.
This question is answered by the following theorem.

######  Theorem A.1 ([10]).

Let $M$ and $G=\langle\Sigma\mid R\rangle$ be monoids with $f:\Sigma\to M$.
There there exists a unique monoid homomorphism $\varphi:G\to M$ such that
$f^{*}=\varphi\circ\pi_{G}$ if and only if $f^{*}(q)=f^{*}(r)$ for all
$q\approx_{R}r$. In this case,
$\imaginary(\varphi)=\langle\varphi(\pi_{G}(\Sigma))\rangle$.

Theorem A.1 characterizes when $f$ induces a monoid homomorphism, and how to
construct this induced homomorphism $\varphi$. It can then be asked how the
construction of $\varphi$ interacts with the introduction or elimination of
generators. As outlined by the following theorems, the elimination of
generators corresponds to certain restrictions of $\varphi$, whereas the
introduction of generators corresponds to certain unique extensions of
$\varphi$.

######  Lemma A.2.

Let $\Sigma$ be an alphabet, $x\in\Sigma$,
$\Sigma^{\prime}=\Sigma\setminus\\{x\\}$, and $D=\\{x\approx w\\}$ for some
$w\in(\Sigma^{\prime})^{*}$. If $q\in\Sigma^{*}$, then there exists a
$q^{\prime}\in(\Sigma^{\prime})^{*}$ such that $q\sim_{D}q^{\prime}$.

###### Proof.

Let $f:\Sigma^{*}\to\mathbb{N}$ count the $x$ symbols in a word. Then the
proof follows by induction on $f(q)$.

  1. –

Base Case. If $f(q)=0$, then $q\in(\Sigma^{\prime})^{*}$.

  2. –

Inductive Hypothesis. Assume that for some $k\in\mathbb{N}$, if $f(q)=k$, then
there exists some $q^{\prime}\in(\Sigma^{\prime})^{*}$ such that
$q\sim_{D}q^{\prime}$.

  3. –

Inductive Step. Assume $f(q)=k+1$. Since $f(q)>1$, then there exists some
$u,v\in\Sigma^{*}$ such that $q=u\cdot x\cdot v$. Since $k+1=f(q)=f(u\cdot
x\cdot v)=f(u)+f(x)+f(v)=f(u)+f(v)+1$, then $k=f(u)+f(v)$. Since
$x\approx_{D}w$, then $q\sim_{D}u\cdot w\cdot v$ with $f(u\cdot w\cdot
v)=f(u)+f(v)=k$. Then by the inductive hypothesis, there exists some
$q^{\prime}\in(\Sigma^{\prime})^{*}$ such that $u\cdot w\cdot
v\sim_{D}q^{\prime}$. Then $q\sim q^{\prime}$.

By the principle of induction, there exists some
$q^{\prime}\in(\Sigma^{\prime})^{*}$ such that $q\sim_{D}q^{\prime}$. ∎

######  Theorem A.3.

Let $M$ and $G=\langle\Sigma\mid R\rangle$ be monoids with $f:\Sigma\to M$,
and $H=\langle\Sigma\cup\\{x\\}\mid R\cup\\{x\approx w\\}\rangle$ be a monoid
for some $x\not\in\Sigma$ and $w\in\Sigma^{*}$. Define $g:\Sigma\cup\\{x\\}\to
M$ such that $g|_{\Sigma}=f$ and $g:x\mapsto f^{*}(w)$. If $f$ induces a
monoid homomorphism from $G$ to $M$, then $g$ is the unique extension of $f$
to induce a monoid homomorphism from $H$ to $M$. Furthermore, if $f$ induces
an injection (resp. surjection) from $G$ to $M$, then $g$ induces an injection
(resp. surjection) from $H$ to $M$.

###### Proof.

Let $\Pi=\Sigma\cup\\{x\\}$ and $Q=R\cup\\{x\approx w\\}$. Assume that $f$
induces a homomorphism from $G$ to $M$.

  * –

(Induced Hom). Let $q\approx_{Q}r$. Then either $q\approx_{R}r$ or
$(q,r)=(x,w)$. First, assume that $q\approx_{R}r$. Then $f^{*}(q)=f^{*}(r)$ by
Theorem A.1. Then
$g^{*}(q)=(g|_{\Sigma})^{*}(q)=f^{*}(q)=f^{*}(r)=(g|_{\Sigma})^{*}(r)=g^{*}(r)$.
Next, assume that $(q,r)=(x,w)$. Then
$g^{*}(x)=g(x)=f^{*}(w)=(g|_{\Sigma})^{*}(w)=g^{*}(w)$. In either case
$g^{*}(q)=g^{*}(r)$. Since $q\approx_{R}r$ was arbitrary, then
$g^{*}(q)=g^{*}(r)$ for all $q\approx_{R}r$. Then $g$ induce a monoid
homomorphism from $H$ to $M$ by Theorem A.1.

  * –

(Uniqueness). Assume that $k:\Sigma\cup\\{x\\}\to M$ is an extension of $f$
which induces a monoid homomorphism. Since $k$ induces a monoid homomorphism
and $x\approx_{Q}w$, then $k^{*}(x)=k^{*}(w)$ by Theorem A.1. Then
$k(x)=k^{*}(x)=k^{*}(w)=(k|_{\Sigma})^{*}(w)=f^{*}(w)=g(x)$ by construction of
$g$. Moreover, since $k|_{\Sigma}=f=g|_{\Sigma}$, then $k=g$. Since $k$ was
arbitrary, then $g$ is unique.

  * –

(Injectivity). Let $f$ induce $\varphi$ and $g$ induce $\rho$. Assume that
$\varphi$ is injective. Let $q,r\in\Pi^{*}$ such that
$\rho(\pi_{H}(q))=\rho(\pi_{H}(r))$. Since $x\approx_{Q}w$, then by Lemma A.2
there exists $q^{\prime},r^{\prime}\in\Sigma^{*}$ such that
$q\sim_{Q}q^{\prime}$ and $r\sim_{Q}r^{\prime}$. Then
$\pi_{H}(q)=\pi_{H}(q^{\prime})$ and $\pi_{H}(r)=\pi_{H}(r^{\prime})$. Then
$\rho(\pi_{H}(q^{\prime}))=\rho(\pi_{H}(r^{\prime}))$. Then
$g^{*}(q^{\prime})=g^{*}(r^{\prime})$. Since
$q^{\prime},r^{\prime}\in\Sigma^{*}$, then
$f^{*}(q^{\prime})=f^{*}(r^{\prime})$. Then
$\varphi(\pi_{G}(q^{\prime}))=\varphi(\pi_{G}(r^{\prime}))$. Since $\varphi$
is injective, then $\pi_{G}(q^{\prime})=\pi_{G}(r^{\prime})$. Then
$q^{\prime}\sim_{R}r^{\prime}$. Since $R\subseteq Q$, then
$q^{\prime}\sim_{Q}r^{\prime}$. Then
$\pi_{H}(q^{\prime})=\pi_{H}(r^{\prime})$. Then $\pi_{H}(q)=\pi_{H}(r)$. Since
$q$ and $r$ were arbitrary, then $\rho$ is injective.

  * –

(Surjectivity). Let $f$ induce $\varphi$ and $g$ induce $\rho$. Assume that
$\varphi$ is surjective. Since
$\varphi(\pi_{G}(y))=f^{*}(y)=g^{*}(y)=\rho(\pi_{H}(y))$ for each
$y\in\Sigma$, then $\varphi(\pi_{G}(\Sigma))\subseteq\imaginary(\rho)$. Since
$\varphi$ is surjective, then
$H=\imaginary(\varphi)=\langle\varphi(\pi_{G}(\Sigma))\rangle\leq\imaginary(\rho)\leq
H$ and $\rho$ is surjective.

Therefore, $g$ is the unique extension of $f$ to induce a monoid homomorphism
from $H$ to $M$, with $g$ inducing an injection (resp. surjection) whenever
$f$ induces an injection (resp. surjection). ∎

######  Theorem A.4.

Let $M$ and $G=\langle\Sigma\mid R\rangle$ be monoids with $f:\Sigma\to M$ and
$H=\langle\Pi\mid Q\rangle$ where $\Pi=\Sigma\setminus\\{x\\}$ for some
$x\in\Sigma$ and $Q=R\setminus\\{x\approx w\\}$ for some $x\approx_{R}w$. If
$Q\subseteq\Pi^{*}\times\Pi^{*}$ and $f$ induces a monoid homomorphism from
$G$ to $M$, then $f|_{\Pi}$ induces a monoid homomorphism from $H$ to $M$.
Furthermore, if $f$ induces an injection (resp. surjection) from $G$ to $M$,
then $f|_{\Pi}$ induces an injection (resp. surjection) from $H$ to $M$.

###### Proof.

Assume that $f$ induces a homomorphism from $G$ to $M$.

  * –

(Induced Hom). Since $f$ induces a monoid homomorphism, then
$f^{*}(q)=f^{*}(r)$ for all $q\approx_{R}r$ by Theorem A.1. Since $Q\subseteq
R$ and $Q\subseteq\Pi^{*}\times\Pi^{*}$, then
$f|_{\Pi}^{*}(q)=f^{*}(q)=f^{*}(r)=f|_{\Pi}^{*}(r)$ for all $q\approx_{Q}r$.
Then $f|_{\Pi}$ induces a monoid homomorphism from $H$ to $M$ by Theorem A.1.

  * –

(Injectivity). Let $f$ induce $\varphi$ and $f|_{\Pi}$ induce $\rho$. Assume
that $\varphi$ is injective. Let $q,r\in\Pi^{*}$ such that
$\rho(\pi_{H}(q))=\rho(\pi_{H}(r))$. Then $f|_{\Pi}^{*}(q)=f|_{\Pi}^{*}(r)$.
Then $f^{*}(q)=f^{*}(r)$. Then $\varphi(\pi_{G}(q))=\varphi(\pi_{G}(r))$.
Since $\varphi$ is an injective, then $\pi_{G}(q)=\pi_{G}(r)$. Then
$q\sim_{R}r$. Since $Q=R\setminus\\{x\approx w\\}$,
$Q\subseteq\Pi^{*}\times\Pi^{*}$, and $q,r\in\Pi^{*}$, then $q\sim_{Q}r$. Then
$\pi_{H}(q)=\pi_{H}(r)$. Since $q$ and $r$ were arbitrary, then $\rho$ is
injective.

  * –

(Surjectivity). Let $f$ induce $\varphi$ and $f|_{\Pi}$ induce $\rho$. Assume
that $\varphi$ is surjective. Since
$\varphi(\pi_{G}(y))=f^{*}(y)=f|_{\Pi}^{*}(y)=\rho(\pi(y))\in\imaginary(\rho)$
for each $y\in\Pi$, then $\varphi(\pi_{G}(\Pi))\subseteq\imaginary(\rho)$.
Since $x\approx_{R}w$, then $\pi_{G}(x)=\pi_{G}(w)$, and consequently
$\varphi(\pi_{G}(x))=\varphi(\pi_{G}(w))=f^{*}(w)=f|_{\Pi}^{*}(w)=\rho(\pi_{H}(w))\in\imaginary(\rho)$.
Then $\varphi(\pi_{G}(\Sigma))\subseteq\imaginary(\rho)$. Since $\varphi$ is
surjective, then
$H=\imaginary(\varphi)\langle\varphi(\pi_{G}(\Sigma))\leq\imaginary(\rho)\leq
H$ and $\rho$ is surjective.

Therefore, $f|_{\Pi}$ induces a monoid homomorphism from $H$ to $M$ with
$f|_{\Pi}$ inducing an injection (resp. surjection) whenever $f$ induces an
injection (resp. surjection). ∎

###  A.2 Semantic Interpretations and Relations

Let $G=\langle\Sigma\mid R\rangle$ be a monoid presentation with an
interpretation $[\\![\cdot]\\!]_{G}:\Sigma\mapsto H$. The Rel($+$)
transformation states that if $r\in\Sigma^{*}$ and $q\in\Sigma^{*}$ with
$r\sim_{R}q$, then $\langle\Sigma\mid R\rangle\cong\langle\Sigma\mid
R\cup\\{r\\}\rangle$. In practice, deriving $q$ from $r$ can be challenging,
and on a theoretical level, this is known to be undecidable [14]. However, it
is rarely the case that one would try to prove $r\sim_{R}q$ without some
intuition that $\pi_{G}(r)=\pi_{G}(q)$. In the case of this paper, this
intuition comes from knowledge about operators in $O(8,\mathbb{D})$. For
example, if $M\circ N=A\circ B$, then for any complete set of relations $R$,
it must be the case that $M\cdot N\sim_{R}A\cdot B$. More generally, if
$[\\![r]\\!]_{\Sigma}^{*}=[\\![q]\\!]_{\Sigma}^{*}$ with
$[\\![\cdot]\\!]_{\Sigma}^{*}$ inducing an injection, then $r\sim_{R}q$. This
claim is established by the following theorem, and used freely throughout the
paper to simplify derivations.

######  Definition A.5 (Valid Semantic Interpretation).

A semantic interpretation $[\\![\cdot]\\!]_{\Sigma}:G\to H$ for a presentation
$G=\langle\Sigma\mid R\rangle$ is valid if
$[\\![q]\\!]_{\Sigma}^{*}=[\\![r]\\!]_{\Sigma}^{*}$ for all $r\approx_{R}q$.

######  Theorem A.6.

Let $G=\langle\Sigma\mid R\rangle$ be a presentation with a valid semantic
interpretation $[\\![\cdot]\\!]_{G}:\Sigma\mapsto H$. If $[\\![\cdot]\\!]_{G}$
is injective and $[\\![q]\\!]_{\Sigma}^{*}=[\\![r]\\!]_{\Sigma}^{*}$, then
$q\sim_{R}r$.

###### Proof.

Since $[\\![\cdot]\\!]_{\Sigma}$ is valid, then by Theorem A.1,
$[\\![\cdot]\\!]_{\Sigma}$ induces a monoid homomorphism $\varphi:G\to H$ such
that $[\\![\cdot]\\!]_{\Sigma}^{*}=\varphi\circ\pi_{G}$. Assume that
$[\\![q]\\!]_{\Sigma}^{*}=[\\![r]\\!]_{\Sigma}^{*}$. Then
$\varphi(\pi_{G}(q))=[\\![q]\\!]_{\Sigma}^{*}=[\\![r]\\!]_{\Sigma}^{*}=\varphi(\pi_{G}(r))$.
Since $\varphi$ is injective, then $\pi_{G}(q)=\pi_{G}(r)$. Then $q\sim_{R}r$.
∎

###  A.3 Semantics and Generator Introduction

In the previous section, it was assumed that $[\\![\cdot]\\!]_{\Sigma}$
inducted an injection. This is a reasonable assumption. For example, if
$G=\langle\Sigma\mid R\rangle$ is a presentation for $H$, then there exists an
isomorphism $G\cong H$ from which $[\\![\cdot]\\!]_{\Sigma}$ can be extracted.

This can become problematic when trying to translate a known presentation to a
desired generator set. Assume that $\langle\Pi\mid Q\rangle$ is a known
presentation with a semantic interpretation $[\\![\cdot]\\!]_{\Pi}:\Pi\to H$,
from with a presentation $\langle\Sigma\mid R\rangle$ is derivable via a
sequence of Tietze transformations. One would hope that after each Tietze
transformation, the semantic interpretation continues to induce an injection,
so that Theorem A.6 continues to hold. Furthermore, one would hope that after
all of the Tietze transformations, $[\\![\cdot]\\!]_{\Sigma}$ is a valid
semantic interpretation.

It will be shown that under reasonable assumptions, all Tietze transformations
satisfy these assumptions. The first concern is answered by Theorem A.3 and
Theorem A.4, which state that after each Gen($+$) or Gen($-$) transformation,
$[\\![\cdot]\\!]_{\Pi}$ continues to induce a monoid homomorphism (resp.
injection, surjection, isomorphism). The only time injectivity might fail is
after a new generator is added. In Gen($+$), the symbol $x\in\Sigma$ becomes
an alias for $w\in\Pi^{*}$. Then it suffices to check that
$[\\![x]\\!]_{\Sigma}=[\\![w]\\!]^{*}_{\Pi}$.

##  Appendix B From Derivations to Tietze Transformations

This section describes higher-level structures to reason about Tietze
transformations. It is proven that each structure corresponds to a valid
sequence of Tietze transformations, and is therefore sound for the isomorphism
of finite monoid presentations. The structures described in this section are
used throughout Section 4 and Section 5.

###  B.1 Digraphs and Termination

This section reviews the basics of directed graphs. A directed graph is a
tuple $(V,E)$ such that $V\subseteq E\times E$. A vertex $v$ is a _child_ of
$u$ if $(u,v)\in E$. A vertex $v$ is a _parent_ of $u$ if $(v,u)\in E$. A
_path_ in $(V,E)$ is some sequence $(u_{0},u_{1},\ldots,u_{n})$ over $V$ such
that $(u_{k-1},u_{k})\in E$ for all $k\in\\{1,2,\ldots,n\\}$. A directed graph
$(V,E)$ is _acyclic_ if $u_{0}\neq u_{n}$ for all paths
$(u_{0},u_{1},\ldots,u_{n})$ in $(V,E)$.

######  Lemma B.1 ([7, Sect. 2.2]).

If a digraph $(V,E)$ is finite and acyclic, then for every vertex $v\in V$,
there exists some path of length $n$ ending (resp. starting) at $v$ such that
every path ending (resp. starting) at $v$ has length at most $n$. In
particular, there exists a vertex $v\in V$ such that $v$ has no children
(resp. parents) in $(V,E)$.

Note that the original statement of Lemma B.1 concerned the termination of
abstract rewriting systems (which can be modelled using paths through
digraphs). In the proofs that follow, this intuition is useful to keep in
mind. Indeed, Lemma B.1 is used to argue that certain rewriting procedures
terminate, though the rewriting systems are never stated explicitly for
simplicity.

###  B.2 Derived Generators and Tietze Transformations

${{{X}_{1}}}$${{{C{Z}}_{{0},{1}}}}$${{{Z}_{1}}}$${{{C{X}}_{{2},{0}}}}$${{{C{X}}_{{2},{1}}}}$${{{C{X}}_{{1},{2}}}}$${{{C{Z}}_{{0},{2}}}}$${{{Z}_{0}}}$${{{C{X}}_{{1},{0}}}}$${{K_{0,1}}}$${{\sigma_{0,2}}}$${{{C{X}}_{{0},{2}}}}$${{\sigma_{1,2}}}$${{{C{Z}}_{{1},{2}}}}$${{{Z}_{2}}}$${{\sigma_{0,1}}}$${{{CC{X}}_{{0},{2}}}}$${{{CC{X}}_{{0},{1}}}}$${{{X}_{2}}}$
Figure 9: The derived generator graph for the defining relations in $R_{0}$.

In Section 4.1, it was claimed that $19$ of the generators in $\Sigma_{D}$
could be introduced freely, because their defining relations formed an acyclic
dependency graph. Later, in Appendix E, the same argument was used to remove
these $19$ generators from the generating set for $W(E_{8})$. Similar
arguments appear throughout Section 5. The goal of this section is to
establish both directions rigorously. First, formal definitions are given for
defining relations and derived generator graphs (i.e., the graph of
dependencies between the relations). Then, Theorem B.6 and Theorem B.11 are
established to justify the claims of Section 4.1 and Section 4.5 respectively.
Finally, it is shown that these theorems apply to the generators in Section 4.

######  Definition B.2 (Defining Relations).

Let $\Sigma$ be an alphabet. A _$\Sigma$ -defining relation_ for $x\in\Sigma$
is a relation of the form $x\approx w$ where $w\in\Sigma^{*}$. A _family of
$\Sigma$-defining relations for $\Pi\subseteq\Sigma$_ is a set $\\{r_{x}\mid
x\in\Pi\\}$ such that for each $x\in\Pi$, $r_{x}$ is a $\Sigma$-defining
relation for $x$.

######  Definition B.3 (Derived Generator Graph).

Let $D$ be a family of $\Sigma$-defining relations for $\Pi\subseteq\Sigma$.
The _derived generator graph for $D$_ is the digraph $\Gamma_{D}(D):=(\Pi,E)$
such that $(x,y)\in E$ if and only if there exists $w,w^{\prime}\in\Sigma^{*}$
such that $x\approx w\cdot y\cdot w^{\prime}$ is a relation in $D$.

The proofs of Theorem B.6 and Theorem B.11 both rely heavily on derived
generator graphs. Intuitively, a generator can be introduced (resp.
eliminated) if it has no dependencies (resp. dependants) in the derived
generator graph. It is always possible to find such a generator, provided the
graph is acyclic. However, once a generator has been removed from the defining
relations, it is important that the new derived generator graph is also
acyclic. In fact, the new derived generator graph is always a subgraph of the
previous derived generator graph, as outlined in Lemma B.4.

######  Lemma B.4.

If $D$ is a family of $\Sigma$-defining relations and $D^{\prime}\subseteq D$,
then $\Gamma_{D}(D^{\prime})$ is a subgraph of $\Gamma_{D}(D)$.

###### Proof.

If $D$ is a family of $\Sigma$-defining relations for $\Pi$, then there exists
$\Pi^{\prime}\subseteq\Pi$ such that $D^{\prime}$ is a family of
$\Sigma$-defining relations for $\Pi^{\prime}$. Then $\Gamma_{D}(D)=(\Pi,E)$
and $\Gamma_{D}(D^{\prime})=(\Pi^{\prime},E^{\prime})$ for some
$E\subseteq\Pi\times\Pi$ and $E^{\prime}\subseteq\Pi^{\prime}\times\Pi$. Let
$(x,y)\in E^{\prime}$, Then there exists some $w,w^{\prime}\in\Sigma^{*}$ such
that $x\approx_{D^{\prime}}w\cdot y\cdot w^{\prime}$. Since
$D^{\prime}\subseteq D$, then $x\approx_{D}w\cdot y\cdot y^{\prime}$. Then
$(x,y)\in E$. Since $(x,y)$ was arbitrary, then $E^{\prime}\subseteq E$. Since
$\Pi^{\prime}\subseteq\Pi$ and $E^{\prime}\subseteq E$, then
$\Gamma_{D}(D^{\prime})$ is a subgraph of $\Gamma_{D}(D)$. ∎

####  B.2.1 Introduction of Derived Generators

The goal of this section is to prove Theorem B.6. First, Lemma B.5 is
introduced to prove that every finite set of defining relations with an
acyclic graph must contain at least one defining relation $x\approx w$ whose
right-hand side consists only of primitive generators. Since $w$ is consists
only of primitive generators, then it may be introduced by a Gen($+$)
transformation. The proof then follows by induction on the number of defining
relations, as outlined below.

######  Lemma B.5.

If $D$ is a family of $\Sigma$-defining relations for $\Pi$ with $\Pi$ finite
and $\Gamma_{D}(D)$ acyclic, then there exists a relation $x\approx w$ in $D$
such that $w\in(\Sigma\setminus\Pi)^{*}$.

###### Proof.

Since $\Pi$ is finite and $\Gamma_{D}(D)$ is acyclic, the by Lemma B.1, there
exists some vertex $x\in\Pi$ such that $x$ has no children in $\Gamma_{D}(D)$.
Let $x\approx_{D}w$ be the $\Sigma$-defining relation for $x$ in $D$ with
$n=|w|$. Let $k\in[n]$. Assume for the intent of contradiction that
$w_{k}\in\Pi$. Then there exists some
$w^{\prime},w^{\prime\prime}\in\Sigma^{*}$ such that $w=w^{\prime}\cdot
w_{k}\cdot w^{\prime\prime}$. Then $w_{k}$ is a child of $x$ by definition.
However, $x$ has no children by assumption. Then $w_{k}\not\in\Pi$ by
contradiction. Since $k$ was arbitrary, then $w\in(\Sigma\setminus\Pi)^{*}$. ∎

######  Theorem B.6.

Let $\Sigma\subseteq\widehat{\Sigma}$ be an alphabet with
$\Pi=\widehat{\Sigma}\setminus\Sigma$ finite and
$R\subseteq\Sigma^{*}\times\Sigma^{*}$. If $D$ is a family of
$\widehat{\Sigma}$-defining relations for $\Pi$ with $\Gamma_{D}(D)$ acyclic,
then there exists a length $|\Pi|$ sequence of Gen($+$) transformations
between $\langle\Sigma\mid R\rangle$ and $\langle\widehat{\Sigma}\mid R\cup
D\rangle$.

###### Proof.

The proof follows by induction on $|\Pi|$.

  1. –

Base Case. Assume that $|\Pi|=0$. Then $|D|=0$ and $\langle\Sigma\mid
R\rangle=\langle\Sigma^{\prime}\mid R\cup D\rangle$. Then there exists a
length $0$ sequence of Gen($+$) transformations between $\langle\Sigma\mid
R\rangle$ and $\langle\widehat{\Sigma}\mid R\cup D\rangle$.

  2. –

Inductive Hypothesis. Assume that for some $k\in\mathbb{N}$, if $|\Pi|=k$ and
$\Pi_{D}(D)$ is acyclic, then there exists a length $k$ sequence of Gen($+$)
transformations between $\langle\Sigma\mid R\rangle$ and
$\langle\widehat{\Sigma}\mid R\cup D\rangle$.

  3. –

Inductive Step. Assume that $|\Pi|=k+1$ and $\Gamma_{D}(D)$ is acylic. Since
$\Pi$ is finite and $\Gamma_{D}(D)$ is acyclic, then by Lemma B.5 there exists
a $\widehat{\Sigma}$-defining relation $x\approx w$ in $D$. Let
$\Lambda=\Sigma\cup\\{x\\}$ and $Q=R\cup\\{x\approx w\\}$. Then
$D\setminus\\{r_{x}\\}$ is a family of $\widehat{\Sigma}$-defining relations
for $\Pi\setminus\\{x\\}$ and $Q\subseteq\Lambda^{*}\times\Lambda^{*}$. Since
$\Gamma_{D}(D\setminus\\{r_{x}\\})$ is a subgraph of $\Gamma_{D}(D)$ by Lemma
B.4 with $\Gamma_{D}(D)$ acyclic, then $\Gamma_{D}(D\setminus\\{r_{x}\\})$ is
also acyclic. Since $|\Pi\setminus\\{x\\}|=|\Pi|-1=k$ and
$\Gamma_{D}(D\setminus\\{r_{x}\\})$ is acyclic, then by the inductive
hypothesis, there exists a length $k$ sequence of Gen($+$) transformations
from $\langle\Lambda\mid Q\rangle$ to $\langle\widehat{\Sigma}\mid R\cup
D\rangle$. Furthermore, $\langle\Sigma\mid R\rangle\cong\langle\Lambda\mid
Q\rangle$ by Gen($+$). Then there exists a length $k+1$ sequence of Gen($+$)
transformations between $\langle\Sigma\mid D\rangle$ and
$\langle\widehat{\Sigma}\mid R\cup D\rangle$.

By the principle of induction, there exists a length $|\Pi|$ sequence of
Gen($+$) transformations between $\langle\Sigma\mid D\rangle$ and
$\langle\Sigma^{\prime}\mid R\cup D\rangle$. ∎

####  B.2.2 Tietze Transformations to Exchange Relations

The goal of this section is to introduce a technique necessary to prove that
derived generators can be eliminated via finite sequences of Tietze
transformations. Using the Tietze transformations discussed so far, it is
possible to remove and introduce redundant relation. In practice, one often
wishes to replace a relation $q\approx w$ with a relation $q^{\prime}\approx
w^{\prime}$, where neither $q\approx w$ nor $q^{\prime}\approx w^{\prime}$ is
redundant without the other relation. The following lemma gives a sufficient
condition for when $q\approx w$ can be exchanged with $q^{\prime}\approx
w^{\prime}$, and provides an upper bound on the number of Tietze
transformations required to carry out the exchange.

######  Lemma B.7.

Let $G=\langle\Sigma\mid R\rangle$ be a presentation with $q\approx w$ in $R$
and $Q=R\setminus\\{q\approx w\\}$. If there exists $q^{\prime}\in\Sigma^{*}$
and $w^{\prime}\in\Sigma^{*}$ such that $q\sim_{Q}q^{\prime}$ and
$w\sim_{Q}w^{\prime}$, then there exists a finite sequence of Tietze
transformations between $G$ and $\langle\Sigma\mid Q\cup\\{q^{\prime}\approx
w^{\prime}\\}\rangle$ of length between $1$ and $2$.

###### Proof.

Let $S=R\cup\\{q^{\prime}\approx w^{\prime}\\}$ and
$T=Q\cup\\{q^{\prime}\approx w^{\prime}\\}$. If
$q^{\prime}\approx_{R}w^{\prime}$, then $\langle\Sigma\mid
R\rangle=\langle\Sigma\mid S\rangle$. Assume instead that $q\not\approx_{R}w$.
Since $Q\subseteq R$, then $q\sim_{R}q^{\prime}$ and $w\sim_{R}w^{\prime}$.
Then $q^{\prime}\sim_{R}q$ by the symmetry of $(\sim_{R})$. Since
$q^{\prime}\sim_{R}q$, $q\sim_{R}w$, and $w\sim_{R}w^{\prime}$, then
$q^{\prime}\sim_{R}w^{\prime}$ by transitivity. Then $\langle\Sigma\mid
R\rangle\cong\langle\Sigma\mid S\rangle$ by a single Rel($+$) transformation.
In either case, there exists a sequence of Tietze transformations between
$\langle\Sigma\mid R\rangle$ and $\langle\Sigma\mid S\rangle$ of length at
most one. Since $Q\subseteq T$, then $q\sim_{T}q^{\prime}$ and
$w\sim_{T}w^{\prime}$. Then $w^{\prime}\sim_{T}w$ by the symmetry of
$(\sim_{T})$. Since $q\sim_{T}q^{\prime}$, $q^{\prime}\sim_{T}w^{\prime}$, and
$w^{\prime}\sim_{T}w$, then $q\sim_{T}w$ by the transitivity of $(\sim_{S})$.
Since $S\neq T$, then $\langle\Sigma\mid S\rangle\cong\langle\Sigma\mid
T\rangle$ by a single Rel($+$) transformation. In conclusion, there exists a
sequence of Tietze transformations between $\langle\Sigma\mid R\rangle$ and
$\langle\Sigma\mid S\rangle$ of length at between $1$ and $2$. ∎

####  B.2.3 Elimination of Derived Generators

The goal of this section is to prove Theorem B.11. The first step in this
proof is to show that the set of relations can be replaced by $Q\cup D$ where
$Q$ is a set of relations over the primitive generators and $D$ is the set of
defining relations. This follows by induction in Lemma B.9, where Lemma B.8 is
used to find new relations of the form, and then Lemma B.7 is used to exchange
the relations. The second step in this proof is to show that the derived
generators can be eliminated through a finite sequence of Tietze
transformations. This follows by induction in Theorem B.11, where Lemma B.10
is used to find a derived generator upon which non other derived generator
depends. Such a generator is necessarily redundant, and may be eliminated via
a Rel($-$) transformation.

######  Lemma B.8.

Let $\Sigma\setminus\widehat{\Sigma}$ be an alphabet with
$\Pi=\widehat{\Sigma}\setminus\Sigma$. If $D$ is a family of
$\widehat{\Sigma}$-defining relations for $\Pi$ with $\Gamma_{D}(D)$ acyclic,
then for each $w\in\Sigma^{*}$, there exists some
$w^{\prime}\in(\Sigma^{\prime})^{*}$ such that $w\sim_{D}w^{\prime}$.

###### Proof.

The proof follows by induction on the size of $\Pi$.

  1. –

Base Case. Assume that $|\Pi|=0$ and $w\in\widehat{\Sigma}^{*}$. Then
$\Pi=\varnothing$ and $w\in\Sigma^{*}$. Since $w\sim_{D}w$ by the symmetry of
$(\sim_{D})$, then there exists some $w^{\prime}\in\Sigma^{*}$ such that
$w\sim_{D}w^{\prime}$.

  2. –

Inductive Hypothesis. Assume that for some $k\in\mathbb{N}$, if $|\Pi|=k$,
$\Gamma_{D}(D)$ is acyclic, and $w\in\widehat{\Sigma}^{*}$, then there exists
some $w^{\prime}\in\Sigma^{*}$ such that $w\sim_{D}w^{\prime}$.

  3. –

Inductive Step. Assume that $|\Pi|=k+1$ and $\Gamma_{D}(D)$ is acyclic. Since
$\Pi$ is finite and $\Gamma_{D}(D)$ is acyclic, then by Lemma B.10, there
exists a $\widehat{\Sigma}$-defining relation $x\approx q$ in $D$ such that
$D\setminus\\{r_{x}\\}$ is a family of
$(\widehat{\Sigma}\setminus\\{x\\})$-defining relations for
$\Pi\setminus\\{x\\}$. Then by Lemma A.2, there exists some
$w^{\prime}\in(\widehat{\Sigma}\setminus\\{x\\})^{*}$ such that
$w\sim_{D}w^{\prime}$. Since $\Gamma_{D}(D\setminus\\{r_{x}\\})$ is a subgraph
of $\Gamma_{D}(D)$ by Lemma B.4 with $\Gamma_{D}(D)$ acyclic, then
$\Gamma_{D}(D\setminus\\{r_{x}\\})$ is also acyclic. Then
$D\setminus\\{r_{x}\\}$ is a family of
$(\widehat{\Sigma}\setminus\\{x\\})$-defining relations for
$\Pi\setminus\\{x\\}$ with $\Gamma_{D}(D)$ acyclic and
$w^{\prime}\in(\widehat{\Sigma}\setminus\\{x\\})^{*}$. Since
$|\Pi\setminus\\{x\\}|=|\Pi|-1=k$, then by the inductive hypothesis, there
exists some $w^{\prime\prime}\in\Sigma^{*}$ such that
$w^{\prime}\sim_{D^{\prime}}w^{\prime\prime}$. Since $D^{\prime}\subseteq D$,
then $w^{\prime}\sim_{D}w^{\prime\prime}$. Since $\sim_{D}$ is transitive,
then $w\sim_{D}w^{\prime\prime}$. Then there exists a
$w^{\prime\prime}\in\Sigma^{*}$ such that $w\sim_{D}w^{\prime\prime}$.

Since $\Gamma_{D}(D)$ is acyclic, then by the principle of induction, there
exists a $w^{\prime}\in\Sigma^{*}$ such that $w\sim_{D}w^{\prime}$. ∎

######  Lemma B.9.

Let $\Sigma\subseteq\widehat{\Sigma}$ be an alphabet with
$\Pi=\widehat{\Sigma}\setminus\Sigma$ and
$R\subseteq\widehat{\Sigma}^{*}\times\widehat{\Sigma}^{*}$ finite. If
$D\subseteq R$ is a family of $\widehat{\Sigma}$-defining relations for $\Pi$
with $\Gamma_{D}(D)$ acyclic, then there exists a
$Q\subseteq\Sigma^{*}\times\Sigma^{*}$ with $|Q|\leq|R\setminus D|$ and a
finite sequence of Tietze transformations between $\langle\widehat{\Sigma}\mid
R\rangle$ and $\langle\widehat{\Sigma}\mid Q\cup D\rangle$ of length between
$k$ and $2k$ where $k=|R|-|R\cap(\Sigma^{*}\times\Sigma^{*})|-|D|$.

###### Proof.

Let $S=R\cap(\Sigma^{*}\times\Sigma^{*})$ and $\overline{S}=R\setminus(S\sqcup
D)$. Then $R=S\sqcup D\sqcup\overline{S}$. The proof follows by induction on
$|\overline{S}|$ in this decomposition.

  1. –

Base Case. Assume that $R$ decomposes into $S\sqcup D\sqcup\overline{S}$ with
$|\overline{S}|=0$. Then $\langle\widehat{\Sigma}\mid
R\rangle=\langle\widehat{\Sigma}\mid S\cup D\rangle$. Then there exists a
length $0$ sequence of Tietze transformations between
$\langle\widehat{\Sigma}\mid R\rangle$ and $\langle\widehat{\Sigma}\mid S\cup
D\rangle$. Clearly $|S|=|R\setminus D|$.

  2. –

Inductive Hypothesis. Assume that for some $k\in\mathbb{N}$, if $R$ decomposes
as $S\sqcup D\sqcup\overline{S}$ with $|\overline{S}|=k$, then there exists
some $Q\subseteq\Sigma^{*}\times\Sigma^{*}$ with $|Q|\leq|R\setminus D|$ and a
sequence of Tietze transformations between $\langle\widehat{\Sigma}\mid
R\rangle$ and $\langle\widehat{\Sigma}\mid Q\cup D\rangle$ of length at most
$2k$.

  3. –

Inductive Step. Assume that $R$ decomposes into $S\sqcup D\sqcup\overline{S}$
with $|\overline{S}|=k+1$. Let $q\approx w$ in $\overline{S}$. Then by Lemma
B.8, there exists $q^{\prime}\in\Sigma^{*}$ and $r^{\prime}\in\Sigma^{*}$ such
that $q\sim_{D}q^{\prime}$ and $r\sim_{D}r^{\prime}$. Then by Lemma B.7, there
exists a finite sequence of Tietze transformations between
$\langle\widehat{\Sigma}\mid R\rangle$ and $\langle\widehat{\Sigma}\mid
R^{\prime}\rangle$ of length between $1$ and $2$, where
$R^{\prime}=R\cup\\{q^{\prime}\approx w^{\prime}\\}\setminus\\{q\approx w\\}$.
Then $R^{\prime}$ decomposes as $S^{\prime}\sqcup
D\sqcup\overline{S}^{\prime}$ where $S^{\prime}=S\cup\\{q^{\prime}\approx
r^{\prime}\\}$ and $\overline{S}^{\prime}=\overline{S}\setminus\\{q\approx
r\\}$. Since $q\approx_{S}r$, then
$|\overline{S}^{\prime}|=|\overline{S}|-1=k$. Then the inductive hypothesis
holds, and there exists some $Q\subseteq\Sigma^{*}\times\Sigma^{*}$ with
$|Q|\leq|R^{\prime}\setminus D|$ and a sequence of Tietze transformations
between $\langle\widehat{\Sigma}\mid R^{\prime}\rangle$ and
$\langle\widehat{\Sigma}\mid Q\cup D\rangle$ of length between $k$ and $2k$.
Then there exists a sequence of Tietze transformations between
$\langle\widehat{\Sigma}\mid R\rangle$ and $\langle\widehat{\Sigma}\mid Q\cup
D\rangle$ of length between $k+1$ and $2(k+1)$. Since $|S^{\prime}|\leq|S|$
and $|\overline{S}^{\prime}|=|\overline{S}|$, then
$|Q|\leq|S^{\prime}|+|\overline{S}^{\prime}|\leq|S|+|\overline{S}|=|R\setminus
D|$.

By the principle of induction, there exists a
$Q\subseteq\Sigma^{*}\times\Sigma^{*}$ with $|Q|\leq|R\setminus D|$ and a
sequence of Tietze transformations between $\langle\widehat{\Sigma}\mid
R\rangle$ and $\langle\widehat{\Sigma}\mid Q\cup D\rangle$ of length between
$|\overline{S}|$ and $2|\overline{S}|$. ∎

######  Lemma B.10.

If $D$ is a family of $\Sigma$-defining relations for $\Pi$ with $\Pi$ finite
and $\Gamma_{D}(D)$ acyclic, then there exists a relation $x\approx w$ in $D$
such that $D\setminus\\{x\approx w\\}$ is a family of
$(\Sigma\setminus\\{x\\})$-defining relations for $\Pi\setminus\\{x\\}$.

###### Proof.

Since $\Pi$ is finite and $\Gamma_{D}(D)$ is acyclic, then by Lemma B.1, there
exists some vertex $x\in\Pi$ such that $x$ has no parents in $\Gamma_{D}(D)$.
Since $x$ is a vertex in $\Gamma_{D}(D)$, then there exists a
$\Sigma$-defining relation $x\approx w$ in $D$. Let
$D^{\prime}=D\setminus\\{x\approx w\\}$. Let $y\approx q$ be a
$\Sigma$-defining relation in $D^{\prime}$ with $n=|q|$. Let $k\in[n]$. Assume
for the intent of contradiction that $q_{k}=x$. Then there exists some
$q^{\prime},q^{\prime\prime}\in\Sigma^{*}$ such that $q=q^{\prime}\cdot x\cdot
q^{\prime\prime}$. Then $x$ is a child of $y$ by definition. However, $x$ has
no parents by assumption. Then $q_{k}\neq x$ by contradiction. Since $k$ was
arbitrary, then $q\in(\Sigma\setminus\\{x\\})^{*}$. Since $y\approx q$ was
arbitrary, then $D^{\prime}$ is a family of
$(\Sigma\setminus\\{x\\})$-defining relations for $\Pi\setminus\\{x\\}$. ∎

######  Theorem B.11.

Let $\Sigma^{\prime}\subseteq\Sigma$ be an alphabet with
$\Pi=\Sigma\setminus\Sigma^{\prime}$ finite and
$R\subseteq\Sigma^{*}\times\Sigma^{*}$ finite. If $D\subseteq R$ is a family
of defining relations for $\Pi$ with $\Gamma_{D}(D)$ acyclic, then there
exists a $Q\subseteq(\Sigma^{\prime})^{*}\times(\Sigma^{\prime})^{*}$ with
$|Q|\leq|R\setminus D|$ and a sequence of Tietze transformations between
$\langle\Sigma\mid R\rangle$ and $\langle\Sigma^{\prime}\mid Q\rangle$ of
length between $n+k$ and $2n+k$ where
$n=|R|-|R\cap((\Sigma^{\prime})^{*}\times(\Sigma^{\prime})^{*})|-|D|$ and
$k=|\Pi|$.

###### Proof.

By Lemma B.9, there exists a
$Q\subseteq(\Sigma^{\prime})^{*}\times(\Sigma^{\prime})^{*}$ with
$|Q|\leq|R\setminus D|$ and a sequence of Tietze transformations between
$\langle\Sigma\mid R\rangle$ and $\langle\Sigma\mid Q\cup D\rangle$ of length
between $n$ and $2n$. The proof follows by induction on $|\Pi|$.

  1. –

Base Case. If $|\Pi|=0$, then $|D|=0$. Then $\langle\Sigma\mid Q\cup
D\rangle=\langle\Sigma^{\prime}\mid Q\rangle$. Then there exists a length $0$
sequence of Tietze transformations between $\langle\Sigma\mid Q\cup D\rangle$
and $\langle\Sigma^{\prime}\mid Q\rangle$.

  2. –

Inductive Case. Assume that for some $k\in\mathbb{N}$, if $|\Pi|=k$ and
$\Pi_{D}(D)$ is acyclic, then there exists a length $k$ sequence of Tietze
transformations between $\langle\Sigma\mid Q\cup D\rangle$ and
$\langle\Sigma^{\prime}\mid Q\rangle$.

  3. –

Inductive Step. Assume that $|\Pi|=k+1$ and $\Gamma_{D}(D)$ is acyclic. Since
$\Pi$ is finite and $\Gamma_{D}(D)$ is acyclic, then by Lemma B.1 there exists
some vertex $x\in\Pi$ such that $x$ has no parents in $\Gamma_{D}(D)$. Define
$\Lambda=\Sigma\setminus\\{x\\}$ and $D^{\prime}=D\setminus\\{r_{x}\\}$. Let
$y\approx_{D^{\prime}}w$ and assume for the intent of contradiction that
$w\not\in\Lambda^{*}$. Then there exists
$w^{\prime},w^{\prime\prime}\in\Sigma^{*}$ such that $w=w^{\prime}\cdot x\cdot
w^{\prime\prime}$. Then $x$ is a child of $y$ in $\Gamma_{D}(D)$. However, $x$
has no parents by assumption. Then $w\in\Lambda^{*}$ by contradiction. Since
$y\approx_{D^{\prime}}w$ was arbitrary, then
$D^{\prime}\subseteq\Lambda^{*}\times\Lambda^{*}$. Then $Q\cup
D^{\prime}\subseteq\Lambda^{*}\times\Lambda^{*}$. It follows that
$\langle\Sigma\mid Q\cup D\rangle\cong\langle\Lambda\mid Q\cup
D^{\prime}\rangle$ by Gen($-$). Furthermore, $D^{\prime}$ is a family of
defining relations for $\Pi\setminus\\{x\\}$. Since $|\Pi\setminus\\{x\\}|=k$
and $\Gamma_{D}(D^{\prime})$ is acyclic by Lemma B.4, then there exists a
length $k$ sequence of Tietze transformations between $\langle\Lambda\mid
Q\cup D^{\prime}\rangle$ and $\langle\Sigma^{\prime}\mid Q\rangle$ by the
inductive hypothesis. Then there exists a length $k+1$ sequence of Tietze
transformations between $\langle\Sigma\mid R\rangle$ and
$\langle\Sigma^{\prime}\mid Q\rangle$.

Then by the principle of induction, there exists a length $k$ sequence of
Tietze transformations between $\langle\Sigma\mid Q\cup D\rangle$ and
$\langle\Sigma^{\prime}\mid Q\rangle$. Then there exists a sequence of Tietze
transformations between $\langle\Sigma\mid R\rangle$ and
$\langle\Sigma^{\prime}\mid Q\rangle$ of length between $n+k$ and $2n+k$. ∎

####  B.2.4 The Derived Generator Graph for $W(E_{8})$

The derived generators for $W(E_{8})$ are
$\Pi:=\Sigma_{D}\setminus\\{{X}_{0},{C{X}}_{{0},{1}},{CC{X}}_{{1},{2}},K_{1,2}\\}$.
The defining relations $D\subseteq R_{0}$ for $\Pi\subseteq\Sigma_{D}$ are
given by Relation 1 through to Relation 19 in Figure 4. An illustration of the
derived generator graph $\Gamma_{D}(D)$ can be found in Figure 9. Since this
graph is acyclic, then Theorem B.6 and Theorem B.11 apply. The derived
generator graphs for $O(n,\mathbb{D})$ have paths of length at most one, and
are therefore trivially acyclic.

###  B.3 Derivational Proofs and Tietze Transformation

Assume that $G\cong\langle\Sigma\mid R\rangle$ with semantic interpretation
$[\\![\cdot]\\!]_{G}$. During proofs based on Tietze transformations, it is
often necessary to find a sequence of Rel($-$) and Rel($+$) transformations
between $\langle\Sigma\mid R\rangle$ and $\langle\Sigma\mid Q\rangle$. For
example, this case arises in Section 4, where $R=R_{E8}\cup R_{D(E8)}$ and
$Q=R_{E8(D)}\cup R_{D}$. If $[\\![\cdot]\\!]_{G}$ induces an isomorphism and
every relation $w\approx_{Q}w^{\prime}$ satisfies
$[\\![w]\\!]^{*}=[\\![w^{\prime}]\\!]$, then using Theorem A.6 there exists a
sequence of Tietze transformations between $\langle\Sigma\mid R\rangle$ and
$\langle\Sigma\mid R\rangle$. Eliminating the relations in $R$ requires more
care. For example, if $r\in R$ is not derivable from $(R\cup
Q)\setminus\\{r\\}$, then $\langle\Sigma\mid R\cup Q\rangle$ is a proper
quotient of $\langle\Sigma\mid Q\rangle$. Instead, it must be shown that for
each $w\approx_{R}w^{\prime}$, it follows that $w\sim_{Q}w^{\prime}$. One way
to approach this problem is to first derive some auxiliary relations $A$ from
$Q$, and then use $Q\cup A$ to derive $R$. However, transforming these
derivations into a sequence of Tietze transformations is often tedious, and
not well-aligned with the process of proof discovery. On the other hand, if
the derivations are not transformed into a valid sequence of Tietze
transformations, then it is possible to obtain invalid proofs, such as those
with cyclic derivations (see Example B.16).

This section formalizes the ad-hoc proof technique described above,and
identifies sufficient conditions for when such a family of derivations induces
a valid sequence of Tietze transformations between $\langle\Sigma\mid
R\rangle$ and $\langle\Sigma\mid Q\rangle$. In the following definitions,
$L(\Sigma)=\mathbb{N}\times(\Sigma^{*}\times\Sigma^{*})$ will represent a set
of indexed relations over $\Sigma$. For example, let $(n,(w,w^{\prime}))\in
L(\Sigma)$. The index $n$ in $(n,(w,w^{\prime}))$ indicates that
$(n,(w,w^{\prime}))$ is a derived relation, and allows for multiple
derivations of the same relation. More concretely, if $n=3$, $w=a\cdot b$, and
$w^{\prime}=x\cdot y\cdot z$, then $(n,(w,w^{\prime}))$ is the third
derivation that yields $a\cdot b\approx x\cdot y\cdot z$.

######  Definition B.12 (Derivational Proof).

A _derivational proof in $\langle\Sigma\mid R\rangle$_ is a subset $P\subseteq
L(\Sigma)\times(L(\Sigma)\cup R)^{*}$ which satisfies the following
conditions.

  * –

Indexed. For all $(\ell,d)\in P$ and $(\ell^{\prime},d^{\prime})\in P$
distinct, $\ell\neq\ell^{\prime}$.

  * –

Well-founded. For all $(\ell,d)\in P$ and $k\in\\{1,2,\ldots,|d|\\}$, either
$d_{k}\in R$ or $d_{k}\in L(\Sigma)$ and there exists some
$d^{\prime}\in(L(\Sigma)\cup R)^{*}$ such that $(d_{k},d^{\prime})\in P$.

  * –

Valid. For all $(\ell,d)\in P$ with $(n,(w,w^{\prime}))=\ell$ and $m=|d|$,
there exists some $v\in(\Sigma^{*}){}^{m+1}$ such that $v_{1}=w$,
$v_{m+1}=w^{\prime}$, and for all $k\in[m]$ either $d_{k}\in R$ and
$v_{k}\xrightarrow{d_{k}}v_{k+1}$ or $(n^{\prime},r)=d_{k}$ and
$v_{k}\xrightarrow{r}v_{k+1}$.

A set $Q\subseteq\Sigma^{*}\times\Sigma^{*}$ is _entailed by $P$_, written
$P\models Q$, if $Q\subseteq R\cup\\{r\mid((n,r),d)\in P\\}$.

######  Definition B.13 (Proof Substitution).

Let $P$ be a proof in $\langle\Sigma\mid R\rangle$. If $(\ell,d)\in P$,
$d\in(L(\Sigma)\cup R)^{*}$, and
$P^{\prime}=(P\setminus\\{(\ell,d)\\})\cup\\{(\ell,d^{\prime})\\}$ is a proof
for $\langle\Sigma\mid R\rangle$, then we say that $P^{\prime}$ is a
_substitution of $P$ by $d^{\prime}$ at $\ell$_, written $P[\ell\mapsto
d^{\prime}]$.

######  Definition B.14 (Derivation Graph).

Let $P$ be a proof in $\langle\Sigma\mid R\rangle$. The _derivation graph for
$P$_ is the digraph $\Gamma_{D}(P)=(V,E)$ such that $V=\\{\ell\mid(\ell,d)\in
P\\}$ and $(\ell,\ell^{\prime})\in E$ if and only if there exists $(\ell,d)\in
P$ and $k\in\\{1,2,\ldots,|d|\\}$ such that $d_{k}=\ell^{\prime}$.

######  Example B.15 (Derivations and Substitutions).

Consider $G=\langle x,y\mid x^{2}\approx\epsilon,y^{2}\approx\epsilon\rangle$.
It is not hard to show $x\cdot y\cdot x\cdot y^{2}\cdot x\cdot y\cdot
x\sim\epsilon$. However, it helps to first prove that $x\cdot y^{2}\cdot
x\sim\epsilon$. This can be written as a derivation proof. There will be two
derivations, with labels $\ell=(0,(x\cdot y^{2}\cdot x,\epsilon))$ and
$\ell^{\prime}=(0,(x\cdot y\cdot x\cdot y^{2}\cdot x\cdot y\cdot x,\epsilon))$
respectively. Associated with $\ell$ and $\ell^{\prime}$ are two derivations
$d$ and $d^{\prime}$, defined as follows. Let $r=(x^{2},\epsilon)$ and
$r^{\prime}=(y^{2},\epsilon)$.

$\displaystyle(d):$ $\displaystyle\;\;x\cdot y\cdot y\cdot
x\xrightarrow{r^{\prime}}x\cdot x\xrightarrow{r}\epsilon$
$\displaystyle(d^{\prime}):$ $\displaystyle\;\;x\cdot y\cdot x\cdot y\cdot
y\cdot x\cdot y\cdot x\xrightarrow{\ell}x\cdot y\cdot y\cdot
x\xrightarrow{\ell}\epsilon$

These pieces can be assembled into a derivational proof
$P=\\{(\ell,d),(\ell^{\prime},d^{\prime})\\}$. This proof is indexed, since
$\ell$ and $\ell^{\prime}$ each appear exactly once as labels. This proof is
well-formed, since $r$, $r^{\prime}$, $d$, and $d^{\prime}$ are all in-scope.
The proof is valid, since each step of each derivation follows. Of course, it
is possible to expand out $d^{\prime}$ using the steps of $d$. This yields a
new derivation $d^{\prime\prime}$ defined as follows.

$(d^{\prime\prime}):\;\;x\cdot y\cdot x\cdot y\cdot y\cdot x\cdot y\cdot
x\xrightarrow{r^{\prime}}x\cdot y\cdot x\cdot x\cdot y\cdot
x\xrightarrow{r}x\cdot y\cdot y\cdot x\xrightarrow{r^{\prime}}x\cdot
x\xrightarrow{r}\epsilon$

This new derivational proof corresponds to the substitution
$P[\ell^{\prime}\mapsto d^{\prime\prime}]$. In this new proof, the derivation
of $\ell^{\prime}$ no longer relies on the lemma $\ell$. Later in this
section, lemma eliminating substitutions will be used to extract Tietze
transformations from derivational proofs with acyclic derivation graphs. ∎

######  Example B.16 (Cyclic Derivations).

Consider $G=\langle x,y\mid x^{2}\approx\epsilon,y^{2}\approx\epsilon\rangle$.
It is not hard to show that $G\cong\mathbb{Z}_{2}\star\mathbb{Z}_{2}$, where
$(\star)$ denotes the free product of groups. It follows that $G$ is non-
abelian. In particular, $\pi_{G}(x\cdot y)\neq\pi_{G}(y\cdot x)$. Now,
consider the proof $P=\\{((0,(x\cdot y,y\cdot x)),d),((0,(x\cdot y^{3},y\cdot
x\cdot y)),d^{\prime})\\}$, where $d$ and $d^{\prime}$ are defined as follows.
Let $r=(y^{2},\epsilon)$, $\ell=(0,(x\cdot y,y\cdot x))$ and
$\ell^{\prime}=(0,(x\cdot y^{3},y\cdot x\cdot y^{2}))$.

$\displaystyle(d):$ $\displaystyle\;\;x\cdot y\xleftarrow{r}x\cdot
y^{3}\xrightarrow{\ell^{\prime}}y\cdot x\cdot y^{2}\xrightarrow{r}y\cdot x$
$\displaystyle(d^{\prime}):$ $\displaystyle\;\;x\cdot
y^{3}\xrightarrow{\ell}y\cdot x\cdot y^{2}$

This proof is indexed, well-formed, and valid. However, these derivations
suggest that $x\cdot y\sim y\cdot x$. The problem in this proof is that $d$
depends on $d^{\prime}$ and $d^{\prime}$ depends on $d$. In other words, the
proof is self-referential. It will be shown later in this section that if
$\Gamma_{D}(P)$ is acyclic, then $P$ is not self-referential. This motivates
the requirement that $\Gamma_{D}(P)$ is acyclic throughout the rest of this
section. ∎

####  B.3.1 Substitutions and Derivation Graphs

This section relates derivational proofs and substitutions to the derivation
graphs they induce. When a derivation $(\ell,d)$ depends on a derivation
$(\ell^{\prime},d^{\prime})$, we say that $\ell^{\prime}$ is a lemma for
$\ell$. In Lemma B.17, lemma-free derivations are characterized by their
vertices in a derivation graph. Similarly, Lemma B.18 characterizes lemma-free
proofs in terms of their derivation graphs. As expected, Lemma B.19 shows that
if a substitution only eliminates the use of lemmas, such as in Example B.15,
then the resulting derivation graph is a subgraph of the original graph. To
this end, Lemma B.20 provides sufficient conditions for a valid substitution.
Together, these four lemmas give a graph-theoretic characterization of the
lemma substitution in Example B.15.

######  Lemma B.17.

Let $P$ be a proof for $\langle\Sigma\mid R\rangle$. If $(\ell,d)\in P$ and
$\ell$ has no children in $\Gamma_{D}(P)$, then $d\in R^{*}$.

###### Proof.

Let $k\in\\{1,2,\ldots,|d|\\}$. Assume for the intent of contradiction that
$d_{k}\not\in R^{*}$. Then $(\ell,d_{k})$ is an edge in $\Gamma_{D}(P)$.
However, $\ell$ has no children in $\Gamma_{D}(P)$. Then $d_{k}\in R$. Since
$k$ was arbitrary, then $d\in R^{*}$. ∎

######  Lemma B.18.

If $P$ is a proof for $\langle\Sigma\mid R\rangle$, then $\Gamma_{D}(P)$ is
edgeless if and only if $d\in R^{*}$ for all $(\ell,d)\in P$.

###### Proof.

Let $\Gamma_{D}(P)=(V,E)$. Consider the contrapositive statement. Then there
exists an $(\ell,\ell^{\prime})\in E$. This is true if and only if there
exists a $(\ell,d)\in P$ and $k\in\\{1,2,\ldots,|d|\\}$ such that
$d_{k}=\ell^{\prime}$. This is true if and only if there exists an
$(\ell,d)\in P$ such that $d\not\in R^{*}$. ∎

######  Lemma B.19.

Let $P$ be a proof for $\langle\Sigma\mid R\rangle$ and $(V,E)=\Gamma_{D}(P)$.
If $(\ell,d)\in P$ and there exists some $d^{\prime}\in R^{*}$ such that
$P^{\prime}=P[l\mapsto d^{\prime}]$ is also a proof for $\langle\Sigma\mid
R\rangle$, then $\Gamma_{D}(P^{\prime})=(V,E_{\ell})$ where
$E_{\ell}=\\{(\ell^{\prime},\ell^{\prime\prime})\in
E\mid\ell\neq\ell^{\prime}\\}$.

###### Proof.

Let $\Gamma_{D}(P^{\prime})=(V^{\prime},E^{\prime})$.

  1. –

Vertices ($\subseteq$). Let $\ell^{\prime}\in V^{\prime}$. Then there exists
some $\delta\in(L(\Sigma)\cup R)^{*}$ such that $(\ell^{\prime},\delta)\in
P^{\prime}$. Then either $(\ell^{\prime},\delta)\in P$ or
$(\ell^{\prime},\delta)=(\ell,d^{\prime})$. If $(\ell^{\prime},\delta)\in P$,
then $\ell\in V$. If $(\ell^{\prime},\delta)=(\ell,d^{\prime})$, then
$\ell^{\prime}\in V$ since $(\ell,d)\in P$. In either case $\ell^{\prime}\in
V$. Since $\ell^{\prime}$ was arbitrary, then $V^{\prime}\subseteq V$.

  2. –

Vertices ($\supseteq$). Let $\ell^{\prime}\in V$. Then there exists some
$\delta\in(L(\Sigma)\cup R)^{*}$ such that $(\ell^{\prime},\delta)\in P$. Then
either $\ell^{\prime}=\ell$ or $\ell^{\prime}\neq\ell$. If
$\ell^{\prime}=\ell$, then $\ell^{\prime}\in V^{\prime}$ since
$(\ell^{\prime},d^{\prime})\in P^{\prime}$. If $\ell^{\prime}\neq\ell$, then
$\ell^{\prime}\in V^{\prime}$ since $(\ell^{\prime},\delta)\in
P\setminus\\{(\ell,d)\\}$. In either case, $\ell^{\prime}\in V$, Since
$\ell^{\prime}$ was arbitrary, then $V^{\prime}\subseteq V$.

  3. –

Edges ($\subseteq$). Let $(\ell^{\prime},\ell^{\prime\prime})\in E^{\prime}$.
Then there exists some $\delta\in(L(\Sigma)\cup R)^{*}$ and
$k\in\\{1,2,\ldots,|\delta|\\}$ such that $(\ell^{\prime},\delta)\in
P^{\prime}$ and $\delta_{k}=\ell^{\prime\prime}$. Then $\delta\not\in R^{*}$.
Consequently, $\delta\neq d^{\prime}$. Then $\ell\neq\ell^{\prime}$, since
$P^{\prime}$ is indexed. Then $(\ell^{\prime},\delta)\in P$. Consequently,
$(\ell^{\prime},\ell^{\prime\prime})\in E$. Since $\ell^{\prime}\neq\ell$,
then $(\ell^{\prime},\ell^{\prime\prime})\in E_{\ell}$. Since
$(\ell^{\prime},\ell^{\prime\prime})$ was arbitrary, then $E^{\prime}\subseteq
E_{\ell}$.

  4. –

Edges ($\supseteq$). Assume that $(\ell^{\prime},\ell^{\prime\prime})\in
E_{\ell}$. Then $\ell^{\prime}\neq\ell$ and
$(\ell^{\prime},\ell^{\prime\prime})\in E$. Then there exists some
$\delta\in(L(\Sigma)\cup R)^{*}$ and $k\in\\{1,2,\ldots,|\delta|\\}$ such that
$(\ell^{\prime},\delta)\in P$ and $\delta_{k}=v$. Since
$\ell^{\prime}\neq\ell$, then $(\ell^{\prime},\delta)\in P^{\prime}$. Then
$(\ell^{\prime},\ell^{\prime\prime})\in E^{\prime}$. Since
$(\ell^{\prime},\ell^{\prime\prime})$ was arbitrary, then $E_{\ell}\subseteq
E^{\prime}$.

Then $\Gamma_{D}(P^{\prime})=(V,E_{\ell})$. ∎

######  Lemma B.20.

Let $P$ be a proof for $\langle\Sigma\mid R\rangle$ and
$V=\\{\ell\mid(\ell,d)\in P\\}$. If $(\ell,d)\in P$, $d^{\prime}\in(V\cup
R)^{*}$, and $(\ell,d^{\prime})$ is valid, then $P[\ell\mapsto d^{\prime}]$ is
a proof for $\langle\Sigma\mid R\rangle$.

###### Proof.

Let $P^{\prime}=[\ell\mapsto d^{\prime}]$. It must be shown that $P^{\prime}$
is indexed, well-formed, and valid.

  1. –

Indexed. Let $(\ell^{\prime},\delta)\in P^{\prime}$ and
$(\ell^{\prime\prime},\delta^{\prime})\in P^{\prime}$ distinct. Without loss
of generality, assume $\ell^{\prime}\neq\ell$. Then $(\ell^{\prime},\delta)\in
P$. Now, these are two cases to consider, depending on whether
$\ell^{\prime\prime}=\ell$. If $\ell^{\prime\prime}=\ell$, then
$(\ell^{\prime\prime},d)\in P$ and $\ell^{\prime}\neq\ell^{\prime\prime}$
since $P$ is indexed. If $\ell^{\prime\prime}\neq\ell$, then
$(\ell^{\prime\prime},\delta^{\prime})\in P$ and
$\ell^{\prime}\neq\ell^{\prime\prime}$ since $P$ is indexed. In either case
$\ell^{\prime}\neq\ell^{\prime}$. Since $(\ell^{\prime},\delta)$ and
$(\ell^{\prime\prime},\delta^{\prime})$ were arbitrary, then $P^{\prime}$ is
indexed.

  2. –

Well-formed. Let $(\ell^{\prime},\delta)\in P^{\prime}$. There are two cases
to consider, depending on whether $\ell^{\prime}=\ell$.

    1. –

If $\ell^{\prime}=\ell$, then $\delta=d^{\prime}$, since $P^{\prime}$ is
indexed. Then $\delta\in(V\cup R)^{*}$. Then for all
$k\in\\{1,2,\ldots,|\delta|\\}$, either $\delta_{k}\in R$ or $\delta_{k}\in
V$. If $\delta_{k}\in V$ and $\delta_{k}=\ell$, then
$(\delta_{k},d^{\prime})\in P^{\prime}$. If $\delta_{k}\in V$ and
$\delta_{k}\neq\ell$, then there exists some $\delta^{\prime}\in(L(\Sigma)\cup
R)^{*}$ such that $(d_{k},\delta^{\prime})\in P$. Since $\delta_{k}\neq\ell$,
then $(\delta_{k},\delta^{\prime})\in P^{\prime}$. In either case, if
$\delta_{k}\in V$, then there exists some $\delta^{\prime}\in(L(\Sigma)\cup
R)^{*}$ such that $(d_{k},d^{\prime\prime})\in P^{\prime}$ Since $k$ was
arbitrary, then $(\ell^{\prime},\delta)$ is well-formed.

    2. –

If $\ell^{\prime}\neq\ell$, then $(\ell^{\prime},\delta)\in P$. Let
$k\in\\{1,2,\ldots,|\delta|\\}$. Since $P$ is well-formed, then either
$\delta_{k}\in R$ or there exists some $\delta^{\prime}\in(L(\Sigma)\cup
R)^{*}$ such that $(\delta_{k},\delta^{\prime})\in P$. There are two cases to
consider, depending on whether $\delta_{k}=\ell$. If $\delta_{k}=\ell$, then
$(\ell,d^{\prime})\in P^{\prime}$. If $\delta_{k}\neq\ell$, then
$(\delta_{k},\delta^{\prime})\in P^{\prime}$. In either case, there exists
some $\delta^{\prime}\in(L(\Sigma)\cup R)^{*}$ such that
$(\delta_{k},\delta^{\prime})\in P^{\prime}$. Since $k$ was arbitrary, then
$(\ell^{\prime},\delta)$ is well-formed.

In either case, $(\ell^{\prime},\delta)$ is well-formed. Since
$(\ell^{\prime},\delta)$ was arbitrary, then $P^{\prime}$ is well-formed.

  3. –

Valid. Let $(\ell^{\prime},\delta)\in P^{\prime}$. Now these are two cases to
consider, depending on whether $\ell^{\prime}=\ell$. If $\ell^{\prime}=\ell$,
then $\delta=d^{\prime}$ since $P^{\prime}$ is indexed, and consequently
$\delta$ is valid by assumption. If $\ell^{\prime}\neq\ell$, then
$(\ell^{\prime},\delta)\in P$ and $\delta$ is valid by the validity of $P$. In
either case, $(\ell^{\prime},\delta)$ is valid. Since $(\ell^{\prime},\delta)$
was arbitrary, then $P^{\prime}$ is valid.

Then $P^{\prime}$ is a proof for $\langle\Sigma\mid R\rangle$. ∎

####  B.3.2 From Derivational Proofs to Tietze Transformations

Let $\langle\Sigma\mid R\rangle$ be a monoid presentation. The goal of this
section is to prove Theorem B.25, which states that acyclic derivational
proofs are sound for the isomorphism of finite monoid presentations. The
completeness of acyclic derivational proofs follows immediately from the fact
that every statement of the form $w\sim_{R}w^{\prime}$ corresponds to at least
one finite derivation. The proof proceeds as follows. First, Lemma B.21 shows
that the lemma substitutions outlined in Example B.15 preserve the structure
of derivational proofs. This is used in Lemma B.22 to show that if a
derivation $(\ell,d)$ in a proof $P$ depends on a lemma
$(\ell^{\prime},d^{\prime})$ which follows directly from $R$, then $d$ can be
rewritten so that all dependencies on $\ell^{\prime}$ are removed without
introducing any new dependencies. This is used repeated in Lemma B.23 to show
that any derivation $(\ell,d)$ which depends only on lemmas which follow
directly from $R$, can be rewritten to also follow directly from $R$. This is
extended in Lemma B.24 to show that any finite and acyclic derivational proof
$P$ can be written into a proof $P^{\prime}$ such that every derivation
depends only on $R$. Then each derivation in $P^{\prime}$ follows from
$(\sim_{R})$, and Theorem B.25 follows immediately by induction.

######  Lemma B.21.

Let $P$ be a proof for $\langle\Sigma\mid R\rangle$. If $(\ell,d)$ and
$(\ell^{\prime},d^{\prime})$ are derivations in $P$ and there exists
$\delta,\delta^{\prime}\in(L(\Sigma)\cup R)^{*}$ such that
$d=\delta\cdot\ell^{\prime}\cdot\delta^{\prime}$, then
$P[\ell\mapsto\delta\cdot d^{\prime}\cdot\delta^{\prime}]$ is a proof for
$\langle\Sigma\mid R\rangle$.

###### Proof.

Let $L_{P}=\\{\ell\mid(\ell,d)\in P\\}$, $d^{\prime\prime}=\delta\cdot
d^{\prime}\cdot\delta^{\prime}$, and $(x,(q,r))=\ell$. Since
$\delta,d^{\prime},\delta^{\prime}\in(L_{p}\cup R)^{*}$, then
$d^{\prime\prime}\in(L_{p}\cup R)^{*}$. Since $P$ is valid, then there exists
$v\in(\Sigma^{*})^{n+1}$ such that $v_{1}=q$, $v_{n+1}=r$, and
$v_{k}\xrightarrow{d_{k}}v_{k+1}$ for all $k\in[n]$, where $n=|d|$. Let
$m=|\delta|$. Since $P$ is valid and
$v_{m}\xrightarrow{\ell^{\prime}}v_{m+1}$, then there exists some
$u\in(\Sigma^{*})^{s+1}$ such that $u_{1}=v_{m}$, $u_{s+1}=v_{m+1}$, and