  The "Sum-Over-Paths" formalism is a way to symbolically manipulate linear
maps that describe quantum systems, and is a tool that is used in formal
verification of such systems. We give here a new set of rewrite rules for the
formalism, and show that it is complete for "Toffoli-Hadamard", the simplest
approximately universal fragment of quantum mechanics. We show that the
rewriting is terminating, but not confluent (which is expected from the
universality of the fragment). We do so using the connection between
Sum-over-Paths and graphical language ZH-calculus, and also show how the
axiomatisation translates into the latter. We provide generalisations of the
presented rewrite rules, that can prove useful when trying to reduce terms in
practice, and we show how to graphically make sense of these new rules. We show
how to enrich the rewrite system to reach completeness for the dyadic fragments
of quantum computation, used in particular in the Quantum Fourier Transform,
and obtained by adding phase gates with dyadic multiples of $\pi$ to the
Toffoli-Hadamard gate-set. Finally, we show how to perform sums and
concatenation of arbitrary terms, something which is not native in a system
designed for analysing gate-based quantum computation, but necessary when
considering Hamiltonian-based quantum computation.
