{'fraction_non_alphanumeric': 0.055851157795066386, 'fraction_numerical': 0.01659141175389877, 'mean_word_length': 3.4855784469096673, 'pattern_counts': {'":': 0, '<': 21, '<?xml version=': 0, '>': 52, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 87, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Polynomial-time proofs that groups are hyperbolic

It is undecidable in general whether a given finitely presented group is word hyperbolic. We use the concept of pregroups, introduced by Stallings, to define a new class of van Kampen diagrams, which represent groups as quotients of virtually free groups. We then present a polynomial-time procedure which analyses these diagrams, and either returns an explicit linear Dehn function for the presentation, or returns fail, together with its reasons for failure. Furthermore, if our procedure succeeds we are often able to produce in polynomial time a word problem solver for the presentation that runs in linear time. Our algorithms have been implemented, and are often many orders of magnitude faster than KBMAG, the only comparable publicly available software.


Introduction
We describe a new, polynomial-time procedure for proving that a group defined by a finite presentation is word hyperbolic, and for obtaining a linear upper bound on its Dehn function: the Dehn function of a group is bounded by a linear function if and only if the group is hyperbolic. Our procedure returns a positive answer significantly faster than other methods, and in particular always terminates in low degree polynomial time, although sometimes it will terminate with fail even when the input group is hyperbolic. Our approach also has the advantage that it can sometimes be carried out by hand, which can enable one to prove the hyperbolicity of infinite families of groups.
Our methods are based on a generalisation of small cancellation, where we average the cancellation over the relators. Short relators are problematic for small cancellation, so we start in Section 2 by using the notion of a pregroup, due to Stallings in [18], to define a new kind of presentation, called a pregroup presentation, for a group G. It was shown by Rimlinger in [16] that a finitely generated group H is virtually free if and only if H is the universal group U (P ) of a finite pregroup P : see Theorem 2.11. Pregroup presentations enable us to view the group G as a quotient of a virtually free group U (P ), rather than just as a quotient of a free group, and hence to ignore any failures of small cancellation on the defining relators of U (P ).
In Section 3 we define coloured van Kampen diagrams over these new pregroup presentations, where the relators of the virtually free group U (P ) are coloured red, and the additional relators (which we collect in a set R) are green. We show in Proposition 3.15 that given any coloured van Kampen diagram Γ satisfying a certain technical condition, there exists a coloured van Kampen diagram Γ ′ , with the same boundary word as Γ, whose area is bounded by an explicit linear function of the number of green faces of Γ.
Hence, to prove that a group is hyperbolic it suffices to prove a linear upper bound on the number of green faces appearing in any coloured diagram of boundary length n.
In Section 4 we show that if we replace our presentation by a certain related presentation, then we can assume without loss of generality that each vertex of a coloured diagram is incident with at least two green faces.
In Section 5 we present an overall schema for the design of many possible methods for proving that a group given by a finite pregroup presentation is hyperbolic: since a pregroup presentation is a generalisation of a standard presentation, these methods apply to all finite presentations. In Theorem 5.6 we characterise how these schema can produce explicit bounds on the Dehn function. In this paper we shall describe only one such method, but our approach can be used to define many others.
In Section 6 we present, for reasons of space and ease of comprehension, a particularly straightforward example of one of the methods described in Section 5, which we call RSym. Theorem 6.11 gives an explicit bound on the Dehn function of the presentation when RSym succeeds on all coloured van Kampen diagrams of minimal coloured area.
In Section 7 we prove (see Theorems 7.14 and 7.16) that under some mild and easily testable assumptions on the set R of green relators, one can test whether RSym succeeds on all of the (infinitely many) coloured van Kampen diagrams of minimal area in time O(|X| 5 + r 3 |X| 4 |R| 2 ), where X is the set of generators, and r is the length of the longest green relator. Our assumptions hold, for example, for all groups given as quotients of free products of free and finite groups. We also prove that without these assumptions, one can test whether RSym succeeds on all minimal diagrams in time polynomial in |X| and r|R|.
In Section 8 we go on to consider the word problem. Whilst a successful run of our RSym tester proves an explicit linear bound on the Dehn function, to construct a set of Dehn rewrites using previously-existing methods can take exponential time and space. We present a low degree polynomial-time method to construct a word problem solver: see Theorem 8.4. The construction of the solver succeeds in many but not all examples in which RSym succeeds, and the solver itself runs in linear time: see Theorem 8.6 and Proposition 8. 9.
In Section 9 we consider a variety of examples of finite group presentations, and show how RSym can be used by hand to prove that the groups are hyperbolic. In particular, we prove that RSym succeeds on groups satisfying any of a wide variety of small cancellation conditions, and we use RSym to analyse two infinite families of presentations.
Our procedures have been released as part of both the GAP [4] and MAGMA [1] computer algebra systems, and in Section 10 we present runtimes on a variety of examples, including some with very large numbers of generators and relations. Almost none of these examples could have been analysed using previously existing methods, due to the size of the presentations.
As far as we know, the only other publicly available software that can prove hyperbolicity of a group defined by an arbitrary finite presentation is the first author's KBMAG package [10] for computing automatic structures. Hyperbolicity is verified by proving that geodesic bigons in the Cayley graph are uniformly thin, as described in [9,Section 5]. It was proved by Papasoglu in [15] that this property implies hyperbolicity, but it does not provide a useful bound on the Dehn function. An algorithm for computing the "thinness" constant for geodesic triangles in the Cayley graph of a hyperbolic group is described in [3], but this is of limited applicability in practice, on account of its high memory requirements. Even on the simplest examples, the KBMAG programs involve far too many computational steps for them to be carried out by hand, and they can only be applied to individual presentations. The automatic structure does however provide a fast method of reducing words to normal form and hence solving the word problem in the group.
Shortly before submitting this paper, we became aware of a paper by Lysenok [14], which explores similar concepts of redistributing curvature to prove hyperbolicity to those presented in Section 5 of this paper. His main theorem is similar to our Theorem 5.6, but the ideas are less fully developed.
The word w = x 1 · · · x n ∈ X * is P -reduced if either n ≤ 1, or n > 1 and no pair (x i , x i+1 ) lies in D(P ). The word w is cyclically P -reduced if either (i) n ≤ 1; or (ii) w is P -reduced, n > 1, and (x n , x 1 ) ∈ D(P ).
Stallings defines a relation ≈ on the set of P -reduced words in X * as follows.
Definition 2.6. Let v = y 1 · · · y n ∈ X * be P -reduced and let w = x 1 · · · x m be any word in X * . Then we write v ≈ w if n = m and there exist s 0 = 1, s 1 , . . . , s n−1 , s n = 1 ∈ P such that (s σ i−1 , y i ), (y i , s i ), ([s σ i−1 y i ], s i ) ∈ D(P ) for all i, and x i = [s σ i−1 y i s i ]. We say that w is an interleave of v. In the case when s i = 1 for a single value of i, we call the transformation from v to w a single rewrite. . Let P be a pregroup, let X = P \ {1}, and let u, v ∈ U (P ), with u a P -reduced word. Then (i) if v ≈ w then w is P -reduced; (ii) interleaving is an equivalence relation on the set of P -reduced words over X; (iii) each element g ∈ U (P ) can be represented by a P -reduced word in X * ; (iv) if v is P -reduced, then u and v represent the same element of U (P ) if and only if u ≈ v. In particular, P embeds into U (P ).
Corollary 2.8. Let P be a finite pregroup. Then the word problem in U (P ) is soluble in linear time.
Proof. The only P -reduced word representing 1 U(P ) is the empty word, so we can solve the word problem in U (P ) by reducing words using the products in D(P ). This process is a Dehn algorithm, which by [2] requires time linear in the length of the input word.
Definition 2.9. We now define a new type of presentation, which we shall call a pregroup presentation. Let P be a pregroup, let X = P \ {1}, let σ be the involution giving inverses in X, and let R ⊂ X * be a set of cyclically P -reduced words. We write P = X σ | V P | R to define a group presentation P = X | {xx σ : x ∈ X} ∪ V P ∪ R on the set X of monoid generators.
Remark 2.10. We shall assume throughout the rest of the paper that there are no relators of the form x 2 for x ∈ X in R and that, instead, we have chosen a pregroup P such that x σ = x. This can always be achieved by, for example, choosing P such that U (P ) = F (X σ ). Notice also that R ∩ V P = ∅, since each element of R is cyclically P -reduced.
We finish this section by considering the applicability of these presentations.

Theorem 2.11 ([16, Corollary to Theorem B]). A finitely generated group G is virtually free if and only if G is the universal group of a finite pregroup.
The class of virtually free groups includes amalgamated free products of finite groups, and HNN extensions with finite base groups, which is the source of many of the pregroups that are useful in the algorithmic applications to proving hyperbolicity that are described in this paper. More generally, a group is virtually free if and only if it is the fundamental group of a finite graph of groups with finite vertex groups [17,Proposition 11].
For the remainder of the paper, we shall be working with groups given by finite pregroup presentations. The following immediate corollary shows that this includes all quotients of virtually free groups by finitely many additional relators.
Corollary 2.12. Let a group G have pregroup presentation P = X σ | V P | R , as in Definition 2.9. Then G ∼ = U (P )/ R , where R denotes the normal closure of R in U (P ). Furthermore, any group that is a quotient of a virtually free group by finitely many additional relators has a finite pregroup presentation.

Diagrams over pregroups
In this section, we introduce coloured van Kampen diagrams, which are a natural generalisation of van Kampen diagrams to pregroup presentations. We show that, if a word of length n can be written as a product of conjugates of k relators from R ± over U (P ), then it can be written as a product of conjugates of λk + n relators from R ± ∪ V P over F (X σ ), where λ depends only on the maximum length r of the relators in R, and R ± denotes R ∪ {R −1 : R ∈ R}.
In general we follow standard terminology for van Kampen diagrams, as given in [13,Chapter 5,§1] for example. For clarity, we record some definitions that will be useful in what follows.
Definition 3.1. We shall orient each face clockwise. We shall count all incidences with multiplicities, for example a vertex may be incident more than once with the same face.
In the present article, we shall require our diagrams to be simply connected. There is therefore a unique external face, and its label is the external word. All other faces are internal. If an element x ∈ X is self-inverse in P , then x has order 2 in U (P ) and we will identify x with x σ , so that an edge may have label x on both sides.
We will refer to a nontrivial path of maximal length that is common to two adjacent faces of a diagram as a consolidated edge.
We denote the boundary of a face f or a diagram Γ by ∂(f ) and ∂(Γ), respectively. We consider ∂(f ) (and ∂(Γ)) to contain both vertices and edges, but abuse notation and write |∂(f )| for the number of edges. An internal face f of a diagram Γ is a boundary face if |∂(f ) ∩ ∂(Γ)| ≥ 1. A vertex or edge of Γ is a boundary vertex or edge if it is contained in ∂(Γ).

Definition 3.2.
A coloured van Kampen diagram over the pregroup presentation P = X σ | V P | R is a van Kampen diagram with edge labels from X σ , and face labels from V P ∪ R ± , in which the faces labelled by an element of V P are coloured red, and the faces labelled by an element of R ± , together with the external face, are coloured green. We shall often refer to a coloured van Kampen diagram as a coloured diagram.
For v a vertex in a coloured diagram, we shall write δ(v) for the degree of v, δ G (v) for green degree of v: the number of green faces incident with v, and δ R (v) for the number of red faces incident with v.
Notice from our relator set V P that all red faces are triangles, and we shall often refer to them as such. If a word w is a product of conjugates of exactly k relators from R ± in U (P ), then there exists a coloured diagram for w with exactly k internal green faces. The proof of this is essentially the same as for standard van Kampen diagrams; see [13, Chapter V, Theorem 1.1], for example.
The area of a coloured diagram Γ is its total number of internal faces, both red and green, and is denoted Area(Γ). However, when comparing areas of diagrams, it is convenient to count green faces first and then red triangles. Definition 3.3. Let Γ be a coloured diagram. The coloured area CArea(Γ) of Γ is an ordered pair (a, b) ∈ N × N, where a is the number of internal green faces of Γ and b is the number of red triangles. Let ∆ be a coloured diagram with CArea(∆) = (c, d). We say that CArea(Γ) ≤ CArea(∆) if a < c or if a = c and b ≤ d. A diagram has minimal coloured area for a word w if its coloured area is minimal over all diagrams with boundary word w.
Definition 3.4. Let Γ be a coloured van Kampen diagram. A subdiagram of Γ is a subset of the faces, edges and vertices of Γ that form a coloured diagram in their own right.
In particular, we do not allow annular subdiagrams. Definition 3.5. A coloured diagram is semi-σ-reduced if no two distinct adjacent faces are labelled by w 1 w 2 and w −1 2 w −1 1 for some relator w 1 w 2 ∈ V P ∪ R ± and have a common consolidated edge labelled by w 1 and w −1 1 . It is σ-reduced if the same also holds for a single face adjacent to itself.
Our definition of a σ-reduced coloured diagram corresponds to the usual definition of a reduced diagram; see [13, p241], for example. Unfortunately, the proof in [13, Chapter V, Lemma 2.1] that a diagram of minimal area is reduced breaks down in our situation for faces adjacent to themselves, because two cyclic conjugates of a P -reduced word can be mutually inverse in F (X σ ): we shall eventually get around this problem, and the first step in this direction is Proposition 3.8.
First, however, we make a natural generalisation of σ-reduction.
Definition 3.6. A coloured diagram is semi-P -reduced if no two distinct adjacent green faces are labelled by w 1 w 2 and w −1 and have a common consolidated edge labelled by w 1 and w −1 1 , where w 2 and w 3 are equal in U (P ) (which, by Theorem 2.7 is equivalent to w 2 ≈ w 3 ).
Notice in particular that a semi-P -reduced diagram is semi-σ-reduced.
Proposition 3.7. Let Γ be a coloured diagram with boundary word w. Then there exists a semi-P -reduced coloured diagram ∆ with boundary word w such that CArea(∆) ≤ CArea(Γ), and if Γ is not already semi-P -reduced, then this inequality is strict. In particular, ∆ is semi-σ-reduced.
Proof. If a coloured diagram Γ fails to be semi-P -reduced, then Γ contains two adjacent green faces labelled by w 1 w 2 and w −1 3 w −1 1 , as in Definition 3.6. Since w 2 = U(P ) w 3 , we can remove the consolidated edge labelled w 1 , identify any consecutive edges with inverse labels, and fill in the resulting the new face with label the cyclically σ-reduced word resulting from w 2 w −1 3 by a number of red triangles. This may increase the total area of Γ, but it decreases its coloured area, since it now has two fewer green faces.
The following result will enable us to restrict our attention to σ-reduced diagrams later in the paper. Proposition 3.8. Let G have pregroup presentation P. Suppose that there exists a coloured diagram Γ over P that contains a face f that is adjacent to itself in such a way that Γ is not σ-reduced. Then f is green, and there exists t ∈ X such that t σ = t and t = G 1.
Furthermore, there exists such a t ∈ X with the property that a coloured diagram ∆ of minimal coloured area with boundary label t is σ-reduced and semi-P -reduced, and CArea(∆) < CArea(Γ).
Proof. The only way that a red triangle could be adjacent to itself is if an element of X is trivial in U (P ), contradicting Theorem 2.7. Hence f is green.
Let f be adjacent to itself via a consolidated edge labeled w 1 , so that reading ∂(f ) from the side of the edge labelled w 1 gives w 1 w 2 , and from the other side gives w −1 1 w −1 2 . Then w 2 contains a subword w −1 1 , so there are words v 1 and v 2 with We have assumed that w 2 is the inverse of the cyclic subword of w that starts just after w −1 1 and finishes just before it, namely v 2 w 1 v 1 . So and hence, since there is no cancellation in these products, v 1 Both v 1 and v 2 are σ-reduced, so each is an F (X σ )-conjugate of a self-inverse element of X σ .
The face f in Γ encloses regions with boundary labels v 1 and v 2 , so the corresponding involutions are trivial in G. In fact these regions are subdiagrams Γ 1 and Γ 2 of Γ, and at least one of them, say Γ 1 , does not contain f , and hence has coloured area less than that of Γ. By identifying inverse pairs of edges on ∂(Γ 1 ) we obtain a diagram with the same coloured area as Γ 1 , and with boundary label a self-inverse element of X σ . Now let ∆ be a diagram with smallest possible coloured area such that its boundary label is some t ∈ X with t = t σ . Then ∆ is semi-P -reduced by Proposition 3.7, and it must be σ-reduced, since otherwise we could repeat the above argument and obtain such a diagram with smaller coloured area. Furthermore, CArea(∆) ≤ CArea(Γ 1 ) < CArea(Γ). Definition 3.9. A plane graph is a planar graph embedded in the plane, so that the faces are determined. In a coloured van Kampen diagram or the corresponding facecoloured graph, we denote the numbers of red faces and internal green faces by F R and F G , respectively, so that F R + F G = F , the number of internal faces of the diagram or graph. For an edge e, we define e G to be the number of green faces incident with e. So e G = 0, 1 or 2.
Recall from Definition 3.1 that we count incidences of faces with edges and vertices with multiplicity: we do the same in the corresponding plane graph. Recall from Definition 3.2 that the external face of any coloured diagram is green, and so contributes 1 to the value of e G for each edge on its boundary. Recall also from Definition 3.2 the definition of δ G (v). Proposition 3.10. Let Γ be a simply-connected plane graph, where all faces have been coloured red or green and the unique external face is green. Assume that the boundary of every red face has length 3. With the notation of Definition 3.9, Proof. Let E = |E(Γ)| and V = |V (Γ)|. The proof is by induction on F R , so suppose first that F R = 0. Then F G = F and v∈V (Γ) (δ G (v) − 1) = 2E − V , so the right hand side of the above equation is 2(1 − F + 2E − V ), which by Euler's formula is equal to 2E = e∈E e G .
For the inductive step, it is enough to prove that the equation remains true when we change the colour of an internal triangle from green to red, since any two-face-coloured graph can be made by first colouring all faces one colour and then re-colouring some faces the other. The triangle has three sides, so when it changes colour, e∈E e G decreases by 3, the value of F R increases by 1 and F G decreases by 1. The triangle is incident with three vertices, so v∈V (δ G (v) − 1) decreases by 3. Thus, the formula still holds. Lemma 3.11. Let Γ be a coloured diagram with cyclically σ-reduced boundary word. Then Γ contains no vertices of valency 1.
Proof. We assumed in Definition 2.9 that all boundary labels of internal green faces are cyclically P -reduced, and hence in particular are cyclically σ-reduced. Furthermore, all boundary labels of red triangles are σ-reduced by the definition of V P . We have now assumed that the boundary word of Γ is cyclically σ-reduced. If v is a vertex in Γ of valency 1, then the boundary of the face containing v has label containing a subword xx σ , where x is the label on the unique edge incident with v. This is a contradiction.
A number of the results that we prove later require the assumption that certain elements of X are not trivial in G, as in Proposition 3.8. A potential problem with this assumption is that, on the one hand the triviality of generators is known to be undecidable in general in finitely presented groups, but on the other hand our algorithms need to be able to test whether it holds on the presentations which we want to test for hyperbolicity.  Figure 1: Reducing the valency of v Fortunately, as we shall see in Theorem 6.10, there is a way of avoiding these difficulties, and the next definition arises from this situation.
, and such that ∆ contains a loop that is labelled by some V σ -letter x ∈ X.
If no V σ -letter is trivial in G, then all coloured diagrams over P are loop-minimal. This happens, for example, whenever U (P ) is a free group. Otherwise, we can find a loop-minimal diagram over P by choosing a diagram of smallest possible coloured area with boundary word equal to a V σ -letter.
In the remainder of this section, we shall work towards a proof of Proposition 3.15: the total area of a loop-minimal coloured diagram is bounded above by a linear function of the boundary length and the number of green faces. First we shall prove two results which allow us to assume that every vertex v in a coloured diagram satisfies δ G (v) ≥ 1.
Lemma 3.13. Let Γ be a coloured diagram over P. Assume that Γ contains a vertex v with three consecutive adjacent red triangles, and that none of the edges in any red triangle incident with v is a loop based at v. Then there is a diagram ∆ over P having the same green faces as Γ and such that CArea(∆) ≤ CArea(Γ), in which v is incident with at least one fewer red triangle than it is in Γ, and none of the edges of any of the red triangles incident with v is a loop based at v.
Proof. Let f 1 , f 2 and f 3 be the three consecutive red triangles, with edge labels as in the left hand picture of Figure 1, and assume first that all five vertices are distinct. Thus a σ = P bc σ , d = P c σ e and g = P ef . Hence by Axiom (P5) at least one of the pairs ([bc σ ], e), ([c σ e], f ) is in D(P ). Suppose that ([bc σ ], e) ∈ D(P ) (the other case is similar), and let x = [bc σ e]. Then If x = P 1 then e = a and d = b σ , so Γ is not semi-σ-reduced, and we may delete faces f 1 and f 2 , identifying v 1 with v 3 , the directed edge labelled b with the one labelled d σ , and the edge labelled a with the one labelled e. This reduces the number of red triangles incident with v by two, and does not produce any loops at v (since no vertex is identified with v).
Otherwise, x = 1, and so axe σ , x σ bd ∈ V P , and there is a diagram ∆ in which the triangles f 1 and f 2 have been replaced by triangles f ′ 1 and f ′ 2 respectively, with labels axe σ and x σ bd (as in the right hand picture of Figure 1). The number of red and green faces of ∆ is identical to that of Γ, but v has smaller degree. Since we have not added any edges that are incident with v, the condition on loops based at v still holds.
We need to consider the possibility that some pairs of the vertices in Figure 1 could coincide: this includes the case where v 1 = v 4 and the edge labelled a is the same as Figure 2: Triangles with two or three coincident vertices the edge labelled g. By the assumption on loops based at v, none of v 1 , v 2 , v 3 and v 4 coincide with v. If Γ is not semi-σ-reduced then f 2 and either f 1 or f 3 are deleted, and no triangles are created, so the number of red triangles incident with v decreases. No vertex is identified with v, and so no loops based at v are created. If Γ is semi-σ-reduced then an edge incident with v is deleted, and an edge not incident with v is created. Hence v is incident with fewer red triangles, and no loops at v are created.
Theorem 3.14. Let Γ be a loop-minimal coloured diagram over P with cyclically σreduced boundary word w. Then w is the boundary word of a loop-minimal coloured diagram ∆ with CArea(∆) ≤ CArea(Γ), the same green faces as Γ, and in which every Proof. Suppose that v is a vertex of Γ such that δ G (v) = 0. We shall show that it is possible to modify Γ to produce a diagram ∆ with the same boundary word and green faces, but fewer red triangles. Since CArea(∆) < CArea(Γ), the new diagram ∆ must be loop-minimal. A vertex of valency 1 does not exist in Γ by Lemma 3.11. We prove the result first under the assumption that the three vertices of any red triangle are distinct. Suppose that δ(v) = 2. Let the outgoing edge labels be a and b. Then one of the incident triangles has label a σ b[b σ a] and the other has label b σ a[a σ b], and so Γ is not semi-σ-reduced. Thus there is a diagram ∆ with boundary word w in which v and both triangles have been removed from Γ, and in which the edges labelled a σ b and b σ a have been identified. Then ∆ has the same green faces as Γ, but two fewer red triangles.
Suppose δ(v) ≥ 3. Since δ G (v) = 0, the vertex v ∈ ∂(Γ), so the loop-minimality of Γ ensures that there are no loops based at v. Hence by Lemma 3.13, we can replace Γ by a diagram ∆ with boundary word w, with coloured area at most that of Γ, and with the same green faces, in which v is incident with at least one fewer red triangle than in Γ, and in which there are no loops based at v. By repeating this process, we eventually reduce to the situation in which δ(v) = 2, and the coloured area can then be reduced. This completes the proof in the case that no red triangle of Γ meets itself at one or more vertices. Now we allow for the possibility that not all vertices of a red triangle are distinct. Figure 2 shows the possible configurations of a red triangle in Γ in which two or more of the vertices coincide. The red triangle is labelled T and other regions of the diagram, which may contain additional vertices, edges, and faces, are labelled Θ, Θ 1 or Θ 2 .
In the third of these configurations, two consecutive letters of a word in V P σ-cancel, which contradicts the definition of V P . In the second and the fourth, there is an internal loop labelled by a single letter from V P , contradicting Definition 3.12.
It therefore remains only to consider the case where the whole of Γ has the structure of the first diagram in Figure 2. Here, the sub-diagram labelled Θ has no loops labelled by V σ -letters, and so it can have no red triangles with coincident vertices. The boundary word of Θ is σ-reduced, by definition of V P , and so, by the arguments above, we may assume that all vertices of Θ have green valency at least 1. But we have to consider the possibility that the only green face of Θ that is incident with the vertex labelled v in Γ is the external face of Θ, which is coloured red as a face of Γ. We shall now show that this case does not occur.
If δ(v) = 2, then the face of Θ incident with v is a red triangle, and so Θ contains a loop labelled by a V σ -letter, contradicting our assumption of loop-minimality. If δ(v) ≥ 3, there are three consecutive red triangles incident with v. Since Γ has no loops based at v, we can repeatedly apply Lemma 3.13 to v to reduce its valency, and hence reduce the coloured area, until δ(v) = 2. This yields the same contradiction to our assumption of loop-minimality as at the beginning of this paragraph.
Recall the definitions of F R , F G and e G from Definition 3.9.
Proposition 3.15. Let Γ be a loop-minimal coloured van Kampen diagram with cyclically P -reduced boundary word w of length n and let r = max{|R| : R ∈ R}. Then there exists a loop-minimal coloured diagram ∆ with boundary word w, such that Area(∆) ≤ (3 + r)F G + n − 2. If every vertex v of Γ satisfies δ G (v) ≥ 1 then ∆ can be taken to be Γ.
Proof. By Theorem 3.14, there exists a loop-minimal coloured diagram ∆ with boundary word w and the same green faces as Γ, in which every vertex v satisfies δ G (v) − 1 ≥ 0. Hence for ∆, Proposition 3.10 gives the inequality Each contribution to e G comes either from the boundary of the external face (of length n), or from an internal green face (of which there are F G , each of boundary length at most r), so we deduce that and Area(∆) = F R + F G ≤ (3 + r)F G + n − 2, as claimed.

Interleaving the green relators
In Subsection 4.1 we shall generalise interleaving (Definition 2.6) to cyclic interleaving, and show that this gives an equivalence relation on cyclically P -reduced words. Then in Subsection 4.2 we shall prove our main result in this section, Proposition 4.9. This shows that if we replace R by the set I(R) of all cyclic interleaves of elements of R, then a cyclically P -reduced word w is equal to 1 in G = X σ | V P | R if and only if some cyclic interleave of w is the boundary of a coloured diagram over X σ | V P | I(R) in which each vertex is incident with at least two green faces. Finally, in Subsection 4.3 we shall study the regions of coloured diagrams that are composed entirely of red triangles.

Cyclic interleaving
Recall Definition 2.6 of interleaving, and that this yields an equivalence relation on Preduced words, with one equivalence class for each element of U (P ). Let v = y 1 y 2 · · · y n ∈ X * be cyclically P -reduced. If v ≈ w, then w is cyclically P -reduced.
Proof. If n ≤ 1 then the result is trivial, so assume that n > 1, and let s 0 = 1, s 1 , . . . , s n = 1 be the elements of P from Definition 2.6.
By Theorem 2.7, it suffices to consider a single rewrite, so assume that s i is nontrivial for a single i. The result is immediate unless i = 1 or i = n − 1, so assume without loss of generality that s 1 = 1.
We now define a coarser relation than ≈, by allowing the elements s 0 and s n from Definition 2.6 to be nontrivial but equal.

Definition 4.2.
Let v = y 1 · · · y n ∈ X * be cyclically P -reduced, and let w = x 1 · · · x m ∈ X * . Then we write v ≈ c w if either n ≤ 1 and v = w, or if n = m > 1 and there exist s 0 , s 1 , . . . , s n−1 , s n = s 0 ∈ P such that (s We say that w is a cyclic interleave of v. Theorem 4.3. Let v = y 1 · · · y n ∈ X * be cyclically P -reduced. If w = x 1 · · · x n ≈ c v, then w is cyclically P -reduced. Furthermore, ≈ c is an equivalence relation on the set of all cyclically P -reduced words.
Proof. Since ≈ c is the identity relation on words of length at most 1, we may assume without loss of generality that n > 1.
We can move from v to w by a sequence of single rewrites. By Lemma 4.1, a single rewrite with i = n replaces v by another cyclically P -reduced word and, by applying the lemma to a cyclic permutation of v, we see that the same applies when i = n. So w is cyclically P -reduced.
To show that ≈ c is an equivalence relation, it is sufficient to prove that if w ≈ c u, where u = z 1 . . . z n is the result of applying a single rewrite to w, then v ≈ c u.
Suppose first that this rewrite consists of replacing (x n , . Let s 0 , s 1 , . . . , s n−1 , s n = s 0 ∈ P be as in Definition 4.2, cyclically interleaving v to w. Then x n = [s σ n−1 y n s n ] and x 1 = [s σ n y 1 s 1 ]. Since w is cyclically P -reduced, x n x 1 is P -reduced, and hence (s n , t) ∈ D(P ) by [18, 3.A.2.6]. So, putting s ′ i = s i for 1 ≤ i < n and The argument in the case when the single rewrite from w to u consists of the replacement of (x i , x i+1 ) with 1 ≤ i < n is similar.
Definition 4.4. Let w ∈ X * be cyclically P -reduced. We denote by I(w), called the cyclic interleave class of w, the set We record the following easy lemma for later use. . . x n ∈ X * be cyclically P -reduced with n > 1. Then the cyclic interleave class of w can be made by applying all possible sets of up to n single rewrites, so that each letter of w is multiplied at most once on each side.
Proof. We showed in Theorem 4.3 that ≈ c is an equivalence relation, so it suffices to apply a single rewrite between each pair of letters of w (including x n and x 1 ). Definition 4.6. We write I(R) for ∪ R∈R I(R), and let I(P) be the pregroup presentation Faces of diagrams over I(P) are coloured red and green, just as for coloured diagrams over P.
Hence, G is defined by P if and only if G is defined by I(P).
Proof. One containment is clear, since R ⊂ I(R). For the other, by Lemma 4.5 each element of I(R) is made by applying a finite number of single rewrites to each R = x 1 . . . x n ∈ R, and so is conjugate to a word that is equal in U (P ) to an element of R. The final statement follows from Corollary 2.12.
As a result of the above theorem, we shall move between working with a presentation P and a presentation I(P) without further comment.

Green-rich diagrams
Recall Definitions 3.1 and 3.2 and in particular our conventions on counting incidence, and on the boundary of diagrams.
The following is our main result in this section. (i) Assume first that w is cyclically P -reduced and that, if |w| = 1, then the unique boundary face of Γ is green. Then some w ′ ∈ I(w) is the boundary word of a greenrich loop-minimal coloured diagram ∆ over I(P) with CArea(∆) ≤ CArea(Γ).
(ii) If, instead, |w| > 1 and w is not cyclically P -reduced, then w is the boundary word of a loop-minimal coloured diagram ∆ over I(P) with CArea(∆) ≤ CArea(Γ), in which all non-boundary vertices v satisfy δ G (v) ≥ 2.
Proof. The assumptions of loop-minimality, and that if |w| = 1 then the unique boundary face of Γ is green, together imply that Γ does not have a unique boundary face that is red. The loop-minimality then implies that the vertices of each red triangle of Γ are distinct, and that if |w| = 1, with v 0 the unique boundary vertex, then δ G (v 0 ) ≥ 3. By Theorem 3.14 we may assume that every vertex v of Γ satisfies δ G (v) ≥ 1. Assume that δ G (v) = 1, and that if v ∈ ∂(Γ) then w is cyclically P -reduced. Let ab be the length two subword of the boundary label of the unique green face f that is incident with v, so that v is between a and b. We shall construct a coloured diagram ∆ with boundary word w ′ ∈ I(w), in which v no longer exists, and such that CArea(∆) < CArea(Γ). The loop-minimality of Γ implies that ∆ is loop-minimal.
If v is incident with a unique red triangle T , then δ(v) = 2, which implies that b σ a σ is a subword of the boundary label of T , and so (b σ , a σ ) ∈ D(P ). Elements of R (and by Theorem 4.3 also of I(R)) are cyclically P -reduced, so v ∈ ∂(Γ). But in this case w was assumed to be cyclically P -reduced, a contradiction.
If v is incident with exactly two red triangles, then they must be distinct and share an edge. Let the third edge incident with v be labelled c, so that the triangles have labels with subwords c σ a σ and b σ c. Then (a, c) and (c σ , b) are also in D(P ), and ([ac], [c σ b]) / ∈ D(P ) by Theorem 4.3. A single rewrite can therefore be applied to the label of f , replacing ab with [ac][c σ b]. This has the effect of replacing f by a face labelled with a cyclic interleave of the label of f , removing the vertex v and its two incident red triangles from Γ, and leaving the number of green faces unchanged.
Assume finally that δ R (v) ≥ 3. Since v is not a boundary vertex of a diagram with boundary length 1, the loop-minimality of Γ means that there are no loops based at v. Hence we can repeatedly apply Lemma 3.13 to reduce δ R (v) to two, and then delete v and the final two red triangles incident with it, as in the previous paragraph.
In what follows, we shall often assume that we work with green-rich van Kampen diagrams. But, since we have not been able to eliminate the existence of non-greenrich loop-minimal diagrams with boundary length 1 and the unique boundary face a red triangle, we need to take that possibility into account when developing algorithms, as we shall do in Theorem 6.10.

Red blobs
We now turn our attention to the regions of coloured diagrams that are comprised entirely of red triangles. Definition 4.10. A red blob in a coloured diagram Γ is a nonempty subset B of the set of closed red triangles of Γ, with the property that any nonempty proper subset C of B has at least one edge in common with B \ C. Equivalently, the induced subgraph B of the dual graph Γ of Γ on those vertices that correspond to the triangles in B is connected.
A red blob is simply connected if its interior is homeomorphic to a disc: its boundary may pass more than once through a vertex.
Lemma 4.11. Let B be a red blob in a coloured diagram Γ, with boundary length l and area t. Then l ≤ t + 2, and l ≤ t if B is not simply connected. Furthermore, if B is simply connected, and every vertex of B lies on ∂(B) (which holds in particular when Γ is green-rich), then l = t + 2.
Proof. Let B be the induced subgraph of Γ that corresponds to the triangles in B, as in Definition 4.10. A vertex of valency 1 in B corresponds to a triangle in B that has two edges on ∂(B). Deleting this triangle reduces both the number of boundary edges and the number of triangles by 1, and B remains connected. We repeatedly remove degree 1 vertices from B until none remain. At that stage, either a single vertex remains, in which case l = t + 2, or the remaining vertices all have degree at least two. Such vertices correspond to triangles with at most one edge on the boundary, so the number of triangles is at least the boundary length, and l ≤ t.
If B is not simply connected, then B contains a circuit, and so the second of the above two situations arises, and l ≤ t.
Now assume that all vertices of B lie on ∂(B), and B is simply connected. We shall show that B is a tree, from which the final claim follows. By way of contradiction, let C be a circuit in B. It is a standard result from graph theory (see, for example, [19,Corollary 4.15]) that the corresponding edges in B form a cutset in B. Hence the circuit must enclose at least one vertex of B. We have assumed that all vertices of B lie on ∂(B), so this contradicts the fact that B is simply connected. Proof. Let B be a simply connected red blob in Γ with boundary word w = x 1 . . . x n . First note that by Theorem 3.14, we may assume that all vertices of Γ have green valency at least one. Hence all vertices of B lie on ∂(B), and Area(B) = n − 2 by Lemma 4.11.
We first consider σ-reduction, so assume (without loss of generality) that w = x 1 x σ 1 w 1 . Notice that w = U(P ) 1, so w 1 = U(P ) 1. Hence we can identify the vertices at the beginning of the edge labelled x 1 and the end of the edge labelled x σ 1 , and replace B by a coloured sub-diagram Θ consisting of a red blob B 1 with boundary word w 1 , with a single edge added to the boundary. The blob B 1 is simply connected with all vertices on the boundary, and |∂(B 1 )| = |w 1 | = n − 2, so Area(B 1 ) = n − 4 by Lemma 4.11. The diagram ∆ in which B has been replaced by Θ satisfies CArea(∆) < CArea(Γ), so ∆ is loop-minimal. Replacing B by Θ cannot decrease the green degrees of vertices, so if Γ is green-rich then ∆ is green-rich. Now we consider subwords of w of length greater than 2. Assume that w has a factorisation w = w 1 w 2 such that w 1 and w 2 have lengths b 1 , b 2 ≥ 3, and w 1 = U(P ) 1 = U(P ) w 2 . We can produce a new diagram ∆ in which the two vertices where w 1 and w 2 start and end are identified, and B has been replaced by two red blobs B 1 and B 2 with boundary words w 1 and w 2 , of area b 1 − 2 and b 2 − 2, respectively. From b 1 + b 2 = n, we see that Area(B 1 ) + Area(B 2 ) = n − 4, so CArea(∆) < CArea(Γ), and hence ∆ is loop-minimal. As before, if Γ was green-rich then ∆ is still green-rich.
Definition 4.13. We say that a ∈ X intermults with b ∈ X if b = a σ and either (a, b) ∈ D(P ) or there exists x ∈ X such that (a, x), (x σ , b) ∈ D(P ). We also say that (a, b) is an intermult pair.
Lemma 4.14. If ga is a subword of the boundary label of a red blob with σ-reduced boundary word, then g intermults with a.
Proof. If g and a lie on a common triangle, then (g, a) ∈ D(P ). So suppose not, and let g lie on a triangle T and a on a triangle U , which must meet T at a vertex v. If T and U do not share an edge between g and a, then there exists a sequence T 1 , . . . , T k of triangles with common vertex v, such that T and T 1 share an edge, T i and T i+1 share an edge, and T k and U share an edge. Then we may repeatedly re-triangulate the blob as in Figure 1 until there is a single edge z between g and a: this is immediate from Lemma 3.13 if there are no loops at v, but even if v is on a loop the re-triangulation of Figure 1 is possible: it does not reduce δ(v) but it does reduce the number of edges incident with v that lie between the edge labelled g and the edge labelled a, reading anticlockwise around v as in Figure 1. Thus (g, z), (z σ , a) are defined.

Curvature distribution schemes
In this section, we introduce the concept of curvature distribution schemes, and prove that they can be used to show that groups given by a pregroup presentation satisfy an explicit linear isoperimetric inequality, and hence are hyperbolic.
Definition 5.1. Let Γ be a coloured van Kampen diagram over the pregroup presentation P with vertex set V (Γ), edge set E(Γ), set of red triangles F R (Γ) and set of internal Definition 5.2. Let K be a set of coloured diagrams over I(P). A curvature distribution scheme on K is a map Ψ : K → {ρ Γ : Γ ∈ K}, that associates a curvature distribution to every diagram in K.
Example 5.3. For any coloured diagram Γ we can define a curvature distribution by setting ρ(v) := +1 for each vertex v, setting ρ(e) := −1 for each edge e, and setting ρ(f ) := +1 for each internal face f . Euler's formula ensures that the total sum of all curvature values is +1. Since this defines a curvature distribution for every diagram, it gives rise to a curvature distribution scheme on K, where K is any set of coloured diagrams over I(P), for any pregroup presentation P.
Definition 5.4. Let Γ be a plane graph, and let Γ be its dual. Let f 1 and f 2 be faces of Γ, corresponding to vertices v 1 and v 2 of Γ.
Remark 5.5. In the following theorem, and elsewhere throughout this paper, we give the Dehn function D(n) of X σ | V P ∪ R or of X σ | V P ∪ I(R) . This can be converted to a standard Dehn function by multiplying by a constant, as follows. First replace X by a minimal subset Y of X such that X = Y ∪ Y σ , to get a set of group generators. Then replace all symbols x ∈ Y σ \ Y occurring in relators by (x σ ) −1 . For R ∈ V P ∪ R, let R I denote the number of involutory generators occurring in R (with multiplicity). Then a diagram over F (X σ ) needs to have at most D(n)R I digons added to turn it into a diagram over F (X), so the Dehn function of Theorem 5.6. Let P = X σ | V P | R be a pregroup presentation for a group G, and let r be the maximum length of a relator in R. Let K be a set of coloured van Kampen diagrams over I(P), and let Ψ : K → {ρ Γ : Γ ∈ K} be a curvature distribution scheme.
Assume that there exist constants ε ∈ R >0 , λ, µ, m ∈ R ≥0 and d ∈ Z >0 such that the following conditions hold, for all Γ ∈ K: Then each Γ ∈ K with boundary length n and area greater than 1 satisfies Assume now that, in addition, the following holds: (e) if w ∈ X * is cyclically P -reduced, and satisfies w = G 1, then there exists a diagram Γ ∈ K with boundary word some w ′ ∈ I(w).
Then the group G is hyperbolic. In particular, if I(w) = {w} for all w ∈ X * , then the Dehn function of X σ | V P ∪ R is bounded above by max{f (n), 1}.
Let I be the set of green faces that are dual distance at least d + 1 from the external face (the set I may be empty). From Condition (a) we deduce that and Equation (1) follows. Now assume that Condition (e) also holds. It follows from Lemma 4.5 that, if there is a diagram Γ with boundary label a word w of length n then, for any w ′ ∈ I(w), there is a diagram of area at most Area(Γ) + 2n with boundary label w ′ (each single rewrite adds two red triangles to the diagram, as in the proof of Proposition 4.9), and so there is a linear upper bound on the Dehn function of G. The remaining assertions now follow.
In practice, we shall generally set d = 1 and m = 1/2. Corollary 5.7. Let P = X σ | V P | R be a pregroup presentation for a group G, such that each x ∈ X is nontrivial in G. Let r be the maximum length of a relator in R, let K consist of all diagrams over P of minimal coloured area for each cyclically P -reduced word w that is trivial in G, and let Ψ be a curvature distribution scheme on K.
If there exists ε > 0 such that Conditions (a), (b) and (c) of Theorem 5.6 hold, with m = 1/2 and d = 1, then G is hyperbolic, and the Dehn function of X σ | V P ∪ R is bounded above by Proof. Notice that since each x ∈ X is nontrivial in G, all diagrams are loop-minimal. By Theorem 3.14, each diagram of minimal coloured area for its boundary word satisfies δ G (v) ≥ 1 for each vertex v. Hence by Proposition 3.15 each diagram of minimal coloured area for its boundary word satisfies Condition (d) of Theorem 5.6, with λ = 3 + r and µ = 1. Substituting for λ, µ, m and d into Equation 1 yields This gives an upper bound on the area of all diagrams whose area is greater than 1.
The assumption that each x ∈ X is nontrivial in G implies that any diagram of area 1 has n ≥ 2, and one may check that if n ≥ 2 then f (n) ≥ 1. Hence f (n) bounds the Dehn function of G.
In general, it is not practical to let K consist only of diagrams of minimal coloured area for their boundary word, as membership of K cannot easily be tested. We shall however define in the next section a useful set of diagrams with an easily-testable membership condition. We shall also deal with the condition in the above corollary that each generator is nontrivial in the group G.
The remainder of this paper presents and analyses one curvature distribution scheme, chosen because it can be tested in time that is bounded by a low-degree polynomial function of |X|, |R| and r, and because it verifies that V σ -letters are nontrivial in G. There are, of course, infinitely many possible such schemes, and we leave as an open problem the development of others that are also computationally or theoretically useful. 6 The RSym scheme In this section we describe a curvature distribution scheme which treats each vertex and each edge of each diagram symmetrically, and so is called the RSym scheme. We first specify the set D of diagrams on which RSym operates. Definition 6.1. Let P be a pregroup presentation. Then D denotes the set of all coloured diagrams Γ over I(P) with the following properties: 1. the boundary word of Γ is cyclically P -reduced (see Definition 2.5); 2. Γ is σ-reduced and semi-P -reduced (see Definitions 3.5 and 3.6); 3. Γ is green-rich (see Definition 4.8); 4. no proper subword of the boundary word of a simply connected red blob in Γ is equal to 1 in U (P ).
Recall Definitions 3.1 and 3.2 for our conventions on coloured diagrams.
In a coloured diagram, we shall consider each edge to be composed of two coloured half-edges, oppositely oriented. Each half-edge is associated with the face on that side, and inherits its colour and orientation from that face.
For Γ ∈ D, the following algorithm computes κ Γ := RSym(Γ). We shall write κ rather than κ Γ when there is no risk of confusion. The algorithm to compute RSym(Γ) assigns and alters curvature on the vertices, edges and faces of Γ in several successive steps: the external face has curvature 0 throughout.
Step 2 Each green half-edge gives curvature −1/2 to its end vertex, and each red half-edge gives curvature −1/2 to its triangle.
Step 3 Each vertex divides its curvature equally amongst its incident internal green faces, counting incidences with multiplicity. If there are none, then the curvature remains on the vertex. Step 4 Each red blob B such that ∂(B) ⊆ ∂(Γ) sums the curvatures of its red triangles, to get the blob curvature β(B). A red blob with b := |∂(B) \ ∂(Γ)| then gives curvature β(B)/b across each such edge to the (internal) green face on the other side.
Step 5 (Optional) Each green face with curvature less than −ε, for some user-determined ε, gives some of its curvature to any adjacent non-boundary green faces f for which f has curvature greater than −ε.
Step 6 Return the function κ Γ : Step 5 is left deliberately imprecise and is included mainly for hand calculations. It is not at present implemented. The example studied in Theorem 9.6 below illustrates its usefulness. By default, we assume that this step is not applied, and we shall refer to versions of RSym that include it as RSym + .
Since the curvature in Step 1 is precisely the curvature distribution from Example 5.3, and curvature is neither created nor destroyed by the algorithm, the following is immediate: Recall Definition 5.4 of dual distance. Definition 6.4. Let P = X σ | V P | R be a pregroup presentation, and let ε > 0 be a constant. RSym succeeds with constant ε on a diagram Γ ∈ D if κ Γ (f ) ≤ −ε for all internal non-boundary green faces of Γ.
More generally if, for some d ≥ 1, we can bound κ Γ (f ) ≤ −ε for all green faces of Γ that are at dual distance at least d + 1 from the external face, then RSym succeeds with constant ε at level d. (So the default level is d = 1.) RSym succeeds on P with constant ε (at level d) if this is true for every Γ ∈ D, and RSym succeeds on P (at level d) if there exists an ε > 0 for which RSym succeeds.
Our goal in the rest of this section is to show that if RSym succeeds on a pregroup presentation P, then the group presented by P is hyperbolic. Before we can do that, we need first to study the behaviour of RSym, and then prove two technical lemmas which will allow us to deal with our frequent assumption of loop-minimality in earlier sections.
We first show, amongst other things, that for each Γ ∈ D the curvature distribution κ Γ satisfies Condition (a) of Theorem 5.6 for vertices.
to each incident internal green face (once for each incidence). (iii) If v G > 2 then each incident internal green face receives at most −1/6 of curvature from v.
Proof. The vertex v begins with curvature +1, and v G ≥ 2 since Γ is green-rich. Thus v has at least two incoming green half-edges, so receives at most −1 in curvature in Step 2 of the algorithm to compute RSym(Γ). Thus Part (i) holds, and Part (ii) is now clear. For Part (iii), notice that if v G > 2 and x = v G then the maximum value of 2−vG 2(vG−x) is attained when x = 0 and v G = 3.
We now show that for each Γ in D the curvature distribution κ satisfies Condition (a) of Theorem 5.6 for red faces. Recall our conventions in Definition 3.1 on boundaries of faces.   Figure 3). Then δ G (v) ≥ 4, and f is incident with no red blobs at v.
Proof. First assume that ∂(f ) \ ∂(Γ) contains no edge. Since Area(Γ) > 1, each vertex v 0 that lies on both ∂(f ) and an edge of ∂(Γ) \ ∂(f ) satisfies δ G (v 0 ) ≥ 3, and is incident at least twice with the external face. By Lemma 6.5, each such vertex v 0 therefore gives at most −1/2 of curvature to f in Step 3 of the algorithm to compute RSym(Γ), so κ(f ) ≤ 1/2 and both claims follow.
Assume instead that ∂(f )\ ∂(Γ) contains an edge. Let β denote a maximal sequence of incident vertices and (consolidated) edges on ∂(f ), such that each edge of β is internal in Γ, and let v 1 and v 2 be the vertices at the beginning and end of β. Notice that δ G (v i ) ≥ 2 for i = 1, 2, since Γ is green-rich. If δ G (v i ) ≥ 3 then we can apply Lemma 6.5 with x ≥ 1 and v G ≥ 3 to deduce that v i gives curvature at most −1/4 to f in Step 3 of the algorithm to compute RSym(Γ), and κ gives curvature at most −1/2 to f , by Lemma 6.6.
Suppose now that κ(f ) > 0. Then, by the previous paragraph, there must be exactly one such maximal sequence β on ∂(f ). Suppose that β contains a vertex v = v 1 , v 2 that lies on ∂(Γ). If δ G (v) = 2, then there are two red blobs adjacent to f at v (either or both of which may be equal to B 1 or B 2 ), giving additional combined curvature at most −1/2 to f , and so κ(f ) ≤ 0, contrary to assumption. If δ G (v) = 3, then f is adjacent to at least one red blob B 3 at v, and the combined additional curvature that B 3 and v give to f is at most −1/2, giving κ(f ) ≤ 0 again. Hence δ G (v) ≥ 4, and so v gives at most −1/3 of curvature to f , and there can be at most one such v.
In particular, we have now shown that if RSym succeeds on a diagram Γ ∈ D, then κ Γ satisfies Conditions (a), (b) and (c) (with m = 1/2) of Theorem 5.6. Since all diagrams in D are green-rich, if no V σ -letter is trivial in G it follows immediately from Proposition 3.15 that κ Γ satisfies Condition (d).
We shall show next that the set D satisfies Condition (e) of Theorem 5.6, provided that no V σ -letter is trivial in G.
Proposition 6.8. Let P be a pregroup presentation for a group G, and let w be a cyclically P -reduced word that is equal to 1 in G. Assume that no V σ -letter is trivial in G. Then there exists w ′ ∈ I(w) that is the boundary word of a coloured diagram Γ ∈ D.
Proof. Let Γ be a coloured diagram of minimal coloured area, amongst all coloured diagrams of words w ′ ∈ I(w), and let w ′ be the boundary word of Γ. We shall show that Γ ∈ D.
Since w ′ ≈ c w, it follows from Theorem 4.3 that w ′ is cyclically P -reduced. The assumption that Γ has minimal coloured area implies that Γ is semi-P -reduced, by Proposition 3.7.
We have assumed that no V σ -letter is trivial in G, so Γ is loop-minimal, and if |∂(Γ)| = 1 then the unique boundary face is green. No letter x ∈ X such that x = x σ is trivial in G, so by Proposition 3.8 the diagram Γ is σ-reduced. It now follows from Proposition 4.9(i) and the minimality of CArea(Γ) that Γ is green-rich.
Finally, the loop-minimality of Γ and the minimality of CArea(Γ) imply that the boundary word of each simply connected red blob has no proper subwords equal to 1 in U (P ), by Proposition 4.12. Hence Γ ∈ D.
It remains to deal with the assumption that no V σ -letter is trivial in G. We prove next that, subject to some easily-checkable conditions on the set R of relators, if RSym succeeds then there are no diagrams in D of boundary length two. Lemma 6.9. Let P = X σ | V P | R be a pregroup presentation. Suppose that no R ∈ R has length 1 or 2 and that no two distinct cyclic conjugates of relators R, S ∈ I(R) ± have a common prefix consisting of all but one letter of R or S. Let Γ be a diagram in D with boundary length 2. Then RSym does not succeed on Γ.
Proof. Assume that RSym succeeds on Γ. Since each R ∈ R has length at least three, Area(Γ) > 1. Each boundary face f of Γ satisfies κ(f ) ≤ 1/2 if f is green, by Lemma 6.7, and κ(f ) ≤ 0 if f is red. Hence, since all of the positive curvature of κ lies in the boundary faces, Γ must have exactly two boundary faces, f 1 and f 2 say, both green. The two vertices v 1 and v 2 on ∂(Γ) both satisfy δ G (v i ) ≥ 3, so by Lemma 6.5 in Step 3 of the algorithm to compute RSym they each give curvature at most −1/4 to each of f 1 and f 2 . So in fact δ G (v 1 ) = δ G (v 2 ) = 3, and both give curvature exactly −1/4 to each of f 1 and f 2 , after which f 1 and f 2 have total curvature +1. So there can be no other green faces in Γ. The assumptions on common prefixes of relators imply that Area(Γ) > 2. So f 1 and f 2 must both be adjacent to red blobs, and by Lemma 6.6 they receive a nonzero amount of curvature from these blobs in Step 4 of the algorithm to compute RSym, giving a contradiction.
We now give a condition under which the success of RSym shows that no V σ -letter is trivial in G. Theorem 6.10. Let P be a pregroup presentation for a group G. Assume that no R ∈ R has length 1 or 2 and that no two distinct cyclic conjugates of relators R, S ∈ I(R) ± have a common prefix consisting of all but one letter of R or S. If RSym succeeds on P at level 1, then no V σ -letter is trivial in G.
Proof. Suppose that some V σ -letter x is equal to 1 in G, and let Γ be a coloured diagram over I(P) with boundary word x, and with smallest possible coloured area for diagrams with boundary word a single V σ -letter. We do not assume that Γ ∈ D. We shall show that Γ does not exist.
Proposition 3.7 shows that Γ is semi-P -reduced. The diagram Γ is loop-minimal by definition, and Γ is σ-reduced by Proposition 3.8. Our assumption that no R ∈ R has length 1 implies that Area(Γ) > 1. Let f be the unique boundary face of Γ.
Suppose that Γ is green-rich. Then, since we chose Γ to have minimal coloured area, Proposition 4.12 implies that Γ ∈ D. Hence RSym succeeds on Γ for some ε > 0, and in particular Lemma 6.7 implies that κ(f ) ≤ 1/2, which contradicts the total curvature of Γ being 1.
Hence Γ is not green-rich. By Proposition 4.9 (i), this can only occur when f is a red triangle. The fact that Γ is loop-minimal implies that Γ looks like the left hand picture in Figure 2. The boundary label of the subdiagram labelled Θ in Figure 2 is cyclically σ-reduced, since the label of f is in V P , so by Proposition 4.9 (ii), with the possible exception of v and the other vertex in Figure 2, which we shall call u, all vertices w in Θ satisfy δ G (w) ≥ 2. We shall show that δ G (u) ≥ 2 and δ G (v) ≥ 2, and hence that Γ is in fact green-rich, a contradiction.
Consider first the vertex labelled v in Figure 2. Theorem 3.14 shows that δ G (v) ≥ 1, so assume, by way of contradiction, that δ G (v) = 1, and let f 1 be the green face incident with v. If δ R (v) = 1, then the boundary label z of f 1 is not cyclically P -reduced, a contradiction. If δ R (v) = 2, then both incident red faces are adjacent to f 1 . Then f 1 can be replaced by a green face with boundary label an interleave of z, yielding a diagram with boundary word x but with smaller coloured area, a contradiction. If δ R (v) ≥ 3 then, since the loop-minimality of Γ implies that there are no loops labelled by elements of V P based at v, we can apply Lemma 3.13 to reduce δ R (v) to two, and then we reach a contradiction as before. Hence δ G (v) ≥ 2.
Assume next that δ G (u) = 1 in Γ (so the only green face incident with u is the external face), and notice that δ R (u) ≥ 3, since u is incident twice with the red face f , and with at least one other red face. If δ R (u) = 3, then Γ contains a loop at v labelled by a letter from V P , contradicting the minimality of Γ. If δ R (u) = 4, then Θ consists of two red triangles that meet at v, and enclose a subdiagram ∆ of boundary length 2, as in Figure  4. Let the boundary label of ∆ be ab, and notice that b = a σ , as otherwise there would exist a diagram proving that x = U(P ) 1, contradicting Theorem 2.7. If (a, b) ∈ D(P ), then there would exist a diagram consisting of ∆ surrounded by a single red triangle, which would have boundary a single letter from V P but have coloured area less than that of Γ, contradicting the minimality of Γ. Hence ∆ is a σ-reduced, semi-P -reduced, greenrich loop-minimal coloured diagram with cyclically P -reduced boundary word, and the minimality of Γ means that Proposition 4.12 shows that ∆ ∈ D. However, we showed in Lemma 6.9 that RSym fails on all diagrams in D of boundary length 2, contradicting our assumption that RSym succeeds. Hence δ R (u) ≥ 5 in Γ, and so δ R (u) ≥ 3 in Θ. Applying Lemma 3.13 to Θ (in which there are no loops based at u with labels from V P ), allows one to reduce δ R (u) in Θ down to three, eventually yielding a contradiction as in the previous paragraph. Hence δ G (u) ≥ 2, and so Γ is in fact green-rich, a contradiction.
Finally, we are able to prove that, subject to the same conditions on R as in Theorem 6.10, if RSym succeeds on a pregroup presentation P for a group G, then G is hyperbolic. Recall Remark 5.5 about Dehn functions over F (X σ ).
Theorem 6.11. Let P = X σ | V P | R be a pregroup presentation of a group G, and let r be the maximum length of a relator in R.
Assume that no R ∈ R has length 1 or 2 and that no two distinct cyclic conjugates of relators R, S ∈ I(R) ± have a common prefix consisting of all but one letter of R or S.
(i) Suppose that RSym succeeds on the presentation P (at level 1) for some ε > 0. Then the Dehn function of X σ | V P ∪ I(R) is bounded above by (ii) If V P is empty, and RSym succeeds on P, then the Dehn function of X σ | R is bounded above by n( 1 2ε + 1) − 1 ε . (iii) If V P is nonempty, I(w) = w for all cyclically P -reduced words w, and RSym succeeds on P, then the Dehn function of (iv) If no V σ -letter is trivial in G, and RSym succeeds at level d on P then the Dehn function of X σ | V P ∪ I(R) is bounded above by In particular, if RSym succeeds at level 1, or if no V σ -letter is trivial in G and RSym succeeds at level d, then G is hyperbolic.
Proof. We first prove (i), by showing that RSym satisfies all conditions of Theorem 5.6. By Proposition 6.3, RSym is a curvature distribution scheme on D. Let Γ ∈ D, and let κ = RSym(Γ). The fact that κ is non-positive on vertices and red triangles follows from Lemmas 6.5 and 6.6, and it is clear from Step 2 of the algorithm to compute RSym that κ(e) = 0 for each edge e. Hence κ satisfies Condition (a). Condition (b) is satisfied with d = 1 by our assumption that RSym succeeds (at level 1). By Lemma 6.7, κ satisfies Condition (c) with m = 1/2. By Theorem 6.10, no V σ -letter is trivial in G. Hence all coloured diagrams over I(P) are loop-minimal and green-rich, so by Proposition 3.15 all diagrams in D satisfy Condition (d) with λ = 3 + r and µ = 1. It now follows from Theorem 5.6 that if Γ ∈ D has boundary length n and area greater than 1 then, as in Corollary 5.7, A diagram of area 1 has boundary length n ≥ 3, since no R ∈ R has length less than 3. For n ≥ 3 the above bound evaluates to at least 1, so in fact this area bound applies to all Γ ∈ D.
We showed in Proposition 6.8 that if w = G 1 then there exists an w ′ ∈ I(w) that is the boundary of a coloured diagram Γ ∈ D. Hence it follows from the definition of I(w) and Lemma 4.5 that there is a coloured diagram Γ ′ with boundary word w and area at most Area(Γ) + 2n, which gives the bound in the theorem statement.
(ii) Since there are no red triangles, κ satisfies Condition (d) of Theorem 5.6 with λ = 1 and µ = 0, so the formula in Part (i) simplifies as given (and is valid for diagrams consisting of a single face).
(iii) We keep λ and µ as in Part (i), but take w = w ′ in the final paragraph of the proof.
(iv) The assumption that no V σ -letter is trivial in G means that all diagrams are loop-minimal. Hence as in Part (i), by Proposition 3.15 we can set λ = 3 + r and µ = 1 in Theorem 5.6. We can then apply Theorem 5.6 with m = 1 and the specified value of d to diagrams Γ ∈ D. Proposition 6.8 applies, since all diagrams are loop-minimal, and so we can complete the argument as in the case d = 1.

A polynomial-time RSym tester
In this section we describe a procedure, RSymVerify(P, ε), that attempts to verify that RSym succeeds on a given presentation P = X σ | V P | R with a given value of ε: recall from Definition 6.4 that this means that RSym succeeds on all of the (infinitely many) diagrams in D. We shall show in Subsection 7.7 that RSymVerify runs in polynomial time.
RSymVerify returns either true or fail. In the first case, RSym is guaranteed to succeed on P with constant ε. If RSymVerify returns fail, then it does not necessarily mean that RSym does not succeed on P. In that case, RSymVerify returns one or more configurations that could arise in a diagram in D over I(P) on which RSym might fail, but such a diagram may not exist. The user can either attempt to show that such a diagram does not exist, or try again with a smaller value of ε.
The majority of the subroutines described in this section will be useful for testing other curvature distribution schemes, not just RSym.
We shall initially explain the algorithms under the assumption that I(R) = R. This is a commonly-occurring special case -for example all quotients of free products of free and finite groups can be presented this way. The necessary modifications for when I(R) = R are given in Subsection 7.8.

Preprocessing
We apply some preprocessing to the presentation, to ensure that the assumptions of Theorem 6.11 hold, and to improve the likelihood that RSym succeeds. The first two steps of preprocessing are done before a pregroup P is chosen, when we just have a group presentation X | R .
Preprocessing step 1: Eliminate any relators of the form x or xy with x, y ∈ X, and x = y, by eliminating generators. Delete any relators of the form x 2 with x ∈ X, and require that x σ = x in the pregroup P .
Preprocessing step 2: Look for pairs R 1 , R 2 ∈ R for which there are distinct cyclic conjugates S 1 , S 2 of R ±1 1 , R ±1 2 that have a common prefix of length greater than half of |S 1 |. That is, S 1 = ww 1 and S 2 = ww 2 with |w| > |w 1 |. If R 1 = R 2 , then replace R 2 by the shorter relator w −1 1 w 2 . Notice that it is not possible to have R 1 = R 2 and S 1 = S 2 with |w 1 | = |w 2 | = 1.
We may need to carry out these two steps repeatedly, but at the end of them all relators have length at least 3, and no two distinct cyclic conjugates of relators in R, S ∈ R ± have a common prefix consisting of all but one letter of R or S. See, for example, [8, Section 5.3.3] for discussion of how to do this efficiently. Note that we are only carrying out Steps 1 and 3 of the simplification in [8]: we are not attempting to eliminate generators using relators of length greater than two.
Preprocessing step 3: Define a pregroup P on the remaining generators (adding additional generators if necessary to close P ), and ensure that all elements of R are cyclically P -reduced. Ideally, as many remaining relators of length 3 as possible should become elements of V P rather than R.
After this, all hypotheses in Theorem 6.11 are satisfied. We assume for now that after Preprocessing step 3, I(R) = R: see Subsection 7.8 for further preprocessing that is required if this assumption does not hold.

Steps, locations and places
RSymVerify needs to check that, for every diagram Γ ∈ D, every non-boundary internal green face f ∈ Γ receives at most −1 − ε of curvature from its incident vertices and red blobs in Steps 3 and 4 of the algorithm to compute RSym. Each such face f has boundary label some R ∈ R ± = I(R ± ), and ∂(f ) is split up into the consolidated edges (see Definition 3.1) that f shares with its adjacent faces in Γ.
The idea is to consider each relator R ∈ R in turn, and to use the relators in V P and R ± to determine the possible decompositions into consolidated edges e i of the boundary of a non-boundary face f with label R. We do not need to consider R −1 , as the situation for R −1 will be equivalent to that for R. Each such decomposition corresponds to an expression of some cyclic conjugate R ′ of R as w 1 w 2 · · · w k , where w i is the label of e i .
We attach a colour C i ∈ {G, R} to each w i in the decomposition, which is the colour of the adjacent region (green face or red blob): there could be more than one decomposition R ′ = w 1 w 2 · · · w k with the same w i but with different colours C i . We have assumed that Γ ∈ D, so Γ is green-rich. Hence if C i = R then |w i | = 1. For reasons that will become clear shortly, we do not allow C 1 = R and C k = G; in that situation, we shall instead consider the decomposition w 2 · · · w k w 1 .
From now on, we shall often think of the triangles within a red blob as having been merged, and treat the blob as having no internal structure other than its area. As a consequence, we will never consider a vertex to have more than one consecutive incident red face.
We use information about the adjacent faces and the vertices v i at the ends of the e i to compute an upper bound χ i on the curvature that v i and a blob incident at e i (if there is one) could give f in Steps 3 and 4 of the algorithm to compute RSym. If we find a decomposition with χ 1 + · · · + χ k > −1 − ε, then RSymVerify returns fail and gives details of the decomposition. Definition 7.1. For a given coloured decomposition R ′ = w 1 w 2 · · · w k as above, a step consists either of a single subword w i , or of two consecutive subwords w i w i+1 , determined as follows, where subscripts should be interpreted cyclically.
(i) If C i = G and C i+1 = R, then w i w i+1 is a step.
(ii) If neither w i−1 w i nor w i w i+1 is a step by Condition (i), then w i is a step.
We have disallowed the combination, C 1 = R, C k = G, so this cannot give rise to a step w k w 1 . Note that the steps are the same for any cyclic permutation of the decomposition that does not violate the C 1 = R, C k = G condition.
We define the stepwise curvature of a step to be χ i when the step is w i and χ i + χ i+1 when it is w i w i+1 . The length of a step is the number of letters of R ′ that it comprises.
The reason for defining the steps in this way is that, as we shall see in Lemma 7.13, this guarantees that each stepwise curvature is at most −1/6, giving an upper bound on the number of steps that must be considered for each such R ′ .
Definition 7.2. Let R ∈ R ± , and fix a word w = x 1 x 2 · · · x |w| such that R = w k with k maximal amongst such expressions for R. A location on R is an ordered triple (i, a, b), denoted R(i, a, b), where i ∈ {1, . . . , |w|}, a = x i−1 (or x |w| if i = 1), and b = x i .
For example, if R = abab = (ab) 2 then the locations are R (1, b, a) and R(2, a, b). We shall present a method to find such a w and k in the proof of Theorem 7.16. (ii) the half-edge on f 2 after b σ is labelled c; (ii) if C = G then f 2 is green, and if C = R then f 2 is a red blob.
We say that P is green if C = G and red otherwise.
Notice that if C = G then, by the fact that Γ is semi-σ-reduced, there exists a location R ′ (j, b σ , c) such that the label of R ′ beginning at b σ is not equal in F (X σ ) to the inverse of the label of R that ends at b. If C = R, then b σ must intermult with c, as in Definition 4.13.
RSymVerify computes an array of all intermult pairs, and then finds all locations of relators R ∈ R ± . For each location R(i, a, b) with R ∈ R, it must find all instantiable places. To do so, it considers each letter c ∈ X, and each C ∈ {R, G}. For C = R it checks that b σ intermults with c. For C = G it checks that there exists a location R ′ (j, b σ , c) such that a diagram of area two with faces labelled by R and R ′ , sharing the edge labelled b, is σ-reduced.

Vertex data and the Vertex function
In the following description, we fix a relator R ∈ R and let f be a non-boundary face labelled R in a diagram in D. When decomposing R into steps, we find an upper bound on the curvature that can come to f from its incident vertices in Step 3 of the algorithm to compute RSym. Whilst there are infinitely many possible vertices v that can arise in such a diagram, almost all vertices have high green valency, and so give f not much more than −1/2 of curvature in Step 3. In this section we show how to produce a list of descriptions of vertices v that could give f curvature at least −1/3. We do not completely describe each such v, but only store information on the possibilities for three consecutive incident faces, reading anticlockwise, together with the maximal corresponding curvature.
Let P = (R(i, a, b), c, C) be a place, and let v be a vertex on ∂(f ) between the edges labelled a and b in a diagram Γ ∈ D that instantiates P, such that f is non-boundary. Let f 1 and f 2 be the faces incident with the edges labelled a and b, respectively, as in Figure 5(b), so that f 2 is as in Definition 7.3. We design a function Vertex, which takes as input a description of such a triple (f 1 , f, f 2 ), and returns an upper bound on the curvature χ(v, f, Γ) that v gives to f in Step 3 of the algorithm to compute RSym.
To do so we shall compute minimal weights of paths between vertices in a certain directed edge-weighted graph G, which we shall now define. We shall refer to the vertices and edges of G as G-vertices and G-edges, to avoid confusion with the vertices and edges of coloured diagrams.  There is a (directed) G-edge from (a, b, G) to (b σ , c, G) if there exist locations R(i, a, b) and R ′ (j, b σ , c) such that the two-face diagram in which faces labelled R and R ′ share this edge labelled b is σ-reduced. There is a G-edge from each (a, b, G) to each (b σ , c, R). There is a G-edge from each (a, b, R) to each (b σ , c, G). There are no G-edges between red G-vertices, since we do not allow red blobs to share edges with other red blobs. The G-edges have weight 1 if their source is green and weight 0 if it is red.
After computing the list of all places, the next step in RSymVerify is to compute G. We also store a list of the locations that correspond to each green G-vertex.
The Vertex function takes as input a triple (ν 1 , ν, ν 2 ) of G-vertices for which ν is green and there is a (directed) path ν 1 , ν, ν 2 in G, and returns a curvature bound. Here ν 1 , ν and ν 2 represent subwords of boundary labels of adjacent faces f 1 , f and f 2 around a vertex in a coloured diagram, as in Figure 5(b), together with their colours.
It remains to describe how to bound χ(v, f, Γ). Non-boundary vertices of green degree k correspond to directed G-circuits of weight k. The following lemma limits the G-paths that we need to find. Lemma 7.5. Let v be a vertex in a diagram Γ ∈ D, and let f be an internal green face incident with v. If v is incident more than once with the external face, then v gives curvature at most −1/2 to f in Step 3 of the algorithm to compute RSym(Γ). Otherwise, the curvatures χ int and χ boundary given to f by v, when v is and is not a boundary vertex, respectively, are as in Table 1.
Proof. The diagram Γ is green-rich, so δ G (v) ≥ 2. Let x be the number of times that v is incident with the external face. Then δ G (v) > x because f is incident with v. By Lemma 6.5, v gives curvature χ = χ(v, f, Γ) = (2 − δ G (v))/(2(δ G (v) − x)) to f . The result follows by computing χ for δ G (v) ≤ 7 and 0 ≤ x < δ G (v), and noticing that χ decreases as δ G (v) and x increase.
By the smallest weight of a G-path from ν 2 to ν 1 , we mean the smallest weight of a path in G with at least one G-edge. (So in the case ν 1 = ν 2 this cannot be 0.) If there is no G-path from ν 2 to ν 1 , then we take its weight to be infinite.
For each G-vertex ν, and for each path ν 1 , ν, ν 2 in G, we let w(ν 2 , ν 1 ) denote the smallest weight of a path in G from ν 2 to ν 1 . We then do the following.
The case ν 1 red and ν 2 green is similar, except that the weights w(ν 2 , ν 1 ) are increased by one, since every edge leaving ν 2 has weight one.
Finally, if ν 1 and ν 2 are both red, then β = 0, which by Lemma 7.5 is an upper bound on χ.
Remark 7.7. When testing RSym at level 1, each non-boundary face f ∈ Γ may be at dual distance two from the external face. Since we are not recording whether the next edges on f 1 and f 2 (the ones labelled c and d in Figure 5(b)) are boundary edges, we allow the Vertex function to consider them as boundary. See Remark 7.11.
Similarly, as a consequence of the possible presence of the external face at dual distance two, the bracketed values of χ true and χ false in Table 1 are not used by RSymVerify, and we impose a lower bound of −1/3 on the return values of the Vertex function. However if, for example, we are testing RSym at level 2 and V P = ∅ (so there are no red triangles in any diagram, and U (P ) is a free product of copies of Z and C 2 ), then all boundary vertices v of a face f to be tested satisfy δ G (v) ≥ 6, and so we can make use of these smaller curvature values.

Red blob data and the Blob function
Similarly to vertices, there are infinitely many possible red blobs in diagrams in D. The procedures described in this section collect information about red blobs that could give curvature more than −5/14 to an adjacent green face in Step 4 of the algorithm to compute RSym.
We create a function Blob(a, b, c), which takes as input (a, b, c) ∈ X 3 such that (a, b) and (b, c) intermult, and returns an upper bound on the curvature χ(a, b, c) that could be given by a red blob with abc as a subword of its boundary word across the edge labelled b to an adjacent green face.   Table 2.
Proof. Let B have boundary length l and area t. If B is not simply connected, then by Lemma 4.11, l ≤ t, so χ ≤ −1/2. Hence B is simply connected and Γ is green-rich, and so t = l − 2, by Lemma 4.11. The values in Table 2 now follow easily from Lemma 6.6.
Definition 7.9. We call x ∈ X an R-letter if x occurs in an element of I(R ± ).
Notice that non-R-letters can only appear on the boundary of a diagram, and that our present assumptions imply that an R-letter occurs in an element of R ± .
We compute a list of cyclic words w ∈ X * that satisfy all of the following conditions: 1. w is equal to 1 in U (P ).

4.
No proper nonempty subword of w is equal to 1 in U (P ).

w contains at most one non-R-letter, and none if |w| > 4.
When RSymVerify bounds the curvature that could come from a red blob B, it has specified three consecutive letters a, b, c on ∂(B). The function Blob(a, b, c) checks to see if abc is a cyclic subword of one of the words in the above list. If so, it returns the maximal curvature from Lemma 7.8 over all such words, and otherwise it returns −5/14 if at most one of a and c is not an R-letter, and −1/2 otherwise. Lemma 7.8 ensures that the words in the list above contains all boundary words of such red blobs: notice in particular that if a red blob is simply connected, then its boundary word is equal to 1 in U (P ), and if a red blob has at least two boundary edges then it gives curvature at most −1/2 across each internal edge. Recall from Definition 6.1 that the boundary words of all red blobs in diagrams in D have no proper subwords that are equal to 1 in U (P ). The following is therefore immediate: Remark 7.11. In Remark 7.7 we observed that the Vertex function often assumes that the face f is dual distance two from the external face. At present this data is not being used by the Blob function, which may be bounding curvature as if any corresponding blobs have no boundary edges. Some curvature is potentially being missed. We plan

One-step reachable places and the OneStep lists
Recall Definition 7.1 of step and step curvature. For each place P on each relator R, we create a list OneStep(P) of those places Q on R that can be reached from P in a single step, together with the largest possible associated step curvature χ. If R = w k is proper power, then each place occurs k times on R. So a place Q could occur several times in OneStep(P), corresponding to different positions on R relative to P. To differentiate them, we store the number of letters of R between P and Q for each item on the list. We describe how to compute this data in this section. Definition 7.12. Let P be a place with location R (i, a, b). A place Q is one-step reachable at distance l from P, where 1 ≤ l < |R|, if the following hold: (i) Q has location R(j, s, t) for some s, t ∈ X, where j = i + l (interpreted cyclically).
(ii) If P is red, then l = 1 (and so s = b).
(iii) If P is green, then exactly one of the following occurs: (a) there exists a green face f ′ instantiating P, and a consolidated edge between f and f ′ of length l from the location of P to that of Q, and Q is green; (b) there exists an intermediate place P ′ whose location is R(j − 1, u, s) and whose colour is red, there is a green face f ′ instantiating P such that there is a consolidated edge between f and f ′ of length l − 1 between the locations of P and P ′ , and there is red edge between P ′ and Q.
For each place P = (R(i, a, b), c, C) on R, we compute the list OneStep(P) as follows. In the description below, by including an item (Q, l, χ) in OneStep(P), we mean append it to the list if there is no entry of the form (Q, l, χ ′ ) already or, if there is such an entry with χ > χ ′ , then replace that entry with (Q, l, χ).
Case C = G. For each location R ′ (k, b σ , c) instantiating P, proceed as follows.
1. If P ′ is green then include (P ′ , l, χ ′ ) in OneStep(P). (See Figure 6(b).) 2. If P ′ is red then P ′ is the intermediate place of the step. Find all places Q that are one letter further along R than P ′ . (See Figure 6(c).) Just as in Case R, compute the combined maximum curvature χ ′′ returned by the red blob between P ′ and Q and the vertex at Q. Include (Q, l + 1, χ ′ + χ ′′ ) in OneStep(P). (i) The place Q is one-step reachable from P at distance l.
(ii) There exists a coloured decomposition of a cyclic conjugate R ′ of R such that a subword w k or w k w k+1 of R ′ between a location of P and a location of Q is a step of length l, the face adjacent to f at w k has colour C, and edge after w −1 k labelled c, and the face adjacent to f at the letter after the end of the step has colour C ′ and next letter c ′ .
Proof. It follows from the definitions that (i) and (ii) are equivalent: the only thing for the reader to check is that enough conditions have been placed in (ii) to uniquely identify the place Q at distance l from P.
It is also clear that the OneStep algorithm finds all one-step reachable places, and does not find any places that are not one-step reachable, so the equivalence of (i) and (iii) follows.
The fact that χ is an upper bound on the step curvature is immediate from Definition 7.1 and Lemmas 7.6 and 7.10. When C = R, or when C = G and P ′ = Q so that P ′ is red, the claim that χ ≤ −1/6 follows from Blob(y, b, c) ≤ −1/6 for all y, b, c. Otherwise C = G and P ′ = Q is green, and the vertex v at any instantiation of P ′ has δ G (v) ≥ 3, so the first case of the Vertex function applies, and returns a bound of at most −1/6.

The main RSymVerify procedure
We now choose a value of ε > 0 to test, and check whether the steps computed in the lists OneStep(P) could be combined around a relator to leave it with more than −ε of curvature. In this subsection, we shall first present the main RSymVerify(P, ε) procedure which carries out these checks and then prove that it works.
After computing the data and functions from the previous subsections, RSymVerify(P, ε) runs a procedure, RSymVerifyAtPlace(P s , ε), at each start place P s on each relator R ∈ R in turn. If every call to RSymVerifyAtPlace returns true, then RSymVerify returns true, but if any fail, then it aborts and returns fail.
RSymVerifyAtPlace(P s , ε) creates a list L, whose entries are quadruples (Q, l, k, ψ). The first three components represent a place Q at distance l from P s along R that can be reached from P s in k steps. The final component ψ is equal to (1 + ε)l/|R| + χ, where χ is the largest possible total curvature arising from these k steps. If ψ ≤ 0 then we are on track for a final curvature of most −ε, whereas if ψ > 0 then we are not. We shall show in the proof of Theorem 7.14 that there is no need to keep a record of situations in which ψ < 0. In other words, we may assume that if the test fails then ψ ≥ 0 after each step in the failing decomposition. By Lemma 7.13, the largest possible step curvature is −1/6, so the cumulative curvature after ⌈6(1 + ε)⌉ steps is at most −ε, and we only need consider ⌈6(1 + ε)⌉ − 1 steps from P s . There can also be at most r steps, where r is the length of the longest relator in R, so we define (iv) else include (Q, l + l ′ , i, ψ ′ ) in L.

Return true.
We now make a couple of remarks on the procedure. First, notice that if on the ith iteration of Step 2 there are no places Q that can be reached from any P with non-positive curvature, then RSymVerifyAtPlace stops early. As we shall see in the proof of Theorem 7.14, Lemma 7.15 implies that, if there is a decomposition of a cyclic conjugate of R that leads to failure of RSymVerifyAtPlace, then there is a start place from which each intermediate place can be reached with non-negative curvature.
Another observation is that, in Step 2 (iv), a list entry (Q, l + l ′ , k, ψ ′′ ) can be replaced by (Q, l+l ′ , i, ψ ′ ) with i > k. If there is a failing decomposition of R ′ involving the original entry, then there must be a (possibly longer) failing decomposition involving the new entry.
Theorem 7.14. Let P = X σ | V P | R be a pregroup presentation, such that I(R) = R for all R ∈ R, and let ε > 0. If RSymVerify(P, ε) returns true then RSym succeeds on P with constant ε.
Before proving Theorem 7.14 we prove a useful combinatorial lemma. Proof. If S = s 1,ℓ is the minimum of {s 1,i | i ∈ L}, then all partial sums starting at a 1 are positive, so we can set j = 1. Otherwise, choose j ∈ L \ {1} such that s 1,j−1 ≤ s 1,i for all i ∈ L.
Notice that s a,b + s a+b,c = s a,b+c for all a, b, c ∈ Z >0 . Thus s j,i = s 1,j+i−1 − s 1,j−1 for all i ∈ Z >0 . However, s 1,j+i−1 = s 1,j+i−1 + kS for some k ∈ Z ≥0 . So in any case, s j,i = kS + s 1,j+i−1 − s 1,j−1 ≥ 0 by the choice of j.
Proof of Theorem 7.14 Assume that there exists a diagram Γ ∈ D over P, and a face f ∈ Γ, such that f is green, has no boundary edges, and satisfies κ(f ) > −ε. We shall show that RSymVerifyAtPlace(P s , ε) returns fail for some P s on f .
Let the label on ∂(f ) be R ∈ R ± . If R ∈ R, then the corresponding face f ′ in the diagram where all faces have labels the inverses of the labels of those in Γ will satisfy κ(f ′ ) > −ε, so assume without loss of generality that R ∈ R.
As discussed in Subsection 7.2, for some cyclic conjugate R ′ of R, we have R ′ = w 1 w 2 · · · w k , where each w i labels a consolidated edge e i in Γ, and each w i has an associated colour C i ∈ {C, R} describing the colour of the other face incident with e i in Γ. Recall that we do not allow the combination C 1 = R, C k = G. From this we derive a decomposition R ′ = v 1 v 2 · · · v ℓ , where each v i labels a step and is equal either to a single w j or to some w j w j+1 with w j green and w j+1 red.
Let the step curvature given to f by the step corresponding to v i be s i , let l i be the number of letters in v i , let λ i = (1 + ε)l i /|R|, and let By Lemma 7.15 there exists an i such that the partial sums a i , a i + a i+1 , . . . , a i + · · · + a ℓ + a 1 + · · · + a i−1 are all non-negative. Replace R ′ if necessary by its cyclic conjugate R ′′ := v i v i+1 · · · v i−1 , and observe that the steps induced by the corresponding decomposition into consolidated edges are the same subwords v i as before.
Let P s be the place on R at the beginning of R ′′ (which is instantiable because Γ ∈ D). We showed in Lemma 7.13 that each step v i corresponds to a pair P, Q of places on R, and that there exist l and χ such that (Q, l, χ) ∈ OneStep(P), with χ an upper bound on the step curvature. RSymVerifyAtPlace(P s , ε) uses this upper bound on the curvature of each step, so the partial sums calculated for each place are greater than or equal to the actual curvature sums, and in particular are all non-negative. Thus RSymVerifyAtPlace(P s , ε) returns fail. ✷

Summary of RSymVerify, and complexity
We now summarise the steps carried out by RSymVerify, specify the subsections in which each step is described, and show that RSymVerify runs in time polynomial in |X|, |R| and r, where r = max{|R| : R ∈ R} is the length of the longest relator.
Step 0 describes preprocessing that takes place before we define the pregroup and the presentation P = X σ | V P | R , so we do not regard this as part of RSymVerify, which takes P as input. However, the presentation simplification process involves comparing subwords of cyclic conjugates of the relators, and any simplification reduces the total length of the presentation, so it is clear that this can be carried out in polynomial time. We assume that products and inverses in the pregroup can be computed in constant time.
Proof. We shall work through steps 1 to 8 of the above summary of RSymVerify, bounding the time complexity of each step. We are not attempting to find the optimal bounds, simply to show that the process runs in low-degree polynomial time.
In Step 1, we compute an X × X boolean array describing the set of all intermult pairs (a, b) ∈ X 2 . For each a ∈ X, and for each b ∈ X \ {a σ }, we must check whether (a, b) ∈ D(P ) and, if not, whether there exists an x ∈ X such that (a, x) ∈ D(P ) and (x σ , b) ∈ D(P ). This can be done in time O(|X| 3 ).
In Step 2, for each R ∈ R we first find w that maximises the value of k for which R = w k . For 2 ≤ l ≤ |R|/2, we let w be the length l prefix of R, and test whether w |R|/l = R, in total time O(r 2 |R|). There are at most 2r|R| locations defined by R ± . When compiling the list of locations, we record which pairs of locations are mutually inverse, in the sense that they describe corresponding positions in inverse pairs of relators.
In Step 3, we find the O(r|X||R|) places P = (R(i, a, b), c, C) with R ∈ R. To do so, for each of the O(r|R|) locations R(i, a, b) we first find all c such that (b σ , c) is an intermult pair, and hence all instantiable red places P = (R(i, a, b), c, R), in time O(|X|). Then, for each location R ′ (j, b σ , c) there is a green place (R(i, a, b), c, G) if and only if the locations R(i, a, b) and R ′ (j, b σ , c) are not mutual inverses. We computed the inverse pairs of locations in Step 2. So Step 3 requires time O(r|R|(|X| + r|R|)) = O(r 2 |X||R| 2 ).
In Step 4, we compute the vertex graph G. It has at most 2|X| 2 G-vertices. We can find these, and also list the locations corresponding to each green G-vertex, in time O(r|R| + |X| 2 ). Let ν = (a, b, G) be a green G-vertex. There is a G-edge from ν to the G-vertex ν 1 = (c, d, G) if and only if (i) c = b σ ; and (ii) if d = a σ then there is more than one location corresponding to ν 1 . (Condition (ii) ensures that there exists a σ-reduced diagram instantiating this G-edge.) These two conditions can be tested in constant time for each G-vertex ν 1 . There is a G-edge from ν to each G-vertex (b σ , c, R) and one from each G-vertex (c, a σ , R) to ν. We can find all of these edges from and to In Step 5, we compute the values of χ(ν 1 , ν, ν 2 ) for the Vertex function. We begin by using the Johnson-Dijkstra algorithm [12] to find the smallest weights of paths between all pairs of G-vertices in the vertex graph. This algorithm runs in time O(|V | 2 log |V |+|V ||E|), on a graph with |V | vertices and |E| edges, so O(|X| 5 ) in our case, and returns a matrix of path weights. We then consider each of the O(|X| 2 ) green G-vertices ν in turn, and for each of the O(|X| 2 ) directed G-paths ν 1 , ν, ν 2 , we carry out whichever of Steps 1 to 4 from the end of Subsection 7.3 applies. The total time complexity of Step 5 is O(|X| 5 ).
In Step 6, we compute the values of the Blob function. We first identify the set of R-letters, in time O(r|R|), and store this information as a boolean array. We next use the intermult table to construct all of the O(|X| 5 ) words of length l between 3 and 5 such that each cyclically consecutive pair of letters intermult, and that include at most one non-R-letter when they have length 3 or 4, and none otherwise. We then discard all such words w that have length 3 or 4 and are not equal to 1 in U (P ), or have length 5 and are not equal in U (P ) to some a ∈ P . Finally, if l = 5, and w = U(P ) a = 1, then we check that a σ is an R-letter, and that all cyclic subwords of wa σ of length 2 or 3 are not equal to 1 in U (P ). The checks on each word take constant time, so the time complexity of Step 6 is O(|X| 5 ).
In Step 7, we compute OneStep(P), for each of the O(r|X||R|) places P in turn. If P is red then there are O(|X|) 1-step reachable places Q and, for each of them we make O(|X|) calls to both Vertex and Blob to find the maximum step curvature. If P is green, then there are O(r|X|) 1-step reachable places (Q, l). To find them, we look up all O(r|R|) locations for the second face f 1 that instantiates P, and for each of them we find the length l 1 of the maximal consolidated edge between f and f 1 in time O(r). For each such f 1 , there are O(l|X|) = O(r|X|) possibilities for the place P ′ at the end of the consolidated edge. If P ′ is green, then P ′ = Q, and we include its step curvature with a single call to Vertex. If P ′ is red, then we need a further O(|X| 2 ) calls to Vertex and Blob to find all possible triples (Q, l, χ) at the end of the step. So the time complexity of Step 7 is O(r 3 |X| 4 |R| 2 ).
Step 8 runs RSymVerifyAtPlace at each of the O(r|X||R|) places. The length of the list L constructed by RSymVerifyAtPlace is O(r|X|). Each item on L is considered at most ζ ≤ r times, so the time complexity of Step 8 is O(r 3 |X| 2 |R|).

RSym with interleaving
In the previous subsections, we described a procedure, RSymVerify, that checks whether RSym succeeds on a pregroup presentation P under the assumption that I(R) = R. We now describe the modifications that we make when this assumption does not hold, defining a more general procedure RSymIntVerify(P, ε). It follows the same overall steps as RSymVerify, and the reader may wish to refer to Subsection 7.7 for these steps.
The set I(R) is potentially of exponential size, since it might be possible to interleave between each pair of letters of each R ∈ R (for an example of this, see the construction of an amalgamated free product in Theorem 9.4). Despite this, we shall show that RSymIntVerify runs in polynomial time.
The overall strategy of RSymIntVerify is the same as that of RSymVerify: we consider each relator R ∈ R in turn, and look for ways to decompose each cyclic conjugate R ′ of each element of I(R) into words w 1 w 2 · · · w k that maximise the curvature received by R ′ in Steps 3 and 4 of the algorithm to compute RSym. Each w i is an interleave of in is the corresponding subword of the corresponding cyclic conjugate of R. It follows from Lemma 4.5 that all elements of I(R) have a description of this form.
In the preprocessing stage (corresponding to Step 0 of RSymVerify, see Subsection 7.1), we first carry out Preprocessing steps 1 to 3. Once the pregroup has been chosen, if I(R) = R then in Preprocessing step 4 we find all R 1 , R 2 ∈ R for which there exist distinct cyclic conjugates S 1 , S 2 in I(R ± 1 ), I(R ± 2 ) with S 1 = ww 1 , S 2 = ww 2 and |w| > |w 1 |. Each such common prefix w is equal in U (P ) to s σ w ′ t for some s, t ∈ P , where w ′ has length |w| and is a prefix of a cyclic conjugate of R 1 or R −1 1 . We can solve the word problem in U (P ) in linear time by Corollary 2.8, so we can find all such S 1 , S 2 in polynomial time.
As in preprocessing step 2, if we find such a pair and R 1 = R 2 , then we replace R 2 by w −1 1 w 2 . It is conceivable that R 1 = R 2 , S 1 = S 2 and |w 1 | = |w 2 | = 1. In that case we use the implied length two relator w −1 1 w 2 to adjust the pregroup. So again the simplification process ensures that the hypothesis, and hence also the conclusion, of Theorem 6.11 holds.
In Step 1 of RSymIntVerify (see Subsection 7.2), in addition to computing the intermult pairs, for each (a, b) ∈ X × X such that (a, b) ∈ D(P ), we compute the interleave set I (a, b), which consists of all s ∈ P such that (a, s), (s σ , b) ∈ D(P ). We explicitly permit s = 1, so that no interleave set is empty. a, b, s), where R(i, a, b) is a location, and s ∈ I(a, b). Let the subword of the cyclic word R containing the location R(i, a, b) be dabe with d, e ∈ X. The pre-interleave set Pre(R(i)) of R(i, a, b, s) is I (d, a), and the post-interleave set Post(R(i)) is I(b, e).
We now generalise Definition 7.3 to cover non-trivial interleaves. Recall that [a 1 a 2 · · · a n ], with a i ∈ P , denotes the element of P that is the product in U (P ) of the a i . Definition 7.18. A potential decorated place P is a triple (R(i, a, b, s), c, C), where R (i, a, b, s) is a decorated location, c ∈ X, and C ∈ {G, R}. A potential decorated place is a decorated place if it is instantiable in the following sense: 1. There exists a σ-reduced and semi-P -reduced diagram Γ over I(P) with a face f labelled by an element of I(R), elements t ∈ Pre(R(i)) and u ∈ Post(R(i)), a face f 2 meeting f at an edge labelled [s σ bu] ∈ X, and the vertex between the edges of f labelled [t σ as] ∈ X and [s σ bu] has degree at least three; 2. the half-edge on f 2 after [s σ bu] σ is labelled c; 3. if C = G then f 2 is green, and if C = R, then f 2 is a red blob.
Notice in particular that we require ([s σ b], u), ([t σ a], s) ∈ D(P ). In Steps 2 and 3, RSymIntVerify finds all decorated locations of relators R ∈ R ± , and associated decorated places with R ∈ R. For this last task, we determine whether a potential decorated place P = (R(i, a, b, s), c, C) is instantiable as follows. If C = R, then P is a decorated place if and only if there exists u ∈ Post(R(i)) such that [s σ bu] σ is an element of X that intermults with c. When C = G, for each decorated location R ′ (j, d, e, v), we first check whether there exists x ∈ Post(R ′ (j)) such that [v σ ex] = P c. Then, for each u ∈ Post(R(i)) we check whether there exists y ∈ Pre(R ′ (j)) such that [y σ dv] = P [s σ bu] σ . Finally, we check whether the resulting diagram is σ-reduced and semi-P -reduced. If there exist such R ′ (j, d, e, v), u, x and y, then P is a green decorated place.
Definition 7.19. The decorated vertex graph V of I(P) has two sets of vertices. There is a green V-vertex (a, b, s, G) if and only if there exists a decorated location R(i, a, b, s). There is a red V-vertex (a, b, R) for each intermult pair (a, b).
There is a V-edge from (a, b, s, G) to (d, e, v, G) if there exist decorated locations R(i, a, b, s) and R ′ (j, d, e, v) such that the two-face diagram with faces labelled by elements of I(R) and I(R ′ ), sharing an edge at these locations labelled [s σ bu] ∈ X on the R-side and [y σ dv] = [s σ bu] σ on the R ′ -side, is σ-reduced and semi-P -reduced, for some u ∈ Post(R(i)) and y ∈ Pre(R ′ (j)).
There is a V-edge from (a, b, s, G) to each ([s σ bu] σ , c, R), where u ∈ Post(R(i)) for some R(i, a, b, s) and [s σ bu] ∈ X. There is a V-edge from (a, b, R) to (c, d, t, G) if and only if there exists a decorated location R(j, c, d, t), and a u ∈ Pre(R(j)), such that [u σ ct] = b σ .
The V-edges have weight 1 if their source is green, and weight 0 if it is red.
The computation of V is Step 4. We then use V to compute the vertex data in Step 5, just as in Subsection 7.3. The computation of the red blob data in Step 6 proceeds as in Subsection 7.4: notice that the set of R-letters is all elements of X of the form [s σ bu], where R(i, a, b, s) is a decorated location and u ∈ Post(R(i)).
The most significant difference between RSymVerify and RSymIntVerify is in finding the one-step reachable decorated places in Step 7 (see Subsection 7.5). To simplify the exposition, we shall break this task into two parts: finding the edges between green faces, and finding the steps. It would be quicker to carry out these tasks concurrently.
The following algorithm, FindEdges, takes as input R ∈ R and S ∈ R ± , and returns a list L R,S of all possible consolidated edges e between faces f and f 1 with labels in I(R) and I(S). The list L R,S consists of a 5-tuple for each (not necessarily maximal) consolidated edge e: the decorated locations of R at the beginning and end of e in f , the two corresponding decorated locations of S, and the length of e. 2. For each pair of decorated locations R(i, u 0 , u 1 , s) and S(j, v 1 , v 0 , t), with corresponding cyclic conjugates u 0 u 1 . . . u n−1 of R and v σ 0 v σ 1 . . . v σ m−1 of S −1 : (a) Test, using V, whether these could be the beginning of a consolidated edge e. (b) If so, then consider each possible consolidated edge length l = 1, 2, . . . r. For each s l ∈ I(u l , u l+1 ) and each t l ∈ I(v l+1 , v l ), if Proof. Let R = u 1 u 2 · · · u n and S = v m v m−1 · · · v 1 . Assume that have a consolidated edge e between them.
Since FindEdges considers each possible pair of starting decorated locations, we may assume without loss of generality that e is labelled by the subwords of R ′ and S ′ , respectively. Hence and these words are P -reduced. So So e will be found by FindEdges(R, S). For the complexity claims, notice that there are O(r 2 |X| 2 ) decorated locations in Step 2 of FindEdges, that l ≤ r, that for each l we consider O(|X| 2 ) pairs (s l , t l ) of interleaving elements, and that can be tested in time O(l) = O(r), by Corollary 2.8.

In
Step 7, for each decorated place P = (R(i, a, b, s), c, C), we compute a list OneStep(P) of decorated places that are 1-step reachable from P, together with an upper bound on the corresponding step curvature, as follows.
If C = G then we use those 5-tuples in the list L R,S with first entry R(i, a, b, s) to locate the possible decorated places P ′ = (R(j, d, e, s l ), c, C ′ ) that can be reached from P by a single consolidated edge. For each such 5-tuple, the fifth data item specifies the length of this edge, the second identifies the location of P ′ , and the fourth identifies the V-vertex ν 1 , in the notation of Case C = G in Subsection 7.5. Furthermore, the component c of P must be equal to [t σ v 0 u] for some u ∈ P , where R 1 (j, v 1 , v 0 , t) is the second entry of the 5-tuple. Otherwise, Case G is as described in Subsection 7.5. In Step 8 (see Subsection 7.6), RSymIntVerifyAtPlace works with decorated places, but otherwise is identical to RSymVerifyAtPlace.
It is clear that RSymIntVerify runs in polynomial time, although with a higher time complexity than that of RSymVerify.

RSym and the word problem
Suppose that RSym succeeds on a presentation P = X σ | V P | R for a group G. We shall show in this section that this leads to a linear time algorithm for solving the word problem in G, which can be made into a practical algorithm in many examples. One approach is to use the following result.
Proposition 8.1. Let G be defined by the pregroup presentation P = X σ | V P | R . Let r be the length of the longest relator in V P ∪ R. Suppose that, for some constant λ, the Dehn function D P of X σ | V P ∪ I(R) satisfies D P (n) ≤ λn for all n ≥ 0. Then any word w over X with w = G 1 has a subword of length at most 384λr(r − 1) + 64 that is not geodesic.
Proof. It is shown in the proof of [11, Theorem 6.5.3] that G is hyperbolic and that all geodesic triangles in its Cayley graph of G are δ-slim with δ ≤ 96λr 2 + 4. In fact the result of [11, Lemma 6.5.1] can easily be improved from area(∆) ≥ mn/l 2 to area(∆) ≥ 4mn/l(l − 1), which results in the improved bound δ ≤ 24λr(r − 1) + 4. It is proved in [11, Theorem 6.1.3] that all geodesic triangles in the Cayley graph are 4δ-thin, and then [11,Theorem 6.4.1] implies that any word w with w = G 1 must contain a non-geodesic word of length at most 16δ, which is at most 384λr(r − 1) + 64, We proved in Theorem 6.11 that if RSym succeeds with constant ε, then D P (n) ≤ λn, where the constant λ depends only on r and ε. So we can apply Proposition 8.1, and compute γ = 384λr(r − 1) + 64 explicitly, which is typically a moderately large but not a huge number. We can therefore solve the word problem in linear time using a Dehn algorithm, provided that we can solve it for words of length at most γ, which can in principal be accomplished in constant time. In practice, one possibility is to use KBMAG for this purpose, but that is only possible if KBMAG can compute the automatic structure, which may not be feasible, particularly for examples with large numbers of generators.
An alternative approach to solving the word problem, which succeeds in many examples, is to use the success of RSym directly to produce a linear-time word problem solver RSymSolve, and the main purpose of this section is to describe how to do that. It is not guaranteed that such a solver can be constructed, even when RSym succeeds, but the attempted construction of RSymSolve takes low-degree polynomial time.
The remainder of the section is structured as follows: first we define an extra condition that RSym may satisfy, which guarantees that RSymSolve works. Then we present a procedure called VerifySolver, which tests for this extra condition. Finally we describe the algorithm RSymSolve, which solves the word problem, and prove its correctness and complexity. It is similar in spirit to a Dehn algorithm, with complications arising from the fact that we work over I(P) whilst only storing rewrites arising from V P ∪ R, and that we need to work with P -reductions rather than just free reductions. We assume in the above that RSym has succeeded. In fact, it is possible to use RSym to solve the word problem under somewhat weaker hypotheses: see Remark 8.8.
VerifySolver seeks to check that RSym verifies a solver for I(P). It is very similar to the main RSym tester, except that the places at the beginning and end of each run are on ∂(Γ), and are not equal to one another. We describe it only for the case where I(R) = R: the modifications necessary when I(R) = R are straightforward. We shall describe the word problem solver RSymSolve in the general case I(R) = R: as we shall explain in Remark 8.7 below, if VerifySolver succeeds then we can use a standard Dehn algorithm when I(R) = R.
The procedure VerifySolver runs a subprocedure, VerifySolverAtPlace, from each place P s on each relator R ∈ R. The procedure VerifySolver returns true if every call to VerifySolverAtPlace returns true, and fail otherwise.
For a start place P s = (R(i, a, b), c, C) on a face f labelled by R, VerifySolverAtPlace works along all possible sequences of internal edges of f starting at P s , bounding the resulting curvature of f . We seek to show that if κ(f ) > 0, then these internal edges take up less than half of ∂(f ).
The vertex where VerifySolverAtPlace terminates is on the boundary of the diagram, so need not be a place in the sense of Definition 7.3, as it need not be instantiable for any choice of extra letter c ∈ X. a, b) is a location. A terminal place is green, and has no extra letter. For use in this section, Definition 7.12 should be modified, to say that no place is 1-step reachable from a terminal place.
For the rest of this section, a place may be terminal, unless specified otherwise. Before running VerifySolver we re-run the algorithm to compute the lists OneStep(P) (Subsection 7.5), to also find the one-step reachable terminal places from each non-terminal place P. The curvature values χ of the triples (Q, l, χ) in OneStep(P), when Q is terminal, are as follows (we shall justify them in the proof of Theorem 8.4). C = R. We set χ to be the maximum curvature given to R by a boundary red blob at P (calculated using Lemma 7.8 with |δ(B) ∩ δ(Γ)| ≥ 1). C = G. If P ′ = Q we set χ = −1/4. If P ′ = Q then we let χ be the maximum sum of the curvature given to R by the vertex at P ′ and a boundary red blob at P ′ .
For a non-terminal place P s on R, VerifySolverAtPlace(P s ) makes a list of 4-tuples (Q, l, t, ψ). The first three components represent a place Q at distance l from P s along R that can be reached from P s in t steps, where if P s is green then the first "step" consists of only the boundary vertex. The final component ψ is 1 + χ, where χ is the largest possible curvature given to R by these steps: unlike in Subsection 7.6 we do not adjust for the length of the step. The algorithm VerifySolverAtPlace(P s ) returns fail if there is a sequence of neighbouring green faces and red blobs, starting at P s , that occupies at least half of ∂(f ) and from which f receives more than −1 of curvature, and true otherwise.
In the description below, the meaning of including an entry in a list is the same as in Subsection 7.6.
3. If C = R then for each non-terminal place P 1 at distance 1 from P s , calculate the maximum value χ of the sum of the curvature given to R by a boundary red blob between P s and P 1 , and the corresponding curvature of the vertex at P 1 . Include (P 1 , 1, 1, 1 + χ) in L.

Return true.
Note that we do nothing in Step 4 if neither of the specified conditions hold.
We now prove correctness of the VerifySolver procedure. Proof. Let f be a boundary green face of a diagram Γ ∈ D such that κ(f ) > 0, and assume that at most half of the edges of f are contained in ∂(Γ). Let the label of f be R ∈ I(R). We show that VerifySolverAtPlace returns fail for at least one start place P s on R.
By Lemma 7.5, a boundary vertex of green valency at least three gives at most −1/4 of curvature to each incident internal face, so Step 2 of VerifySolverAtPlace, and the value of χ in OneStep(P) when P is green and Q = P ′ is terminal, correctly bound on the curvature received by f when the first or last edge of ∂(f ) \ ∂(Γ) is incident with a green internal face.
Step 3 of VerifySolverAtPlace, and the remaining cases of OneStep(P) when Q is terminal, bound curvature as if the corresponding red blob is on the boundary. To see why this is correct, first notice that the label of any non-boundary red blob is permissable as a label of a boundary red blob. Let B be a red blob at P s with boundary length l and area t (the case where the red blob is at the end of ∂(f ) \ ∂(Γ) is equivalent). By Lemma 4.11, the curvature given to f is maximised by assuming that B is simply-connected, in which case l = t + 2 since Γ is green-rich. If B has a boundary edge at P s , then by Lemmas 6.5 and 6.6, f receives 0 from the vertex v at P s , and receives at most −t 2(t+1) from B. If B has no boundary edge at P s , then f receives at most −1/4 from v and −t 2(t+2) from B. For all t −t 2(t + 1) so f receives at most −t 2(t+1) from v and B. Hence Step 3 of VerifySolverAtPlace and OneStep(P) correctly bound the curvature received by R when the first or last edge of ∂(f ) \ ∂(Γ) is incident with with a red blob. We showed in Lemma 7.13 that the OneStep lists correctly bound all other step curvatures.
We showed in Lemma 6.7 that ∂(f )∩∂(Γ) consists of at most one consolidated edge together with at most one isolated vertex v, and that the internal edges of ∂(f ) form a path. Therefore each place on R at a vertex along these internal edges (except for the last one) has a face of Γ instantiating it, and so is not terminal. Therefore VerifySolverAtPlace is correct to require in Steps 3 and 4(a) that all places are non-terminal.
It remains only to show that ∂(f ) \ ∂(Γ) consists of at most three steps along R, after the initial one (which may not formally be a "step"). Assume first that f ∩ ∂(Γ) contains an isolated vertex v. Then we can decompose ∂(f ) into v 1 , β 1 , v, β 2 , v 2 , β 3 , where v 1 , v 2 , v are vertices on ∂(Γ), and each β i is a sequence of edges and vertices such that β 3 ⊂ ∂(Γ), and β 1 and β 2 are internal to Γ (see Figure 3). As we have just seen, the curvature given to f by the vertices and blobs at the beginning of β 1 and the end of β 2 sums to at most −1/2. We showed in Lemma 6.7 that f is incident with no red blobs at v, and that δ G (v) ≥ 4, so v gives at most −1/3 of curvature to f .
Since the curvature of f is assumed to be positive, by Lemmas 7.5 and 7.8 the face f is adjacent to only these two green internal faces (and possibly some red blobs at v 1 and v 2 ), and so VerifySolverAtPlace will return fail when i ≤ 2, with P s a place at v 1 .
Next assume that f ∩∂(Γ) consists of a single consolidated edge e. Write the boundary of f as e, v 1 , β, v 2 , where β is a sequence of edges and vertices internal to Γ. The vertices v 1 and v 2 , together with any incident red blobs, give at most −1/2 of curvature to f . Excluding the red blobs that might be incident with v 1 and v 2 , by Lemmas 7.5 and 7.8 the path β can be incident with at most two red blobs, or at most two vertices of green degree greater than two, or exactly one of each. Hence f is adjacent to at most three internal green faces, and VerifySolver will return fail.
The complexity claims follow as in the proof of Theorem 7.16.
We now show how to solve the word problem, provided that RSym verifies a solver. First we show that any word w = x 1 . . . x n can be cyclically P -reduced in linear time.
5. P -reduce at the beginning of v: If [x i−1 v 1 ] = P s = 1, then replace v 1 by s, and move CutStart to x i−2 . If [x i−1 v 1 ] = P 1, then move NewStart and CutStart to v 2 and x i−2 .

Repeat
Step 5 until one of the following: no further reductions are found; CutStart should be moved back past x 1 ; NewStart should be moved forward past v l .
7. Provided that there is at least one letter left in v, perform Steps 5 and 6 (with the appropriate pointers) to P -reduce at the end of v.
8. Update the links in the list describing w so that whatever remains of v is now inserted into the correct place in x 1 . . . x n , yielding a word w 1 .
9. Cyclically P -reduce w 1 , as in the proof of Proposition 8.5, yielding a word w 2 . If w 2 is empty, then terminate and return true.
(We start the search for the next rewrite at x α , as earlier untouched letters will still not be eligible for rewriting.) Theorem 8.6. Let P = X σ | V P | R be a pregroup presentation for a group G, such that RSym succeeds on P. If VerifySolver succeeds on I(P) then for all n ∈ N, and for all x 1 . . . x n ∈ X * , the algorithm RSymSolve(x 1 . . . x n ) correctly tests whether Proof. Let w = x 1 . . . x n ∈ X * . By Proposition 8.5 in O(n) we can replace w by a word w 1 = y 1 . . . y k that is cyclically P -reduced. By Theorem 6.11, since RSym succeeds on P, for some w 2 ∈ I(w 1 ) there exists a diagram Γ ∈ D with boundary word w 2 . By Lemma 6.7, either Γ consists of a single face f 1 , which must be green and have curvature +1, or there are at least two boundary faces f 1 and f 2 of Γ with positive curvature. In this second case, since VerifySolver succeeds, the faces f 1 and f 2 each have more than half of their boundary length as a continuous subword of the boundary of Γ.
Hence a rewrite applies to at least one subword z i . . . z i+m−1 of w 2 . Such a subword is equal in U (P ) to [a σ y i ] . . . [y i+m−1 b] for some a ∈ I(y i−1 , y i ) and b ∈ I(y i+m−1 , y m ), and so will be found by RSymSolve.
On input a cyclically P -reduced word w of length n, RSymSolve runs O(n) tests of equality in U (P ) of words of the form a σ w ′ b, where w ′ = t 1 . . . t m is a subword of w with m ≤ (r + 1)/2 such that (a σ , t 1 ) ∈ D(P ) and (t m , b) ∈ D(P ), with the first entry of each pair in L. It also tests for O(n) (cyclic) P -reductions. Every time a letter of w (or of a substring v for replacement into w) is changed, it is due to a shortening of |w|, so at most O(n) letter replacements occur.
Remark 8.7. If VerifySolver succeeds and I(R) = R, then we can replace RSymSolve by a standard Dehn algorithm using the length reducing rewrite rules derived from V P ∪R. The presence of the rules from V P ensures that we reduce our input word w to a P -reduced word. There is no need to carry out any additional cyclic reduction or cyclic P -reduction on w.
This is because cyclic (P -)reduction might delete some letters at the beginning and end of w, and might insert a single new letter at the beginning of w. If the resulting cyclically P -reduced word w ′ was equal to the identity in G, then a diagram Γ ∈ D for w ′ would either consist of a single green face, or have at least two green regions with more than half of their length on the boundary. In the former case, all but one letter of w ′ is a subword of the original word w. In the latter case, the label of the intersection of at least one of these two regions with the boundary of Γ would be a subword of w. So this subword would be reduced in length by the application of one of the rewrite rules.
Although a standard Dehn algorithm is no faster than RSymSolve in terms of complexity (both are linear in the length of w) it has the advantage that it can be implemented efficiently using a two stack model, as described for example in [2].
An improvement to VerifySolver is sometimes possible: for example, when P is the standard pregroup for a free product of finite and free groups. In the following sections we shall refer to this improved version as VerifySolver + .
Remark 8.8. Consider the situation where if (a, b) is an intermult pair, then (a, b) ∈ D(P ). Note that this implies in particular that I(R) = R. Let Γ be a diagram in D and let f be a boundary face of Γ with κ(f ) > 0, with k boundary edges and l internal edges. By Lemma 6.7, the edges in ∂(f ) \ ∂(Γ) form a path e 1 , . . . , e l , say.
If exactly one of e 1 or e l is incident to a red blob whose next edge is on the boundary, then deleting f leaves a red blob B with two edges appearing consecutively on ∂(Γ). By Lemma 4.14 the labels a and b of these two edges intermult. Hence (a, b) ∈ D(P ), so the new boundary word can be P -reduced, deleting at least one red triangle. Hence, deleting f followed by P -reduction shortens ∂(Γ) by at least (k + 1) − l edges. If both e 1 and e l are incident with boundary red blobs, then deleting f , followed by P -reduction, shortens ∂(Γ) by at least (k + 2) − l edges.
Hence one can modify VerifySolverAtPlace and the OneStep values for terminal places. The list L should contain two types of entries, those that record places on paths that start at a boundary red blob, and those that do not.
In Step 4(a) of VerifySolverAtPlace, we replace l + l ′ < n/2 by l + l ′ < (n + 2)/2. In Step 4(b) of VerifySolverAtPlace, if there is a boundary red blob at either P s or just before Q, then failure is only reported if l+l ′ ≥ (n+1)/2. If P s and the edge before Q are both incident with boundary red blobs, then failure is only reported if l+l ′ ≥ (n+2)/2. When using this modified version of VerifySolver, appropriate additions need to be made to the list L of rewrites for RSymSolve to adjoin the letters which can appear on such boundary red blobs. We shall refer to the enhanced version as RSymSolve + .
As in the previous remark, in many situations (we omit the details) we can use a standard Dehn algorithm in place of RSymSolve + , with the modified list L. We can use the success of VerifySolver or VerifySolver + to upgrade our bound on the Dehn function of G. Proposition 8.9. Let D(n) be the Dehn function of X σ | V P ∪ I(R) . If both RSym and VerifySolver succeed, then D(n) ≤ n. If RSym and VerifySolver + succeed, then D(n) ≤ 3n.
Proof. The first claim is clear, since RSymSolve is essentially a Dehn algorithm. For the second, notice that the removal of at most three faces from each diagram results in a shortening of the boundary word.
Remark 8.10. Assume that we know that all V σ -letters are nontrivial in G. Then with a little effort one may show that we can deduce the same bounds on Dehn function of G from the success of RSymSolve and RSymSolve + , even when RSym fails, provided that RSym is able to show that all green faces at dual distance at least two from the external face have non-positive curvature. The assumption that no V σ -letters are trivial in G means that all diagrams are loop-minimal, which permits us to use Proposition 3.15, and to deduce that if w = G 1 then there is a diagram Γ ∈ D with boundary word w. We excluded this case from our earlier analysis as it gave no immediate upper bound on the Dehn function, but RSymSolve and RSymSolve + together provide such a bound.

Examples
In this section we shall first show that RSym generalises several small cancellation conditions. We then show how RSym can be verified by hand to prove the hyperbolicity of various infinite families of presentations. This is an advantage over the algorithm based on the theory of automatic groups that is used by the KBMAG package, which can only handle individual groups and is not susceptible to hand-calculation.

Small cancellation conditions
As a first example of the applicability of RSym, we consider various small cancellation conditions, thereby recovering the result proved in [5,Corollary 3.3]. Furthermore, in many cases RSymSolve solves the word problem. Proof. We set V P = ∅, so all faces are green. Let f be a non-boundary face of Γ. In Step 3 of the algorithm to compute RSym(Γ), a vertex v of f that is not on ∂(Γ) gives curvature gives f curvature at most −1/3, by Lemma 7.5. If, in addition, f is at dual distance at least 3 from the external face, then δ(v) ≥ 6, and so v gives curvature at most −2/5 to f . The claim that RSym succeeds, and the stated values of ε, follow from the fact that f has at least p incident vertices of valency at least q. There are no V σ -letters, so by Theorem 6.11, G is hyperbolic.
With metric small cancellation conditions, RSymSolve solves the word problem.
Proof. The success of RSym follows from Theorem 9.1. VerifySolver considers up to three steps from each place on each relator, with the vertices at each end giving curvature at most −1/4, and the intermediate vertices giving curvature at most 1/q − 1/2, where q ∈ {3, 4}. Hence for C ′ (1/6) a boundary face f with κ(f ) > 0 has at most three internal consolidated edges, and for C ′ (1/4) − T (4) it has at most two. By Lemma 6.7 these internal consolidated edges are contiguous, and comprise less than half of the length of the relator.
Our second example considers the generalisation of small cancellation to amalgamated free products, as described in [13,Chapter V §11]. Let X 1 , . . . , X m be finite groups with proper subgroups A i ≤ X i , let A = A 1 , and let ψ i : A → A i be isomorphisms. Let F = * X i : A = ψ i (A i ) be the free product of the X i , amalgamated over the A i .
A normal form for g ∈ F \ {1} is any expression y 1 y 2 · · · y n such that g = F y 1 y 2 · · · y n , each y i ∈ X j for some j, successive y i come from different X j , and no y i is in A unless n = 1. The length n, and the factors in which the y i lie, are uniquely determined by g. An element g ∈ F \ {1} with normal form y 1 · · · y n is cyclically reduced if n = 1 or y 1 and y n are in different factors, and weakly cyclically reduced if n = 1 or y n y 1 ∈ A. A product of normal forms y 1 · · · y n x 1 · · · x m is semi-reduced if y n x 1 ∈ A and neither normal form is a single element of A.
Let R be a set of weakly cyclically reduced elements of F \ A. The symmetrised set R of R consists of all normal forms of all weakly cyclically reduced F -conjugates of elements of R ± . An element b ∈ F \ A is a piece (of R) if there exist distinct R 1 , R 2 ∈ R such that R 1 = bc 1 and R 2 = bc 2 , where b, c 1 and c 2 are normal forms, and the products are both semi-reduced.
(ii) if R = bc ∈ R, where b is a piece, b and c are normal forms, and the product bc is semi-reduced, then |b| < λ|R|; Theorem 9.4. Let X 1 , . . . , X n be finite groups, let F = * X i : A = ψ i (A i ) be a free product with amalgamation, and let R be a finite set of cyclically reduced elements of F such that R satisfies C ′ F A (1/6).
, with products defined within each X i but not across factors. Then P is a pregroup and RSym succeeds on the presentation (P \ 1) σ | V P | R .
Proof. The fact that P is a pregroup and U (P ) = F is established in [18, 3.A.5.2]. The set of all cyclic interleaves of all cyclic conjugates of elements of R is contained in the set R: the set R also contains elements of F that are weakly cyclically reduced but not cyclically P -reduced.
We shall use the approach of RSymVerifyAtPlace and consider each possible decomposition of R ∈ R into steps. We shall show that the cumulative curvature of R is negative after at most three steps, and hence, by the same use of Lemma 7.15 as in the proof of Theorem 7.14, the overall curvature of R must be negative and so RSym succeeds. If R is not cyclically P -reduced and b is a piece of R, then there is another piece, of the same length as b, of a cyclically P -reduced conjugate of R, so we can assume without loss of generality that R is cyclically P -reduced, and so |R| is as in RSymVerifyAtPlace.
Each R ∈ R has length at least 7, by Definition 9.3(i), so by Lemma 7.13 the curvature of R is immediately negative if the first step consists of a single red edge. All other steps involve a green consolidated edge, so let R ′ , S ′ ∈ R be such that R ∈ I(R ′ ) and S ∈ I(S ′ ) are incident with a consolidated edge e labelled x 1 x 2 · · · x k . Notice that interleaving does not change the factor X i to which a given letter x i belongs, and that |R| = 6k + m for some m > 0, by Definition 9.3(ii).
If the step consists just of the edge e, so that we are in Case 3(a) of Definition 7.12, then the step length is k < |R|/6, and the curvature of R becomes negative. So assume that the step consists of e, followed by a vertex v, and then a red edge between R and a blob B 1 , so that the step length is k + 1. Let χ 1 denote the step curvature. The ratio of the step length to |R| is k+1 6k+m , so the curvature of R becomes negative unless k+1 6k+m ≥ 1/6, and we may assume that k+1 6k+m ≥ 1/6. Notice that k+1 6k+m < 3/10, since k and m are positive integers. Hence, if χ 1 ≤ −3/10, then the curvature of R becomes negative, so assume otherwise. If δ G (v) > 2 or |∂(B 1 )| ≥ 5, then χ 1 ≤ −3/10, a contradiction. Hence δ G (v) = 2 (so R and S are both adjacent to B 1 ), and |∂(B 1 )| ≤ 4.
If the letter of R after e lies in the same free factor X i as the corresponding letter of S, then a semi-reduced expression for R contains a piece of length k + 1, and so k+1 6k+m < 1/6, a contradiction. Hence |∂(B 1 )| = 4, and so χ 1 ≤ −1/4. Hence for the curvature to remain non-negative, we may assume that k+1 6k+m ≥ 1/4, and so |R| is 7 or 8. Therefore, there are no pieces on R of length 2, and so no two consecutive letters of R can lie in the same free factors X i as the corresponding letters of any other element of R ± . Let v 1 be the vertex at the end of B 1 . If δ G (v 1 ) > 2, then χ 1 ≤ −5/12 < −3/10, a contradiction. Hence δ G (v 1 ) = 2, and χ 1 = −1/4.
Since |∂(B 1 )| = 4, it follows as in the previous paragraph that the next step is red, corresponding to a blob B 2 . Let v 2 be the vertex at the end of B 2 , and let χ 2 be the step curvature. If δ G (v 2 ) > 2 or |∂(B 2 )| ≥ 4, then χ 1 + χ 2 < −1/2, so the curvature of R becomes negative. So assume that δ G (v 2 ) = 2 and B 2 is a single red triangle, so that χ 2 ≤ −1/6. This forces the step after this to once again be red. These three steps give a maximum of −1/4 − 1/6 − 1/6 of curvature, for a maximum of 4/7 of the length of R. Since 7/12 > 4/7, the curvature of R is now negative.

Families of presentations
We shall now consider some infinite families of presentations where we can show by hand that RSym succeeds. To help make our descriptions clear and concise, we shall not work through every step of RSymVerify, but just extract the parts that we need.
For our first family of examples we consider the triangle groups. The following result is well known, but it illustrates how we can use RSym to provide a straightforward proof.
Suppose first that ℓ ≥ 3 and hence n ≥ 4. Then are there no instantiable green places, so all steps are red and have length 1. Each step curvature is at most −1/6 by Lemma 7.13, so each non-boundary face receives curvature at most −4/3 in Step 4 of the algorithm to compute RSym, and so RSym succeeds with ε = 1/3. Furthermore, if a boundary face f satisfies κ(f ) > 0, then f has at most four internal consolidated edges, which must be contiguous by Lemma 6.7. Hence if n > 4 then more than half of ∂(f ) is on ∂(Γ), and so VerifySolver succeeds. If n = 4, and f satisfies κ(f ) > 0 and has four contiguous internal edges, then the first or last such edge is incident with a boundary red blob. If (a, b) is an intermult pair then (a, b) ∈ D(P ), so VerifySolver + succeeds and RSymSolve + solves the word problem.
So suppose that ℓ = 2, and so m ≥ 3. Then on R 1 there is a single instantiable (non-terminal) green place P 1 = (R 1 (1, y, x), y, G). Furthermore, the consolidated edges between two adjacent green faces in any diagram Γ ∈ D have length 1. So each step in a decomposition of R 1 has length at most 2.
If n ≥ 7, then κ(R 1 ) ≤ −1/6, and so RSym succeeds with ε = 1/6. The longest possible sequence of edges between a boundary face with positive curvature and the interior of a diagram is length 7 (with label y(xy) 3 ). This sequence of edges has a red blob at each end, so VerifySolver + succeeds (note that VerifySolver fails when n = 7 and succeeds when n ≥ 8). This completes the proof when m = 3.
Suppose that m ≥ 4, so that n ≥ 5. A step of length 2 consists of two consolidated edges e 1 and e 2 of length 1, labelled x and y, for which the adjacent faces are green and red, respectively. Let v be the vertex between e 1 and e 2 . If δ G (v) ≥ 3 then the step curvature is at most −1/3. So assume that δ(v) = 3 and δ G (v) = 2. Then the red blob B incident with e 2 has two successive edges both labelled y −1 = y m−1 .
If Area(B) > 1, then B gives at most −1/4 of curvature to R 1 , and since n ≥ 5, RSym succeeds with ε = 1/4. So assume that B is a triangle. Then the third edge of ∂(B) is labelled y 2 , which is not equal to y −1 since m ≥ 4. Hence B is a boundary red blob, so again gives curvature at most −1/4 to R 1 .
The longest possible sequence of edges between a boundary face with positive curvature and the interior is length 5, with label y(xy) 2 , so VerifySolver + succeeds.
The next result is a more complicated application and is, as far we know, new. (Note Gromov's more general result about appending high powers of a word to a presentation of a hyperbolic group.) Recall that RSym + refers to versions of RSym in which Optional Step 5 is applied: see Section 6.
Furthermore, G is hyperbolic in all of these situations.
Proof. We let P = {1, x, y, Y }, with products x = x σ , Y = y σ , y 2 = Y and Y 2 = y. So the only red blobs in diagrams in D are single red triangles with boundary yyy or Y Y Y , and we can take R ± = {R 1 := (xy) m , R 2 := (xY ) m , R 3 := (xyxY ) n }.
We start by listing the possible labels of consolidated edges between two green faces in any diagram Γ ∈ D, but we omit those in which one of the two faces is labelled R 2 , since these correspond in an obvious way to those with a face labelled R 1 . In each case, we have specified the words labelling the two faces, with the labels of the consolidated edge positioned at the beginning of each of the two words.
Since consolidated edges have length at most 3, each step has length at most 4 and so, if m ≥ 13 and n ≥ 7, then there are least 7 steps in any decomposition of a relator and hence RSym succeeds with ε = 1/6. The longest possible sequence of edges between a boundary face with positive curvature and the interior of Γ is comprised of three steps together with a red triangle at the beginning; and hence has length at most 13. Any such sequence of edges has a red triangle at each end of it, so if m ≥ 13 and n ≥ 7 then VerifySolver + succeeds. This proves Part (i) of the theorem.
For Part (ii), assume that m ≥ 7. Let f 1 be a non-boundary face with boundary label R 1 = (xy) m , in a diagram Γ ∈ D. We consider the possible decompositions of R 1 into steps. A step of length k on R 1 constitutes a proportion k/(2m) ≥ k/14 of |R 1 |, and the step curvature is at most −1/6. So, when k ≤ 2, the step curvature is less than its length requires on average for κ(f 1 ) ≤ 0. In fact, the step curvature is less than required by a factor of at least 7/6. Consider a consolidated edge labelled xy, as in item 4 of the list above. The edges of all red triangles are labelled y or Y , and the letter following xy in R 1 is x, so such an edge must be followed by another green consolidated edge. So this step consists of the consolidated edge xy only and hence has length 2. Hence the step curvature is less than required by a factor of at least 7/6. This deals with items 1, 2, 3 and 7 of the list above.
Consider next a consolidated edge e labelled xyx, as in item 5 of the list above, and let v be the vertex at the end of e. There are two places that could come at v, namely P 1 = (R 1 (2, x, y), Y, R) and P 2 = (R 1 (2, x, y), x, G). For P 2 , the step consists of e, and it is easily checked that δ G (v) ≥ 4 and hence v gives curvature at most −1/4 to f 1 . Since 1/4 > 3/14, such a step gives less than its proportionate contribution to f 1 , by a factor of 7/6. The same is true for P 1 , except when δ(v) = 3 and δ G (v) = 2.
Similar considerations apply to consolidated edges labelled yx, as in item 6 of the list above, so there are just two types of steps that give more than their proportionate contribution to f 1 , namely those consisting of a consolidated edge labelled xyx or yx together with a red edge, with the property that the vertex in the middle of the step has total valency 3. These steps have lengths 4 and 3, respectively, and have curvature −1/6.
Let us call these consolidated edges labelled xyx or yx in these steps bad consolidated edges. Then the other face f 2 incident with a bad consolidated edge is labelled R 3 = (xyxY ) n and, since a bad consolidated edge on R 3 is immediately preceded by a red edge labelled y, there can be at most n bad consolidated edges on ∂(f 2 ). (Note that the bad consolidated edges of f 2 could also be incident with faces labelled R 2 = (xY ) n , but the same restrictions apply.) Now suppose that n ≥ 19. Then, since the steps have length at most 4 and the step curvature is at most −1/6, a non-boundary face f 2 labelled R 3 satisfies κ(f 2 ) ≤ 1 − n/6. For such faces, we can now apply Step 5 of RSym + , as follows. Fix some small ε > 0. Then f 2 donates curvature −1/6 + (1 + ε)/n across each of its bad consolidated edges. Since there at most n of these, it still has curvature at most −ε after making these donations.
A face f 1 labelled R 1 (corresponding considerations apply to faces labelled R 2 ) that is at dual distance at least 3 from ∂(Γ) receives at most −1/6 + (1 + ε)/19 curvature across each bad consolidated edge in Step 5 of RSym + . If f 1 has d bad consolidated edges, then 2d ≤ m, so the curvature of f 1 before and after Step 5 is at most It can be checked that this is negative for all m ≥ 7 and d ≤ m/2, with ε close to 0. The proof in the case n ≥ 4 and m ≥ 25 is analogous, and is omitted.
To deduce hyperbolicity of G, we apply Theorem 6.11(i) when RSym succeeds at level 1. To apply Theorem 6.11(iii) in the cases when RSym succeeds only at level 2, we need to know that neither x nor y is trivial in G. We could verify that in each of the individual cases by describing a finite homomorphic image of G in which the images of x and y are nontrivial, but it is quicker just to observe that if either x or y were trivial in G then G would be finite of order at most 3 and hence hyperbolic. It seems possible that by working a little harder we could slightly improve the above result to include more pairs (m, n), but we have not done this, because we can use the KBMAG package to test hyperbolicity in individual cases. By doing that, and combining it with the result of Theorem 9.6, we obtain Theorem 9.7. Let G = x, y | x 2 , y 3 , (xy) m , (xyxy −1 ) n . Then G is infinite hyperbolic whenever any of the following conditions hold.
In the cases (m, n) = (7, 12), (8,7), (9,6), (10,5) and (14,4), the group G is automatic and infinite. In each of these examples, by using straightforward searches through the elements of G of bounded length, we were able to find a pair g, h of commuting elements that project onto a free abelian group of rank 2 in an abelian quotient of a suitably chosen subgroup of finite index in G. So these group all contain free abelian subgroups of rank 2, and hence they are not hyperbolic.
These groups are finite for some smaller values of m and n. The final case to be settled was (m, n) = (13, 4), which was proved finite by coset enumeration. In the cases (m, n) = (7, 10), (7,11), (8,6) and (12,4), G has been proved to be infinite, and we conjecture that it is not automatic, and hence also not hyperbolic, but we are unable to prove this. See [6] for details and further references on the finiteness question.

Implementation
We have implemented RSymVerify, for the case where I(R) = R for all R ∈ R, in the computer algebra systems GAP and MAGMA, as IsHyperbolic. It is in the released version of MAGMA, and in the deposited GAP package Walrus. The two implementations are moderately different in their details, so we have used each of them as a test of correctness of the other. We have provided methods to produce a pregroup whose universal group is a given free product of free and finite groups. The user is then able to add any additional relators. We have also implemented VerifySolver + and RSymSolve + in MAGMA, with the same restrictions on interleaving.
In this section we describe some run times, using the MAGMA version. The experiments were run on a MacBook Pro laptop with a 3.1GHz processor, and all set ε = 1/10. We have not compared timings with the KBMAG package, as with the exception of the very smallest presentations it is not possible to run KBMAG on any our our instances.
We first ran IsHyperbolic on presentations of the form x, y | x 2 , y m , (xy) n , constructed as a quotient of the free product C 2 * C m , for 3 ≤ m ≤ 6 and n ∈ {5, 10, 15}. As expected, it succeeded for all (m, n) = (3, 5). The time taken was not noticeably dependent on m or n and was less than 0.01 seconds for each trial.
We then tested presentations of the form x, y | x 2 , y 3 , (xy) m , [x, y] n , again constructed as a quotient of C 2 * C 3 , for 10 ≤ m ≤ 20 and 6 ≤ n ≤ 15. IsHyperbolic failed for m ≤ 12 or n = 6, and otherwise succeeded on all trials. Again, the time taken was not noticeably dependent on m or n and was less than 0.01 seconds for each trial.
We have also run experiments with randomly chosen relators, and the results appear in Table 3. For each, we take the average time for 20 sets of random relators with the given parameters. After each run time we give the number of times IsHyperbolic successfully proved that the group was hyperbolic, with ε = 1/10.
For random quotients of free groups we choose random, freely cyclically reduced words of the given length as additional relators. For random quotients of free products of two groups we choose random nontrivial group elements alternating between the two factors. For random quotients of three finite groups, we choose a factor at random (other than the previous factor) and then a random nontrivial element from that factor. For free products with a nontrivial free factor we allow the free factor to be chosen twice in a row, but not then to choose the inverse of the previously-chosen letter.
Let F be a free group of rank n, and consider the quotient of F by r random, freely cyclically reduced relators of length 3. There are 2m(4m 2 − 6m + 3) ∼ (2m) 3 such words of length 3 over {a ±1 1 , . . . , a ±1 m }, so define the density d ∈ (0, 1) of the presentation by r = (2m) 3d .Żuk showed in [20] that if d < 1/2 then the probability that P defines an infinite hyperbolic group tends to 1 as m → ∞, whilst if d > 1/2 then the probability that P defines the trivial group tends to 1 as m → ∞. These asymptotic results tell us what to expect when we choose r random cyclically reduced relators of length 3 in the cases when r/n is either very small or very large, and it seemed interesting to study the case when n → ∞ with r/n constant. We used our MAGMA implementation of IsHyperbolic to investigate this situation experimentally, and also attempted to analyse it theoretically Provided that we enforce our condition that there are no pieces of length 2 in the presentation, the most common cause of failure of RSym for moderate values of r/n is   (4) 7.60 (19) 38.36 (20) m = 3 n = 12 20 30 26.58 (19) 98.67 (20) 302.00 (20) m = 5 n = 15 25 35 184.92 (19) 638.24 (20) 1575.63 (20) the possible existence of an internal vertex of valency 3 in a van Kampen diagram. A simple calculation, of which we omit the details, shows that the expected number of triples {a, b, c} of distinct elements of X which could label the edges incident with such a vertex tends to λ := 9(r/n) 3 /2 as n → ∞. Assuming that the number of such vertices forms a Poisson distribution, this would imply that the probability of there being no such triples would tend to exp(−λ). This estimate agrees surprisingly well with our experiments with RSym. When r/n = 1/2, for example, we have exp(−λ) ≃ 0.570 and, the proportion of successes over 1000 runs of our implementation with n = 100, 500 and 1000, were 0.510, 0.577, and 0.569.
If d > 1/3, then the probability that two relators share a subword of length 2, and hence that our "preprocessing step" simplifies the presentation, tends to 1, and renders the presentation non-random. It is therefore unclear to us how to complete the analysis.