# Help me understand whether these critical pairs are joinable

I have the following TRS $$R$$: $$l_1 = f(g(x)) \to f(x) = r_1 \\ l_2 = g(f(y)) \to g(y) = r_2$$

I want to know if $$R$$ is confluent, and whether $$g(f(f(x))) \leftrightarrow_R^* g(g(g(x)))$$. I have already proven termination.

1. I use the fact that $$t = f(y)$$ is a subterm of $$l_2$$ and can find a substitution $$\sigma$$ that unifies $$t$$ with $$l_1$$, namely $$\sigma(y) = g(x)$$. This yields critical pair $$\langle g(g(x)), g(f(x)) \rangle$$.

I can use similar reasoning to unify $$t = g(x)$$ with $$l_2$$ and find critical pair $$\langle f(f(y)), f(g(y)) \rangle$$.

Now I wonder whether these critical pairs converge (i.e. whether they are joinable). For example, I consider the former critical pair. If I understand correctly, I need to find whether there exist a $$v$$ such that $$g(g(x)) \to_R^* v \leftarrow_R^ * g(f(x))$$.

However, I do not understand whether I can conclude that they are not joinable since $$g(g(x))$$ is in normal form and $$g(f(x)) \to g(x)$$, $$g(x) \ne g(g(x))$$, or, whether I can rename the second to $$g(z)$$ and unify. Say, $$g(z)\tau = g(g(x))$$ for $$\tau(z) = g(x)$$ and conclude that the critical pair is joinable.

2. If they are joinable, then $$R$$ is locally confluent. By Newman's theorem, I have that $$R$$ is confluent, since $$R$$ is also terminating. But then $$g(f(f(x))) \leftrightarrow_R^* g(g(g(x)))$$ iff the normal forms of both side are equal.

Here I have the same problem, $$g(g(g(x)))$$ is already in normal form, and $$g(f(f(x))) \to g(f(x) \to g(x)$$. Strictly speaking these are not equal, or can I rename the latter (to $$g(z)$$) and conclude they are equal for a substitution $$\tau(z) = g(g(x))$$?