Here the Natural numbers have a more familiar look (the basic Maude modules prelude.maude has been loaded, that can be done with the command "in prelude", or 1 can be replaced by s(0) and 2 by s(s(0)) if you don't want to load the default Maude-modules), naturally Maude has built-in support for ordinary structures like integers and floats and so on. The natural numbers are still members of the built-in sort Nat. We state that we want to search for a transition using one rewrite rule (=>1), which rewrites the first term into the other. The result of the investigation is not shocking but still, sometimes proving the obvious is all we can do. If we let Maude use more than one step we should see a different result: