Proof of Equation (80):

$$ (H_{[0,1]}H_{[0,2]}) (H_{[1,3]}H_{[0,4]}) (H_{[1,5]}H_{[0,1]}) ((-1)_{[1]}(-1)_{[0]}) (H_{[0,4]}H_{[1,5]}) (H_{[0,2]}H_{[1,3]}) $$

$$ \text{Corollary A.5} \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[6]}X_{[2,3]}) (H_{[0,1]}H_{[0,2]}) (H_{[1,3]}H_{[0,4]}) (H_{[1,5]}H_{[0,1]}) ((-1)_{[1]}(-1)_{[0]}) (H_{[0,4]}H_{[1,5]}) (H_{[0,2]}H_{[1,3]}) $$

$$ \text{Corollary A.10} \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,1]}H_{[0,3]}) ((-1)_{[2]}X_{[0,3]}) ((-1)_{[6]}X_{[2,3]}) (H_{[1,3]}H_{[0,4]}) (H_{[1,5]}H_{[0,1]}) ((-1)_{[1]}(-1)_{[0]}) (H_{[0,4]}H_{[1,5]}) (H_{[0,2]}H_{[1,3]}) $$

$$ \text{Corollary A.10} \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,1]}H_{[0,3]}) (H_{[1,2]}H_{[3,4]}) (X_{[1,2]}X_{[0,3]}) ((-1)_{[6]}X_{[2,3]}) (H_{[1,5]}H_{[0,1]}) ((-1)_{[1]}(-1)_{[0]}) (H_{[0,4]}H_{[1,5]}) (H_{[0,2]}H_{[1,3]}) $$

$$ \text{Corollary A.10} \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,1]}H_{[0,3]}) (H_{[1,2]}H_{[3,4]}) (H_{[2,5]}H_{[3,2]}) (X_{[1,2]}X_{[0,3]}) ((-1)_{[6]}X_{[2,3]}) ((-1)_{[1]}(-1)_{[0]}) (H_{[0,4]}H_{[1,5]}) (H_{[0,2]}H_{[1,3]}) $$

$$ \text{Corollary A.5} \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,1]}H_{[0,3]}) (H_{[1,2]}H_{[3,4]}) (H_{[2,5]}H_{[3,2]}) ((-1)_{[2]}(-1)_{[3]}) (X_{[1,2]}X_{[0,3]}) ((-1)_{[6]}X_{[2,3]}) (H_{[0,4]}H_{[1,5]}) (H_{[0,2]}H_{[1,3]}) $$

$$ \text{Corollary A.10} \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,1]}H_{[0,3]}) (H_{[1,2]}H_{[3,4]}) (H_{[2,5]}H_{[3,2]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[3,4]}H_{[2,5]}) (X_{[1,2]}X_{[0,3]}) ((-1)_{[6]}X_{[2,3]}) (H_{[0,2]}H_{[1,3]}) $$

$$ \text{Corollary A.10} \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,1]}H_{[0,3]}) (H_{[1,2]}H_{[3,4]}) (H_{[2,5]}H_{[3,2]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[3,4]}H_{[2,5]}) (H_{[0,3]}H_{[1,2]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[6]}X_{[2,3]}) $$

$$ (70)_{\approx}^{(73)} \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,1]}H_{[0,3]}) (H_{[1,2]}H_{[3,4]}) (H_{[2,5]}H_{[3,2]}) (H_{[7,6]}H_{[4,5]}) (H_{[7,6]}H_{[4,5]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[3,4]}H_{[2,5]}) (H_{[0,3]}H_{[1,2]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[6]}X_{[2,3]}) $$

$$ (73) \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,1]}H_{[0,3]}) (H_{[1,2]}H_{[3,4]}) (H_{[2,5]}H_{[7,6]}) (H_{[3,2]}H_{[4,5]}) (H_{[7,6]}H_{[4,5]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[3,4]}H_{[2,5]}) (H_{[0,3]}H_{[1,2]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[6]}X_{[2,3]}) $$

$$ (66) \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,1]}H_{[0,3]}) (H_{[1,2]}H_{[3,4]}) (H_{[7,6]}H_{[2,5]}) (H_{[3,2]}H_{[4,5]}) (H_{[7,6]}H_{[4,5]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[3,4]}H_{[2,5]}) (H_{[0,3]}H_{[1,2]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[6]}X_{[2,3]}) $$

$$ (73) \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,1]}H_{[0,3]}) (H_{[1,2]}H_{[7,6]}) (H_{[3,4]}H_{[2,5]}) (H_{[3,2]}H_{[4,5]}) (H_{[7,6]}H_{[4,5]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[3,4]}H_{[2,5]}) (H_{[0,3]}H_{[1,2]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[6]}X_{[2,3]}) $$

$$ (66) \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,1]}H_{[0,3]}) (H_{[7,6]}H_{[1,2]}) (H_{[3,4]}H_{[2,5]}) (H_{[3,2]}H_{[4,5]}) (H_{[7,6]}H_{[4,5]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[3,4]}H_{[2,5]}) (H_{[0,3]}H_{[1,2]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[6]}X_{[2,3]}) $$

$$ (73) \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,1]}H_{[7,6]}) (H_{[0,3]}H_{[1,2]}) (H_{[3,4]}H_{[2,5]}) (H_{[3,2]}H_{[4,5]}) (H_{[7,6]}H_{[4,5]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[3,4]}H_{[2,5]}) (H_{[0,3]}H_{[1,2]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[6]}X_{[2,3]}) $$

$$ (46) \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,3]}H_{[1,2]}) (H_{[3,4]}H_{[2,5]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[7,6]}H_{[4,5]}) (H_{[3,2]}H_{[4,5]}) (H_{[3,4]}H_{[2,5]}) (H_{[0,3]}H_{[1,2]}) (H_{[0,1]}H_{[7,6]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[6]}X_{[2,3]}) $$

$$ (73)_{\approx}^{(70)66} \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,3]}H_{[1,2]}) (H_{[3,4]}H_{[2,5]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[3,2]}H_{[7,6]}) (H_{[3,4]}H_{[2,5]}) (H_{[0,3]}H_{[1,2]}) (H_{[0,1]}H_{[7,6]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[6]}X_{[2,3]}) $$

$$ (73) \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,3]}H_{[1,2]}) (H_{[3,4]}H_{[2,5]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[3,2]}H_{[3,4]}) (H_{[7,6]}H_{[2,5]}) (H_{[0,3]}H_{[1,2]}) (H_{[0,1]}H_{[7,6]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[6]}X_{[2,3]}) $$

$$ (66) \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,3]}H_{[1,2]}) (H_{[3,4]}H_{[2,5]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[3,2]}H_{[3,4]}) (H_{[2,5]}H_{[7,6]}) (H_{[0,3]}H_{[1,2]}) (H_{[0,1]}H_{[7,6]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[6]}X_{[2,3]}) $$

$$ (73) \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,3]}H_{[1,2]}) (H_{[3,4]}H_{[2,5]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[3,2]}H_{[3,4]}) (H_{[2,5]}H_{[0,3]}) (H_{[7,6]}H_{[1,2]}) (H_{[0,1]}H_{[7,6]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[6]}X_{[2,3]}) $$

$$ (66) \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,3]}H_{[1,2]}) (H_{[3,4]}H_{[2,5]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[3,2]}H_{[3,4]}) (H_{[2,5]}H_{[0,3]}) (H_{[1,2]}H_{[7,6]}) (H_{[7,6]}H_{[0,1]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[6]}X_{[2,3]}) $$

$$ (71) \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,3]}H_{[1,2]}) (H_{[3,4]}H_{[2,5]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[3,2]}H_{[3,4]}) (H_{[2,5]}H_{[0,3]}) (H_{[1,2]}H_{[0,1]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[6]}X_{[2,3]}) $$

$$ \text{Corollary A.10} \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,3]}H_{[1,2]}) (H_{[3,4]}H_{[2,5]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[3,2]}H_{[3,4]}) (H_{[2,5]}H_{[0,3]}) ((-1)_{[3]}X_{[1,2]}) ((-1)_{[6]}X_{[2,3]}) (H_{[1,5]}H_{[0,1]}) $$

$$ \text{Corollary A.10} \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,3]}H_{[1,2]}) (H_{[3,4]}H_{[2,5]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[3,2]}H_{[3,4]}) (X_{[1,2]}X_{[0,3]}) ((-1)_{[6]}X_{[2,3]}) (H_{[1,5]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) $$

$$ \text{Corollary A.10} \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,3]}H_{[1,2]}) (H_{[3,4]}H_{[2,5]}) ((-1)_{[2]}(-1)_{[3]}) (X_{[1,2]}X_{[0,3]}) ((-1)_{[6]}X_{[2,3]}) (H_{[0,1]}H_{[0,4]}) (H_{[1,5]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) $$

$$ \text{Corollary A.5} \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,3]}H_{[1,2]}) (H_{[3,4]}H_{[2,5]}) (X_{[1,2]}X_{[0,3]}) ((-1)_{[6]}X_{[2,3]}) ((-1)_{[1]}(-1)_{[0]}) (H_{[0,1]}H_{[0,4]}) (H_{[1,5]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) $$

$$ \text{Corollary A.10} \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) (H_{[0,3]}H_{[1,2]}) (X_{[1,2]}X_{[0,3]}) ((-1)_{[6]}X_{[2,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}(-1)_{[0]}) (H_{[0,1]}H_{[0,4]}) (H_{[1,5]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) $$

$$ \text{Corollary A.10} \quad \approx \quad ((-1)_{[6]}X_{[2,3]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[2]}(-1)_{[3]}) ((-1)_{[6]}X_{[2,3]}) (H_{[0,2]}H_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}(-1)_{[0]}) (H_{[0,1]}H_{[0,4]}) (H_{[1,5]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) $$

$$ \text{Corollary A.5} \quad \approx \quad (H_{[0,2]}H_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}(-1)_{[0]}) (H_{[0,1]}H_{[0,4]}) (H_{[1,5]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) $$
Notice that since Corollary A.10 supersedes both Corollary A.5 and Equations (66), (70), (71) and (73), all the steps in the two derivations above could have been justified by Corollary A.10, except the use of Equation (45) and Equation (46) respectively. □

**Corollary A.12.** The equational theory of Figure 8 is complete, i.e. for any two words $w, w'$ over the generators of $\mathcal{P}_N$, if $\llbracket w \rrbracket = \llbracket w' \rrbracket$ then $w \approx w'$.

**PROOF.** By the Reidemeister-Schreier theorem, it suffices to prove that all the equations of Appendix A.3.2 are consequences of those of Figure 8. Note that all the equations of Appendix A.3.2, except Equations $(\epsilon-b6^*)$ to (HZ-b6^*) and $(\epsilon-d3^*)$ to (HZ-d4^*), are such that one of the two sides contains at most one generator of the form $(H_{[a,b]}H_{[c,d]})$ and the other side contains at most two such generators : therefore, since those equations are semantically sound, Corollary A.10 shows that they are consequences of the equations of Figure 8. Therefore, it only remains to derive Equations $(\epsilon-b6^*)$ to (HZ-b6^*) and $(\epsilon-d3^*)$ to (HZ-d4^*) by hand.

**Proof of Equation $(\epsilon-b6^*)$:**

$$ (H_{[0,1]}H_{[0,1]}) (H_{[0,1]}H_{[2,3]}) \stackrel{(71)}{\approx} (H_{[0,1]}H_{[2,3]}) $$

$$ \stackrel{(66)}{\approx} (H_{[2,3]}H_{[0,1]}) $$

$$ \stackrel{(71)}{\approx} (H_{[2,3]}H_{[0,1]}) (H_{[0,1]}H_{[0,1]}) $$

**Proof of Equation (Z-b6^*):**

$$ ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,1]}) (H_{[0,1]}H_{[2,3]}) \stackrel{(70)}{\approx} ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[2,3]}) $$

$$ \stackrel{\text{Corollary A.10}}{\approx} (H_{[0,1]}H_{[2,3]}) ((-1)_{[0]}X_{[0,1]}) $$

$$ \stackrel{(66)}{\approx} (H_{[2,3]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) $$

$$ \stackrel{(70)}{\approx} (H_{[2,3]}H_{[0,1]}) (H_{[0,1]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) $$

**Proof of Equation (H-b6^*):**

$$ (H_{[0,1]}H_{[0,1]}) (H_{[2,3]}H_{[0,1]}) \stackrel{(70)}{\approx} (H_{[2,3]}H_{[0,1]}) $$

$$ \stackrel{(66)}{\approx} (H_{[0,1]}H_{[2,3]}) $$

$$ \stackrel{(70)}{\approx} (H_{[0,1]}H_{[2,3]}) (H_{[0,1]}H_{[0,1]}) $$

**Proof of Equation (HZ-b6^*):**

$$ (H_{[0,1]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) (H_{[2,3]}H_{[0,1]}) \stackrel{(70)}{\approx} ((-1)_{[0]}X_{[0,1]}) (H_{[2,3]}H_{[0,1]}) $$

$$ \stackrel{(66)}{\approx} ((-1)_{[0]}X_{[0,1]}) (H_{[0,1]}H_{[2,3]}) $$

$$ \stackrel{(75)}{\approx} (H_{[0,1]}H_{[2,3]}) ((-1)_{[1]}X_{[0,1]}) $$

$$ \stackrel{(70)}{\approx} (H_{[0,1]}H_{[2,3]}) ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,1]}) $$

**Proof of Equation $(\epsilon-d3^*)$:**

