Adian–Rabin theorem

No Markov property of finitely presented groups is decidable by an algorithm taking an arbitrary finite group presentation as input. The proof reduces the word problem for a group to property recognition using an effective construction which collapses when an input word is trivial and embeds the input group when it is nontrivial.

In the effective group form used for recognition problems, a finite group presentation of $K$ and a word $w$ yield, by an algorithm, a finite presentation of a group $K_w$. If $w=1$ in $K$, then $K_w$ is trivial; if $w\ne 1$ in $K$, then the specified generators embed $K$ in $K_w$. One can additionally arrange that the normal closure of the image of $w$ is all of $K_w$. The finite presentation can be written without first deciding which case holds. This is the collapse-versus-embedding construction behind the Adian–Rabin theorem.