Using the two equations in the rewrite theory NAT Maude was able to reduce our term into the desired term, the representation of the number two i.e. the second successor of 0. At that point no other application of the two equations were possible, so Maude halts. Maude rewrites terms according to the equations whenever there is a match between the closed terms that one tries to rewrite (or reduce) and the left hand side of an equation in our equation-set. A match in this context is a substitution of the variables in the left hand side of an equation which leaves it identical to the term that one tries to rewrite/reduce.