$$ \begin{aligned} & (H_{[0,1]}H_{[0,1]}) (H_{[0,1]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) (H_{[0,1]}H_{[0,1]}) \\ & ((-1)_{[1]}(-1)_{[0]}) ((-1)_{[1]}(-1)_{[1]}) (H_{[0,2]}H_{[0,1]}) (H_{[0,1]}H_{[1,3]}) \end{aligned} $$

$$ \stackrel{(20)^{(71)}}{\approx} (H_{[0,1]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) ((-1)_{[1]}(-1)_{[0]}) (H_{[0,2]}H_{[1,3]}) $$

$$ \stackrel{(79)}{\approx} (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}(-1)_{[0]}) (H_{[0,1]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) $$

$$ \stackrel{(20)^{(70)(71)}}{\approx} (H_{[0,2]}H_{[0,1]}) (H_{[0,1]}H_{[1,3]}) (H_{[0,1]}H_{[0,1]}) ((-1)_{[1]}(-1)_{[0]}) ((-1)_{[1]}(-1)_{[1]}) (H_{[0,1]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) (H_{[0,1]}H_{[0,1]}) $$

**Proof of Equation (Z-d3^*):**

$$ \begin{aligned} & ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,1]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]}) (H_{[0,1]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) \\ & ((-1)_{[1]}(-1)_{[0]}) ((-1)_{[1]}(-1)_{[1]}) (H_{[0,2]}H_{[0,1]}) (H_{[0,1]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) \end{aligned} $$
$$ (20)^{(71)} \stackrel{\approx}{\sim} ((-1)_{[1]} X_{[0,1]} (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]} (H_{[1,3]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]} ((-1)_{[1]} (-1)_{[0]}) (H_{[0,2]} H_{[1,3]} ((-1)_{[1]} X_{[1,3]} $$

$$ \text{Corollary A.10} \stackrel{\approx}{\sim} ((-1)_{[1]} (-1)_{[4]}) ((-1)_{[4]} X_{[0,1]} (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]} (H_{[1,3]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]} ((-1)_{[1]} (-1)_{[0]}) (H_{[0,2]} H_{[1,3]} ((-1)_{[1]} X_{[1,3]} $$

$$ \text{Corollary A.10} \stackrel{\approx}{\sim} ((-1)_{[1]} (-1)_{[4]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[4]} (-1)_{[1]}) ((-1)_{[3]} X_{[1,3]} (H_{[1,3]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]} ((-1)_{[1]} (-1)_{[0]}) (H_{[0,2]} H_{[1,3]} ((-1)_{[1]} X_{[1,3]} $$

$$ \text{Corollary A.10} \stackrel{\approx}{\sim} ((-1)_{[1]} (-1)_{[4]}) (H_{[0,1]} H_{[0,2]}) (H_{[1,3]} H_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) ((-1)_{[4]} (-1)_{[1]}) (H_{[0,2]} H_{[1,3]} ((-1)_{[1]} X_{[1,3]} $$

$$ \text{Corollary A.10} \stackrel{\approx}{\sim} ((-1)_{[1]} (-1)_{[4]}) (H_{[0,1]} H_{[0,2]}) (H_{[1,3]} H_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,2]} H_{[1,3]} ((-1)_{[4]} (-1)_{[1]} $$

$$ (79) \stackrel{\approx}{\sim} ((-1)_{[1]} (-1)_{[4]}) (H_{[0,2]} H_{[1,3]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,1]} H_{[0,2]}) (H_{[1,3]} H_{[0,1]} ((-1)_{[4]} (-1)_{[1]} $$

$$ \text{Corollary A.10} \stackrel{\approx}{\sim} (H_{[0,2]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} (-1)_{[4]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,1]} H_{[0,2]}) (H_{[1,3]} H_{[0,1]} ((-1)_{[4]} (-1)_{[1]} $$

$$ \text{Corollary A.10} \stackrel{\approx}{\sim} (H_{[0,2]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[4]} (-1)_{[1]}) (H_{[1,3]} H_{[0,1]} ((-1)_{[4]} (-1)_{[1]} $$

$$ \text{Corollary A.10} \stackrel{\approx}{\sim} (H_{[0,2]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]} ((-1)_{[0]} X_{[0,1]} $$

$$ (20)^{(70)(71)} \stackrel{\approx}{\sim} (H_{[0,2]} H_{[0,1]} (H_{[0,1]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]} (H_{[0,1]} H_{[0,1]} ((-1)_{[1]} (-1)_{[0]}) ((-1)_{[1]} (-1)_{[1]} (H_{[0,1]} H_{[0,2]} ((-1)_{[3]} X_{[1,3]} (H_{[1,3]} H_{[0,1]} (H_{[0,1]} H_{[0,1]} ((-1)_{[0]} X_{[0,1]} $$

Proof of Equation (H-d3*):

$$ (H_{[0,1]} H_{[0,1]} (H_{[0,2]} H_{[0,1]} (H_{[0,1]} H_{[1,3]} (H_{[0,1]} H_{[0,1]} ((-1)_{[1]} (-1)_{[0]}) ((-1)_{[1]} (-1)_{[1]}) (H_{[0,1]} H_{[0,2]} (H_{[1,3]} H_{[0,1]} $$

$$ (20)^{(70)(71)} \stackrel{\approx}{\sim} (H_{[0,2]} H_{[1,3]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,1]} H_{[0,2]}) (H_{[1,3]} H_{[0,1]} $$

$$ (79) \stackrel{\approx}{\sim} (H_{[0,1]} H_{[0,2]}) (H_{[1,3]} H_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,2]} H_{[1,3]} $$

$$ (20)^{(70)(71)} \stackrel{\approx}{\sim} (H_{[0,1]} H_{[0,2]} (H_{[1,3]} H_{[0,1]} (H_{[0,1]} H_{[0,1]} ((-1)_{[1]} (-1)_{[0]}) ((-1)_{[1]} (-1)_{[1]} (H_{[0,2]} H_{[0,1]} (H_{[0,1]} H_{[1,3]} (H_{[0,1]} H_{[0,1]} $$
Proof of Equation (HZ-d3*):

$$
\begin{align*}
& (H_{[0,1]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]}) (H_{[0,2]} H_{[0,1]}) (H_{[0,1]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) (H_{[0,1]} H_{[0,1]}) \\
& ((-1)_{[1]} (-1)_{[0]}) ((-1)_{[1]} (-1)_{[1]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) \\
(20)_{70}^{(71)} &\approx (H_{[0,1]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]}) (H_{[0,2]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) \\
& (71)_{(66)} \approx (H_{[0,1]} H_{[4,5]}) (H_{[0,1]} H_{[4,5]}) ((-1)_{[0]} X_{[0,1]}) (H_{[0,2]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) \\
& Corollary A.10 \approx (H_{[0,1]} H_{[4,5]}) ((-1)_{[1]} X_{[0,1]}) (H_{[0,1]} H_{[4,5]}) (H_{[0,2]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) \\
& (73)_{(66)} \approx (H_{[0,1]} H_{[4,5]}) ((-1)_{[1]} X_{[0,1]}) (H_{[0,1]} H_{[0,2]}) (H_{[1,3]} H_{[4,5]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) \\
& Corollary A.10 \approx (H_{[0,1]} H_{[4,5]}) ((-1)_{[1]} X_{[0,1]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[4,5]}) ((-1)_{[1]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) \\
& (71) \approx (H_{[0,1]} H_{[4,5]}) ((-1)_{[1]} X_{[0,1]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[4,5]}) ((-1)_{[1]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,1]} H_{[4,5]}) (H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) \\
& Corollary A.10 \approx (H_{[0,1]} H_{[4,5]}) ((-1)_{[1]} X_{[0,1]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[4,5]}) (H_{[4,5]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[4,5]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) \\
& (71) \approx (H_{[0,1]} H_{[4,5]}) ((-1)_{[1]} X_{[0,1]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[4,5]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) \\
& Corollary A.10 \approx (H_{[0,1]} H_{[4,5]}) ((-1)_{[1]} X_{[0,1]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) ((-1)_{[3]} X_{[1,3]}) (H_{[0,2]} H_{[4,5]}) (H_{[1,3]} H_{[0,1]}) \\
& (73) \approx (H_{[0,1]} H_{[4,5]}) ((-1)_{[1]} X_{[0,1]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) ((-1)_{[3]} X_{[1,3]}) (H_{[0,2]} H_{[1,3]}) (H_{[4,5]} H_{[0,1]}) \\
& Corollary A.10 \approx (H_{[0,1]} H_{[4,5]}) ((-1)_{[1]} X_{[0,1]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,2]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) (H_{[4,5]} H_{[0,1]}) \\
& (20)_{71} \approx (H_{[0,1]} H_{[4,5]}) ((-1)_{[1]} X_{[0,1]}) (H_{[0,1]} H_{[0,1]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) (H_{[0,1]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]} \\
& ((-1)_{[1]} (-1)_{[0]}) ((-1)_{[1]} (-1)_{[1]}) (H_{[0,2]} H_{[0,1]}) (H_{[0,1]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) (H_{[4,5]} H_{[0,1]}) \\
& (Z.d3') \approx (H_{[0,1]} H_{[4,5]}) (H_{[0,2]} H_{[0,1]}) (H_{[0,1]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) (H_{[0,1]} H_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) ((-1)_{[1]} (-1)_{[1]}) \\
& (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) (H_{[0,1]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]}) (H_{[4,5]} H_{[0,1]}) \\
& (20)_{70}^{(71)} \approx (H_{[0,1]} H_{[4,5]}) (H_{[0,2]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]}) (H_{[4,5]} H_{[0,1]}) \\
& Corollary A.10 \approx (H_{[0,1]} H_{[4,5]}) (H_{[0,2]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,1]} H_{[0,2]}) (H_{[4,5]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) \\
& (73)_{(66)} \approx (H_{[0,1]} H_{[4,5]}) (H_{[0,2]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[4,5]} H_{[0,1]}) (H_{[0,2]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) \\
& Corollary A.10 \approx (H_{[0,1]} H_{[4,5]}) ((-1)_{[3]} X_{[1,3]}) (H_{[0,2]} H_{[1,3]}) (H_{[4,5]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,2]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) \\
& (73)_{(66)} \approx (H_{[0,1]} H_{[4,5]}) ((-1)_{[3]} X_{[1,3]}) (H_{[4,5]} H_{[0,2]}) (H_{[1,3]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,2]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) \\
& Corollary A.10 \approx (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,2]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) \\
& (20)_{70}^{(71)} \approx (H_{[0,1]} H_{[0,2]}) ((-1)_{[3]} X_{[1,3]}) (H_{[1,3]} H_{[0,1]}) (H_{[0,1]} H_{[0,1]}) ((-1)_{[0]} X_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) ((-1)_{[1]} (-1)_{[1]}) \\
& (H_{[0,2]} H_{[0,1]}) (H_{[0,1]} H_{[1,3]}) ((-1)_{[1]} X_{[1,3]}) ((-1)_{[1]} X_{[0,1]}) (H_{[0,1]} H_{[0,1]})
\end{align*}
$$

Proof of Equation (e-d4*):

$$
\begin{align*}
& (H_{[0,1]} H_{[0,1]}) (H_{[0,1]} H_{[0,2]}) (H_{[1,3]} H_{[0,1]}) (H_{[0,1]} H_{[0,4]}) (H_{[1,5]} H_{[0,1]}) (H_{[0,1]} H_{[0,1]}) \\
& ((-1)_{[1]} (-1)_{[0]}) ((-1)_{[1]} (-1)_{[1]}) (H_{[0,4]} H_{[0,1]}) (H_{[0,1]} H_{[1,5]}) (H_{[0,2]} H_{[0,1]}) (H_{[0,1]} H_{[1,3]}) \\
(20)_{71}^{(71)} &\approx (H_{[0,1]} H_{[0,2]}) (H_{[1,3]} H_{[0,4]}) (H_{[1,5]} H_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,4]} H_{[1,5]}) (H_{[0,2]} H_{[1,3]}) \\
& (80) \approx (H_{[0,2]} H_{[1,3]}) (H_{[0,4]} H_{[1,5]}) ((-1)_{[1]} (-1)_{[0]}) (H_{[0,1]} H_{[0,4]}) (H_{[1,5]} H_{[0,2]}) (H_{[1,3]} H_{[0,1]}) \\
(20)_{70}^{(71)} &\approx (H_{[0,2]} H_{[0,1]}) (H_{[0,1]} H_{[1,3]}) (H_{[0,4]} H_{[0,1]}) (H_{[0,1]} H_{[1,5]}) (H_{[0,1]} H_{[0,1]}) ((-1)_{[1]} (-1)_{[0]}) ((-1)_{[1]} (-1)_{[1]}) \\
& (H_{[0,1]} H_{[0,4]}) (H_{[1,5]} H_{[0,1]}) (H_{[0,1]} H_{[0,2]}) (H_{[1,3]} H_{[0,1]}) (H_{[0,1]} H_{[0,1]})
\end{align*}
$$
Proof of Equation (Z-d4*):

$$ ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,1]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]}) (H_{[0,1]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,1]}) (H_{[0,1]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) \\ ((-1)_{[1]}(-1)_{[0]}) ((-1)_{[1]}(-1)_{[1]}) (H_{[0,4]}H_{[0,1]}) (H_{[0,1]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[0,2]}H_{[0,1]}) (H_{[0,1]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) $$

(20)$(71) \approx$

$$ ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) \\ ((-1)_{[1]}(-1)_{[0]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) $$

Corollary A.10 $\approx$

$$ ((-1)_{[1]}(-1)_{[6]}) ((-1)_{[6]}X_{[0,1]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) \\ ((-1)_{[1]}(-1)_{[0]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) $$

Corollary A.10 $\approx$

$$ ((-1)_{[1]}(-1)_{[6]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[6]}(-1)_{[1]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) \\ ((-1)_{[1]}(-1)_{[0]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) $$

Corollary A.10 $\approx$

$$ ((-1)_{[1]}(-1)_{[6]}) (H_{[0,1]}H_{[0,2]}) (H_{[1,3]}H_{[0,4]}) ((-1)_{[6]}(-1)_{[1]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) \\ ((-1)_{[1]}(-1)_{[0]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) $$

Corollary A.10 $\approx$

$$ ((-1)_{[1]}(-1)_{[6]}) (H_{[0,1]}H_{[0,2]}) (H_{[1,3]}H_{[0,4]}) (H_{[1,5]}H_{[0,1]}) ((-1)_{[6]}(-1)_{[1]}) \\ ((-1)_{[1]}(-1)_{[0]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) $$

Corollary A.10 $\approx$

$$ ((-1)_{[1]}(-1)_{[6]}) (H_{[0,1]}H_{[0,2]}) (H_{[1,3]}H_{[0,4]}) (H_{[1,5]}H_{[0,1]}) \\ ((-1)_{[1]}(-1)_{[0]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[6]}(-1)_{[1]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) $$

Corollary A.10 $\approx$

$$ ((-1)_{[1]}(-1)_{[6]}) (H_{[0,1]}H_{[0,2]}) (H_{[1,3]}H_{[0,4]}) (H_{[1,5]}H_{[0,1]}) \\ ((-1)_{[1]}(-1)_{[0]}) (H_{[0,4]}H_{[1,5]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[6]}(-1)_{[1]}) $$

(80) $\approx$

$$ ((-1)_{[1]}(-1)_{[6]}) (H_{[0,2]}H_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}(-1)_{[0]}) \\ (H_{[0,1]}H_{[0,4]}) (H_{[1,5]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) ((-1)_{[6]}(-1)_{[1]}) $$

Corollary A.10 $\approx$

$$ (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) ((-1)_{[1]}(-1)_{[6]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}(-1)_{[0]}) \\ (H_{[0,1]}H_{[0,4]}) (H_{[1,5]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) ((-1)_{[6]}(-1)_{[1]}) $$

Corollary A.10 $\approx$

$$ (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}(-1)_{[6]}) ((-1)_{[1]}(-1)_{[0]}) \\ (H_{[0,1]}H_{[0,4]}) (H_{[1,5]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) ((-1)_{[6]}(-1)_{[1]}) $$

Corollary A.10 $\approx$

$$ (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) ((-1)_{[1]}(-1)_{[0]}) \\ (H_{[0,1]}H_{[0,4]}) ((-1)_{[1]}(-1)_{[6]}) (H_{[1,5]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) ((-1)_{[6]}(-1)_{[1]}) $$

Corollary A.10 $\approx$

$$ (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) ((-1)_{[1]}(-1)_{[0]}) \\ (H_{[0,1]}H_{[0,4]}) ((-1)_{[1]}X_{[1,5]}) (H_{[1,5]}H_{[0,2]}) ((-1)_{[1]}(-1)_{[6]}) (H_{[1,3]}H_{[0,1]}) ((-1)_{[6]}(-1)_{[1]}) $$

Corollary A.10 $\approx$

$$ (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) ((-1)_{[1]}(-1)_{[0]}) \\ (H_{[0,1]}H_{[0,4]}) ((-1)_{[1]}X_{[1,5]}) (H_{[1,5]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) $$

(20)$(70)$(71) $\approx$

$$ (H_{[0,2]}H_{[0,1]}) (H_{[0,1]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[0,1]}) (H_{[0,1]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,1]}) ((-1)_{[1]}(-1)_{[0]}) ((-1)_{[1]}(-1)_{[1]}) \\ (H_{[0,1]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,1]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]}) (H_{[0,1]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) $$

Proof of Equation (H-d4*):

$$ (H_{[0,1]}H_{[0,1]}) (H_{[0,2]}H_{[0,1]}) (H_{[0,1]}H_{[1,3]}) (H_{[0,4]}H_{[0,1]}) (H_{[0,1]}H_{[1,5]}) (H_{[0,1]}H_{[0,1]}) \\ ((-1)_{[1]}(-1)_{[0]}) ((-1)_{[1]}(-1)_{[1]}) (H_{[0,1]}H_{[0,4]}) (H_{[1,5]}H_{[0,1]}) (H_{[0,1]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) $$
$$
\begin{align*}
(20)(70)(71) &\approx (H_{[0,2]}H_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}(-1)_{[0]}) (H_{[0,1]}H_{[0,4]}) (H_{[1,5]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) \\
&\approx (H_{[0,1]}H_{[0,2]}) (H_{[1,3]}H_{[0,4]}) (H_{[1,5]}H_{[0,1]}) ((-1)_{[1]}(-1)_{[0]}) (H_{[0,4]}H_{[1,5]}) (H_{[0,2]}H_{[1,3]}) \\
(20)(70)(71) &\approx (H_{[0,1]}H_{[0,2]}) (H_{[1,3]}H_{[0,1]}) (H_{[0,1]}H_{[0,4]}) (H_{[1,5]}H_{[0,1]}) (H_{[0,1]}H_{[0,1]}) ((-1)_{[1]}(-1)_{[0]}) ((-1)_{[1]}(-1)_{[1]}) \\
&\approx (H_{[0,4]}H_{[0,1]}) (H_{[0,1]}H_{[1,5]}) (H_{[0,2]}H_{[0,1]}) (H_{[0,1]}H_{[1,3]}) (H_{[0,1]}H_{[0,1]})
\end{align*}
$$

Proof of Equation (HZ-d4*):

$$
\begin{align*}
(20)(71) &\approx (H_{[0,1]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) (H_{[0,2]}H_{[0,1]}) (H_{[0,1]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[0,1]}) (H_{[0,1]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) \\
&\qquad ((-1)_{[1]}(-1)_{[0]}) (H_{[0,1]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
(71)(66) &\approx (H_{[0,1]}H_{[6,7]}) (H_{[0,1]}H_{[6,7]}) ((-1)_{[0]}X_{[0,1]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) \\
&\qquad ((-1)_{[1]}(-1)_{[0]}) (H_{[0,1]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
\text{Corollary A.10} &\approx (H_{[0,1]}H_{[6,7]}) ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[6,7]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) \\
&\qquad ((-1)_{[1]}(-1)_{[0]}) (H_{[0,1]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
(73)(66) &\approx (H_{[0,1]}H_{[6,7]}) ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,2]}) (H_{[1,3]}H_{[6,7]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) \\
&\qquad ((-1)_{[1]}(-1)_{[0]}) (H_{[0,1]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
\text{Corollary A.10} &\approx (H_{[0,1]}H_{[6,7]}) ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[6,7]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) \\
&\qquad ((-1)_{[1]}(-1)_{[0]}) (H_{[0,1]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
(73)(66) &\approx (H_{[0,1]}H_{[6,7]}) ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,4]}) (H_{[1,5]}H_{[6,7]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) \\
&\qquad ((-1)_{[1]}(-1)_{[0]}) (H_{[0,1]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
\text{Corollary A.10} &\approx (H_{[0,1]}H_{[6,7]}) ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[6,7]}) ((-1)_{[1]}X_{[0,1]}) \\
&\qquad ((-1)_{[1]}(-1)_{[0]}) (H_{[0,1]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
(71) &\approx (H_{[0,1]}H_{[6,7]}) ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[6,7]}) ((-1)_{[1]}X_{[0,1]}) \\
&\qquad ((-1)_{[1]}(-1)_{[0]}) (H_{[0,1]}H_{[6,7]}) (H_{[6,7]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
\text{Corollary A.10} &\approx (H_{[0,1]}H_{[6,7]}) ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) \\
&\qquad ((-1)_{[1]}(-1)_{[0]}) (H_{[6,7]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
(71) &\approx (H_{[0,1]}H_{[6,7]}) ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) \\
&\qquad ((-1)_{[1]}(-1)_{[0]}) (H_{[6,7]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[6,7]}) (H_{[6,7]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
\text{Corollary A.10} &\approx (H_{[0,1]}H_{[6,7]}) ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) \\
&\qquad ((-1)_{[1]}(-1)_{[0]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[6,7]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
(71) &\approx (H_{[0,1]}H_{[6,7]}) ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) \\
&\qquad ((-1)_{[1]}(-1)_{[0]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[6,7]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[6,7]}) (H_{[6,7]}H_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
\text{Corollary A.10} &\approx (H_{[0,1]}H_{[6,7]}) ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) \\
&\qquad ((-1)_{[1]}(-1)_{[0]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[6,7]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[6,7]}) (H_{[6,7]}H_{[0,1]})
\end{align*}
$$
$$
\begin{align*}
(20)\text{(70)(71)} &\approx (H_{[0,1]}H_{[6,7]}) ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,1]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]}) (H_{[0,1]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,1]}) (H_{[0,1]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) \\
&\qquad ((-1)_{[1]})(-1)_{[0]} ((-1)_{[1]})(-1)_{[1]} (H_{[0,4]}H_{[0,1]}) (H_{[0,1]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[0,2]}H_{[0,1]}) (H_{[0,1]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[6,7]}H_{[0,1]}) \\
(Z-d4') &\approx (H_{[0,1]}H_{[6,7]}) (H_{[0,2]}H_{[0,1]}) (H_{[0,1]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[0,1]}) (H_{[0,1]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,1]}) ((-1)_{[1]})(-1)_{[0]} ((-1)_{[1]})(-1)_{[1]} \\
&\qquad (H_{[0,1]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,1]}) (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]}) (H_{[0,1]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) (H_{[6,7]}H_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
(20)\text{(70)(71)} &\approx (H_{[0,1]}H_{[6,7]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) ((-1)_{[1]})(-1)_{[0]} \\
&\qquad (H_{[0,1]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) (H_{[6,7]}H_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
\text{Corollary A.10} &\approx (H_{[0,1]}H_{[6,7]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) ((-1)_{[1]})(-1)_{[0]} \\
&\qquad (H_{[0,1]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]}) (H_{[6,7]}H_{[0,1]}) ((-1)_{[1]}X_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
\text{Corollary A.10} &\approx (H_{[0,1]}H_{[6,7]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) ((-1)_{[1]})(-1)_{[0]} \\
&\qquad (H_{[0,1]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,2]}) (H_{[6,7]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) ((-1)_{[1]}X_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
(73)\text{(66)} &\approx (H_{[0,1]}H_{[6,7]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) ((-1)_{[1]})(-1)_{[0]} \\
&\qquad (H_{[0,1]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[6,7]}H_{[1,5]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) ((-1)_{[1]}X_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
\text{Corollary A.10} &\approx (H_{[0,1]}H_{[6,7]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) ((-1)_{[1]})(-1)_{[0]} \\
&\qquad (H_{[0,1]}H_{[0,4]}) (H_{[6,7]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) ((-1)_{[1]}X_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
(73)\text{(66)} &\approx (H_{[0,1]}H_{[6,7]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) ((-1)_{[1]}X_{[0,1]}) ((-1)_{[1]})(-1)_{[0]} \\
&\qquad (H_{[6,7]}H_{[0,1]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) ((-1)_{[1]}X_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
\text{Corollary A.10} &\approx (H_{[0,1]}H_{[6,7]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[6,7]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) ((-1)_{[1]})(-1)_{[0]} \\
&\qquad (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) ((-1)_{[1]}X_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
(73)\text{(66)} &\approx (H_{[0,1]}H_{[0,2]}) (H_{[1,3]}H_{[6,7]}) ((-1)_{[1]}X_{[1,3]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[6,7]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) ((-1)_{[1]})(-1)_{[0]} \\
&\qquad (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) ((-1)_{[1]}X_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
\text{Corollary A.10} &\approx (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[6,7]}) (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[6,7]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) ((-1)_{[1]})(-1)_{[0]} \\
&\qquad (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) ((-1)_{[1]}X_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
(73)\text{(66)} &\approx (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,4]}) (H_{[1,5]}H_{[6,7]}) ((-1)_{[1]}X_{[1,5]}) (H_{[6,7]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) ((-1)_{[1]})(-1)_{[0]} \\
&\qquad (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) ((-1)_{[1]}X_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
\text{Corollary A.10} &\approx (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) ((-1)_{[1]})(-1)_{[0]} \\
&\qquad (H_{[0,4]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[0,2]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) ((-1)_{[1]}X_{[0,1]})
\end{align*}
$$

$$
\begin{align*}
(20)\text{(70)(71)} &\approx (H_{[0,1]}H_{[0,2]}) ((-1)_{[3]}X_{[1,3]}) (H_{[1,3]}H_{[0,1]}) (H_{[0,1]}H_{[0,4]}) ((-1)_{[5]}X_{[1,5]}) (H_{[1,5]}H_{[0,1]}) (H_{[0,1]}H_{[0,1]}) ((-1)_{[0]}X_{[0,1]}) ((-1)_{[1]})(-1)_{[0]} ((-1)_{[1]})(-1)_{[1]} \\
&\qquad (H_{[0,4]}H_{[0,1]}) (H_{[0,1]}H_{[1,5]}) ((-1)_{[1]}X_{[1,5]}) (H_{[0,2]}H_{[0,1]}) (H_{[0,1]}H_{[1,3]}) ((-1)_{[1]}X_{[1,3]}) ((-1)_{[1]}X_{[0,1]}) (H_{[0,1]}H_{[0,1]})
\end{align*}
$$

<figure><img src="image_5.png" /></figure>

# B Some auxiliary Equations and Useful Properties

## B.1 A Few Useful General Properties of Circuits

**Definition B.1.** The mirrored version of a circuit C, denoted by $C^\dagger$, is inductively defined as:

$$
\bullet \quad \text{for } g \in \left\{ \begin{array}{c} \text{C} \\ \text{X} \\ \text{H} \\ \text{L} \\ \text{R} \end{array} \right\}, \quad g^\dagger = g
$$

$$
\bullet \quad (C_1 \circ C_2)^\dagger = C_2^\dagger \circ C_1^\dagger
$$
Proof of Equation (87):

<figure><img src="image_6.png" /></figure>

Proof of Equation (88):

<figure><img src="image_7.png" /></figure>

Proof of Equation (89):

<figure><img src="image_8.png" /></figure>

Proof of Equation (90):

<figure><img src="image_9.png" /></figure>

Proof of Equation (91):

<figure><img src="image_10.png" /></figure>

Proof of Equation (92):

<figure><img src="image_11.png" /></figure>

Proof of Equation (93):

<figure><img src="image_12.png" /></figure>

Proof of Equation (94):

<figure><img src="image_13.png" /></figure>

Proof of Equation (95):

<figure><img src="image_14.png" /></figure>

Proof of Equation (96):

<figure><img src="image_15.png" /></figure>

<figure><img src="image_16.png" /></figure>

<figure><img src="image_17.png" /></figure>

<figure><img src="image_18.png" /></figure>

<figure><img src="image_19.png" /></figure>

<figure><img src="image_20.png" /></figure>

<figure><img src="image_21.png" /></figure>
$$ \begin{align*} (92)(7) &\equiv \text{---H---}\text{---H---} \\ &= \text{---}\text{---}\text{---} \end{align*} $$

Proof of Equation (97):

$$ \begin{array}{ccc} & \text{---H---}\text{---H---} & \\ \text{---H---}\text{---H---} & (83) & \text{---H---}\text{---H---} \end{array} $$

$$ (81)(96) \equiv \text{---H---}\text{---H---} $$

$$ (84) \equiv \text{---H---}\text{---H---} $$

$$ (81) \equiv \text{---H---}\text{---H---}\text{---H---} $$

$$ (84) \equiv \text{---H---}\text{---H---}\text{---H---} $$

$$ (83) \equiv \text{---H---} $$

Proof of Equation (98):

$$ \begin{array}{ccc} & \text{---H---}\text{---H---} & (97) \equiv \text{---H---}\text{---H---} \end{array} $$

Proof of Equation (99):

$$ \text{---H---}\text{---H---} \equiv \text{---H---}\text{---H---} \quad (9) $$

$$ (98) \equiv \text{---H---}\text{---H---}\text{---H---} $$

$$ (95)(81)(10) \equiv \text{---H---}\text{---H---}\text{---H---} $$

$$ (98) \equiv \text{---H---}\text{---H---} $$

$$ (9) \equiv \text{---H---} $$

Proof of Equation (100):

$$ \begin{array}{ccc} & \text{---H---}\text{---H---} & (84) \equiv \text{---H---}\text{---H---} \end{array} $$

Proof of Equation (101):

$$ \text{---H---}\text{---H---} \equiv \text{---H---}\text{---H---} \quad (100) $$
Proof of Equation (102):

<figure><img src="image_22.png" /></figure>

Proof of Equation (103):

<figure><img src="image_23.png" /></figure>

Proof of Equation (104):<fnref n="17" />

<figure><img src="image_24.png" /></figure>

Proof of Equation (105):

<figure><img src="image_25.png" /></figure>

Proof of Equation (106):

<figure><img src="image_26.png" /></figure>

Proof of Equation (107):

<figure><img src="image_27.png" /></figure>

Proof of Equation (108):

<figure><img src="image_28.png" /></figure>

Proof of Equation (109):

<figure><img src="image_29.png" /></figure>

<figure><img src="image_30.png" /></figure>

<figure><img src="image_31.png" /></figure>

<figure><img src="image_32.png" /></figure>

<figure><img src="image_33.png" /></figure>

<figure><img src="image_34.png" /></figure>

<figure><img src="image_35.png" /></figure>

<figure><img src="image_36.png" /></figure>

<footnote n="17">¹⁷Note that up to deformation, Equation (104) is just Equation (87) with the LHS and RHS exchanged and with an additional swap on the left, therefore we could also have proved it in one step by invoking Equation (87).</footnote>
<figure><img src="image_37.png" /></figure>

<figure><img src="image_38.png" /></figure>

<figure><img src="image_39.png" /></figure>

<figure><img src="image_40.png" /></figure>

<figure><img src="image_41.png" /></figure>

<figure><img src="image_42.png" /></figure>

Proof of Equation (110):

<figure><img src="image_43.png" /></figure>

(5)

<figure><img src="image_44.png" /></figure>

(92)(7)

<figure><img src="image_45.png" /></figure>

(1)

<figure><img src="image_46.png" /></figure>

(2)

<figure><img src="image_47.png" /></figure>

Lemma 7.1

<figure><img src="image_48.png" /></figure>

(109)

<figure><img src="image_49.png" /></figure>

(11)

<figure><img src="image_50.png" /></figure>

Lemma 7.1

<figure><img src="image_51.png" /></figure>

(81)(5)

<figure><img src="image_52.png" /></figure>

(92)(7)

<figure><img src="image_53.png" /></figure>
<figure><img src="image_54.png" /></figure>

<figure><img src="image_55.png" /></figure>

# C Two-Qubit Completeness

## C.1 Proof of Lemma 7.4

We are going to prove the slightly stronger result that for any $n$-qubit circuit $C \in \mathcal{QC}$, any $C' \in \mathcal{QC}_{\text{seq}}$ such that $|C'| = C$, and any $k, \ell$ such that $k + n + \ell = 2$,

$$ \mathrm{QC} \vdash D(E_{k,l}(C')) = \mathrm{id}_k \otimes C \otimes \mathrm{id}_l. $$

More precisely, we are going to prove the equivalent statement that for any $n$-qubit raw circuit $C''$ such that $|||C''||| = C$, and any $k, \ell$, such that $k + n + \ell = 2$, one has

$$ \mathrm{QC} \vdash D(E_{k,l}(\|C''\|)) = \mathrm{id}_k \otimes C \otimes \mathrm{id}_l $$

where $\|C''\|$ (resp. $\|C''\|$) denotes the image of $\|C''\|$ by the canonical projection onto $\mathcal{QC}_{\text{seq}}$ (resp. onto $\mathcal{QC}$). For simplicity, by abuse of notation we will omit the canonical projection $\| \cdot \|$ in the rest of the proof. We proceed by structural induction on $C''$.

For any two $n$-qubit raw circuits $C_1, C_2$ such that $k + n + \ell = 2$, one has

$$ D(E_{k,l}(C_2 \circ C_1)) = D(E_{k,l}(C_2)) \circ D(E_{k,l}(C_1)) $$

and for any $n$-qubit raw circuit $C_1$ and $m$-qubit raw circuit $C_3$ such that $k + n + m + \ell = 2$,

$$ D(E_{k,l}(C_1 \otimes C_3)) = D(E_{k+n,l}(C_3)) \circ D(E_{k,l+m}(C_1)). $$

Hence, it remains the base cases:

$$ D(E_{0,0}(\mathcal{C})) = D(X_{[1,2]}) = \mathcal{C}, $$

$$ D(E_{k,l}(\mathcal{C})) = D(\epsilon) = \mathcal{C}, $$

$$ D(E_{k,l}(\mathcal{C})) = D(\epsilon) = \mathcal{C}, $$

$$ D(E_{1,0}(-\mathcal{H})) = D(H_{[0,1]}H_{[2,3]}) = \mathcal{H} \stackrel{(7)}{=} \mathcal{H}, $$

$$ D(E_{0,1}(-\mathcal{H})) = D(H_{[0,2]}H_{[1,3]}) = \mathcal{H} \stackrel{(7)}{=} \mathcal{H}, $$

$$ D(E_{1,0}(\mathcal{H})) = D((-1)_{[1]}(-1)_{[3]}) = \mathcal{H} \stackrel{(6)}{=} \mathcal{H}, $$

$$ D(E_{0,1}(\mathcal{H})) = D((-1)_{[2]}(-1)_{[3]}) = \mathcal{H} \stackrel{(9)(6)}{=} \mathcal{H}, $$

$$ D(E_{0,0}(\mathcal{H})) = D((-1)_{[3]}) = \mathcal{H}, $$

$$ D(E_{0,0}(\mathcal{H})) = D(H_{[2,3]}) = \mathcal{H}. $$

## C.2 Proof of Lemma 7.5

By Proposition 4.8, it suffices to prove that for each rule of Figure 7, of the form $w_1 \approx w_2$ where $w_1, w_2 \in \mathcal{G}_4^*$, and for any two words $w_0, w_3 \in \mathcal{G}_4^*$, one has $\mathrm{QC} \vdash D(w_0 w_1 w_3) = D(w_0 w_2 w_3)$. Since $D$ is a monoid homomorphism, it suffices to prove that $\mathrm{QC} \vdash D(w_1) = D(w_2)$. Note that since we are only working in dimension 4, we do not need to treat Equation (d4*).

Decoding Equation (a1*):

$$ D((-1)_{[0]}^2) = \mathcal{H} \stackrel{(81)(4)}{=} \mathcal{H} = D(\epsilon) $$

Decoding Equation (a3): One has $D(H_{[j,k]}^2) = D(H_{[j,k]}^2)$, and one can check that for any $j, k$, the circuit $D(H_{[j,k]}^2)$ is symmetric (between left and right). Since according to Equations (1), (2), (4), (5) and (g), all generators are self-inverse, this implies that $D(H_{[j,k]}^2)$ can be reduced to the identity.

Decoding Equation (a2): The argument is the same as for Equation (a3), after noting that $\mathcal{H} \stackrel{\oplus}{=} \mathcal{H}$.

Decoding Equation (b1*):

$$ D((-1)_{[0]}(-1)_{[1]}) = \mathcal{H} \stackrel{(81)(91)}{=} \mathcal{H} = D((-1)_{[1]}(-1)_{[0]}) $$
<table><caption>Table 1: Equations needed to transform $D(X_{[j,k]}) \circ D(H_{[l,m]}) \circ D(X_{[j,k]})$ into some $D(H_{[l',m']})$, together with the picture of the resulting $D(H_{[l',m']})$. We implicitly use Lemma B.3 when needed (as well as the topological rules and the shortcut definitions).</caption><thead><tr><th>D(H<sub>[l,m]</sub>)</th><th>D(X<sub>[2,3]</sub>)<br>= ⊕<br>⊕</th><th>D(X<sub>[0,1]</sub>)<br>= ⊕<br>⊕</th><th>D(X<sub>[0,2]</sub>)<br>= ⊕<br>⊕</th><th>D(X<sub>[1,3]</sub>)<br>= ⊕<br>⊕</th><th>D(X<sub>[1,2]</sub>)<br>= ⊕<br>⊕</th><th>D(X<sub>[0,3]</sub>)<br>= ⊕<br>⊕</th></tr></thead><tbody><tr><td>D(H<sub>[2,3]</sub>) = ⊕<br>⊕</td><td>(83)(94)(84)<br>⊕ ⊕ ⊕</td><td></td><td>none</td><td>none</td><td></td><td>none</td></tr><tr><td>D(H<sub>[0,1]</sub>) = ⊕<br>⊕</td><td></td><td>(82)(95)(84)<br>⊕ ⊕ ⊕</td><td>none</td><td>none</td><td>none</td><td>none</td></tr><tr><td>D(H<sub>[0,2]</sub>) = ⊕<br>⊕</td><td>(105)<br>⊕ ⊕ ⊕</td><td></td><td>(82)(95)(84)<br>⊕ ⊕ ⊕</td><td>none</td><td>none</td><td>none</td></tr><tr><td>D(H<sub>[1,3]</sub>) = ⊕<br>⊕</td><td>none<br>⊕ ⊕ ⊕</td><td></td><td></td><td>(83)(94)(84)<br>⊕ ⊕ ⊕</td><td>none</td><td>none</td></tr><tr><td>D(H<sub>[3,2]</sub>) = ⊕<br>⊕</td><td>(88)(94)(83)<br>⊕ ⊕ ⊕</td><td></td><td>(81)<br>⊕ ⊕ ⊕</td><td>none</td><td>none</td><td>none</td></tr><tr><td>D(H<sub>[1,0]</sub>) = ⊕<br>⊕</td><td>(89)(95)(82)<br>⊕ ⊕ ⊕</td><td></td><td>(81)(105)(101)<br>⊕ ⊕ ⊕</td><td></td><td></td><td>(81)<br>⊕ ⊕</td></tr><tr><td>D(H<sub>[2,0]</sub>) = ⊕<br>⊕</td><td>(81)(105)(101)<br>⊕ ⊕ ⊕</td><td></td><td>(89)(95)(82)<br>⊕ ⊕</td><td></td><td></td><td>(81)<br>⊕ ⊕</td></tr><tr><td>D(H<sub>[3,1]</sub>) = ⊕<br>⊕</td><td></td><td>(81)(106)<br>⊕ ⊕ ⊕</td><td></td><td>(88)(94)(83)<br>⊕ ⊕</td><td>none</td><td>none</td></tr><tr><td>D(H<sub>[2,1]</sub>) = ⊕<br>⊕</td><td></td><td>(100)(105)(82)<br>⊕ ⊕ ⊕</td><td></td><td>(82)<br>⊕ ⊕</td><td>none</td><td>none</td></tr><tr><td>D(H<sub>[0,3]</sub>) = ⊕<br>⊕</td><td>(105)(82)<br>⊕ ⊕</td><td></td><td></td><td>(82)<br>⊕ ⊕</td><td></td><td>(101)(106)<br>⊕ ⊕ ⊕</td></tr><tr><td>D(H<sub>[1,2]</sub>) = ⊕<br>⊕</td><td>(82)<br>⊕ ⊕</td><td></td><td>(107)<br>⊕ ⊕ ⊕</td><td></td><td>none</td><td>none</td></tr><tr><td>D(H<sub>[3,0]</sub>) = ⊕<br>⊕</td><td>(108)<br>⊕ ⊕ ⊕</td><td></td><td>(81)(82)<br>⊕ ⊕ ⊕</td><td></td><td></td><td>(81)(100)(105)<br>⊕ ⊕ ⊕</td></tr></tbody></table>

$$ \begin{aligned} & (103)^{(9)} \\ & \stackrel{(98)}{=} \text{---} = D((-1)_{[2]}) \end{aligned} $$
<figure><img src="image_56.png" /></figure>

<figure><img src="image_57.png" /></figure>

Decoding Equation (d3*):

<figure><img src="image_58.png" /></figure>
$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$ZX$};
\node[below] at (-0.5,-0.5) {$ZX$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$ZX$};
\node[below] at (-0.5,-0.5) {$ZX$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} \qquad (126) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$ZX$};
\node[below] at (-0.5,-0.5) {$ZX$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$ZX$};
\node[below] at (-0.5,-0.5) {$ZX$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} \qquad (127) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$ZX$};
\node[below] at (-0.5,-0.5) {$ZX$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$ZX$};
\node[below] at (-0.5,-0.5) {$ZX$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} \qquad (128) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$P$};
\node[below] at (-0.5,-0.5) {$P$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$XZ$};
\node[below] at (-0.5,-0.5) {$P$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} \qquad (129) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$P$};
\node[below] at (-0.5,-0.5) {$P$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$P$};
\node[below] at (-0.5,-0.5) {$P$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} \qquad (130) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$P$};
\node[below] at (-0.5,-0.5) {$P$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$P$};
\node[below] at (-0.5,-0.5) {$P$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} \qquad (131) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$H$};
\node[below] at (-0.5,-0.5) {$H$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$H$};
\node[below] at (-0.5,-0.5) {$H$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} \qquad (132) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$H$};
\node[below] at (-0.5,-0.5) {$H$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$H$};
\node[below] at (-0.5,-0.5) {$H$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} \qquad (133) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$H$};
\node[below] at (-0.5,-0.5) {$H$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$H$};
\node[below] at (-0.5,-0.5) {$H$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} \qquad (134) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$H$};
\node[below] at (-0.5,-0.5) {$H$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$H$};
\node[below] at (-0.5,-0.5) {$H$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} \qquad (135) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$ZX$};
\node[below] at (-0.5,-0.5) {$ZX$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$ZX$};
\node[below] at (-0.5,-0.5) {$ZX$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} \qquad (136) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$ZX$};
\node[below] at (-0.5,-0.5) {$ZX$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$ZX$};
\node[below] at (-0.5,-0.5) {$ZX$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} \qquad (137) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$XZ$};
\node[below] at (-0.5,-0.5) {$XZ$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$XZ$};
\node[below] at (-0.5,-0.5) {$XZ$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} \qquad (138) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$ZX$};
\node[below] at (-0.5,-0.5) {$ZX$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$ZX$};
\node[below] at (-0.5,-0.5) {$ZX$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} \qquad (139) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$XZ$};
\node[below] at (-0.5,-0.5) {$XZ$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$XZ$};
\node[below] at (-0.5,-0.5) {$XZ$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} \qquad (140) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$XZ$};
\node[below] at (-0.5,-0.5) {$XZ$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)]
\draw (-0.5,0) -- (0.5,0);
\draw (-0.5,-0.5) -- (0.5,-0.5);
\draw (-0.5,0.5) -- (0.5,0.5);
\draw (-0.5,-0.5) -- (-0.5,0.5);
\node[above] at (-0.5,0.5) {$XZ$};
\node[below] at (-0.5,-0.5) {$XZ$};
\draw[->] (-0.5,0) -- (-0.5,0.5);
\draw[->] (-0.5,0) -- (-0.5,-0.5);
\end{tikzpicture} \qquad (141) $$
$$ \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{ZX}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{ZX}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{ZX}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[above=0.25cm of (mid)] (topmid) {}; \node[below=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} \qquad (142) $$

$$ \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{ZX}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{ZX}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{ZX}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[above=0.25cm of (mid)] (topmid) {}; \node[below=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} \qquad (143) $$

$$ \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{ZX}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{ZX}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{ZX}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[above=0.25cm of (mid)] (topmid) {}; \node[below=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} \qquad (144) $$

$$ \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{ZX}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{ZX}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{ZX}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[above=0.25cm of (mid)] (topmid) {}; \node[below=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} \qquad (145) $$

$$ \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{H}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{H}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{H}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[above=0.25cm of (mid)] (topmid) {}; \node[below=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} \qquad (146) $$

$$ \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{H}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{H}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{H}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[above=0.25cm of (mid)] (topmid) {}; \node[below=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} \qquad (147) $$

PROOF.

*Proof of Equation (117): Equation (117) follows directly from Lemma B.2.*

*Proof of Equation (118): Equation (118) follows directly from Lemma B.2.*

*Proof of Equation (119):*

$$ \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{ZX}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{ZX}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{ZX}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[above=0.25cm of (mid)] (topmid) {}; \node[below=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} \qquad \text{Lemma 7.6} \qquad \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{ZX}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{ZX}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{ZX}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[above=0.25cm of (mid)] (topmid) {}; \node[below=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} $$

*Proof of Equation (120): Equation (120) follows directly from Lemma B.3 applied to Equation (119).*

*Proof of Equation (121):*

$$ \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{ZX}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{ZX}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{ZX}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[above=0.25cm of (mid)] (topmid) {}; \node[below=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} \qquad \text{Lemma 7.6} \qquad \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{ZX}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{ZX}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{ZX}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[above=0.25cm of (mid)] (topmid) {}; \node[below=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} $$

*Proof of Equation (122): Equation (122) follows directly from Lemma B.3 applied to Equation (121).*

*Proof of Equation (123):*

$$ \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{ZX}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{ZX}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{ZX}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (mid)] (topmid) {}; \node[above=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} \qquad \text{Lemma 7.6} \qquad \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{ZX}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{ZX}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{ZX}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (mid)] (topmid) {}; \node[above=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} $$

*Proof of Equation (124):*

$$ \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{ZX}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{ZX}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{ZX}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (mid)] (topmid) {}; \node[above=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} \qquad \text{Lemma 7.6} \qquad \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{ZX}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{ZX}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{ZX}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (mid)] (topmid) {}; \node[above=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} $$

*Proof of Equation (125):*

$$ \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{ZX}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{ZX}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{ZX}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (mid)] (topmid) {}; \node[above=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} \qquad \text{Lemma 7.6} \qquad \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{ZX}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{ZX}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{ZX}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (mid)] (topmid) {}; \node[above=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} $$

*Proof of Equation (126):*

$$ \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{ZX}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{ZX}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{ZX}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (mid)] (topmid) {}; \node[above=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} \qquad \text{Lemma 7.6} \qquad \begin{tikzpicture} [baseline={([yshift=-0.5ex]current bounding box.center)}] \node (top) at (0,0) {}; \node (bottom) at (0,-2) {}; \draw (top) -- (bottom); \node[below=0.25cm of top] (-1.5pt,-1.5pt) {$\mathbf{ZX}$}; \node[above=0.25cm of bottom] (-1.5pt,-2.5pt) {$\mathbf{ZX}$}; \node[below=0.25cm of bottom] (-1.5pt,-3.5pt) {$\mathbf{ZX}$}; \node[left=0.5cm of top] (-1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of top] (1.5pt,-3.5pt) {$=$}; \node[right=0.5cm of bottom] (1.5pt,-2.5pt) {$=$}; \node[left=0.5cm of bottom] (1.5pt,-0.5pt) {$=$}; \node[above=0.25cm of (1.5pt,-0.5pt)] (mid) {}; \node[below=0.25cm of (mid)] (topmid) {}; \node[above=0.25cm of (mid)] (bottommid) {}; \draw (topmid) -- (bottommid); \draw (mid) -- (mid); \draw (mid) -- (bottommid); \draw (bottommid) -- (bottom); \draw (top) -- (bottom); \end{tikzpicture} $$
### Proof of Equation (127):

<figure><img src="image_59.png" /></figure>

### Proof of Equation (128):

<figure><img src="image_60.png" /></figure>

### Proof of Equation (129):

<figure><img src="image_61.png" /></figure>

### Proof of Equation (130):

<figure><img src="image_62.png" /></figure>

### Proof of Equation (131):

<figure><img src="image_63.png" /></figure>

### Proof of Equation (132):

<figure><img src="image_64.png" /></figure>

### Proof of Equation (133):

<figure><img src="image_65.png" /></figure>

### Proof of Equation (134):

<figure><img src="image_66.png" /></figure>

### Proof of Equation (135):

<figure><img src="image_67.png" /></figure>

### Proof of Equation (136):

<figure><img src="image_68.png" /></figure>
$$ (5) \quad \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (0,0) -- (1,0) -- (1,1) -- (0,1) -- (0,0); \node[below] at (0,0) {ZX}; \node[above] at (1,1) {ZX}; \node[above] at (1,0) {ZX}; \node[below] at (0,1) {ZX}; \end{tikzpicture} $$

$$ = \quad \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (0,0) -- (1,0) -- (1,1) -- (0,1) -- (0,0); \node[below] at (0,0) {ZX}; \node[above] at (1,1) {ZX}; \node[above] at (1,0) {ZX}; \node[below] at (0,1) {ZX}; \end{tikzpicture} $$

$$ (123) \quad \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (0,0) -- (1,0) -- (1,1) -- (0,1) -- (0,0); \node[below] at (0,0) {ZX}; \node[above] at (1,1) {ZX}; \node[above] at (1,0) {ZX}; \node[below] at (0,1) {ZX}; \end{tikzpicture} $$

$$ (118) \quad \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (0,0) -- (1,0) -- (1,1) -- (0,1) -- (0,0); \node[below] at (0,0) {ZX}; \node[above] at (1,1) {ZX}; \node[above] at (1,0) {ZX}; \node[below] at (0,1) {ZX}; \end{tikzpicture} $$

*Proof of Equation (137):* Equation (137) follows directly from Equation (136), together with Equation (81).

*Proof of Equation (138):* Equation (138) follows directly from Lemma B.3 applied to Equation (136).

*Proof of Equation (139):*

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (0,0) -- (1,0) -- (1,1) -- (0,1) -- (0,0); \node[below] at (0,0) {ZX}; \node[above] at (1,1) {ZX}; \node[above] at (1,0) {ZX}; \node[below] at (0,1) {ZX}; \end{tikzpicture} = $$

$$ (14) \quad \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (0,0) -- (1,0) -- (1,1) -- (0,1) -- (0,0); \node[below] at (0,0) {ZX}; \node[above] at (1,1) {ZX}; \node[above] at (1,0) {ZX}; \node[below] at (0,1) {ZX}; \end{tikzpicture} $$

$$ (81) \quad \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (0,0) -- (1,0) -- (1,1) -- (0,1) -- (0,0); \node[below] at (0,0) {ZX}; \node[above] at (1,1) {ZX}; \node[above] at (1,0) {ZX}; \node[below] at (0,1) {ZX}; \end{tikzpicture} $$

$$ (81) \quad (132) \quad \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (0,0) -- (1,0) -- (1,1) -- (0,1) -- (0,0); \node[below] at (0,0) {ZX}; \node[above] at (1,1) {ZX}; \node[above] at (1,0) {ZX}; \node[below] at (0,1) {ZX}; \end{tikzpicture} $$

$$ (111) \quad (112) \quad (18) \quad (114) \quad \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (0,0) -- (1,0) -- (1,1) -- (0,1) -- (0,0); \node[below] at (0,0) {ZX}; \node[above] at (1,1) {ZX}; \node[above] at (1,0) {ZX}; \node[below] at (0,1) {ZX}; \node[above] at (1,1) {ZX}; \node[below] at (0,1) {ZX}; \node[above] at (1,0) {ZX}; \node[below] at (0,0) {ZX}; \end{tikzpicture} $$

$$ (81) \quad (17) \quad \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (0,0) -- (1,0) -- (1,1) -- (0,1) -- (0,0); \node[below] at (0,0) {ZX}; \node[above] at (1,1) {ZX}; \node[above] at (1,0) {ZX}; \node[below] at (0,1) {ZX}; \node[above] at (1,1) {ZX}; \node[below] at (0,1) {ZX}; \node[above] at (1,0) {ZX}; \node[below] at (0,0) {ZX}; \end{tikzpicture} $$

$$ (111) \quad (112) \quad (18) \quad (114) \quad \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (0,0) -- (1,0) -- (1,1) -- (0,1) -- (0,0); \node[below] at (0,0) {ZX}; \node[above] at (1,1) {ZX}; \node[above] at (1,0) {ZX}; \node[below] at (0,1) {ZX}; \node[above] at (1,1) {ZX}; \node[below] at (0,1) {ZX}; \node[above] at (1,0) {ZX}; \node[below] at (0,0) {ZX}; \end{tikzpicture} $$
(81)

<figure><img src="image_69.png" /></figure>

similar

<figure><img src="image_70.png" /></figure>

=

<figure><img src="image_71.png" /></figure>

Proof of Equation (140):

<figure><img src="image_72.png" /></figure>

(81)(118)

<figure><img src="image_73.png" /></figure>

(139)

<figure><img src="image_74.png" /></figure>

(117)

<figure><img src="image_75.png" /></figure>

Proof of Equation (141):

<figure><img src="image_76.png" /></figure>

(118)

<figure><img src="image_77.png" /></figure>

(137)

<figure><img src="image_78.png" /></figure>

(15)Lemma B.3

<figure><img src="image_79.png" /></figure>

Proof of Equation (142):

<figure><img src="image_80.png" /></figure>

<figure><img src="image_81.png" /></figure>

(13)

<figure><img src="image_82.png" /></figure>

Proof of Equation (143):

<figure><img src="image_83.png" /></figure>

(81)

<figure><img src="image_84.png" /></figure>

(131)(13)

<figure><img src="image_85.png" /></figure>

(81)

<figure><img src="image_86.png" /></figure>

Proof of Equation (144):

<figure><img src="image_87.png" /></figure>

(2)(123)

<figure><img src="image_88.png" /></figure>

(7)

<figure><img src="image_89.png" /></figure>

=

<figure><img src="image_90.png" /></figure>

(14)Lemma B.3

<figure><img src="image_91.png" /></figure>

(81)(10)(135)

<figure><img src="image_92.png" /></figure>

(14)Lemma B.3

<figure><img src="image_93.png" /></figure>
(7)

<figure><img src="image_94.png" /></figure>

=

<figure><img src="image_95.png" /></figure>

Proof of Equation (145):

<figure><img src="image_96.png" /></figure>

(137)(127)

<figure><img src="image_97.png" /></figure>

(14)

<figure><img src="image_98.png" /></figure>

(14)Lemma B.3

<figure><img src="image_99.png" /></figure>

=

<figure><img src="image_100.png" /></figure>

(81)

<figure><img src="image_101.png" /></figure>

(81)(9)(10)(12)

<figure><img src="image_102.png" /></figure>

(81)(14)

<figure><img src="image_103.png" /></figure>

(135)(9)(10)

<figure><img src="image_104.png" /></figure>

(81)(14)

<figure><img src="image_105.png" /></figure>

(127)(137)

<figure><img src="image_106.png" /></figure>

Proof of Equation (146):

<figure><img src="image_107.png" /></figure>

(81)

<figure><img src="image_108.png" /></figure>

(5)(7)(93)

<figure><img src="image_109.png" /></figure>
(1)

<figure><img src="image_110.png" /></figure>

Lemma 7.6

<figure><img src="image_111.png" /></figure>

Lemma 7.6

<figure><img src="image_112.png" /></figure>

(111)(18)(114)

<figure><img src="image_113.png" /></figure>

(4)

<figure><img src="image_114.png" /></figure>

(14)

<figure><img src="image_115.png" /></figure>

(5)

<figure><img src="image_116.png" /></figure>

Lemma 7.6

<figure><img src="image_117.png" /></figure>

Lemma B.3
together with
previous steps
$\equiv$

<figure><img src="image_118.png" /></figure>

Proof of Equation (147):

<figure><img src="image_119.png" /></figure>

Lemma 7.6
$\equiv$

<figure><img src="image_120.png" /></figure>

Lemma 7.6
$\equiv$

<figure><img src="image_121.png" /></figure>
Lemma 7.6

<figure><img src="image_122.png" /></figure>

Lemma 7.6

<figure><img src="image_123.png" /></figure>

Lemma 7.6

<figure><img src="image_124.png" /></figure>

Lemma 7.6

<figure><img src="image_125.png" /></figure>

(9)(132)

<figure><img src="image_126.png" /></figure>

(81)(10)

<figure><img src="image_127.png" /></figure>

(9)(132)

<figure><img src="image_128.png" /></figure>

(93)

<figure><img src="image_129.png" /></figure>

(81)(5)

<figure><img src="image_130.png" /></figure>

(146)

<figure><img src="image_131.png" /></figure>

Lemma 7.6

<figure><img src="image_132.png" /></figure>
$$ \text{Lemma 7.6} \quad \equiv $$

<figure><img src="image_133.png" /></figure>

$$ (2)(5) \quad \equiv $$

<figure><img src="image_134.png" /></figure>

$$ \text{Lemma 7.6} \quad \equiv $$

<figure><img src="image_135.png" /></figure>

$$ (134)(135) \quad \equiv $$

<figure><img src="image_136.png" /></figure>

$$ (111)(18)(9)(113)(114) \quad \equiv $$

<figure><img src="image_137.png" /></figure>

$$ \text{Lemma 7.6} \quad \equiv $$

<figure><img src="image_138.png" /></figure>

$$ (81)(14) \quad \equiv $$

<figure><img src="image_139.png" /></figure>

$$ (111)(18)(9) \quad \equiv $$

<figure><img src="image_140.png" /></figure>

$$ (81)(10)(9)(132) \quad \equiv $$

<figure><img src="image_141.png" /></figure>

$$ \text{Lemma 7.6} \quad \equiv $$

<figure><img src="image_142.png" /></figure>

$$ (112)(130) \quad \equiv $$

<figure><img src="image_143.png" /></figure>
$$ (18)(111)(112)(114)(113) = $$

$$ (18) = $$

Lemma 7.6
$= $

$$ (5) = $$

$$ (134) = $$

$$ (14) = $$

$$ (112)(113)(18)(9)(114)(111) = $$

$$ (9)(17) = $$

Lemma 7.6 (132)
$= $

$$ (111)(18)(112)(113)(9)(114) = $$

$$ (14) = $$

<figure><img src="image_144.png" /></figure>

<figure><img src="image_145.png" /></figure>

<figure><img src="image_146.png" /></figure>

<figure><img src="image_147.png" /></figure>

<figure><img src="image_148.png" /></figure>

<figure><img src="image_149.png" /></figure>

<figure><img src="image_150.png" /></figure>

<figure><img src="image_151.png" /></figure>

<figure><img src="image_152.png" /></figure>

<figure><img src="image_153.png" /></figure>

<figure><img src="image_154.png" /></figure>
(5)
$\equiv$

<figure><img src="image_155.png" /></figure>

Lemma 7.6
$\equiv$

<figure><img src="image_156.png" /></figure>

(10)(135)
$\equiv$

<figure><img src="image_157.png" /></figure>

Lemma 7.6
$\equiv$

<figure><img src="image_158.png" /></figure>

(5)
$\equiv$

<figure><img src="image_159.png" /></figure>

(134)
$\equiv$

<figure><img src="image_160.png" /></figure>

(14)
$\equiv$

<figure><img src="image_161.png" /></figure>

(112)(113)(18)(9)(114)(111)
$\equiv$

<figure><img src="image_162.png" /></figure>

(9)(17)
$\equiv$

<figure><img src="image_163.png" /></figure>

Lemma 7.6 (132)
$\equiv$

<figure><img src="image_164.png" /></figure>

(111)(18)(114)
$\equiv$

<figure><img src="image_165.png" /></figure>
(81)(14)

<figure><img src="image_166.png" /></figure>

(112)(130)(114)

<figure><img src="image_167.png" /></figure>

(92)(7)

<figure><img src="image_168.png" /></figure>

(112)(130)

<figure><img src="image_169.png" /></figure>

(112)(111)(113)(18)(9)(114)

<figure><img src="image_170.png" /></figure>

(14)

<figure><img src="image_171.png" /></figure>

(5)

<figure><img src="image_172.png" /></figure>

(113)(111)(18)(114)(112)

<figure><img src="image_173.png" /></figure>

(130)

<figure><img src="image_174.png" /></figure>

Lemma 7.6

<figure><img src="image_175.png" /></figure>

Lemma 7.6

<figure><img src="image_176.png" /></figure>
<figure><img src="image_177.png" /></figure>

(179)

<figure><img src="image_178.png" /></figure>

(180)

<figure><img src="image_179.png" /></figure>

(181)

<figure><img src="image_180.png" /></figure>

(182)

<figure><img src="image_181.png" /></figure>

(183)

<figure><img src="image_182.png" /></figure>

(184)

<figure><img src="image_183.png" /></figure>

(185)

<figure><img src="image_184.png" /></figure>

(186)

<figure><img src="image_185.png" /></figure>

(187)

<figure><img src="image_186.png" /></figure>

(188)

<figure><img src="image_187.png" /></figure>

(189)

<figure><img src="image_188.png" /></figure>

(190)

<figure><img src="image_189.png" /></figure>

(191)
<figure><img src="image_190.png" /></figure>

(206)

<figure><img src="image_191.png" /></figure>

(207)

<figure><img src="image_192.png" /></figure>

(208)

<figure><img src="image_193.png" /></figure>

(209)

<figure><img src="image_194.png" /></figure>

(210)

<figure><img src="image_195.png" /></figure>

(211)

<figure><img src="image_196.png" /></figure>

(212)

<figure><img src="image_197.png" /></figure>

(213)

<figure><img src="image_198.png" /></figure>

(214)

<figure><img src="image_199.png" /></figure>

(215)

<figure><img src="image_200.png" /></figure>

(216)

<figure><img src="image_201.png" /></figure>

(217)

<figure><img src="image_202.png" /></figure>

(218)
Proof of Equation (152):

$$ \overset{(9)(12)(4)}{=} \quad \begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
\tikzstyle{every node}=[draw, circle, fill=white, inner sep=1.2pt]
\node (XZ) at (0,0) {};
\node (H) at (1,0) {};
\node (ZX) at (0,1) {};
\draw (XZ) -- (H) -- (ZX);
\draw (XZ) -- (-1,0) -- (-ZX) -- (-1,1);
\end{tikzpicture} $$

$$ = \quad \begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
\tikzstyle{every node}=[draw, circle, fill=white, inner sep=1.2pt]
\node (XZ) at (0,0) {};
\node (XZ1) at (0,1) {};
\draw (XZ) -- (XZ1);
\draw (XZ) -- (-1,0) -- (-XZ1) -- (-1,1);
\draw (XZ) -- (1,0) -- (XZ1) -- (1,1);
\draw (XZ) -- (XZ1) -- (XZ1);
\end{tikzpicture} $$

$$ = \quad \begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
\tikzstyle{every node}=[draw, circle, fill=white, inner sep=1.2pt]
\node (H) at (0,0) {};
\node (ZX) at (0,1) {};
\draw (H) -- (ZX);
\draw (H) -- (-ZX);
\draw (ZX) -- (-1,0) -- (-ZX) -- (-1,1);
\draw (ZX) -- (1,0) -- (ZX) -- (1,1);
\draw (ZX) -- (ZX) -- (ZX);
\draw (ZX) -- (ZX);
\end{tikzpicture} $$

$$ \overset{(4)}{=} \quad \begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
\tikzstyle{every node}=[draw, circle, fill=white, inner sep=1.2pt]
\node (H) at (0,0) {};
\node (ZX) at (0,1) {};
\draw (H) -- (ZX);
\draw (H) -- (-ZX);
\draw (ZX) -- (-1,0) -- (-ZX) -- (-1,1);
\draw (ZX) -- (1,0) -- (ZX) -- (1,1);
\draw (ZX) -- (ZX) -- (ZX);
\draw (ZX) -- (ZX);
\end{tikzpicture} $$

$$ = \quad \begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
\tikzstyle{every node}=[draw, circle, fill=white, inner sep=1.2pt]
\node (H) at (0,0) {};
\node (ZX) at (0,1) {};
\draw (H) -- (ZX);
\draw (H) -- (-ZX);
\draw (ZX) -- (-1,0) -- (-ZX) -- (-1,1);
\draw (ZX) -- (1,0) -- (ZX) -- (1,1);
\draw (ZX) -- (ZX) -- (ZX);
\draw (ZX) -- (ZX);
\end{tikzpicture} $$

$$ \overset{(148)}{=} \quad \begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
\tikzstyle{every node}=[draw, circle, fill=white, inner sep=1.2pt]
\node (H) at (0,0) {};
\node (ZX) at (0,1) {};
\draw (H) -- (ZX);
\draw (H) -- (-ZX);
\draw (ZX) -- (-1,0) -- (-ZX) -- (-1,1);
\draw (ZX) -- (1,0) -- (ZX) -- (1,1);
\draw (ZX) -- (ZX) -- (ZX);
\draw (ZX) -- (ZX);
\end{tikzpicture} $$

$$ \overset{(82)}{=} \quad \begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
\tikzstyle{every node}=[draw, circle, fill=white, inner sep=1.2pt]
\node (H) at (0,0) {};
\node (ZX) at (0,1) {};
\draw (H) -- (ZX);
\draw (H) -- (-ZX);
\draw (ZX) -- (-1,0) -- (-ZX) -- (-1,1);
\draw (ZX) -- (1,0) -- (ZX) -- (1,1);
\draw (ZX) -- (ZX) -- (ZX);
\draw (ZX) -- (ZX);
\end{tikzpicture} $$

$$ = \quad \begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
\tikzstyle{every node}=[draw, circle, fill=white, inner sep=1.2pt]
\node (H) at (0,0) {};
\node (ZX) at (0,1) {};
\draw (H) -- (ZX);
\draw (H) -- (-ZX);
\draw (ZX) -- (-1,0) -- (-ZX) -- (-1,1);
\draw (ZX) -- (1,0) -- (ZX) -- (1,1);
\draw (ZX) -- (ZX) -- (ZX);
\draw (ZX) -- (ZX);
\end{tikzpicture} $$

$$ = \quad \begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
\tikzstyle{every node}=[draw, circle, fill=white, inner sep=1.2pt]
\node (H) at (0,0) {};
\node (ZX) at (0,1) {};
\draw (H) -- (ZX);
\draw (H) -- (-ZX);
\draw (ZX) -- (-1,0) -- (-ZX) -- (-1,1);
\draw (ZX) -- (1,0) -- (ZX) -- (1,1);
\draw (ZX) -- (ZX) -- (ZX);
\draw (ZX) -- (ZX);
\end{tikzpicture} $$

$$ = \quad \begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
\tikzstyle{every node}=[draw, circle, fill=white, inner sep=1.2pt]
\node (H) at (0,0) {};
\node (ZX) at (0,1) {};
\draw (H) -- (ZX);
\draw (H) -- (-ZX);
\draw (ZX) -- (-1,0) -- (-ZX) -- (-1,1);
\draw (ZX) -- (1,0) -- (ZX) -- (1,1);
\draw (ZX) -- (ZX) -- (ZX);
\draw (ZX) -- (ZX);
\end{tikzpicture} $$

$$ = \quad \begin{tikzpicture}[baseline=-0.5ex, scale=0.3, every node/.style={font=\scriptsize}] 
\tikzstyle{every node}=[draw, circle, fill=white, inner sep=1.2pt]
\node (H) at (0,0) {};
\node (ZX) at (0,1) {};
\draw (H) -- (ZX);
\draw (H) -- (-ZX);
\draw (ZX) -- (-1,0) -- (-ZX) -- (-1,1);
\draw (ZX) -- (1,0) -- (ZX) -- (1,1);
\draw (ZX) -- (ZX) -- (ZX);
\draw (ZX) -- (ZX);
\end{tikzpicture} $$
<figure><img src="image_203.png" /></figure>

Proof of Equation (153):

<figure><img src="image_204.png" /></figure>

Proof of Equation (154):

<figure><img src="image_205.png" /></figure>
Proof of Equation (155):

<figure><img src="image_206.png" /></figure>

Proof of Equation (156): Equation (156) follows directly from Equations (154) and (155).
### Proof of Equation (157):

<figure><img src="image_207.png" /></figure>

### Proof of Equation (158):

<figure><img src="image_208.png" /></figure>

<figure><img src="image_209.png" /></figure>

<figure><img src="image_210.png" /></figure>

<figure><img src="image_211.png" /></figure>

<figure><img src="image_212.png" /></figure>

<figure><img src="image_213.png" /></figure>

### Proof of Equation (159):

<figure><img src="image_214.png" /></figure>

### Proof of Equation (160): Equation (160) follows directly from Equations (157) and (159).

### Proof of Equation (161): By Equation (150), we just need to prove the following equation:

<figure><img src="image_215.png" /></figure>

and by Lemma B.4, to do so it suffices to prove the following equation:

<figure><img src="image_216.png" /></figure>
which we do as follows:

<figure><img src="image_217.png" /></figure>
$$ (148)(4) \quad \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.3] % Adjust scale if needed to fit dimensions
    % Top row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Middle row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Bottom row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Connections
    % Top to middle
    \draw (0.5, 0.4) -- (0.5, 1.6);
    \draw (0.5, 1.6) -- (0.5, 2.8);
    \draw (0.5, 2.8) -- (0.5, 4.0);

    % Middle to bottom
    \draw (0.5, 2.8) -- (0.5, 0.4);
    \draw (0.5, 0.4) -- (0.5, -0.8);
    \draw (0.5, -0.8) -- (0.5, -1.2);

    % Bottom to middle
    \draw (0.5, -1.2) -- (0.5, -0.4);
    \draw (0.5, -0.4) -- (0.5, -0.0);
    \draw (0.5, -0.0) -- (0.5, 0.0);

    % Labels
    \node at (0.5, 0.4) {H};
    \node at (0.5, 1.6) {H};
    \node at (0.5, 2.8) {H};
    \node at (0.5, -0.4) {H};
    \node at (0.5, -1.2) {H};

    % Vertices
    \node at (0.5, 0.4) {};
    \node at (0.5, 1.6) {};
    \node at (0.5, 2.8) {};
    \node at (0.5, -0.4) {};
    \node at (0.5, -1.2) {};
    \end{tikzpicture} $$

$$ (4)(5) \quad \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.3] % Adjust scale if needed to fit dimensions
    % Top row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Middle row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Bottom row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Connections
    % Top to middle
    \draw (0.5, 0.4) -- (0.5, 1.6);
    \draw (0.5, 1.6) -- (0.5, 2.8);
    \draw (0.5, 2.8) -- (0.5, 4.0);

    % Middle to bottom
    \draw (0.5, 2.8) -- (0.5, 0.4);
    \draw (0.5, 0.4) -- (0.5, -0.8);
    \draw (0.5, -0.8) -- (0.5, -1.2);

    % Bottom to middle
    \draw (0.5, -1.2) -- (0.5, -0.4);
    \draw (0.5, -0.4) -- (0.5, -0.0);
    \draw (0.5, -0.0) -- (0.5, 0.0);

    % Labels
    \node at (0.5, 0.4) {H};
    \node at (0.5, 1.6) {H};
    \node at (0.5, 2.8) {H};
    \node at (0.5, -0.4) {H};
    \node at (0.5, -1.2) {H};

    % Vertices
    \node at (0.5, 0.4) {};
    \node at (0.5, 1.6) {};
    \node at (0.5, 2.8) {};
    \node at (0.5, -0.4) {};
    \node at (0.5, -1.2) {};
    \end{tikzpicture} $$

Proof of Equation (162):

$$ \begin{array}{ccc} \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.3] % Adjust scale if needed to fit dimensions
    % Top row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Middle row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Bottom row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Connections
    % Top to middle
    \draw (0.5, 0.4) -- (0.5, 1.6);
    \draw (0.5, 1.6) -- (0.5, 2.8);
    \draw (0.5, 2.8) -- (0.5, 4.0);

    % Middle to bottom
    \draw (0.5, 2.8) -- (0.5, 0.4);
    \draw (0.5, 0.4) -- (0.5, -0.8);
    \draw (0.5, -0.8) -- (0.5, -1.2);

    % Bottom to middle
    \draw (0.5, -1.2) -- (0.5, -0.4);
    \draw (0.5, -0.4) -- (0.5, -0.0);
    \draw (0.5, -0.0) -- (0.5, 0.0);

    % Labels
    \node at (0.5, 0.4) {H};
    \node at (0.5, 1.6) {H};
    \node at (0.5, 2.8) {H};
    \node at (0.5, -0.4) {H};
    \node at (0.5, -1.2) {H};

    % Vertices
    \node at (0.5, 0.4) {};
    \node at (0.5, 1.6) {};
    \node at (0.5, 2.8) {};
    \node at (0.5, -0.4) {};
    \node at (0.5, -1.2) {};
    \end{tikzpicture} & = & \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.3] % Adjust scale if needed to fit dimensions
    % Top row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Middle row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Bottom row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Connections
    % Top to middle
    \draw (0.5, 0.4) -- (0.5, 1.6);
    \draw (0.5, 1.6) -- (0.5, 2.8);
    \draw (0.5, 2.8) -- (0.5, 4.0);

    % Middle to bottom
    \draw (0.5, 2.8) -- (0.5, 0.4);
    \draw (0.5, 0.4) -- (0.5, -0.8);
    \draw (0.5, -0.8) -- (0.5, -1.2);

    % Bottom to middle
    \draw (0.5, -1.2) -- (0.5, -0.4);
    \draw (0.5, -0.4) -- (0.5, -0.0);
    \draw (0.5, -0.0) -- (0.5, 0.0);

    % Labels
    \node at (0.5, 0.4) {H};
    \node at (0.5, 1.6) {H};
    \node at (0.5, 2.8) {H};
    \node at (0.5, -0.4) {H};
    \node at (0.5, -1.2) {H};

    % Vertices
    \node at (0.5, 0.4) {};
    \node at (0.5, 1.6) {};
    \node at (0.5, 2.8) {};
    \node at (0.5, -0.4) {};
    \node at (0.5, -1.2) {};
    \end{tikzpicture} \end{array} \quad (161) \quad \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.3] % Adjust scale if needed to fit dimensions
    % Top row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Middle row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Bottom row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Connections
    % Top to middle
    \draw (0.5, 0.4) -- (0.5, 1.6);
    \draw (0.5, 1.6) -- (0.5, 2.8);
    \draw (0.5, 2.8) -- (0.5, 4.0);

    % Middle to bottom
    \draw (0.5, 2.8) -- (0.5, 0.4);
    \draw (0.5, 0.4) -- (0.5, -0.8);
    \draw (0.5, -0.8) -- (0.5, -1.2);

    % Bottom to middle
    \draw (0.5, -1.2) -- (0.5, -0.4);
    \draw (0.5, -0.4) -- (0.5, -0.0);
    \draw (0.5, -0.0) -- (0.5, 0.0);

    % Labels
    \node at (0.5, 0.4) {H};
    \node at (0.5, 1.6) {H};
    \node at (0.5, 2.8) {H};
    \node at (0.5, -0.4) {H};
    \node at (0.5, -1.2) {H};

    % Vertices
    \node at (0.5, 0.4) {};
    \node at (0.5, 1.6) {};
    \node at (0.5, 2.8) {};
    \node at (0.5, -0.4) {};
    \node at (0.5, -1.2) {};
    \end{tikzpicture} \end{array} $$

Proof of Equation (163):

$$ \begin{array}{ccc} \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.3] % Adjust scale if needed to fit dimensions
    % Top row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Middle row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Bottom row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Connections
    % Top to middle
    \draw (0.5, 0.4) -- (0.5, 1.6);
    \draw (0.5, 1.6) -- (0.5, 2.8);
    \draw (0.5, 2.8) -- (0.5, 4.0);

    % Middle to bottom
    \draw (0.5, 2.8) -- (0.5, 0.4);
    \draw (0.5, 0.4) -- (0.5, -0.8);
    \draw (0.5, -0.8) -- (0.5, -1.2);

    % Bottom to middle
    \draw (0.5, -1.2) -- (0.5, -0.4);
    \draw (0.5, -0.4) -- (0.5, -0.0);
    \draw (0.5, -0.0) -- (0.5, 0.0);

    % Labels
    \node at (0.5, 0.4) {H};
    \node at (0.5, 1.6) {H};
    \node at (0.5, 2.8) {H};
    \node at (0.5, -0.4) {H};
    \node at (0.5, -1.2) {H};

    % Vertices
    \node at (0.5, 0.4) {};
    \node at (0.5, 1.6) {};
    \node at (0.5, 2.8) {};
    \node at (0.5, -0.4) {};
    \node at (0.5, -1.2) {};
    \end{tikzpicture} & (150) \\
    & (5) \\
    & (5)(4) \\
    & (150) \\
    & (161) \\
    & (159)(4) \end{array} $$

Proof of Equation (164):

$$ \begin{array}{ccc} \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.3] % Adjust scale if needed to fit dimensions
    % Top row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Middle row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Bottom row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Connections
    % Top to middle
    \draw (0.5, 0.4) -- (0.5, 1.6);
    \draw (0.5, 1.6) -- (0.5, 2.8);
    \draw (0.5, 2.8) -- (0.5, 4.0);

    % Middle to bottom
    \draw (0.5, 2.8) -- (0.5, 0.4);
    \draw (0.5, 0.4) -- (0.5, -0.8);
    \draw (0.5, -0.8) -- (0.5, -1.2);

    % Bottom to middle
    \draw (0.5, -1.2) -- (0.5, -0.4);
    \draw (0.5, -0.4) -- (0.5, -0.0);
    \draw (0.5, -0.0) -- (0.5, 0.0);

    % Labels
    \node at (0.5, 0.4) {H};
    \node at (0.5, 1.6) {H};
    \node at (0.5, 2.8) {H};
    \node at (0.5, -0.4) {H};
    \node at (0.5, -1.2) {H};

    % Vertices
    \node at (0.5, 0.4) {};
    \node at (0.5, 1.6) {};
    \node at (0.5, 2.8) {};
    \node at (0.5, -0.4) {};
    \node at (0.5, -1.2) {};
    \end{tikzpicture} & = & \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.3] % Adjust scale if needed to fit dimensions
    % Top row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Middle row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Bottom row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Connections
    % Top to middle
    \draw (0.5, 0.4) -- (0.5, 1.6);
    \draw (0.5, 1.6) -- (0.5, 2.8);
    \draw (0.5, 2.8) -- (0.5, 4.0);

    % Middle to bottom
    \draw (0.5, 2.8) -- (0.5, 0.4);
    \draw (0.5, 0.4) -- (0.5, -0.8);
    \draw (0.5, -0.8) -- (0.5, -1.2);

    % Bottom to middle
    \draw (0.5, -1.2) -- (0.5, -0.4);
    \draw (0.5, -0.4) -- (0.5, -0.0);
    \draw (0.5, -0.0) -- (0.5, 0.0);

    % Labels
    \node at (0.5, 0.4) {H};
    \node at (0.5, 1.6) {H};
    \node at (0.5, 2.8) {H};
    \node at (0.5, -0.4) {H};
    \node at (0.5, -1.2) {H};

    % Vertices
    \node at (0.5, 0.4) {};
    \node at (0.5, 1.6) {};
    \node at (0.5, 2.8) {};
    \node at (0.5, -0.4) {};
    \node at (0.5, -1.2) {};
    \end{tikzpicture} \end{array} \quad \text{Lemma D.3} \quad = $$

Proof of Equation (165):

$$ \begin{array}{ccc} \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.3] % Adjust scale if needed to fit dimensions
    % Top row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Middle row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Bottom row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Connections
    % Top to middle
    \draw (0.5, 0.4) -- (0.5, 1.6);
    \draw (0.5, 1.6) -- (0.5, 2.8);
    \draw (0.5, 2.8) -- (0.5, 4.0);

    % Middle to bottom
    \draw (0.5, 2.8) -- (0.5, 0.4);
    \draw (0.5, 0.4) -- (0.5, -0.8);
    \draw (0.5, -0.8) -- (0.5, -1.2);

    % Bottom to middle
    \draw (0.5, -1.2) -- (0.5, -0.4);
    \draw (0.5, -0.4) -- (0.5, -0.0);
    \draw (0.5, -0.0) -- (0.5, 0.0);

    % Labels
    \node at (0.5, 0.4) {H};
    \node at (0.5, 1.6) {H};
    \node at (0.5, 2.8) {H};
    \node at (0.5, -0.4) {H};
    \node at (0.5, -1.2) {H};

    % Vertices
    \node at (0.5, 0.4) {};
    \node at (0.5, 1.6) {};
    \node at (0.5, 2.8) {};
    \node at (0.5, -0.4) {};
    \node at (0.5, -1.2) {};
    \end{tikzpicture} & (4)(161)(159) & (4) \\
    & & \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.3] % Adjust scale if needed to fit dimensions
    % Top row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Middle row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Bottom row of AND gates
    \for each [y=0.2] of \yaxis nodes {
        \node at (0, \y) {H};
    }

    % Connections
    % Top to middle
    \draw (0.5, 0.4) -- (0.5, 1.6);
    \draw (0.5, 1.6) -- (0.5, 2.8);
    \draw (0.5, 2.8) -- (0.5, 4.0);

    % Middle to bottom
    \draw (0.5, 2.8) -- (0.5, 0.4);
    \draw (0.5, 0.4) -- (0.5, -0.8);
    \draw (0.5, -0.8) -- (0.5, -1.2);

    % Bottom to middle
    \draw (0.5, -1.2) -- (0.5, -0.4);
    \draw (0.5, -0.4) -- (0.5, -0.0);
    \draw (0.5, -0.0) -- (0.5, 0.0);

    % Labels
    \node at (0.5, 0.4) {H};
    \node at (0.5, 1.6) {H};
    \node at (0.5, 2.8) {H};
    \node at (0.5, -0.4) {H};
    \node at (0.5, -1.2) {H};

    % Vertices
    \node at (0.5, 0.4) {};
    \node at (0.5, 1.6) {};
    \node at (0.5, 2.8) {};
    \node at (0.5, -0.4) {};
    \node at (0.5, -1.2) {};
    \end{tikzpicture} \end{array} $$
### Proof of Equation (166):

<figure><img src="image_218.png" /></figure>

### Proof of Equation (167):

<figure><img src="image_219.png" /></figure>

### Proof of Equation (168):

<figure><img src="image_220.png" /></figure>

### Proof of Equation (169):

<figure><img src="image_221.png" /></figure>

### Proof of Equation (170): To prove the first equality, we have

<figure><img src="image_222.png" /></figure>
$$ \text{Lemma 7.6} \\ \equiv $$

<figure><img src="image_223.png" /></figure>

$$ (149) \\ \equiv $$

<figure><img src="image_224.png" /></figure>

$$ (142)(9)(168) \\ \equiv $$

<figure><img src="image_225.png" /></figure>

$$ (143)(142)(141)(81)(117) \\ \equiv $$

<figure><img src="image_226.png" /></figure>

and to prove the second equality, we have

<figure><img src="image_227.png" /></figure>

Proof of Equation (171):

<figure><img src="image_228.png" /></figure>

Proof of Equation (172):

<figure><img src="image_229.png" /></figure>
<figure><img src="image_230.png" /></figure>

<figure><img src="image_231.png" /></figure>

<figure><img src="image_232.png" /></figure>

*Proof of Equation (173):* Given Equation (172), Equation (173) follows from Lemma B.5 used together with Equation (166).

*Proof of Equation (174):*

<figure><img src="image_233.png" /></figure>

<figure><img src="image_234.png" /></figure>

<figure><img src="image_235.png" /></figure>

*Proof of Equation (175):*

<figure><img src="image_236.png" /></figure>

<figure><img src="image_237.png" /></figure>

<figure><img src="image_238.png" /></figure>

<figure><img src="image_239.png" /></figure>

<figure><img src="image_240.png" /></figure>

<figure><img src="image_241.png" /></figure>

<figure><img src="image_242.png" /></figure>
### Proof of Equation (176):

<figure><img src="image_243.png" /></figure>

### Proof of Equation (177):

<figure><img src="image_244.png" /></figure>

### Proof of Equation (178):

<figure><img src="image_245.png" /></figure>
<figure><img src="image_246.png" /></figure>

Proof of Equation (179):

<figure><img src="image_247.png" /></figure>

(81)

<figure><img src="image_248.png" /></figure>

(9)(168)Lemma B.3 (12)

<figure><img src="image_249.png" /></figure>

(139)(140)(9)(168)Lemma B.3

<figure><img src="image_250.png" /></figure>

(9)(168)Lemma B.3 (12)

<figure><img src="image_251.png" /></figure>

(139)(140)(9)(168)Lemma B.3

<figure><img src="image_252.png" /></figure>

(81)

<figure><img src="image_253.png" /></figure>

Proof of Equation (180):

<figure><img src="image_254.png" /></figure>

(81)

<figure><img src="image_255.png" /></figure>

(9)(168)Lemma B.3 (131)

<figure><img src="image_256.png" /></figure>

(139)(140)(9)(168)Lemma B.3

<figure><img src="image_257.png" /></figure>

(9)(168)Lemma B.3 (131)

<figure><img src="image_258.png" /></figure>
<figure><img src="image_259.png" /></figure>

Proof of Equation (181):

<figure><img src="image_260.png" /></figure>

(112)(157)(161)(153)(81) =

<figure><img src="image_261.png" /></figure>

(174)(114)(111) =

<figure><img src="image_262.png" /></figure>

(168)(127)(139)Lemma B.3 (140) =

<figure><img src="image_263.png" /></figure>

Lemma 7.6 =

<figure><img src="image_264.png" /></figure>

(2) =

<figure><img src="image_265.png" /></figure>

(81) =

<figure><img src="image_266.png" /></figure>

(9)(13) =

<figure><img src="image_267.png" /></figure>

(5)(9)(13) =

<figure><img src="image_268.png" /></figure>
(17)

<figure><img src="image_269.png" /></figure>

(17)

<figure><img src="image_270.png" /></figure>

(9)(13)(5)

<figure><img src="image_271.png" /></figure>

(81)

<figure><img src="image_272.png" /></figure>

(169)Lemma B.3

<figure><img src="image_273.png" /></figure>

(127)Lemma B.3 (81)(140)

<figure><img src="image_274.png" /></figure>

(169)Lemma B.3

<figure><img src="image_275.png" /></figure>

(81)

<figure><img src="image_276.png" /></figure>

(5)(9)(13)

<figure><img src="image_277.png" /></figure>

(17)

<figure><img src="image_278.png" /></figure>
$$ (9)(13)(5) = $$

<figure><img src="image_279.png" /></figure>

$$ (81) = $$

<figure><img src="image_280.png" /></figure>

$$ (169)(127)(139) = $$

<figure><img src="image_281.png" /></figure>

$$ \text{Lemma 7.6} = $$

<figure><img src="image_282.png" /></figure>

$$ (2) = $$

<figure><img src="image_283.png" /></figure>

$$ (111)(174)(114) = $$

<figure><img src="image_284.png" /></figure>

$$ (81)(153)(161)(157)(112) = $$

<figure><img src="image_285.png" /></figure>

*Proof of Equations (182) to (189):* Equations (182) to (189) follow directly from Equation (181) together with Equations (81), (157), (161) and (162).

*Proof of Equation (190):*

<figure><img src="image_286.png" /></figure>

$$ (112)(161)(157)(153)(81) = $$

<figure><img src="image_287.png" /></figure>

$$ (111)(18)(9) = $$

<figure><img src="image_288.png" /></figure>
(127)(168)Lemma B.3
$\equiv$

<figure><img src="image_289.png" /></figure>

Lemma D.3
$\equiv$

<figure><img src="image_290.png" /></figure>

(112)(18)
$\equiv$

<figure><img src="image_291.png" /></figure>

(9)(168)Lemma B.3
$\equiv$

<figure><img src="image_292.png" /></figure>

(112)(111)(18)
$\equiv$

<figure><img src="image_293.png" /></figure>

Lemma D.3
$\equiv$

<figure><img src="image_294.png" /></figure>

(112)(18)
$\equiv$

<figure><img src="image_295.png" /></figure>

(9)(168)Lemma B.3
$\equiv$

<figure><img src="image_296.png" /></figure>

(112)(111)(18)
$\equiv$

<figure><img src="image_297.png" /></figure>

(9)(111)(18)
$\equiv$

<figure><img src="image_298.png" /></figure>
$$ (111)(18)(9) $$

<figure><img src="image_299.png" /></figure>

$$ (127)(168)\text{Lemma B.3 (13)} $$

<figure><img src="image_300.png" /></figure>

$$ (9)(18) $$

<figure><img src="image_301.png" /></figure>

$$ \text{Lemma D.3} $$

<figure><img src="image_302.png" /></figure>

$$ (112)(18) $$

<figure><img src="image_303.png" /></figure>

$$ (9)(168) $$

<figure><img src="image_304.png" /></figure>

$$ (112)(111)(18) $$

<figure><img src="image_305.png" /></figure>

$$ \text{Lemma D.3} $$

<figure><img src="image_306.png" /></figure>

$$ (112)(18) $$

<figure><img src="image_307.png" /></figure>

$$ (9)(168) $$

<figure><img src="image_308.png" /></figure>
<figure><img src="image_309.png" /></figure>

*Proof of Equations (191) to (194): Equations (191) to (194) follow directly from Equation (190) together with Equations (81), (157), (161) and (162).*

*Proof of Equation (195):*

<figure><img src="image_310.png" /></figure>

(81)(166)(161)(170)

<figure><img src="image_311.png" /></figure>

<figure><img src="image_312.png" /></figure>

(194)

<figure><img src="image_313.png" /></figure>

<figure><img src="image_314.png" /></figure>

(112)(111)(18)

<figure><img src="image_315.png" /></figure>

<figure><img src="image_316.png" /></figure>

Lemma 7.6

<figure><img src="image_317.png" /></figure>

<figure><img src="image_318.png" /></figure>

(157)(163)(155)

<figure><img src="image_319.png" /></figure>

<figure><img src="image_320.png" /></figure>

Lemma 7.6

<figure><img src="image_321.png" /></figure>

<figure><img src="image_322.png" /></figure>

(18)(112)

<figure><img src="image_323.png" /></figure>

<figure><img src="image_324.png" /></figure>
<figure><img src="image_325.png" /></figure>

Proof of Equation (196):

<figure><img src="image_326.png" /></figure>

$$ (161)(157)(178)(81) = $$

<figure><img src="image_327.png" /></figure>

$$ (175) = $$

<figure><img src="image_328.png" /></figure>

$$ (162)(157)(183) = $$

<figure><img src="image_329.png" /></figure>

$$ (175) \text{ Lemmas B.2 and B.6} = $$

<figure><img src="image_330.png" /></figure>

$$ (162)(157)(183) = $$

<figure><img src="image_331.png" /></figure>

$$ (81)(157)(178)(161) = $$

<figure><img src="image_332.png" /></figure>

Proof of Equation (197):

<figure><img src="image_333.png" /></figure>

$$ (81)(166)(161)(170) = $$

<figure><img src="image_334.png" /></figure>

$$ (196) = $$

<figure><img src="image_335.png" /></figure>

$$ (112) = $$

<figure><img src="image_336.png" /></figure>
<figure><img src="image_337.png" /></figure>

<figure><img src="image_338.png" /></figure>

<figure><img src="image_339.png" /></figure>

<figure><img src="image_340.png" /></figure>

<figure><img src="image_341.png" /></figure>

*Proof of Equations (198) to (200): Equations (198) to (200) follow directly from Equation (196) together with Equations (81), (157), (161) and (162).*

*Proof of Equation (201): Equation (201) follows directly from Equations (162) and (171).*

*Proof of Equation (202):*

<figure><img src="image_342.png" /></figure>

<figure><img src="image_343.png" /></figure>

<figure><img src="image_344.png" /></figure>

<figure><img src="image_345.png" /></figure>
<figure><img src="image_346.png" /></figure>

<figure><img src="image_347.png" /></figure>

<figure><img src="image_348.png" /></figure>

Proof of Equation (203):

<figure><img src="image_349.png" /></figure>

(112)(157)
≡

<figure><img src="image_350.png" /></figure>

(112)(130)
≡

<figure><img src="image_351.png" /></figure>

(177)(157)(161)
≡

<figure><img src="image_352.png" /></figure>

(9)
≡

<figure><img src="image_353.png" /></figure>

(111)(112)(18)
≡

<figure><img src="image_354.png" /></figure>

(187)
≡

<figure><img src="image_355.png" /></figure>

(177)(157)(161)(81)
≡

<figure><img src="image_356.png" /></figure>
Lemma D.3
$\equiv$

<figure><img src="image_357.png" /></figure>

(161)(157)(81)(164)(163)
$\equiv$

<figure><img src="image_358.png" /></figure>

Lemma D.3
$\equiv$

<figure><img src="image_359.png" /></figure>

(161)(157)(81)(164)(163)
$\equiv$

<figure><img src="image_360.png" /></figure>

(81)(161)(157)(177)
$\equiv$

<figure><img src="image_361.png" /></figure>

(187)
$\equiv$

<figure><img src="image_362.png" /></figure>

(177)(157)(161)(81)
$\equiv$

<figure><img src="image_363.png" /></figure>

Lemma D.3
$\equiv$

<figure><img src="image_364.png" /></figure>

(161)(157)(163)(81)(164)
$\equiv$

<figure><img src="image_365.png" /></figure>

Lemma D.3
$\equiv$

<figure><img src="image_366.png" /></figure>
<figure><img src="image_367.png" /></figure>

Proof of Equation (204):

<figure><img src="image_368.png" /></figure>
(112)

<figure><img src="image_369.png" /></figure>

(112)(130)

<figure><img src="image_370.png" /></figure>

(112)(157)

<figure><img src="image_371.png" /></figure>

Proof of Equation (205):

<figure><img src="image_372.png" /></figure>

(112)(157)

<figure><img src="image_373.png" /></figure>

(112)(130)

<figure><img src="image_374.png" /></figure>

(111)(112)

<figure><img src="image_375.png" /></figure>

(189)

<figure><img src="image_376.png" /></figure>

(112)

<figure><img src="image_377.png" /></figure>

(112)(130)

<figure><img src="image_378.png" /></figure>

(112)(157)

<figure><img src="image_379.png" /></figure>
### Proof of Equation (206):

<figure><img src="image_380.png" /></figure>

### Proof of Equation (207):

<figure><img src="image_381.png" /></figure>

### Proof of Equation (208):

<figure><img src="image_382.png" /></figure>
*Proof of Equation (209): Equation (209) follows from Equations (81) and (208).*

*Proof of Equation (210):*

<figure><img src="image_383.png" /></figure>

*Proof of Equation (211): Given Equation (210), Equation (211) follows from Lemma B.5 used together with Equations (81), (166), (167) and (208).*

*Proof of Equation (212):*

<figure><img src="image_384.png" /></figure>

*Proof of Equation (213): Given Equation (212), Equation (213) follows from Lemma B.5 used together with Equations (4), (81), (167) and (208).*

*Proof of Equation (214): If $a = 0$, then we have*

<figure><img src="image_385.png" /></figure>
and if $a = 1$, we have

<figure><img src="image_386.png" /></figure>

*Proof of Equation (215):* If $a = 0$, then we have

<figure><img src="image_387.png" /></figure>

(212) =

<figure><img src="image_388.png" /></figure>

(162) =

<figure><img src="image_389.png" /></figure>

(212) =

The case $a = 1$ follows by Lemma B.5 used together with Equation (208).

*Proof of Equation (216):*

<figure><img src="image_390.png" /></figure>

Lemma D.3
=

<figure><img src="image_391.png" /></figure>

Lemma D.3 (9)(168) Lemma B.3
=

<figure><img src="image_392.png" /></figure>

Lemma D.3
=

<figure><img src="image_393.png" /></figure>

Lemma D.3 (9)(168)
=

<figure><img src="image_394.png" /></figure>

=

<figure><img src="image_395.png" /></figure>

*Proof of Equation (217):* Given Equation (216), Equation (217) follows by Lemma B.6 used together with Equation (118).
*Proof of Equation (218):* Given Equation (216), Equation (218) follows by Lemma B.6 used together with Equations (81) and (208).

*Proof of Equation (219):*

<figure><img src="image_396.png" /></figure>

*Proof of Equation (220):*

<figure><img src="image_397.png" /></figure>
<figure><img src="image_398.png" /></figure>

<figure><img src="image_399.png" /></figure>

<figure><img src="image_400.png" /></figure>

### Proof of Equation (221):

<figure><img src="image_401.png" /></figure>

<figure><img src="image_402.png" /></figure>

<figure><img src="image_403.png" /></figure>

<figure><img src="image_404.png" /></figure>

<figure><img src="image_405.png" /></figure>

### Proof of Equation (222): Given Equation (221), Equation (222) follows from Lemma B.5 used together with Equations (81), (118) and (208).

### Proof of Equation (223): Equation (223) follows directly from Equation (221) together with Equations (81) and (214).

### Proof of Equation (224): Equation (224) follows directly from Equation (222) together with Equations (81) and (214).

### Proof of Equation (225):

<figure><img src="image_406.png" /></figure>

<figure><img src="image_407.png" /></figure>

<figure><img src="image_408.png" /></figure>

### Proof of Equation (226):

<figure><img src="image_409.png" /></figure>

<figure><img src="image_410.png" /></figure>

<figure><img src="image_411.png" /></figure>

### Proof of Equation (227):

<figure><img src="image_412.png" /></figure>

<figure><img src="image_413.png" /></figure>
<figure><img src="image_414.png" /></figure>

<figure><img src="image_415.png" /></figure>

<figure><img src="image_416.png" /></figure>

<figure><img src="image_417.png" /></figure>

<figure><img src="image_418.png" /></figure>

<figure><img src="image_419.png" /></figure>

<figure><img src="image_420.png" /></figure>

<figure><img src="image_421.png" /></figure>

<figure><img src="image_422.png" /></figure>

Proof of Equation (228): If $\beta = 1$, then we have

<figure><img src="image_423.png" /></figure>

<figure><img src="image_424.png" /></figure>

<figure><img src="image_425.png" /></figure>
$$ (220)(227) = $$

<figure><img src="image_426.png" /></figure>

$$ (111)(157) = $$

<figure><img src="image_427.png" /></figure>

$$ (81)(161)(210)(214) = $$

<figure><img src="image_428.png" /></figure>

And if $\beta = 0$, we have

<figure><img src="image_429.png" /></figure>

$$ (214)(210)(161)(81)(156) = $$

<figure><img src="image_430.png" /></figure>

$$ (81)(167)(171) = $$

<figure><img src="image_431.png" /></figure>

$$ (111)(157) = $$

<figure><img src="image_432.png" /></figure>

$$ (220)\text{Lemma D.3 (227)} = $$

<figure><img src="image_433.png" /></figure>

$$ (111)(157) = $$

<figure><img src="image_434.png" /></figure>

$$ (171)(81)(167) = $$

<figure><img src="image_435.png" /></figure>

$$ (156)(81)(161)(210)(214) = $$

<figure><img src="image_436.png" /></figure>
*Proof of Equation (229)*: Up to using Lemma B.6 (together with Equations (81) and (208)), we can assume without loss of generality that $a = 0$. We have

<figure><img src="image_437.png" /></figure>

*Proof of Equation (230)*:

<figure><img src="image_438.png" /></figure>

*Proof of Equation (231)*:

<figure><img src="image_439.png" /></figure>
$$ = $$

$$ (10) = $$

$$ \text{same as previous steps} = $$

$$ (161)(215)(214) = $$

### Proof of Equation (232):

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (H) at (0,0) {H}; \node (ZX) at (0,-1) {ZX}; \draw (H) -- (ZX); \node[below=2pt of H] {$(135)(164)$}; \node[below=2pt of ZX] {$=$}; \node[above=2pt of H] {(161)(164)}; \node[above=2pt of ZX] {$=$}; \node (Z) at (3,0) {Z}; \node (ZX) at (3,-1) {ZX}; \draw (Z) -- (ZX); \node[below=2pt of Z] {(157)(161)(215)(214)}; \node[below=2pt of ZX] {$=$}; \node[above=2pt of Z] {(214)(215)(161)(157)}; \node[above=2pt of ZX] {$=$}; \end{tikzpicture} $$

### Proof of Equation (233): Given Equation (232), Equation (233) follows from Lemma B.5 used together with Equations (5), (81) and (208).

### Proof of Equation (234):

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (H) at (0,0) {H}; \node (ZX) at (0,-1) {ZX}; \draw (H) -- (ZX); \node[below=2pt of H] {(157)(161)(215)(214)}; \node[below=2pt of ZX] {$=$}; \node (Z) at (3,0) {Z}; \node (ZX) at (3,-1) {ZX}; \draw (Z) -- (ZX); \node[below=2pt of Z] {(214)(215)(161)(157)}; \node[below=2pt of ZX] {$=$}; \node[above=2pt of H] {(161)(164)}; \node[above=2pt of ZX] {$=$}; \node (Z) at (6,0) {Z}; \node (ZX) at (6,-1) {ZX}; \draw (Z) -- (ZX); \node[below=2pt of Z] {(135)(164)}; \node[below=2pt of ZX] {$=$}; \node[above=2pt of Z] {(161)(164)}; \node[above=2pt of ZX] {$=$}; \end{tikzpicture} $$

### Proof of Equation (235): Given Equation (234), Equation (235) follows from Lemma B.5 used together with Equations (5), (81) and (208).

### Proof of Equation (236):

$$ \begin{array}{c} \text{Lemma 7.6} \\ = \\ \begin{array}{c} (81)(5)(215)(232) \\ = \\ (5) \end{array} \end{array} $$
$$ = $$

$$ \stackrel{(7)}{=} $$

Proof of Equation (237):

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (XZ) at (0,0) {XZ}; \draw (0,0) -- (1,1); \draw (0,0) -- (-1,1); \draw (0,0) -- (1,-1); \draw (0,0) -- (-1,-1); \end{tikzpicture} $$

$$ (81)(4)(231) = $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (XZ) at (0,0) {XZ}; \draw (0,0) -- (1,1); \draw (0,0) -- (-1,1); \draw (0,0) -- (1,-1); \draw (0,0) -- (-1,-1); \end{tikzpicture} $$

$$ \text{Lemma 7.6} = $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (XZ) at (0,0) {XZ}; \draw (0,0) -- (1,1); \draw (0,0) -- (-1,1); \draw (0,0) -- (1,-1); \draw (0,0) -- (-1,-1); \end{tikzpicture} $$

$$ (213) = $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (XZ) at (0,0) {XZ}; \draw (0,0) -- (1,1); \draw (0,0) -- (-1,1); \draw (0,0) -- (1,-1); \draw (0,0) -- (-1,-1); \node[below=1pt] at (0,0) {H}; \node[above=1pt] at (1,1) {H}; \node[below=1pt] at (1,-1) {H}; \node[above=1pt] at (-1,1) {H}; \node[below=1pt] at (-1,-1) {H}; \end{tikzpicture} $$

$$ (4) = $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (XZ) at (0,0) {XZ}; \draw (0,0) -- (1,1); \draw (0,0) -- (-1,1); \draw (0,0) -- (1,-1); \draw (0,0) -- (-1,-1); \node[below=1pt] at (0,0) {H}; \node[above=1pt] at (1,1) {H}; \node[below=1pt] at (1,-1) {H}; \node[above=1pt] at (-1,1) {H}; \node[below=1pt] at (-1,-1) {H}; \end{tikzpicture} $$

$$ (212) = $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (XZ) at (0,0) {XZ}; \draw (0,0) -- (1,1); \draw (0,0) -- (-1,1); \draw (0,0) -- (1,-1); \draw (0,0) -- (-1,-1); \end{tikzpicture} $$

$$ (6) = $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (XZ) at (0,0) {XZ}; \draw (0,0) -- (1,1); \draw (0,0) -- (-1,1); \draw (0,0) -- (1,-1); \draw (0,0) -- (-1,-1); \end{tikzpicture} $$

Proof of Equation (238):

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (XZ) at (0,0) {XZ}; \draw (0,0) -- (1,1); \draw (0,0) -- (-1,1); \draw (0,0) -- (1,-1); \draw (0,0) -- (-1,-1); \end{tikzpicture} $$

$$ = $$

$$ (236) = $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (XZ) at (0,0) {XZ}; \draw (0,0) -- (1,1); \draw (0,0) -- (-1,1); \draw (0,0) -- (1,-1); \draw (0,0) -- (-1,-1); \node[below=1pt] at (0,0) {H}; \node[above=1pt] at (1,1) {XZ}; \node[below=1pt] at (1,-1) {H}; \node[above=1pt] at (-1,1) {XZ}; \node[below=1pt] at (-1,-1) {H}; \end{tikzpicture} $$
<figure><img src="image_440.png" /></figure>

<figure><img src="image_441.png" /></figure>

<figure><img src="image_442.png" /></figure>

*Proof of Equation (239):* Up to using Lemma B.6 (together with Equations (81) and (118)), we can assume without loss of generality that $a = 1$. If $\gamma = 1$, then we have

<figure><img src="image_443.png" /></figure>

(214)(215)(161) =

<figure><img src="image_444.png" /></figure>

(127)Lemma B.3 (161)(176) =

<figure><img src="image_445.png" /></figure>

Lemma D.3 =

<figure><img src="image_446.png" /></figure>

(127)(161)(176)Lemmas B.2 and B.6 =

<figure><img src="image_447.png" /></figure>

Lemma D.3 =

<figure><img src="image_448.png" /></figure>

(161)(214)(215) =

<figure><img src="image_449.png" /></figure>

And if $\gamma = 0$, we have

<figure><img src="image_450.png" /></figure>

Lemma D.3 =

<figure><img src="image_451.png" /></figure>
<figure><img src="image_452.png" /></figure>

<figure><img src="image_453.png" /></figure>

<figure><img src="image_454.png" /></figure>

<figure><img src="image_455.png" /></figure>

<figure><img src="image_456.png" /></figure>

<figure><img src="image_457.png" /></figure>

<figure><img src="image_458.png" /></figure>

*Proof of Equation (240)*: Up to using Equation (81), we can assume without loss of generality that $\alpha = 1$. Up to using Equations (81) and (238), we can assume without loss of generality that $\beta = 1$ and $\delta = 1$. And up to using Lemma B.6 (together with Equation (208)), we can assume without loss of generality that $a = 1$ and $b = 1$. That is, we just need to prove the following two equations:

<figure><img src="image_459.png" /></figure>

<figure><img src="image_460.png" /></figure>

To prove the first one, we have

<figure><img src="image_461.png" /></figure>
<figure><img src="image_462.png" /></figure>

and to prove the second one, we have

<figure><img src="image_463.png" /></figure>

*Proof of Equation (241)*: Up to using Equation (81), we can assume without loss of generality that $\alpha = 1$ and $\beta = 1$. Up to using Equations (214) and (215), we can assume without loss of generality that $\gamma \le \delta$. That is, we just need to prove the following three equations:

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (A) at (0,0) {};
\node (B) at (0,1) {};
\draw (A) -- (B) node Midpoint[above] {};
\draw (A) -- (B) node Left[below] {};
\draw (A) -- (B) node Right[above] {};
\node at (0.5,0.5) {$\begin{array}{c} (241a) \\ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (A) at (0,0) {};
\node (B) at (0,1) {};
\draw (A) -- (B) node Midpoint[above] {};
\draw (A) -- (B) node Left[below] {};
\draw (A) -- (B) node Right[above] {};
\node at (0.5,0.5) {$\begin{array}{c} \text{---} \\ \text{---} \end{array}$};
\end{tikzpicture} \end{array}$} $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (A) at (0,0) {};
\node (B) at (0,1) {};
\draw (A) -- (B) node Midpoint[above] {};
\draw (A) -- (B) node Left[below] {};
\draw (A) -- (B) node Right[above] {};
\node at (0.5,0.5) {$\begin{array}{c} (241b) \\ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (A) at (0,0) {};
\node (B) at (0,1) {};
\draw (A) -- (B) node Midpoint[above] {};
\draw (A) -- (B) node Left[below] {};
\draw (A) -- (B) node Right[above] {};
\node at (0.5,0.5) {$\begin{array}{c} \text{---} \\ \text{---} \end{array}$};
\end{tikzpicture} \end{array}$} $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (A) at (0,0) {};
\node (B) at (0,1) {};
\draw (A) -- (B) node Midpoint[above] {};
\draw (A) -- (B) node Left[below] {};
\draw (A) -- (B) node Right[above] {};
\node at (0.5,0.5) {$\begin{array}{c} (241c) \\ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (A) at (0,0) {};
\node (B) at (0,1) {};
\draw (A) -- (B) node Midpoint[above] {};
\draw (A) -- (B) node Left[below] {};
\draw (A) -- (B) node Right[above] {};
\node at (0.5,0.5) {$\begin{array}{c} \text{---} \\ \text{---} \end{array}$};
\end{tikzpicture} \end{array}$} $$

To prove Equation (241a), up to using Lemma B.6 (together with Equations (81) and (208)), we can assume without loss of generality that $a = 1$ and $b = 1$. We have

<figure><img src="image_464.png" /></figure>

To prove Equation (241b), again up to using Lemma B.6 (together with Equations (81) and (208)), we can assume without loss of generality that $a = 1$ and $b = 1$. We have

<figure><img src="image_465.png" /></figure>
<figure><img src="image_466.png" /></figure>

<figure><img src="image_467.png" /></figure>

<figure><img src="image_468.png" /></figure>

And to prove Equation (241c), again up to using Lemma B.6 (together with Equations (81) and (208)), we can assume without loss of generality that $a = 1$ and $b = 1$. We have

<figure><img src="image_469.png" /></figure>

<figure><img src="image_470.png" /></figure>

<figure><img src="image_471.png" /></figure>

<figure><img src="image_472.png" /></figure>

*Proof of Equation (242)*: Up to using Equation (81), we can assume without loss of generality that $\alpha = 1$.

First, we treat the case where $\beta = \gamma = \delta = 1$. Up to using Lemma B.6 (together with Equations (81), (111) and (208)), we can assume without loss of generality that $a = 0$ and $b = 0$. We have

<figure><img src="image_473.png" /></figure>

<figure><img src="image_474.png" /></figure>

<figure><img src="image_475.png" /></figure>
<figure><img src="image_476.png" /></figure>

<figure><img src="image_477.png" /></figure>

<figure><img src="image_478.png" /></figure>

Then, we treat the case where $\beta = \delta = 1$ and $\gamma = 0$. Again, up to using Lemma B.6 (together with Equations (81), (111) and (208)), we can assume without loss of generality that $a = 0$ and $b = 0$. We have

<figure><img src="image_479.png" /></figure>

<figure><img src="image_480.png" /></figure>

<figure><img src="image_481.png" /></figure>

<figure><img src="image_482.png" /></figure>

<figure><img src="image_483.png" /></figure>

<figure><img src="image_484.png" /></figure>

<figure><img src="image_485.png" /></figure>

Then, to treat the cases where $\beta = 0$ and $\delta = 1$, we have

<figure><img src="image_486.png" /></figure>

<figure><img src="image_487.png" /></figure>

<figure><img src="image_488.png" /></figure>
$$ (111)(113) = $$

<figure><img src="image_489.png" /></figure>

$$ (2)(1)(237)(236) = $$

<figure><img src="image_490.png" /></figure>

previous cases
$= $

<figure><img src="image_491.png" /></figure>

$$ (2)(1)(237)(236) = $$

<figure><img src="image_492.png" /></figure>

$$ (111)(113) = $$

<figure><img src="image_493.png" /></figure>

=

<figure><img src="image_494.png" /></figure>

Finally, to treat the cases where $\delta = 0$, we have

$$ (112)(111)(113) = $$

<figure><img src="image_495.png" /></figure>

=

<figure><img src="image_496.png" /></figure>

<figure><img src="image_497.png" /></figure>

$$ (2)(1)(237)(236) = $$

<figure><img src="image_498.png" /></figure>

$$ (112)(111)(113) = $$

<figure><img src="image_499.png" /></figure>
<figure><img src="image_500.png" /></figure>

<figure><img src="image_501.png" /></figure>

<figure><img src="image_502.png" /></figure>

<figure><img src="image_503.png" /></figure>

<figure><img src="image_504.png" /></figure>

*Proof of Equation (243):* Up to using Equation (81), we can assume without loss of generality that $\alpha = 1$.

First, we treat the case where $\beta = \gamma = \delta = 1$. Up to using Lemma B.6 (together with Equations (81), (111) and (208)), we can assume without loss of generality that $a = 0$ and $b = 0$. We have

<figure><img src="image_505.png" /></figure>

(210)(81) =

<figure><img src="image_506.png" /></figure>

(111)(112) =

<figure><img src="image_507.png" /></figure>

(112)(130) =

<figure><img src="image_508.png" /></figure>

(202)(196)(203)(192) =

<figure><img src="image_509.png" /></figure>

(112)(130)(111) =

<figure><img src="image_510.png" /></figure>
<figure><img src="image_511.png" /></figure>

Then, we treat the case where $\beta = \delta = 1$ and $\gamma = 0$. Again, up to using Lemma B.6 (together with Equations (81), (111) and (208)), we can assume without loss of generality that $a = 0$ and $b = 0$. We have

<figure><img src="image_512.png" /></figure>

Then, to treat the cases where $\beta = 0$ and $\delta = 1$, again up to using Lemma B.6 (together with Equations (81), (111) and (208)), we can assume without loss of generality that $a = 0$ and $b = 0$. We have

<figure><img src="image_513.png" /></figure>
<figure><img src="image_514.png" /></figure>

<figure><img src="image_515.png" /></figure>

<figure><img src="image_516.png" /></figure>

Finally, to treat the cases where $\delta = 0$, again up to using Lemma B.6 (together with Equations (81), (111) and (208)), we can assume without loss of generality that $a = 0$ and $b = 0$. We have

<figure><img src="image_517.png" /></figure>

<figure><img src="image_518.png" /></figure>

<figure><img src="image_519.png" /></figure>

<figure><img src="image_520.png" /></figure>

<figure><img src="image_521.png" /></figure>

<figure><img src="image_522.png" /></figure>

<figure><img src="image_523.png" /></figure>

*Proof of Equation (244):* If $\alpha = \beta = 1$, then up to using Lemma B.6 (together with Equations (81), (111) and (208)), we can assume without loss of generality that $a = 0$ and $b = 0$. We have

<figure><img src="image_524.png" /></figure>

$$ (214)(210)(161)(81) = $$

<figure><img src="image_525.png" /></figure>
(112)
≡

<figure><img src="image_526.png" /></figure>

(112)(130)
≡

<figure><img src="image_527.png" /></figure>

(111)(112)(130)
≡

<figure><img src="image_528.png" /></figure>

(183)(198)
≡

<figure><img src="image_529.png" /></figure>

(111)(112)(130)
≡

<figure><img src="image_530.png" /></figure>

(112)(130)
≡

<figure><img src="image_531.png" /></figure>

(157)(111)
≡

<figure><img src="image_532.png" /></figure>

(184)(206)
≡

<figure><img src="image_533.png" /></figure>

(157)
≡

<figure><img src="image_534.png" /></figure>

(112)(130)
≡

<figure><img src="image_535.png" /></figure>

(112)
≡

<figure><img src="image_536.png" /></figure>
<figure><img src="image_537.png" /></figure>

If $\beta = 1$ and $\alpha = 0$, then again, up to using Lemma B.6 (together with Equations (81), (111) and (208)), we can assume without loss of generality that $a = 0$ and $b = 0$. We have

<figure><img src="image_538.png" /></figure>

And if $\beta = 0$, then we have

<figure><img src="image_539.png" /></figure>
<figure><img src="image_540.png" /></figure>

*Proof of Equation (245):* If $\alpha = \beta = 1$, then up to using Lemma B.6 (together with Equations (81), (111) and (208)), we can assume without loss of generality that $a = 0$ and $b = 0$. We have

<figure><img src="image_541.png" /></figure>
$$ (112) = $$

<figure><img src="image_542.png" /></figure>

$$ (112)(130) = $$

<figure><img src="image_543.png" /></figure>

$$ (111)(112)(130)(157) = $$

<figure><img src="image_544.png" /></figure>

$$ (200)(185) = $$

<figure><img src="image_545.png" /></figure>

$$ (157) = $$

<figure><img src="image_546.png" /></figure>

$$ (130) = $$

<figure><img src="image_547.png" /></figure>

$$ (111)(112) = $$

<figure><img src="image_548.png" /></figure>

$$ (111)(112)(130)(157) = $$

<figure><img src="image_549.png" /></figure>

$$ (112)(130) = $$

<figure><img src="image_550.png" /></figure>

similar to
previous steps
$= $

<figure><img src="image_551.png" /></figure>

$$ (81)(161)(210)(214) = $$

<figure><img src="image_552.png" /></figure>
If $\alpha = 1$ and $\beta = 0$, then again, up to using Lemma B.6 (together with Equations (81), (111) and (208)), we can assume without loss of generality that $a = 0$ and $b = 0$. We have

<figure><img src="image_553.png" /></figure>

Finally, if $\alpha = 0$, then again, up to using Lemma B.6 (together with Equations (81), (111) and (208)), we can assume without loss of generality that $a = 0$ and $b = 0$. We have

<figure><img src="image_554.png" /></figure>

Proof of Equation (246):

<figure><img src="image_555.png" /></figure>

Proof of Equation (247): If $\gamma = 1$, then we have

<figure><img src="image_556.png" /></figure>
<figure><img src="image_557.png" /></figure>

(18)

<figure><img src="image_558.png" /></figure>

And if $\gamma = 0$, then we have

<figure><img src="image_559.png" /></figure>

Lemma 7.6

<figure><img src="image_560.png" /></figure>

previous case

<figure><img src="image_561.png" /></figure>

(229)

<figure><img src="image_562.png" /></figure>

Lemma 7.6

<figure><img src="image_563.png" /></figure>

*Proof of Equation (248)*: If $\gamma = 1$ and $\beta = 1$, then we have

<figure><img src="image_564.png" /></figure>

(111)(18)

<figure><img src="image_565.png" /></figure>

(234)(235)

<figure><img src="image_566.png" /></figure>

(18)

<figure><img src="image_567.png" /></figure>

If $\gamma = 1$ and $\beta = 0$, then up to using Lemma B.6 (together with Equations (81), (111) and (208)), we can assume without loss of generality that $a = 0$. We have

<figure><img src="image_568.png" /></figure>

(81)(208)(215)(221)

<figure><img src="image_569.png" /></figure>
And if $\gamma = 0$, then we have

<figure><img src="image_570.png" /></figure>

<figure><img src="image_571.png" /></figure>

## D.4 Auxiliary Equations on 5 Qubits

Similarly to Appendix D.3, we will use the 4-qubit version of Lemma 5.1:

**Lemma D.6 (Conditional 4-qubit completeness).** For any 4-qubit quantum circuits $C_1, C_2$ over $\{-\mathbf{H}\}, \leftarrow, \rightarrow, \mathbf{H}\right\}$, if $\llbracket C_1 \rrbracket = \llbracket C_2 \rrbracket$ then
$\text{QC} \vdash (\text{---} \otimes C_1) = (\text{---} \otimes C_2)$ and $\text{QC} \vdash (C_1 \otimes \text{---}) = (C_2 \otimes \text{---})$.

**Lemma D.7.** The following equations are consequences of the equations of Figure 4:

$$ \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.7] 
% Vertices
\node[circle, fill, inner sep=1.5pt] (top) at (0,0) {};
\node[circle, fill, inner sep=1.5pt] (bottom) at (0,1) {};
\node[circle, fill, inner sep=1.5pt] (left) at (-1,0) {};
\node[circle, fill, inner sep=1.5pt] (right) at (1,0) {};
\node[circle, fill, inner sep=1.5pt] (topleft) at (-1,1) {};
\node[circle, fill, inner sep=1.5pt] (topright) at (1,1) {};
\node[circle, fill, inner sep=1.5pt] (bottomleft) at (-1,0) {};
\node[circle, fill, inner sep=1.5pt] (bottomright) at (1,0) {};

% Edges
\draw[->] (top) -- (topleft);
\draw[->] (top) -- (topright);
\draw[->] (bottom) -- (bottomleft);
\draw[->] (bottom) -- (bottomright);

% Labels
\node[above] at (top) {---};
\node[above] at (bottom) {---};
\node[below] at (left) {---};
\node[below] at (right) {---};
\node[above] at (topleft) {---};
\node[above] at (topright) {---};
\node[below] at (bottomleft) {---};
\node[below] at (bottomright) {---};

\end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center), scale=0.7] 
% Vertices
\node[circle, fill, inner sep=1.5pt] (top) at (0,0) {};
\node[circle, fill, inner sep=1.5pt] (bottom) at (0,1) {};
\node[circle, fill, inner sep=1.5pt] (left) at (-1,0) {};
\node[circle, fill, inner sep=1.5pt] (right) at (1,0) {};
\node[circle, fill, inner sep=1.5pt] (topleft) at (-1,1) {};
\node[circle, fill, inner sep=1.5pt] (topright) at (1,1) {};
\node[circle, fill, inner sep=1.5pt] (bottomleft) at (-1,0) {};
\node[circle, fill, inner sep=1.5pt] (bottomright) at (1,0) {};

% Edges
\draw[->] (top) -- (topleft);
\draw[->] (top) -- (topright);
\draw[->] (bottom) -- (bottomleft);
\draw[->] (bottom) -- (bottomright);

% Labels
\node[above] at (top) {---};
\node[above] at (bottom) {---};
\node[below] at (left) {---};
\node[below] at (right) {---};
\node[above] at (topleft) {---};
\node[above] at (topright) {---};
\node[below] at (bottomleft) {---};
\node[below] at (bottomright) {---};

\end{tikzpicture} \quad (249)$$
$$ \text{(250)} \qquad \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (P1) at (0,0) {P}; \node (P2) at (2,0) {P}; \draw (P1) -- (P2); \draw (P1) -- (-1,0) node[left] {$=$}; \draw (P2) -- (-1,0) node[left] {$=$}; \end{tikzpicture} $$

$$ \text{(251)} \qquad \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (P1) at (0,0) {P}; \node (P2) at (2,0) {P}; \draw (P1) -- (P2); \draw (P1) -- (-1,0) node[left] {$=$}; \draw (P2) -- (-1,0) node[left] {$=$}; \end{tikzpicture} \end{array} $$

$$ \text{(252)} \qquad \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (P1) at (0,0) {P}; \node (H) at (1,0) {H}; \draw (P1) -- (H); \draw (P1) -- (-1,0) node[left] {$=$}; \draw (H) -- (-1,0) node[left] {$=$}; \end{tikzpicture} \end{array} $$

$$ \text{(253)} \qquad \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (P1) at (0,0) {P}; \node (H) at (1,0) {H}; \draw (P1) -- (H); \draw (P1) -- (-1,0) node[left] {$=$}; \draw (H) -- (-1,0) node[left] {$=$}; \end{tikzpicture} \end{array} $$

$$ \text{(254)} \qquad \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (P1) at (0,0) {P}; \node (H) at (1,0) {H}; \draw (P1) -- (H); \draw (P1) -- (-1,0) node[left] {$=$}; \draw (H) -- (-1,0) node[left] {$=$}; \end{tikzpicture} \end{array} $$

$$ \text{(255)} \qquad \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (P1) at (0,0) {P}; \node (H) at (1,0) {H}; \draw (P1) -- (H); \draw (P1) -- (-1,0) node[left] {$=$}; \draw (H) -- (-1,0) node[left] {$=$}; \end{tikzpicture} \end{array} $$

$$ \text{(256)} \qquad \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (P1) at (0,0) {P}; \node (H) at (1,0) {H}; \draw (P1) -- (H); \draw (P1) -- (-1,0) node[left] {$=$}; \draw (H) -- (-1,0) node[left] {$=$}; \end{tikzpicture} \end{array} $$

$$ \text{(257)} \qquad \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (P1) at (0,0) {P}; \node (H) at (1,0) {H}; \draw (P1) -- (H); \draw (P1) -- (-1,0) node[left] {$=$}; \draw (H) -- (-1,0) node[left] {$=$}; \end{tikzpicture} \end{array} $$

$$ \text{(258)} \qquad \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (P1) at (0,0) {P}; \node (H) at (1,0) {H}; \draw (P1) -- (H); \draw (P1) -- (-1,0) node[left] {$=$}; \draw (H) -- (-1,0) node[left] {$=$}; \end{tikzpicture} \end{array} $$

$$ \text{(259)} \qquad \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (P1) at (0,0) {P}; \node (H) at (1,0) {H}; \draw (P1) -- (H); \draw (P1) -- (-1,0) node[left] {$=$}; \draw (H) -- (-1,0) node[left] {$=$}; \end{tikzpicture} \end{array} $$

$$ \text{(260)} \qquad \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (P1) at (0,0) {P}; \node (H) at (1,0) {H}; \draw (P1) -- (H); \draw (P1) -- (-1,0) node[left] {$=$}; \draw (H) -- (-1,0) node[left] {$=$}; \end{tikzpicture} \end{array} $$
(127)Lemma B.3
$\equiv$

<figure><img src="image_572.png" /></figure>

(19)
$\equiv$

<figure><img src="image_573.png" /></figure>

(127)Lemma B.3
$\equiv$

<figure><img src="image_574.png" /></figure>

Lemma D.6
$\equiv$

<figure><img src="image_575.png" /></figure>

(125)(118)
$\equiv$

<figure><img src="image_576.png" /></figure>

Lemma D.6
$\equiv$

<figure><img src="image_577.png" /></figure>

Proof of Equation (250):

<figure><img src="image_578.png" /></figure>

(153)
$\equiv$

<figure><img src="image_579.png" /></figure>

(174)(18)(111)
$\equiv$

<figure><img src="image_580.png" /></figure>

(124)Lemma B.3 (4)
$\equiv$

<figure><img src="image_581.png" /></figure>

Proof of Equation (251):

<figure><img src="image_582.png" /></figure>

=

<figure><img src="image_583.png" /></figure>
(8)

<figure><img src="image_584.png" /></figure>

(155)(249)

<figure><img src="image_585.png" /></figure>

(8)

<figure><img src="image_586.png" /></figure>

Proof of Equation (252):

<figure><img src="image_587.png" /></figure>

=

<figure><img src="image_588.png" /></figure>

(250)

<figure><img src="image_589.png" /></figure>

(112)(130)

<figure><img src="image_590.png" /></figure>

(251)

<figure><img src="image_591.png" /></figure>

Proof of Equation (253):

<figure><img src="image_592.png" /></figure>

(252)

<figure><img src="image_593.png" /></figure>

(192)

<figure><img src="image_594.png" /></figure>
<figure><img src="image_595.png" /></figure>

Proof of Equation (254):

<figure><img src="image_596.png" /></figure>

(252) =

<figure><img src="image_597.png" /></figure>

(182) =

<figure><img src="image_598.png" /></figure>

(252) =

<figure><img src="image_599.png" /></figure>

Proof of Equation (255):

<figure><img src="image_600.png" /></figure>

(252)(251) =

<figure><img src="image_601.png" /></figure>

(186) =

<figure><img src="image_602.png" /></figure>

(251)(252) =

<figure><img src="image_603.png" /></figure>

Proof of Equation (256):

<figure><img src="image_604.png" /></figure>

(157)(161)(153)(81) =

<figure><img src="image_605.png" /></figure>

(252) =

<figure><img src="image_606.png" /></figure>
$$ \text{Lemma D.6} = $$

<figure><img src="image_607.png" /></figure>

$$ (252) = $$

<figure><img src="image_608.png" /></figure>

$$ \text{Lemma D.6} = $$

<figure><img src="image_609.png" /></figure>

$$ (252) = $$

<figure><img src="image_610.png" /></figure>

$$ \text{Lemma D.6} = $$

<figure><img src="image_611.png" /></figure>

$$ (252) = $$

<figure><img src="image_612.png" /></figure>

$$ \text{Lemma D.6} = $$

<figure><img src="image_613.png" /></figure>

$$ (81)(153)(157)(161) = $$

<figure><img src="image_614.png" /></figure>

Proof of Equation (257):

<figure><img src="image_615.png" /></figure>

$$ (252) = $$

<figure><img src="image_616.png" /></figure>
<figure><img src="image_617.png" /></figure>

<figure><img src="image_618.png" /></figure>

Proof of Equation (258):

<figure><img src="image_619.png" /></figure>

<figure><img src="image_620.png" /></figure>

<figure><img src="image_621.png" /></figure>

Proof of Equation (259):

<figure><img src="image_622.png" /></figure>

<figure><img src="image_623.png" /></figure>

<figure><img src="image_624.png" /></figure>
Proof of Equation (260):

<figure><img src="image_625.png" /></figure>

(202) =

<figure><img src="image_626.png" /></figure>

(252) =

<figure><img src="image_627.png" /></figure>

Proof of Equation (261):

<figure><img src="image_628.png" /></figure>

(210)(81) =

<figure><img src="image_629.png" /></figure>

(252)(251) =

<figure><img src="image_630.png" /></figure>

Lemma D.6 =

<figure><img src="image_631.png" /></figure>

Lemma D.6 =

<figure><img src="image_632.png" /></figure>

Lemma D.6 =

<figure><img src="image_633.png" /></figure>
<figure><img src="image_634.png" /></figure>

<figure><img src="image_635.png" /></figure>

<figure><img src="image_636.png" /></figure>

Proof of Equation (262):

<figure><img src="image_637.png" /></figure>

<figure><img src="image_638.png" /></figure>

<figure><img src="image_639.png" /></figure>

<figure><img src="image_640.png" /></figure>

<figure><img src="image_641.png" /></figure>

<figure><img src="image_642.png" /></figure>

<figure><img src="image_643.png" /></figure>
<figure><img src="image_644.png" /></figure>

Proof of Equation (263):

<figure><img src="image_645.png" /></figure>

(112)(111)(262) =

<figure><img src="image_646.png" /></figure>

(215)(112)(244) =

<figure><img src="image_647.png" /></figure>

(112)(111)(262) =

Proof of Equation (264):

<figure><img src="image_648.png" /></figure>

(112)(246) =

<figure><img src="image_649.png" /></figure>

(112)(111)(262) =

<figure><img src="image_650.png" /></figure>

(244) =

<figure><img src="image_651.png" /></figure>

(112)(111)(262) =

<figure><img src="image_652.png" /></figure>

(246)(112) =
Proof of Equation (265):

<figure><img src="image_653.png" /></figure>

Proof of Equation (266):

<figure><img src="image_654.png" /></figure>
<figure><img src="image_655.png" /></figure>

<figure><img src="image_656.png" /></figure>

<figure><img src="image_657.png" /></figure>

<figure><img src="image_658.png" /></figure>

*Proof of Equation (267):* We can assume without loss of generality that $\alpha = 1$.

If $\beta = \gamma = 1$, then up to using Lemma B.6 (together with Equations (81), (111) and (208)), we can assume without loss of generality that $\alpha = 0$ and $\beta = 1$. We have

<figure><img src="image_659.png" /></figure>

$$ (210)(81) = $$

<figure><img src="image_660.png" /></figure>

$$ (111)(112)(130)(157) = $$

<figure><img src="image_661.png" /></figure>

$$ (259)(256)(257)(254) = $$

<figure><img src="image_662.png" /></figure>

$$ (111)(112)(130)(157) = $$

<figure><img src="image_663.png" /></figure>
<figure><img src="image_664.png" /></figure>

$$ (81)(210) = $$

If $\gamma = 1$ and $\beta = 0$, then we have

<figure><img src="image_665.png" /></figure>

=

<figure><img src="image_666.png" /></figure>

$$ (111)(113) = $$

<figure><img src="image_667.png" /></figure>

$$ (2)(1)(237)(236) = $$

<figure><img src="image_668.png" /></figure>

previous case
$=$

<figure><img src="image_669.png" /></figure>

$$ (2)(1)(237)(236) = $$

<figure><img src="image_670.png" /></figure>

$$ (111)(113) = $$

<figure><img src="image_671.png" /></figure>

=

<figure><img src="image_672.png" /></figure>

And if $\gamma = 0$, then we have

<figure><img src="image_673.png" /></figure>

=

<figure><img src="image_674.png" /></figure>
<figure><img src="image_675.png" /></figure>

<figure><img src="image_676.png" /></figure>

<figure><img src="image_677.png" /></figure>

<figure><img src="image_678.png" /></figure>

<figure><img src="image_679.png" /></figure>

<figure><img src="image_680.png" /></figure>

<figure><img src="image_681.png" /></figure>

<figure><img src="image_682.png" /></figure>

*Proof of Equation (268):* We can assume without loss of generality that $\alpha = 1$.
If $\beta = \gamma = 1$, then up to using Lemma B.6 (together with Equations (81), (111) and (208)), we can assume without loss of generality that $a = 0$ and $b = 1$. We have

<figure><img src="image_683.png" /></figure>

If $\gamma = 1$ and $\beta = 0$, then again, up to using Lemma B.6 (together with Equations (81), (111) and (208)), we can assume without loss of generality that $a = 0$ and $b = 1$. We have

<figure><img src="image_684.png" /></figure>
previous case
$=$

<figure><img src="image_685.png" /></figure>

(111)(174)(112)
$=$

<figure><img src="image_686.png" /></figure>

(81)(221)(215)(208)
$=$

<figure><img src="image_687.png" /></figure>

And if $\gamma = 0$, then again, up to using Lemma B.6 (together with Equations (81), (111) and (208)), we can assume without loss of generality that $a = 0$ and $b = 1$. We have

<figure><img src="image_688.png" /></figure>

(81)(208)(215)(221)
$=$

<figure><img src="image_689.png" /></figure>

previous cases
$=$

<figure><img src="image_690.png" /></figure>

(112)(174)
$=$

<figure><img src="image_691.png" /></figure>

(81)(261)
$=$

<figure><img src="image_692.png" /></figure>

(111)(174)(112)
$=$

<figure><img src="image_693.png" /></figure>
$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (H) at (0,0) {H}; \node (Hbar) at (-1,0) {H}; \draw[->] (H) -- (Hbar); \node[below=2pt of H] (Hbar) {=}; \draw[->] (Hbar) -- (0,0); \end{tikzpicture} \qquad (277) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (H) at (0,0) {H}; \node (ZX) at (0,1) {ZX}; \draw[->] (H) -- (ZX); \draw[->] (ZX) -- (0,1); \node[left=2pt of H] (Hbar) {=}; \node[right=2pt of H] (ZXbar) {=}; \end{tikzpicture} \qquad (278) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (H) at (0,0) {H}; \node (Hbar) at (-1,0) {H}; \draw[->] (H) -- (Hbar); \node[below=2pt of H] (Hbar) {=}; \draw[->] (Hbar) -- (0,0); \end{tikzpicture} \qquad (279) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (H) at (0,0) {H}; \node (Hbar) at (-1,0) {H}; \draw[->] (H) -- (Hbar); \node[below=2pt of H] (Hbar) {=}; \draw[->] (Hbar) -- (0,0); \end{tikzpicture} \qquad (280) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (H) at (0,0) {H}; \node (Hbar) at (-1,0) {H}; \draw[->] (H) -- (Hbar); \node[below=2pt of H] (Hbar) {=}; \draw[->] (Hbar) -- (0,0); \end{tikzpicture} \qquad (281) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (H) at (0,0) {H}; \node (Hbar) at (-1,0) {H}; \draw[->] (H) -- (Hbar); \node[below=2pt of H] (Hbar) {=}; \draw[->] (Hbar) -- (0,0); \end{tikzpicture} \qquad (282) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (H) at (0,0) {H}; \node (ZX) at (0,1) {ZX}; \draw[->] (H) -- (ZX); \draw[->] (ZX) -- (0,1); \node[left=2pt of H] (Hbar) {=}; \node[right=2pt of H] (ZXbar) {=}; \end{tikzpicture} \qquad (283) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (H) at (0,0) {H}; \node (ZX) at (0,1) {ZX}; \draw[->] (H) -- (ZX); \draw[->] (ZX) -- (0,1); \node[left=2pt of H] (Hbar) {=}; \node[right=2pt of H] (ZXbar) {=}; \end{tikzpicture} \qquad (284) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (H) at (0,0) {H}; \node (Hbar) at (-1,0) {H}; \draw[->] (H) -- (Hbar); \node[below=2pt of H] (Hbar) {=}; \draw[->] (Hbar) -- (0,0); \end{tikzpicture} \qquad (285) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (H) at (0,0) {H}; \node (ZX) at (0,1) {ZX}; \draw[->] (H) -- (ZX); \draw[->] (ZX) -- (0,1); \node[left=2pt of H] (Hbar) {=}; \node[right=2pt of H] (ZXbar) {=}; \end{tikzpicture} \qquad (286) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \node (H) at (0,0) {H}; \node (ZX) at (0,1) {ZX}; \draw[->] (H) -- (ZX); \draw[->] (ZX) -- (0,1); \node[left=2pt of H] (Hbar) {=}; \node[right=2pt of H] (ZXbar) {=}; \end{tikzpicture} \qquad (287) $$
$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (-0.5,0) -- (0,0) -- (0.5,0) -- cycle; \node[below=0.25em] at (-0.5,0) {$\box{H}$}; \node[above=0.25em] at (0,0) {$=$}; \node[below=0.25em] at (0.5,0) {$\box{H}$}; \end{tikzpicture} \qquad (297) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (-0.5,0) -- (0,0) -- (0.5,0) -- cycle; \node[below=0.25em] at (-0.5,0) {$\box{H}$}; \node[above=0.25em] at (0,0) {$=$}; \node[below=0.25em] at (0.5,0) {$\box{H}$}; \end{tikzpicture} \qquad (298) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (-0.5,0) -- (0,0) -- (0.5,0) -- cycle; \node[below=0.25em] at (-0.5,0) {$\box{H}$}; \node[above=0.25em] at (0,0) {$=$}; \node[below=0.25em] at (0.5,0) {$\box{H}$}; \end{tikzpicture} \qquad (299) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (-0.5,0) -- (0,0) -- (0.5,0) -- cycle; \node[below=0.25em] at (-0.5,0) {$\box{H}$}; \node[above=0.25em] at (0,0) {$=$}; \node[below=0.25em] at (0.5,0) {$\box{H}$}; \node[above=0.25em] at (0.5,0.5) {$\box{XZ}$}; \node[below=0.25em] at (0.5,0.5) {$\box{XZ}$}; \end{tikzpicture} \qquad (300) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (-0.5,0) -- (0,0) -- (0.5,0) -- cycle; \node[below=0.25em] at (-0.5,0) {$\box{H}$}; \node[above=0.25em] at (0,0) {$=$}; \node[below=0.25em] at (0.5,0) {$\box{H}$}; \node[above=0.25em] at (0.5,0.5) {$\box{H}$}; \node[below=0.25em] at (0.5,0.5) {$\box{H}$}; \end{tikzpicture} \qquad (301) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (-0.5,0) -- (0,0) -- (0.5,0) -- cycle; \node[below=0.25em] at (-0.5,0) {$\box{H}$}; \node[above=0.25em] at (0,0) {$=$}; \node[below=0.25em] at (0.5,0) {$\box{H}$}; \node[above=0.25em] at (0.5,0.5) {$\box{H}$}; \node[below=0.25em] at (0.5,0.5) {$\box{H}$}; \end{tikzpicture} \qquad (302) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (-0.5,0) -- (0,0) -- (0.5,0) -- cycle; \node[below=0.25em] at (-0.5,0) {$\box{H}$}; \node[above=0.25em] at (0,0) {$=$}; \node[below=0.25em] at (0.5,0) {$\box{H}$}; \node[above=0.25em] at (0.5,0.5) {$\box{H}$}; \node[below=0.25em] at (0.5,0.5) {$\box{H}$}; \end{tikzpicture} \qquad (303) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (-0.5,0) -- (0,0) -- (0.5,0) -- cycle; \node[below=0.25em] at (-0.5,0) {$\box{H}$}; \node[above=0.25em] at (0,0) {$=$}; \node[below=0.25em] at (0.5,0) {$\box{H}$}; \node[above=0.25em] at (0.5,0.5) {$\box{H}$}; \node[below=0.25em] at (0.5,0.5) {$\box{H}$}; \end{tikzpicture} \qquad (304) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (-0.5,0) -- (0,0) -- (0.5,0) -- cycle; \node[below=0.25em] at (-0.5,0) {$\box{XZ}$}; \node[above=0.25em] at (0,0) {$=$}; \node[below=0.25em] at (0.5,0) {$\box{XZ}$}; \node[above=0.25em] at (0.5,0.5) {$\box{XZ}$}; \node[below=0.25em] at (0.5,0.5) {$\box{XZ}$}; \end{tikzpicture} \qquad (305) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (-0.5,0) -- (0,0) -- (0.5,0) -- cycle; \node[below=0.25em] at (-0.5,0) {$\box{XZ}$}; \node[above=0.25em] at (0,0) {$=$}; \node[below=0.25em] at (0.5,0) {$\box{XZ}$}; \node[above=0.25em] at (0.5,0.5) {$\box{XZ}$}; \node[below=0.25em] at (0.5,0.5) {$\box{XZ}$}; \end{tikzpicture} \qquad (306) $$

$$ \begin{tikzpicture}[baseline=(current bounding box.center)] \draw (-0.5,0) -- (0,0) -- (0.5,0) -- cycle; \node[below=0.25em] at (-0.5,0) {$\box{XZ}$}; \node[above=0.25em] at (0,0) {$=$}; \node[below=0.25em] at (0.5,0) {$\box{XZ}$}; \node[above=0.25em] at (0.5,0.5) {$\box{XZ}$}; \node[below=0.25em] at (0.5,0.5) {$\box{XZ}$}; \end{tikzpicture} \qquad (307) $$
*Proof of Equation (269)*<sub>n</sub>: Equation (269)<sub>3</sub> is just Equation (126), and for *n* ≥ 4, Equation (269)*<sub>n</sub>* is just the definition of [diagram].*

*Proof of Equation (270)*<sub>n</sub>: Equation (270)<sub>2</sub> is trivial. Equation (270)<sub>3</sub> follows from Lemma 7.6.

If *n* ≥ 4, then we distinguish three cases depending on the vertical position of the Z gate with respect to the multicontrolled-Z gate:

If there are no controls below the Z gate, then we have

<figure><img src="image_694.png" /></figure>

If there is exactly one control below it, then we have

<figure><img src="image_695.png" /></figure>
<figure><img src="image_696.png" /></figure>

If there are two controls or more below it, then we have

<figure><img src="image_697.png" /></figure>

*Proof of Equation (271)$_n$: Equation (271)$_3$ follows from Lemma 7.6. If $n \ge 4$, then we have*

<figure><img src="image_698.png" /></figure>
<figure><img src="image_699.png" /></figure>

*Proof of Equation (272)*<sub>*n*</sub>: Equation (272)<sub>2</sub> follows from Lemma 7.6. If *n* ≥ 3, then we have

<figure><img src="image_700.png" /></figure>
Proof of Equation (273)$_n$:

<figure><img src="image_701.png" /></figure>

$\begin{array}{c} (269)_n \\ = \end{array}$

<figure><img src="image_702.png" /></figure>

$\begin{array}{c} (128) \\ = \end{array}$

<figure><img src="image_703.png" /></figure>

$\begin{array}{c} (9)(271)_n \\ = \end{array}$

<figure><img src="image_704.png" /></figure>

$\begin{array}{c} (9)(272)_n \\ = \end{array}$

<figure><img src="image_705.png" /></figure>

$\begin{array}{c} (9)(12)(128) \text{Lemma B.3} \\ = \end{array}$

<figure><img src="image_706.png" /></figure>

$\begin{array}{c} (9)(271)_n \\ = \end{array}$

<figure><img src="image_707.png" /></figure>

$\begin{array}{c} (269)_n \\ = \end{array}$

<figure><img src="image_708.png" /></figure>

Proof of Equation (274)$_n$:

<figure><img src="image_709.png" /></figure>

=

<figure><img src="image_710.png" /></figure>

$\begin{array}{c} (8) \\ = \end{array}$

<figure><img src="image_711.png" /></figure>

$\begin{array}{c} (285)_{n-1} (272)_n \\ = \end{array}$

<figure><img src="image_712.png" /></figure>
$$ (8) \quad \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (left) at (0,0) {}; \node (right) at (6,0) {}; \draw (left) -- (right); \node[below] at (3,0) {$=$}; \end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)] \node (left) at (0,0) {}; \node (right) at (6,0) {}; \draw (left) -- (right); \node[below] at (3,0) {$=$}; \end{tikzpicture} $$

Proof of Equation (275)$_n$:

<figure><img src="image_713.png" /></figure>

$$ (269)_n = $$

<figure><img src="image_714.png" /></figure>

$$ (127) \quad \begin{array}{c} \text{Lemma B.3} \\ = \end{array} $$

<figure><img src="image_715.png" /></figure>

$$ (274)_n = $$

<figure><img src="image_716.png" /></figure>

$$ (269)_n = $$

<figure><img src="image_717.png" /></figure>

Proof of Equation (276)$_n$: Equation (276)$_2$ follows from Lemma 7.6. Equation (276)$_3$ follows from Equation (111). If $n \ge 4$, then we have

<figure><img src="image_718.png" /></figure>

$$ (284) \quad \begin{array}{c} \begin{tikzpicture}[baseline=(current bounding box.center)] \node (left) at (0,0) {}; \node (right) at (6,0) {}; \draw (left) -- (right); \node[below] at (3,0) {$=$}; \end{tikzpicture} = \begin{tikzpicture}[baseline=(current bounding box.center)] \node (left) at (0,0) {}; \node (right) at (6,0) {}; \draw (left) -- (right); \node[below] at (3,0) {$=$}; \end{tikzpicture} \end{array} $$

<figure><img src="image_719.png" /></figure>

$$ (174) \quad = $$

<figure><img src="image_720.png" /></figure>

$$ \begin{array}{c} \text{Lemma 5.1} \\ = \end{array} $$

<figure><img src="image_721.png" /></figure>

$$ (111)(174) \quad = $$

<figure><img src="image_722.png" /></figure>
Lemma 5.1
$\equiv$

<figure><img src="image_723.png" /></figure>

(111)
$\equiv$

<figure><img src="image_724.png" /></figure>

(124)Lemma B.3
$\equiv$

<figure><img src="image_725.png" /></figure>

(272)$_n$-1
$\equiv$

<figure><img src="image_726.png" /></figure>

*Proof of Equation (277)*<sub>*n*</sub>: Equation (277)<sub>3</sub> and Equation (277)<sub>4</sub> are trivial. If *n* ≥ 5, then we have

<figure><img src="image_727.png" /></figure>

(276)$_n$
$\equiv$

<figure><img src="image_728.png" /></figure>

(112)(130)
$\equiv$

<figure><img src="image_729.png" /></figure>

(274)$_n$
$\equiv$

<figure><img src="image_730.png" /></figure>
*Proof of Equation (278)*<sub>*n*</sub>: Equation (278)<sub>2</sub> follows from Lemma 7.6. Equation (278)<sub>3</sub> is just Equation (145). For *n* ≥ 4, we have

<figure><img src="image_731.png" /></figure>

=

<figure><img src="image_732.png" /></figure>

(4)

<figure><img src="image_733.png" /></figure>

Lemma D.3
$\equiv$

<figure><img src="image_734.png" /></figure>

Lemma 5.1
$\equiv$

<figure><img src="image_735.png" /></figure>

$(317)n-2 \equiv$

<figure><img src="image_736.png" /></figure>

Lemma 5.1
$\equiv$

<figure><img src="image_737.png" /></figure>

Lemma 5.1
$\equiv$

<figure><img src="image_738.png" /></figure>

Lemma D.3
$\equiv$

<figure><img src="image_739.png" /></figure>

$(274)n(277)n \equiv$

<figure><img src="image_740.png" /></figure>
Lemma 5.1
$\equiv$

<figure><img src="image_741.png" /></figure>

(274)$_n$ (277)$_n$ $\equiv$

<figure><img src="image_742.png" /></figure>

Lemma 5.1
$\equiv$

<figure><img src="image_743.png" /></figure>

Proof of Equation (279)$_n$:

<figure><img src="image_744.png" /></figure>

$(355)_{n-1}$

<figure><img src="image_745.png" /></figure>

$(278)_n$

<figure><img src="image_746.png" /></figure>

$(355)_{n-1}$

<figure><img src="image_747.png" /></figure>

Proof of Equation (280)$_n$:

<figure><img src="image_748.png" /></figure>

$(4)$

<figure><img src="image_749.png" /></figure>

$(272)_n$

<figure><img src="image_750.png" /></figure>

$(279)_n$

<figure><img src="image_751.png" /></figure>

$(4)$

<figure><img src="image_752.png" /></figure>

Proof of Equation (281)$_n$: Equation (281)$_2$ is trivial. Equation (281)$_3$ follows from Equation (93). If $n \ge 4$, then we have

<figure><img src="image_753.png" /></figure>

=

<figure><img src="image_754.png" /></figure>

$(113)$

<figure><img src="image_755.png" /></figure>
<figure><img src="image_756.png" /></figure>

*Proof of Equation (282)*<sub>*n*</sub>: Equation (282)<sub>3</sub> and Equation (282)<sub>4</sub> are trivial. If *n* ≥ 5, then we have

<figure><img src="image_757.png" /></figure>

*Proof of Equation (283)*<sub>*n*</sub>: Equation (283)<sub>3</sub> is just Equation (144). For *n* ≥ 4, we have

<figure><img src="image_758.png" /></figure>
(148)

<figure><img src="image_759.png" /></figure>

(82)

<figure><img src="image_760.png" /></figure>

Lemma D.3

<figure><img src="image_761.png" /></figure>

Lemma D.3

<figure><img src="image_762.png" /></figure>

(285)n-1(303)n-1(9)(272)n(282)n

<figure><img src="image_763.png" /></figure>

Lemma 5.1

<figure><img src="image_764.png" /></figure>

(285)n-1(303)n-1(9)(272)n(282)n

<figure><img src="image_765.png" /></figure>

(274)n(277)n

<figure><img src="image_766.png" /></figure>
$$ \text{Lemma 5.1} \quad \equiv $$

<figure><img src="image_767.png" /></figure>

$$ (274)_n(277)_n \equiv $$

<figure><img src="image_768.png" /></figure>

$$ \text{Lemma D.3} \quad \equiv $$

<figure><img src="image_769.png" /></figure>

### Proof of Equation (284)$_n$:

<figure><img src="image_770.png" /></figure>

$$ (269)_n \equiv $$

<figure><img src="image_771.png" /></figure>

$$ (312)_{n-1} \equiv $$

<figure><img src="image_772.png" /></figure>

$$ (283)_n \text{ Lemmas B.2 and B.6} \equiv $$

<figure><img src="image_773.png" /></figure>

$$ (299)_{n-1} \equiv $$

<figure><img src="image_774.png" /></figure>

### Proof of Equation (285)$_n$: Equation (285)$_1$ follows from Lemma 7.1. Equations (285)$_2$ and (285)$_3$ follow from the topological rules. For $n \ge 4$, we have

<figure><img src="image_775.png" /></figure>

$$ (284)_n \equiv $$

<figure><img src="image_776.png" /></figure>
Lemma D.3
$\equiv$

<figure><img src="image_777.png" /></figure>

$$
(281)_{n-1}(9)(282)_n
\equiv
$$

<figure><img src="image_778.png" /></figure>

Lemma D.3
$\equiv$

<figure><img src="image_779.png" /></figure>

$$
(281)_{n-1}
\equiv
$$

<figure><img src="image_780.png" /></figure>

$$
(284)_{n}
\equiv
$$

<figure><img src="image_781.png" /></figure>

Proof of Equation (286)$_n$:

<figure><img src="image_782.png" /></figure>

$$
(269)_{n}
\equiv
$$

<figure><img src="image_783.png" /></figure>

(4)(124)
$\equiv$

<figure><img src="image_784.png" /></figure>

$(9)(272)_n$
$\equiv$

<figure><img src="image_785.png" /></figure>
<figure><img src="image_786.png" /></figure>

Proof of Equation (287)n:

<figure><img src="image_787.png" /></figure>

Proof of Equation (288)n:

<figure><img src="image_788.png" /></figure>
(172)

<figure><img src="image_789.png" /></figure>

(269)$_{n-1}$

<figure><img src="image_790.png" /></figure>

(9)(272)$_n$

<figure><img src="image_791.png" /></figure>

(269)$_{n-1}$

<figure><img src="image_792.png" /></figure>

(9)(271)$_{n-1}$

<figure><img src="image_793.png" /></figure>

(173)

<figure><img src="image_794.png" /></figure>

(160)

<figure><img src="image_795.png" /></figure>
<figure><img src="image_796.png" /></figure>

Proof of Equation (289)$_n$:

<figure><img src="image_797.png" /></figure>

$$ (4)(118)(299)_{n-1} = $$

<figure><img src="image_798.png" /></figure>

$$ (9)(271)_n = $$

<figure><img src="image_799.png" /></figure>

$$ (81)(299)_{n-1} = $$

<figure><img src="image_800.png" /></figure>

$$ (118)(292)_{n-1}(117) = $$

<figure><img src="image_801.png" /></figure>

$$ (301)_{n-1}(302)_{n-1} = $$

<figure><img src="image_802.png" /></figure>

$$ (172) = $$

<figure><img src="image_803.png" /></figure>
$$ (269)_{n-1} $$

<figure><img src="image_804.png" /></figure>

$$ (9)(272)_n $$

<figure><img src="image_805.png" /></figure>

$$ (269)_{n-1} $$

<figure><img src="image_806.png" /></figure>

$$ (301)_{n-1} (302)_{n-1} $$

<figure><img src="image_807.png" /></figure>

$$ (118)(292)_{n-1} (117) $$

$$ (81)(299)_{n-1} $$

<figure><img src="image_808.png" /></figure>

$$ (9)(271)_n $$

<figure><img src="image_809.png" /></figure>

$$ (173) $$

<figure><img src="image_810.png" /></figure>
<figure><img src="image_811.png" /></figure>

Proof of Equation (290)$_n$:

<figure><img src="image_812.png" /></figure>
Proof of Equation (291)$_n$:

<figure><img src="image_813.png" /></figure>

Proof of Equation (292)$_n$:

<figure><img src="image_814.png" /></figure>
<figure><img src="image_815.png" /></figure>

### Proof of Equation (293)$_n$:

<figure><img src="image_816.png" /></figure>

### Proof of Equation (294)$_n$:

<figure><img src="image_817.png" /></figure>
<figure><img src="image_818.png" /></figure>

<figure><img src="image_819.png" /></figure>

<figure><img src="image_820.png" /></figure>

Proof of Equation (295)$_n$:

<figure><img src="image_821.png" /></figure>

(209) =

<figure><img src="image_822.png" /></figure>

(293)$_n$ =

<figure><img src="image_823.png" /></figure>

(294)$_n$ =

<figure><img src="image_824.png" /></figure>

(218) =

<figure><img src="image_825.png" /></figure>
$$ (225)(226) = $$

<figure><img src="image_826.png" /></figure>

$$ (221)(222)(217)(209) = $$

<figure><img src="image_827.png" /></figure>

$$ (223)(224)(240) \quad (290)_n \text{Lemma B.2} = $$

<figure><img src="image_828.png" /></figure>

*Proof of Equation (296)$_n$: Equation (296)$_3$ is just Equation (132). If $n \ge 4$, then to prove Equation (296)$_n$, we have*

<figure><img src="image_829.png" /></figure>

$$ (295)_n = $$

<figure><img src="image_830.png" /></figure>

$$ (232) = $$

<figure><img src="image_831.png" /></figure>

$$ (234) = $$

<figure><img src="image_832.png" /></figure>

$$ (280)_{n-1} = $$

<figure><img src="image_833.png" /></figure>
<figure><img src="image_834.png" /></figure>

*Proof of Equation (297)*<sub>n</sub>: Equation (297)<sub>2</sub> follows directly from Lemma 7.6, and for *n* ≥ 3, Equation (297)*<sub>n</sub> follows directly from Equations (275)*<sub>n</sub> and (296)*<sub>n</sub>.

*Proof of Equation (298)*<sub>n</sub>:

<figure><img src="image_835.png" /></figure>

<figure><img src="image_836.png" /></figure>

<figure><img src="image_837.png" /></figure>
*Proof of Equation (299)*<sub>*n*</sub>: Equations (299)<sub>1</sub> and (299)<sub>2</sub> follow directly from Lemma 7.1. Equation (299)<sub>3</sub> follows directly from Lemma 7.6. If *n* ≥ 4, then to prove Equation (299)*<sub>*n*</sub>, we have

<figure><img src="image_838.png" /></figure>

(4)(273)n

<figure><img src="image_839.png" /></figure>

(5)(298)n

<figure><img src="image_840.png" /></figure>

(4)(273)n

<figure><img src="image_841.png" /></figure>

(5)(298)n

=

<figure><img src="image_842.png" /></figure>

(118)

<figure><img src="image_843.png" /></figure>

(299)n-1

<figure><img src="image_844.png" /></figure>
(117) $=$

<figure><img src="image_845.png" /></figure>

(299)$_{n-1}$ $=$

<figure><img src="image_846.png" /></figure>

(118) $=$

<figure><img src="image_847.png" /></figure>

Proof of Equation (300)$_n$:

<figure><img src="image_848.png" /></figure>

(117)(299)$_{n-1}$ (118) $=$

<figure><img src="image_849.png" /></figure>

(269)$_n$ $=$

<figure><img src="image_850.png" /></figure>

(299)$_n$ $=$

<figure><img src="image_851.png" /></figure>

Proof of Equation (301)$_n$:

<figure><img src="image_852.png" /></figure>

(269)$_n$ (300)$_n$ (81) $=$

<figure><img src="image_853.png" /></figure>

(299)$_{n-1}$ $=$

<figure><img src="image_854.png" /></figure>
$$ (141) = $$

<figure><img src="image_855.png" /></figure>

$$ (142)(9)(272)_n(143) = $$

<figure><img src="image_856.png" /></figure>

Lemma 7.6
$\equiv$

<figure><img src="image_857.png" /></figure>

$$ (305)_{n-1} = $$

<figure><img src="image_858.png" /></figure>

$$ (304)_{n-1} (287)_n = $$

<figure><img src="image_859.png" /></figure>

$$ (143)(142)(141)(81)(117) = $$

<figure><img src="image_860.png" /></figure>

Proof of Equation (302)$_n$:

<figure><img src="image_861.png" /></figure>

$$ (81) = $$

<figure><img src="image_862.png" /></figure>

$$ (301)_n = $$

<figure><img src="image_863.png" /></figure>
<figure><img src="image_864.png" /></figure>

*Proof of Equation (303)*<sub>*n*</sub>: Equation (303)<sub>2</sub> and Equation (303)<sub>3</sub> are trivial. If *n* ≥ 4, then we have

<figure><img src="image_865.png" /></figure>

*Proof of Equation (304)*<sub>*n*</sub>:

<figure><img src="image_866.png" /></figure>
If $C = \overline{H}$, then we have

<figure><img src="image_867.png" /></figure>

If $C = C_2 \circ C_1$ (with $C_1, C_2$ different from the identity$^{19}$), then we have

<figure><img src="image_868.png" /></figure>

Finally, if $C = C_1 \otimes C_2$ (with $C_2 \neq \emptyset$), then we have

<figure><img src="image_869.png" /></figure>

<figure><img src="image_870.png" /></figure>

<footnote n="19">¹⁹Namely, different from $(\overline{\phantom{H}})^n$ if $C$ is an $n$-qubit circuit.</footnote>
Proof of Equation (310):

<figure><img src="image_871.png" /></figure>

Proof of Equation (311): Equation (311) follows directly from Equations (81) and (299).

Proof of Equation (312):

<figure><img src="image_872.png" /></figure>
<figure><img src="image_873.png" /></figure>

<figure><img src="image_874.png" /></figure>

<figure><img src="image_875.png" /></figure>

Proof of Equation (313):

<figure><img src="image_876.png" /></figure>

□

**Lemma D.11.** For any circuit (over $\{-H\-, \leftarrow, \rightarrow, \otimes_H\}$), the following equation is a consequence of the equations of Figure 4:

<figure><img src="image_877.png" /></figure>

**PROOF.** We proceed by structural induction on $C$.<fnref n="20" />

If $C = \otimes$, then the result is trivial. If $C = \boxtimes$, $\{-H\}$ or $\otimes$, then the result follows from Equation (277), (303) or (282) respectively.

If $C = \leftarrow$, then we have

<figure><img src="image_878.png" /></figure>

<footnote n="20">²⁰More precisely, on an underlying raw circuit.</footnote>
<figure><img src="image_879.png" /></figure>

If $C = \boxed{H}$, then we have

<figure><img src="image_880.png" /></figure>
<figure><img src="image_881.png" /></figure>

(318)

<figure><img src="image_882.png" /></figure>

(319)

<figure><img src="image_883.png" /></figure>

(320)

<figure><img src="image_884.png" /></figure>

(321)

<figure><img src="image_885.png" /></figure>

(322)

<figure><img src="image_886.png" /></figure>

(323)

<figure><img src="image_887.png" /></figure>

(324)

<figure><img src="image_888.png" /></figure>

(325)
$$ \text{Circuit Diagram 1} = \text{Circuit Diagram 2} \qquad (326) $$

$$ \text{Circuit Diagram 3} = \text{Circuit Diagram 4} \qquad (327) $$

$$ \text{Circuit Diagram 5} = \text{Circuit Diagram 6} \qquad (328) $$

$$ \text{Circuit Diagram 7} = \text{Circuit Diagram 8} \qquad (329) $$

$$ \text{Circuit Diagram 9} = \text{Circuit Diagram 10} \qquad (330) $$

$$ \text{Circuit Diagram 11} = \text{Circuit Diagram 12} \qquad (331) $$

$$ \text{Circuit Diagram 13} = \text{Circuit Diagram 14} \qquad (332) $$
<figure><img src="image_889.png" /></figure>

<figure><img src="image_890.png" /></figure>

**Lemma D.13.** The following equations are consequences of the equations of Figure 4, where $\leftarrow$ denotes either a black control or a white control:

<figure><img src="image_891.png" /></figure>

<figure><img src="image_892.png" /></figure>

<figure><img src="image_893.png" /></figure>

<figure><img src="image_894.png" /></figure>

<figure><img src="image_895.png" /></figure>

<figure><img src="image_896.png" /></figure>

<figure><img src="image_897.png" /></figure>

<figure><img src="image_898.png" /></figure>

$\forall x, y \in \{0, 1\}^n,$

$\forall x, y \in \{0, 1\}^n,$

$\forall x, y \in \{0, 1\}^n \text{ with } x \neq y,$

$\forall x, y \in \{0, 1\}^n,$

$\forall x, y \in \{0, 1\}^n \text{ with } x \neq y,$

$\forall x, y \in \{0, 1\}^n,$

$\forall x, y \in \{0, 1\}^n,$

$\forall x, y \in \{0, 1\}^n \text{ with } x \neq y,$
$$ \forall x, y \in \{0, 1\}^n \text{ with } x \neq y, \qquad = \qquad (343) $$

$$ \forall x, y \in \{0, 1\}^n \text{ with } x \neq y, \qquad = \qquad (344) $$

$$ \forall x, y \in \{0, 1\}^n, \qquad = \qquad (345) $$

$$ \forall x, y \in \{0, 1\}^n, \qquad = \qquad (346) $$

$$ \forall x, y \in \{0, 1\}^n \text{ with } x \neq y, \qquad = \qquad (347) $$

$$ \forall x, y \in \{0, 1\}^n \text{ with } x \neq y, \qquad = \qquad (348) $$

$$ \forall x, y \in \{0, 1\}^n \text{ with } x \neq y, \qquad = \qquad (349) $$

$$ \forall x, y \in \{0, 1\}^n \text{ with } x \neq y, \qquad = \qquad (350) $$

$$ \forall x, y \in \{0, 1\}^n, \qquad = \qquad (351) $$

$$ \forall x, y \in \{0, 1\}^n \text{ with } x \neq y, \qquad = \qquad (352) $$

PROOF OF LEMMAS D.12 AND D.13. We prove all the equations in order, except Equations (333) and (334) which we prove only after having proved Equations (335) to (345).

*Proof of Equations (315) and (316): Equations (315) and (316) are just particular cases of Equations (308) and (314) respectively. We make them explicit only to add more clarity to subsequent proofs.*

*Proof of Equation (317): Equation (317) follows directly from Equations (5), (81) and (299).*
*Proof of Equation (318):* First, we prove the particular case of the equation where $x = \vec{1}$, $\alpha = \beta = 1$, and $a = 0$:

<figure><img src="image_899.png" /></figure>

The derivation is as follows:

<figure><img src="image_900.png" /></figure>

$$ (269)(81) = $$

<figure><img src="image_901.png" /></figure>

$$ (81)(216) = $$

<figure><img src="image_902.png" /></figure>

$$ (290) = $$

<figure><img src="image_903.png" /></figure>

$$ (81)(217) = $$

<figure><img src="image_904.png" /></figure>

$$ (290) = $$

<figure><img src="image_905.png" /></figure>

$$ (81)(269) = $$

<figure><img src="image_906.png" /></figure>

Then, the cases where $x \neq \vec{1}$ or $\alpha \neq 1$ follow trivially. The cases where $a = 1$ follow by Lemma B.5 (together with Equations (311) and (317)). And the cases where $\beta = 0$ follow by Equation (238) possibly together with Equation (81).

*Proof of Equation (319):* First, we prove the particular case of the equation where $x = \vec{1}$, $\alpha = \beta = 1$, and $a = 0$:

<figure><img src="image_907.png" /></figure>
If $\gamma = 1$, then we have

<figure><img src="image_908.png" /></figure>

And if $\gamma = 0$, then we have

<figure><img src="image_909.png" /></figure>
(309) $=$

<figure><img src="image_910.png" /></figure>

previous case $=$

<figure><img src="image_911.png" /></figure>

(308) $=$

<figure><img src="image_912.png" /></figure>

(215)(290) $=$

<figure><img src="image_913.png" /></figure>

(309) $=$

<figure><img src="image_914.png" /></figure>

(311) $=$

<figure><img src="image_915.png" /></figure>

Finally, the cases where $x \neq \vec{1}, \alpha \neq 1$, or $\beta \neq 1$ follow trivially or by Equation (81), and the cases where $a = 1$ follow by Lemma B.5 (together with Equations (311) and (317)).

*Proof of Equation (320):*

<figure><img src="image_916.png" /></figure>

(295) $=$

<figure><img src="image_917.png" /></figure>
<figure><img src="image_918.png" /></figure>

<figure><img src="image_919.png" /></figure>

<figure><img src="image_920.png" /></figure>

<figure><img src="image_921.png" /></figure>

<figure><img src="image_922.png" /></figure>

<figure><img src="image_923.png" /></figure>

*Proof of Equation (321):* Given Equation (320), Equation (321) follows directly by Equations (81) and (238).

*Proof of Equation (322):* We proceed by induction on the length *n* of *x*. If *n* = 0, then the result follows from Equation (247). If *n* ≥ 1, then we can assume without loss of generality that the last bit of *x* is 1, namely *x* = *z*1 with *z* ∈ {0, 1}*n*−1*. Then we have

<figure><img src="image_924.png" /></figure>
(112)(267)
≡

<figure><img src="image_925.png" /></figure>

(112)(268)
≡

<figure><img src="image_926.png" /></figure>

induction
hypothesis
≡

<figure><img src="image_927.png" /></figure>

(112)(268)(267)
induction
hypothesis
≡

<figure><img src="image_928.png" /></figure>

(81)(320)(321)
≡

<figure><img src="image_929.png" /></figure>

*Proof of Equation (323):* We proceed by induction on the length *n* of *x*. If *n* = 0, then the result follows from Equation (248). If *n* ≥ 1, then we can assume without loss of generality that the last bit of *x* is 1, namely *x* = z1 with *z* ∈ {0, 1}(*n*−1). Then we have

<figure><img src="image_930.png" /></figure>

(320)(321)(81)
≡

<figure><img src="image_931.png" /></figure>
(268)
≡

<figure><img src="image_932.png" /></figure>

(267)
≡

<figure><img src="image_933.png" /></figure>

induction
hypothesis
≡

<figure><img src="image_934.png" /></figure>

(267)(268)
induction
hypothesis
≡

<figure><img src="image_935.png" /></figure>

(81)(320)(321)
≡

<figure><img src="image_936.png" /></figure>

Proof of Equation (324):

<figure><img src="image_937.png" /></figure>

(215)(214)
≡

<figure><img src="image_938.png" /></figure>
<figure><img src="image_939.png" /></figure>

Proof of Equation (325):

<figure><img src="image_940.png" /></figure>

Proof of Equation (326):

<figure><img src="image_941.png" /></figure>
<figure><img src="image_942.png" /></figure>

Proof of Equation (327):

<figure><img src="image_943.png" /></figure>
<figure><img src="image_944.png" /></figure>

Proof of Equation (328):

<figure><img src="image_945.png" /></figure>

<figure><img src="image_946.png" /></figure>

<figure><img src="image_947.png" /></figure>

Proof of Equation (329):

<figure><img src="image_948.png" /></figure>

<figure><img src="image_949.png" /></figure>
<figure><img src="image_950.png" /></figure>

<figure><img src="image_951.png" /></figure>

<figure><img src="image_952.png" /></figure>

<figure><img src="image_953.png" /></figure>

<figure><img src="image_954.png" /></figure>

Proof of Equation (330):

<figure><img src="image_955.png" /></figure>

<figure><img src="image_956.png" /></figure>
$$(112)(262)(111) =$$

<figure><img src="image_957.png" /></figure>

$$(308) =$$

<figure><img src="image_958.png" /></figure>

$$(307)(215)(214)(318) =$$

<figure><img src="image_959.png" /></figure>

$$(308) =$$

<figure><img src="image_960.png" /></figure>

$$(111)(262)(112) =$$

<figure><img src="image_961.png" /></figure>

$$(246)(112) =$$

<figure><img src="image_962.png" /></figure>
Proof of Equation (331):

<figure><img src="image_963.png" /></figure>

(111)(308) =

<figure><img src="image_964.png" /></figure>

(112)(246) =

<figure><img src="image_965.png" /></figure>

(215) =

<figure><img src="image_966.png" /></figure>

(81)(111)(329) =

<figure><img src="image_967.png" /></figure>

(215) =

<figure><img src="image_968.png" /></figure>

(112)(246) =

<figure><img src="image_969.png" /></figure>
<figure><img src="image_970.png" /></figure>

Proof of Equation (332):

<figure><img src="image_971.png" /></figure>

<figure><img src="image_972.png" /></figure>

<figure><img src="image_973.png" /></figure>

Proof of Equation (335): If $x = y$ then the equation is trivial.

If $x \neq y$, then $x$ and $y$ differ by at least one bit, which means that either a black control of $\Lambda^x$ is in front of a white control of $\Lambda^y$, or conversely. Since the equation is symmetric, we can assume without loss of generality that we are in the first case. Then we proceed by induction on $n$ (that is, the length of $x$). We cannot have $n = 0$ since this would imply $x = y$. If $n = 1$, then the result follows from Lemma 7.1. If $n = 2$, then the result follows from Lemma 7.6. If $n \ge 3$, then by Equation (307) we can assume without loss of generality that this is the penultimate bit that differs between $x$ and $y$, that is, $x = za1b$ and $y = tc0d$ where $z, t \in \{0, 1\}^{n-3}$ and $a, b, c, d \in \{0, 1\}$. Then we have

<figure><img src="image_974.png" /></figure>
(240) =

<figure><img src="image_975.png" /></figure>

(241) =

<figure><img src="image_976.png" /></figure>

(318) =

<figure><img src="image_977.png" /></figure>

(241)(240)(318) =

<figure><img src="image_978.png" /></figure>

(81)(319) =

<figure><img src="image_979.png" /></figure>

(81)(318) =

<figure><img src="image_980.png" /></figure>

induction
hypothesis
= =

<figure><img src="image_981.png" /></figure>
$$ (81)(318)(319) \\ \text{induction} \\ \text{hypothesis} \\ = $$

<figure><img src="image_982.png" /></figure>

$$ (240)(241)(318) \\ = $$

<figure><img src="image_983.png" /></figure>

$$ (241)(240)(319) \\ = $$

<figure><img src="image_984.png" /></figure>

$$ (240)(241)(318) \\ = $$

<figure><img src="image_985.png" /></figure>

$$ (81)(319)(318) \\ \text{induction} \\ \text{hypothesis} \\ = $$

<figure><img src="image_986.png" /></figure>

$$ (240)(241)(318) \\ = $$

<figure><img src="image_987.png" /></figure>

$$ (241)(240)(319) \\ = $$

<figure><img src="image_988.png" /></figure>
$$ (81)(320)(321) = \begin{array}{c} \Lambda^y \\ \Lambda^x \end{array} $$

*Proof of Equation (336):* If $n = 0$, then the result follows from Lemma 7.6. If $x = y$ and $n \ge 1$, then by Equation (81), we can assume without loss of generality that $x$ (and therefore also $y$) is the vector consisting only of 1's. By Equation (315), we can also assume without loss of generality that the controls in front of the `1`'s are black as well. Then we have

<figure><img src="image_989.png" /></figure>

(269) =

<figure><img src="image_990.png" /></figure>

(309) =

<figure><img src="image_991.png" /></figure>

(292)(311) =

<figure><img src="image_992.png" /></figure>

(299) =

<figure><img src="image_993.png" /></figure>

(299) =

<figure><img src="image_994.png" /></figure>

(311)(292) =

<figure><img src="image_995.png" /></figure>

(309) =

<figure><img src="image_996.png" /></figure>

(300) =

<figure><img src="image_997.png" /></figure>

If $x \ne y$, then we proceed by induction on $n$. If $n = 1$, then the result follows from Equations (12) and (131) together with Equation (9). If $n \ge 2$, then by Equation (307) we can assume without loss of generality that this is the last bit that differs between $x$ and $y$, and by Equation (81) we can assume that that bit is 1 in $x$ and 0 in $y$. Namely, $x = za1$ and $y = tb0$ where $z, t \in \{0, 1\}^{n-2}$ and $a, b \in \{0, 1\}$. Then we
have

<figure><img src="image_998.png" /></figure>

*Proof of Equation (337):* We proceed by induction on *n*. If *n* = 1, then the result follows from Lemma 7.6. If *n* ≥ 2, then by Equations (307) and (313), we can assume without loss of generality that *x* and *y* differ by the last bit, and by Equation (81) we can assume that that bit is 1 in
$x$ and $0$ in $y$. Namely, $x = za1$ and $y = tb0$, where $z, t \in \{0, 1\}^{n-2}$ and $a, b \in \{0, 1\}$. Thus, we need to prove the following equation:

<figure><img src="image_999.png" /></figure>

And we have (where $c$ denotes the bit corresponding to the control located in front of the $H$):

<figure><img src="image_1000.png" /></figure>

$$ (320)(321)(81) = $$

<figure><img src="image_1001.png" /></figure>

$$ (111) = $$

<figure><img src="image_1002.png" /></figure>

$$ (112)(242) = $$

<figure><img src="image_1003.png" /></figure>

$$ (112)(243) = $$

<figure><img src="image_1004.png" /></figure>

$$ (322) = $$

<figure><img src="image_1005.png" /></figure>

$$ (112)(243)(242)(322) = $$

<figure><img src="image_1006.png" /></figure>
(111)
≡

<figure><img src="image_1007.png" /></figure>

(81)(111)(323)
≡

<figure><img src="image_1008.png" /></figure>

(81)(111)(322)
≡

<figure><img src="image_1009.png" /></figure>

(111)
≡

<figure><img src="image_1010.png" /></figure>

induction
hypothesis
≡

<figure><img src="image_1011.png" /></figure>

(111)
≡

<figure><img src="image_1012.png" /></figure>

(81)(111)(322)(323)
induction
hypothesis
≡

<figure><img src="image_1013.png" /></figure>
(111)
≡

<figure><img src="image_1014.png" /></figure>

similar to
previous steps
≡

<figure><img src="image_1015.png" /></figure>

(81)(320)(321)
≡

<figure><img src="image_1016.png" /></figure>

*Proof of Equation (338):* If $n = 0$, then the result is trivial.

If $n \ge 1$ and $x \ne y$, then we proceed by induction on $n$. If $n = 1$, then the result follows from Equations (13) and (132) together with Equations (9) and (81). If $n \ge 2$, then by Equations (307) and (313), we can assume without loss of generality that this is the last bit that differs between $x$ and $y$, and by Equation (81) we can assume without loss of generality that that bit is 1 in $x$ and 0 in $y$. Namely, $x = za1$ and $y = tb0$ where $z, t \in \{0, 1\}^{n-2}$ and $a, b \in \{0, 1\}$. Moreover, by Equation (316) we can assume without loss of generality that the control in front of the ␣ is black. Then we have

<figure><img src="image_1017.png" /></figure>

(320)(81)(112)
≡

<figure><img src="image_1018.png" /></figure>

(111)
≡

<figure><img src="image_1019.png" /></figure>

(112)(243)
≡

<figure><img src="image_1020.png" /></figure>
(112)(242) =

<figure><img src="image_1021.png" /></figure>

(112)(323) =

<figure><img src="image_1022.png" /></figure>

(112)(242)(243)(323) =

<figure><img src="image_1023.png" /></figure>

(111) =

<figure><img src="image_1024.png" /></figure>

(111) =

<figure><img src="image_1025.png" /></figure>

(111)(242) =

<figure><img src="image_1026.png" /></figure>

(111)(243) =

<figure><img src="image_1027.png" /></figure>
(112)
induction
hypothesis
≡

<figure><img src="image_1028.png" /></figure>

(111)(243)(242)(112)
induction
hypothesis
≡

<figure><img src="image_1029.png" /></figure>

(111)
≡

<figure><img src="image_1030.png" /></figure>

similar to
previous steps
≡

<figure><img src="image_1031.png" /></figure>

(81)(112)(320)
≡

<figure><img src="image_1032.png" /></figure>

If $n \ge 1$ and $x = y$, then again by Equation (316) we can assume without loss of generality that the control in front of the $\hat{H}$ is black. We

<figure><img src="image_1033.png" /></figure>

<figure><img src="image_1034.png" /></figure>

(311)(335)
≡

<figure><img src="image_1035.png" /></figure>

(335)(309)
≡

<figure><img src="image_1036.png" /></figure>
(314) $\equiv$

<figure><img src="image_1037.png" /></figure>

(338) with $x \neq y$ $\equiv$

<figure><img src="image_1038.png" /></figure>

(309)(335) $\equiv$

<figure><img src="image_1039.png" /></figure>

(335)(311) $\equiv$

<figure><img src="image_1040.png" /></figure>

*Proof of Equation (339):* By Equations (307) and (313), we can assume without loss of generality that $x$ and $y$ differ by the last bit, and by Equation (81) we can assume that that bit is 1 in $x$ and 0 in $y$. Moreover, by Equations (315) and (316) we can assume without loss of generality that the controls in front of the `H`'s are black. Thus, it suffices to prove the following variant of the equation:

<figure><img src="image_1041.png" /></figure>

And we have

<figure><img src="image_1042.png" /></figure>

(307)(320)(81)(214) $\equiv$

<figure><img src="image_1043.png" /></figure>

(111) $\equiv$

<figure><img src="image_1044.png" /></figure>

(215)(243) $\equiv$

<figure><img src="image_1045.png" /></figure>
(244) =

<figure><img src="image_1046.png" /></figure>

(308) =

<figure><img src="image_1047.png" /></figure>

(214)(319) =

<figure><img src="image_1048.png" /></figure>

(308) =

<figure><img src="image_1049.png" /></figure>

(244)(215)(243)

(308)(214)(319) =

<figure><img src="image_1050.png" /></figure>

(111) =

<figure><img src="image_1051.png" /></figure>

(111) =

<figure><img src="image_1052.png" /></figure>
(326) =

<figure><img src="image_1053.png" /></figure>

(327) =

<figure><img src="image_1054.png" /></figure>

(308) =

<figure><img src="image_1055.png" /></figure>

(336) =

<figure><img src="image_1056.png" /></figure>

(308) =

<figure><img src="image_1057.png" /></figure>

(327)(326)(308)(336) =

<figure><img src="image_1058.png" /></figure>

(111) =

<figure><img src="image_1059.png" /></figure>
similar to
previous steps,
using also (245)
$\equiv$

<figure><img src="image_1060.png" /></figure>

(81)(214)(320)(307)
$\equiv$

<figure><img src="image_1061.png" /></figure>

Proof of Equation (340):

<figure><img src="image_1062.png" /></figure>

=

<figure><img src="image_1063.png" /></figure>

(111)
$\equiv$

<figure><img src="image_1064.png" /></figure>

(335)
$\equiv$

<figure><img src="image_1065.png" /></figure>

(111)
$\equiv$

<figure><img src="image_1066.png" /></figure>

=

<figure><img src="image_1067.png" /></figure>

Proof of Equation (341): By Equation (316), we can assume without loss of generality that the controls in front of the `□`'s are black. Then we have

<figure><img src="image_1068.png" /></figure>

(307)
$\equiv$

<figure><img src="image_1069.png" /></figure>

(112)(130)
$\equiv$

<figure><img src="image_1070.png" /></figure>
<figure><img src="image_1071.png" /></figure>

*Proof of Equation (342)*: By Equations (307) and (313), we can assume without loss of generality that x and y differ by the last bit, and by Equation (81) we can assume without loss of generality that that bit is 1 in x and 0 in y. Namely, it suffices to prove the following variant of the equation:

<figure><img src="image_1072.png" /></figure>

And we have

<figure><img src="image_1073.png" /></figure>
(111) =

<figure><img src="image_1074.png" /></figure>

(244) =

<figure><img src="image_1075.png" /></figure>

(215)(214)(242) =

<figure><img src="image_1076.png" /></figure>

(328) =

<figure><img src="image_1077.png" /></figure>

(215)(214)(242)
(244)(328) =

<figure><img src="image_1078.png" /></figure>

(112)(130) =

<figure><img src="image_1079.png" /></figure>

(274) =

<figure><img src="image_1080.png" /></figure>
$\begin{array}{c} (111)(112) \\ = \end{array}$

<figure><img src="image_1081.png" /></figure>

$\begin{array}{c} (325) \\ = \end{array}$

<figure><img src="image_1082.png" /></figure>

$\begin{array}{c} (324) \\ = \end{array}$

<figure><img src="image_1083.png" /></figure>

$\begin{array}{c} (274) \\ = \end{array}$

<figure><img src="image_1084.png" /></figure>

$\begin{array}{c} (338) \\ = \end{array}$

<figure><img src="image_1085.png" /></figure>

$\begin{array}{c} (274) \\ = \end{array}$

<figure><img src="image_1086.png" /></figure>

$\begin{array}{c} (324)(325)(274)(338) \\ = \end{array}$

<figure><img src="image_1087.png" /></figure>
<figure><img src="image_1088.png" /></figure>

*Proof of Equation (343):* By Equations (307) and (313), we can assume without loss of generality that $x$ and $y$ differ by the last bit, and by Equation (81) we can assume without loss of generality that that bit is 1 in $x$ and 0 in $y$. Moreover, by Equation (316) we can assume without loss of generality that the controls in front of the `□`'s are black. Thus, it suffices to prove the following variant of the equation:

<figure><img src="image_1089.png" /></figure>

<footnote n="21">²¹Note that the $\Lambda^{0a1}ZX$ and $\Lambda^{0a1}XZ$ gates can be pushed through $\Lambda^{y01}(-I)$ in the same way that $\Lambda^{x11}(-I)$ was pushed through $\Lambda^{01bZX}$.</footnote>
And we have

<figure><img src="image_1090.png" /></figure>
(111)

<figure><img src="image_1091.png" /></figure>

(111)

<figure><img src="image_1092.png" /></figure>

(246)

<figure><img src="image_1093.png" /></figure>

(308)(111)

<figure><img src="image_1094.png" /></figure>

(331)

<figure><img src="image_1095.png" /></figure>

(332)

<figure><img src="image_1096.png" /></figure>
(274)
≡

<figure><img src="image_1097.png" /></figure>

(307)(111)
≡

<figure><img src="image_1098.png" /></figure>

(339)
≡

<figure><img src="image_1099.png" /></figure>

(111)(307)
≡

<figure><img src="image_1100.png" /></figure>

(274)
≡

<figure><img src="image_1101.png" /></figure>

(332)(331)(274)

<figure><img src="image_1102.png" /></figure>

(307)(111)(339)
≡
<figure><img src="image_1103.png" /></figure>

<figure><img src="image_1104.png" /></figure>

<figure><img src="image_1105.png" /></figure>

<figure><img src="image_1106.png" /></figure>

<figure><img src="image_1107.png" /></figure>

<figure><img src="image_1108.png" /></figure>
(265) =

<figure><img src="image_1109.png" /></figure>

(266) =

<figure><img src="image_1110.png" /></figure>

(330) =

<figure><img src="image_1111.png" /></figure>

(266)(265)(330) =

<figure><img src="image_1112.png" /></figure>

(111) =

<figure><img src="image_1113.png" /></figure>

same as
previous steps
= =

<figure><img src="image_1114.png" /></figure>
<figure><img src="image_1115.png" /></figure>

*Proof of Equation (344):* By Equations (307) and (313), we can assume without loss of generality that $x$ and $y$ differ by the last bit, and by Equation (81) we can assume without loss of generality that that bit is 1 in $x$ and 0 in $y$. Moreover, by Equation (316) we can assume without loss of generality that the control in front of the ⊢ is black. Thus, it suffices to prove the following variant of the equation:

<figure><img src="image_1116.png" /></figure>

Then we distinguish whether the control in front of the *H* is black or white.
If it is black, then we have

<figure><img src="image_1117.png" /></figure>

<figure><img src="image_1118.png" /></figure>

<figure><img src="image_1119.png" /></figure>
<figure><img src="image_1120.png" /></figure>

And if it is white, then we have

<figure><img src="image_1121.png" /></figure>
(130) =

<figure><img src="image_1122.png" /></figure>

(308) =

<figure><img src="image_1123.png" /></figure>

(112)(130) =

<figure><img src="image_1124.png" /></figure>

(309) =

<figure><img src="image_1125.png" /></figure>

(336) =

<figure><img src="image_1126.png" /></figure>

(336) =

<figure><img src="image_1127.png" /></figure>

(111)(307) =

<figure><img src="image_1128.png" /></figure>
(309)

<figure><img src="image_1129.png" /></figure>

(111)(308)

<figure><img src="image_1130.png" /></figure>

(112)(130)

<figure><img src="image_1131.png" /></figure>

=

<figure><img src="image_1132.png" /></figure>

black case

<figure><img src="image_1133.png" /></figure>

(310)

<figure><img src="image_1134.png" /></figure>

(312)

<figure><img src="image_1135.png" /></figure>
Proof of Equation (345):

<figure><img src="image_1136.png" /></figure>

Proof of Equation (333):

<figure><img src="image_1137.png" /></figure>

Proof of Equation (334): Equation (334) follows directly from Equation (333) and Lemma B.5 (used together with Equations (311), (312) and (317)).