Now given a subgroup of generated by a set the index of in is the same as the index of the subgroup generated by in . While it is undecidable whether a subgroup has finite index in a group, TC attempts to verify whether the index is finite.
In the following we will always assume that the group and the subgroup are finitely presented respectively generated, i.e. the sets , R and S are finite. Detailed descriptions of TC procedures can be found e. g. in [11,3,15]. We only list some of the properties and their interpretations here: If the index of in is finite the procedure halts and produces a set of coset representatives and a coset table with entries for each coset c and each . The (unique) coset representative for any word in can be computed by tracing it through the coset table starting with . Moreover, given a total well-founded ordering > on which is additionally compatible with right concatenation, we can associate to each coset c the representative of minimal length4. The coset table gives rise to a convergent prefix string rewriting system as follows: To each coset w, each and the respective coset wa corresponding to , associate a rule5 of the form . This prefix string rewriting system then can be used to determine the coset of a word in by prefix reduction.
Let us illustrate these findings with an example from , page 71:
The coset representative of the word aba can be deduced by either tracing the coset table: , and , or by prefix reduction: In both cases we find that aba lies in the coset represented by b-1 which is in fact the minimal representative of this coset with respect to the chosen ordering.