Here we tell the Maude system to rewrite our input term according to the rewrite theory, and we tell it to stop after 3 rewrite steps (remember that rewrite rules do not have to be terminating or confluent so an upper bound is not a bad idea), we just want see what sort of state we end up in after randomly choosing 3 matching rules. And as you can see the state this person ends up in might look a bit strange. (When you're married at the age of one you kind of stick out a bit in kindergarten I guess). It also says 4 rewrite steps, although we specifically stated an upper limit of 3 rewrite steps, this is because rewrite steps that are the result of applying equations does not count (they do not change the term, at least if the equations are sane). In this example one of the equations of the NAT module has been used to reduce the term 0 + s(0) to s(0), which accounts for the 4'th rewrite step.