 Semidecision of nonidentity in simple subgroups

Let $S$ be a nontrivial simple group inside a finitely presented group $P$, and fix $a\ne 1$ in $S$. For an input word $w$ in $S$, enumerate products of conjugates in $P$ of $w^{\pm 1}$ and proofs in $P$ that such a product equals $a$. This search terminates exactly when $w\ne 1$: 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.