Introduce stable letters for and for , using and to implement the maps. Thus is the multiple HNN extension of with the finite presentation
Here each family ranges over its finite instruction set. The enlarged subgroup denoted by is
The prime means this enlarged subgroup, not the commutator subgroup or the unrestricted normal closure of .
The key relationship is
Here is a justification that also identifies the relevant intersection. Set
The basis calculation in the preceding part shows that intersections of with associated subgroups are generated by exactly the halting basis elements whose indices satisfy the appropriate congruences. Since the machine is deterministic and is terminal, halting at is equivalent for the two ends of every instruction edge. Therefore and map these intersections onto the corresponding intersections in their targets. The same assertion holds on the integer lattices after declaring pairs with a negative coordinate nonhalting: the bounds on imply that each coordinate's sign is preserved by a transition and its inverse.
Apply Britton's lemma to a word in which represents an element of . If it has stable letters, it must have a pinch. The base coefficient of that pinch lies in and an associated subgroup, and the intersection property just proved makes its transported image lie in again. Successive pinch removals therefore keep all base coefficients in , and eventually remove every stable letter. It follows that
Finally, belongs to , so . In the opposite direction, induction backwards along any computation ending at shows that every halting basis element lies in : if for the next configuration is in , then the transition identity expresses as or . Thus and
Because is generated by a subset of a free basis of a group of , a single basis element belongs to it exactly when is a halting index. This proves the boxed relationship.

Articles by others on the same topic (0)

There are currently no matching articles.