A recursive Dehn function yields a solution to the word problem

Let $n=\mathrm{\mid }w\mathrm{\mid }$, $L=\max (\{0\}\cup \{\mathrm{\mid }r\mathrm{\mid }:r\in R\})$, and compute $B={\delta }_{\mathcal{P}}(n)$. If $w$ is null, [F1] gives an expression using at most $B$ conjugates of relators (the empty expression when its area is zero). By [L2] there is a singular planar diagram with literal boundary $w$, at most $B$ occupied faces and at most $N=LB+n$ edges. No bound on the conjugator words is asserted or needed.

Enumerate finite connected plane maps with at most $N$ edges: name at most $2N+1$ vertices and $N$ edges, specify the two endpoint occurrences of every edge (including loops), the cyclic order of its incident germs at every vertex, and a distinguished directed outer corner. A finite rotation system determines the facial walks, including twice-traversed bridges. There are finitely many such data up to these bounded names, and face tracing by the next-germ permutation is a finite computation. Retain only connected planar maps whose distinguished outer walk reads the literal word $w$, whose number of bounded faces is at most $B$, and for which every bounded face's directed edge labels read a cyclic conjugate of some word in $R^{\pm 1}$. Assign each edge one of the finitely many generator or inverse labels and check each bounded face by [L3]. The one-vertex, zero-edge map handles $w$ empty and $B=0$. All tests are finite; planarity of the rotation system can be checked by its vertex-edge-face Euler count on the connected orientable ribbon surface, or by finite drawing search.

Every map retained in step 1.2 certifies that $w$ is null. To see this without assuming the group word problem, take a spanning tree of the finite plane graph and a dual spanning tree of bounded faces toward the exterior. Cut along the primal tree and remove bounded faces in reverse dual-tree order. At each removal the exterior boundary word changes by a conjugate of that face word or its inverse, with free cancellations from the two traversals of each cut edge. Once all faces have been removed, the remaining doubled tree edges freely reduce to the empty word. Thus the original exterior word lies in the normal closure of $R$; [L1] makes it trivial in the presented group. This argument also covers loops, repeated vertices and bridges because it uses directed edge occurrences in the facial walks.

If $w$ is null, step 1.1 supplies a diagram satisfying the finite bounds. Its rotation system, outer corner and labels occur in the enumeration of step 1.2, so the search succeeds. Conversely, a successful search certifies nullity by step 2.1. The finite search therefore decides the word problem.