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 length^{4}. The coset table gives rise to a convergent prefix string rewriting system as follows: To each coset w, each and the respective coset w_{a} corresponding to , associate a rule^{5} 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 [3], page 71:
a | b | a^{-1} | b^{-1} | |
b | b^{-1} | |||
b | b^{-1} | b^{-1} | ba^{-1} | |
b^{-1} | ba^{-1} | b | b | |
ba^{-1} | b | ba^{-1} | b^{-1} | ba^{-1} |
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.