in basic-nat.maude fmod NAT3 is including BASIC-NAT . var N : Nat . eq s(s(s(N))) = 0 . endfm red s(s(s(0))) + s(s(0)) . ***( reduce in NAT3 : s(s(s(0))) + s(s(0)) . rewrites: 2 in -10ms cpu (0ms real) (~ rewrites/second) result Nat: s(s(0)) ) red s(s(s(0))) + s(s(0)) + s(s(s(0)) + s(0)) . ***( WARNING: , line 492: Ambiguous term, two parses are: s(s(s(0))) + (s(s(0)) + s(s(s(0)) + s(0))) -versus- (s(s(s(0))) + s(s(0))) + s(s(s(0)) + s(0)) Arbitrarily taking the first as correct. reduce in NAT3 : s(s(s(0))) + (s(s(0)) + s(s(s(0)) + s(0))) . rewrites: 10 in -10ms cpu (0ms real) (~ rewrites/second) result Nat: 0 *** no gathering pattern for _+_, parentheses required *** ) red (s(s(s(0))) + s(s(0))) + s(s(s(0)) + s(0)) . ***( reduce in NAT3 : (s(s(s(0))) + s(s(0))) + s(s(s(0)) + s(0)) . rewrites: 10 in -10ms cpu (0ms real) (~ rewrites/second) result Nat: 0 )