Semidecision of nonidentity in simple subgroups (source code)

= Semidecision of nonidentity in simple subgroups

Let $S$ be a nontrivial <simple group> inside a <finitely presented group> $P$, and fix $a\ne1$ in $S$. For an input word $w$ in $S$, enumerate products of conjugates in $P$ of $w^{\pm1}$ and proofs in $P$ that such a product equals $a$. This search terminates exactly when $w\ne1$: the <normal closure> of a nontrivial element of $S$ is all of $S$, and its conjugators are also elements of $P$, while a null word has only trivial conjugates. Run this search alongside the enumerable proofs that $w=1$. Exactly one search terminates, solving the <word problem for a group> on any specified finitely generated subgroup of $S$. No effective generating set for the possibly infinitely generated $S$ is needed.