and thus $|\partial_2^-(A_1)| = 0$, contradicting our hypothesis on the 3-generators of $\mathbb{P}$. This leaves three cases to handle.

Suppose that $|\lambda_1| = |\rho_1| = 0$. Then,

$$l_1 *_0 \partial_2^-(A_1) *_0 r_1 = \lambda_2 *_0 (l_2 *_0 \partial_2^-(X_{\alpha,u,\beta}) *_0 r_2) *_1 \rho_2.$$

Thus,

$$l_1 *_0 v_{1+|\lambda_2|} *_0 \gamma_{1+|\lambda_2|} *_0 v'_{1+|\lambda_2|} *_0 r_1 = l_2 *_0 \alpha *_0 u *_0 \partial_1^-(\beta) *_0 r_2$$

$$l_1 *_0 v_{2+|\lambda_2|} *_0 \gamma_{2+|\lambda_2|} *_0 v'_{2+|\lambda_2|} *_0 r_1 = l_2 *_0 \partial_1^+(\alpha) *_0 u *_0 \beta *_0 r_2$$

so

$$\gamma_{1+|\lambda_2|} = \alpha, \quad \gamma_{2+|\lambda_2|} = \beta, \quad l_2 = l_1 *_0 v_{1+|\lambda_2|}, \quad r_2 = v'_{2+|\lambda_2|} *_0 r_1$$

and $u$ is the suffix of $l_1 *_0 v_{2+|\lambda_2|}$ of length $|l_1 *_0 v_{2+|\lambda_2|}| - |l_2 *_0 \partial_1^+(\alpha)|$. In particular, $X_{\alpha,u,\beta}$ is completely determined by $A_1$ and $|\lambda_2|$. And since

$$|\lambda_2| = |\partial_2^-(A_1)| - |\partial_2^-(X_{\alpha,u,\beta})| - |\rho_2| \in \{0, \dots, |\partial_2^-(A_1)| - 2\},$$

there is a finite number of possible $X_{\alpha,u,\beta}$ which induce a critical branching $(S_1, S_2)$.

Suppose now that $|\lambda_1| = 1$ and $|\rho_1| = 0$. Then, by Lemma C.1, $|\lambda_2| = 0$. So

$$\lambda_1 = l_2 *_0 \alpha *_0 u *_0 \partial_1^-(\beta) *_0 r_2$$

and

$$l_1 *_0 v_1 *_0 \gamma_1 *_0 v'_1 *_0 r_1 = l_2 *_0 \partial_1^+(\alpha) *_0 u *_0 \beta *_0 r_2.$$

In particular, we have $\beta = \gamma_1$ and $r_2 = v'_1 *_0 r_1$, so $|r_1| \le |r_2|$. By Lemma C.1(v), we have $|r_1| = 0$ and $r_2 = v'_1$. Note that we have $|u| < |v_1|$. Indeed, otherwise $u = u' *_0 v_1$ for some $u'$ and, since

$$|l_1| + |v_1| = |l_2| + |\partial_1^+(\alpha)| + |u|,$$

we get that $|l_2| \le |l_1|$. By Lemma C.1(iv), it implies that $|l_2| = 0$ and $l_1 = \partial_1^+(\alpha) *_0 u'$, which gives

$$S_1 = (\alpha *_0 u' *_0 \partial_1^-(A_1)) *_1 (\partial_1^+(\alpha) *_0 u' *_0 A_1)$$

and

$$S_2 = (X_{\alpha, u' *_0 v_1, \gamma_1} *_0 v'_1) *_0 ((\partial_1^+(\alpha) *_0 u') *_0 ((v_2 *_0 \gamma_2 *_0 v'_2) *_1 \cdots *_1 (v_k *_0 \gamma_k *_0 v'_k)))$$

so that $(S_1, S_2)$ is a natural branching, contradicting the fact that $(S_1, S_2)$ is a critical branching.

Hence, $|u| < |v_1|$ and $u$ is a strict suffix of $v_1$, thus there are $|v_1|$ such possible $u$. Moreover, since $\mathbb{P}_2$ is finite, there are a finite number of possible $\alpha \in \mathbb{P}_2$. Hence, there are a finite number of possible $X_{\alpha,u,\beta} \in \mathbb{P}_2$ that induces a critical branching $(S_1, S_2)$ such that $|\lambda_1| = 1$ and $|\rho_1| = 0$. The case where $|\lambda_1| = 0$ and $|\rho_1| = 1$ is similarly handled, which concludes the proof. $\square$

We can now conclude the finiteness property for critical branchings of Gray presentations:

**Theorem 3.4.6.** Given a Gray presentation $\mathcal{Q}$ where $\mathbb{Q}_2$ and $\mathbb{Q}_3$ are finite and $|\partial_2^-(A)| > 0$ for every $A \in \mathbb{Q}_3$, there is a finite number of local branchings $(S_1, S_2)$ with rewriting steps $S_1, S_2 \in \mathbb{Q}_3^*$ such that $(S_1, S_2)$ is a critical branching.

*Proof.* Let $S_i = \lambda_i *_1 (l_i *_0 A_i *_0 r_i) *_1 \rho_i$ with $l_i, r_i \in \mathbb{Q}_1^*$, $\lambda_i, \rho_i \in \mathbb{Q}_2^*$ and $A_i \in \mathbb{Q}_3$ for $i \in \{1, 2\}$ such that $(S_1, S_2)$ is a critical branching of $\mathcal{Q}$. By Lemma C.4, such a branching is uniquely determined by $A_1, A_2, |\lambda_1|$ and $|\lambda_2|$. By Lemma C.3,

$$|\lambda_1| < |\partial_2^-(A_2)| \quad \text{and} \quad |\lambda_2| < |\partial_2^-(A_1)|.$$

Hence, for a given pair $(A_1, A_2)$, there are a finite number of tuples $(l_1, l_2, r_1, r_2, \lambda_1, \lambda_2, \rho_1, \rho_2)$ such that $(S_1, S_2)$ is a critical branching. Moreover, by Proposition C.2, either $A_1$ or $A_2$ is an operational generator. By symmetry, we can suppose that $A_1$ is operational. Since $\mathbb{Q}_3$ is finite, there is a finite number of such $A_1$. Moreover, there are a finite number of pairs $(A_1, A_2)$ where $A_2$ is operational too. If $A_2$ is an interchange generator, then, by Lemma C.5, there are a finite number of possible $A_2$ for a given $A_1$ such that $(S_1, S_2)$ is a critical branching, which concludes the finiteness analysis. $\square$