1: \begin{abstract}

2:   We give a presentation by generators and relations of the group of

3:   $3$-qubit Clifford+$\CS$ operators. The proof roughly consists of two

4:   parts: (1) applying the Reidemeister-Schreier theorem recursively to

5:   an earlier result of ours; and (2) the simplification of thousands

6:   of relations into 17 relations. Both (1) and (2) have been formally

7:   verified in the proof assistant Agda. The Reidemeister-Schreier

8:   theorem gives a constructive method for computing a presentation of

9:   a sub-monoid given a presentation of the super-monoid. To achieve

10:   (2), we devise an almost-normal form for Clifford+$\CS$

11:   operators. Along the way, we also identify several interesting

12:   structures within the Clifford+$\CS$ group. Specifically, we

13:   identify three different finite subgroups for whose elements we can

14:   give unique normal forms. We show that the $3$-qubit Clifford+$\CS$

15:   group, which is of course infinite, is the amalgamated product of

16:   these three finite subgroups. This result is analogous to the fact

17:   that the $1$-qubit Clifford+$T$ group is an amalgamated product of

18:   two finite subgroups.

19: \end{abstract}

20: