Editing Word problem for groups (section)

===Example===
The following will be proved as an example of the use of this technique:

:: '''Theorem:''' A finitely presented residually finite group has solvable word problem.

''Proof:'' Suppose <math>G = \langle X \, | \, R \rangle</math> is a finitely presented, residually finite group.

Let <math>S</math> be the group of all permutations of the natural numbers <math>\mathbb{N}</math> that fixes all but finitely many numbers. Then:
# <math>S</math> is [[locally finite group|locally finite]] and contains a copy of every finite group.
# The word problem in <math>S</math> is solvable by calculating products of permutations.
# There is a recursive enumeration of all mappings of the finite set <math>X</math> into <math>S</math>.
# Since <math>G</math> is residually finite, if <math>w</math> is a word in the generators <math>X</math> of <math>G</math> then <math>w \neq 1</math> in <math>G</math> if and only if some mapping of <math>X</math> into <math>S</math> induces a homomorphism such that <math>w \neq 1</math> in <math>S</math>.

Given these facts, the algorithm defined by the following pseudocode:

 '''For''' every mapping of X into S
     '''If''' every relator in R is satisfied in S
         '''If''' w ≠ 1 in S
             '''return''' 0
         '''End if'''
     '''End if'''
 '''End for'''

defines a recursive function <math>h</math> such that:

::<math>h(x) = 
\begin{cases} 
0 &\text{if}\ x\neq 1\ \text{in}\ G \\
\text{undefined/does not halt}\ &\text{if}\ x=1\ \text{in}\ G
\end{cases} </math>

This shows that <math>G</math> has solvable word problem.