For a null loop of length , a horizontal row of its combing diagram is encoded by an ordered -tuple of rung words of length at most . If there are such words, there are at most row types. Between two identical labelled rows one can delete the entire intervening annular band and glue the equal boundary paths. Repeating this leaves at most layers of bounded-perimeter cells. Thus a synchronous combable group has a recursive exponential isoperimetric bound. This does not require the combing language to be regular or computable.
First construct the bounded-difference automaton. Fix as above, enlarging it if necessary. Its states are the finitely many elements , together with a reject state and finite flags recording when padding has started on each tape. The initial state is . Read the pair of words synchronously, padding their ends with a symbol representing the identity. If the current prefixes represent , the difference state is . A letter pair updates it by
Reject if the new difference lies outside ; padding must occur only in the final suffix of a tape. The accepting state for the generator is . Induction on the prefix length proves that the machine accepts exactly the padded pairs whose prefix differences stay bounded by and whose final difference is . In particular it correctly recognizes multiplication by for any pair of the chosen combing representatives with adjacent endpoints. Taking accepting state gives the equality machine.
If the combing formal language is regular, take the product with its two word acceptors. These are the usual group multiplier automata, accepting exactly with . From a known representative , a finite-state automaton search with its first tape fixed finds a representative of : existence is guaranteed, so the breadth-first search terminates. Equality is tested by the identity multiplier. Starting with a representative of , repeat these operations over the generators, identifying equal vertices, to build any prescribed finite-radius region of the Cayley graph and all its generator-labelled edges. Iterating multiplication over an input word and testing equality with the identity gives a word problem algorithm.
A bare geometric combing does not imply that is a regular language. Nor can a finite-state automaton recognize the indicated endpoint relation on all words without any restriction: in , which has its usual geodesic synchronous combing, fixing the second word to would make the multiplier for recognize precisely the first words equal to the identity. Intersecting those words with gives , a nonregular language: pumping the initial block changes its exponent without changing the inverse block, contradicting acceptance of precisely the equal exponents. Thus the literal unrestricted-pair request is false; the machines above recognize bounded fellow-travelling pairs, or full representative-pair relations under the additional automatic-language hypothesis.
Nevertheless the final decidability assertion is true for a synchronous combable group, without a regular-language assumption. Here is a terminating filling bound, avoiding any assumption that the given combing is computable. Let be the number of words of length at most over . A horizontal row of the diagram in part (ii) is encoded by its ordered rung words, so there are at most possible row types. If two rows have the same word tuple, delete the band between them and identify corresponding labelled rungs. This preserves the outside boundary and leaves a valid diagram of the same short relators. Equivalently, the first column is always at , so identical rung tuples describe the same vertex configuration. Repeatedly remove such bands. At most distinct rows remain, with at most short-relator cells per layer.
This finite-state row shortening of a combing diagram gives the recursive bound . For the given finite group presentation, every short identity in the finite set has some fixed diagram over its defining relators. Let bound their areas. Replacing each short face by its fixed diagram gives
Part 3(ii) now supplies a terminating word decider. This also constructs finite Cayley graph regions for a nonregular combing: enumerate words of bounded length, use the decider on to identify vertices, and use it on to determine the generator edges. The finite ball and transition table of the bounded-difference machines can consequently be computed. The constants depend on a fixed combing and are not a uniform procedure certifying combability of an arbitrary input group presentation. Every finite group presentation of this synchronous combable group has solvable word problem, by the presentation-invariance proof in Q3.
Work with a finite symmetric alphabet . If , its path starts at , visits at integer time , travels at unit speed along the intervening generator edges, and stays at its endpoint for .
Two such paths synchronously -fellow travel if
An asynchronous version permits increasing time reparametrizations. Checking all integer times suffices after a bounded enlargement of for the edge interiors.
A combing of a group chooses a representative word for every , with empty. A synchronous combing has a uniform constant such that representatives with adjacent endpoints satisfy the synchronous fellow-traveller property. A group admitting this is a synchronous combable group. The formal language need not be regular or computable. A regular language of representatives satisfying the synchronous condition instead gives an automatic group. This distinction is relevant to the finite-state automata request in part (iii); the present argument uses the synchronous meaning throughout. The definitions and distinction are also made explicitly in Combings of Groups and the Grammar of Reparameterization, Section 1.