mod LIBRARY-PETRI-NET is sorts Place Marking . subsort Place < Marking . op 1 : -> Marking . op __ : Marking Marking -> Marking [assoc comm id: 1] . ops a b n r j : -> Place . rl [buy] : r r r r => j j j j j j j j . rl [file] : j => a . rl [borr] : a => b . rl [ret] : b => a . rl [lose] : b => n . rl [disc] : a => n . rl [req1] : n n => r r . rl [req2] : 1 => r . endm set trace on . *** It's wrong. Rule req2 is not applied as expected. rew 1 . ***( rewrite in LIBRARY-PETRI-NET : 1 . *********** rule rl [req2]: 1 => r . empty substitution 1 ---> r rewrites: 1 in -10ms cpu (0ms real) (~ rewrites/second) result Place: r ) rew [10] r r r r . ***( rewrite in LIBRARY-PETRI-NET : 1 . *********** rule rl [req2]: 1 => r . empty substitution 1 ---> r rewrites: 1 in -10ms cpu (0ms real) (~ rewrites/second) result Place: r Maude> rew [10] r r r r . rewrite [10] in LIBRARY-PETRI-NET : r r r r . *********** rule rl [buy]: r r r r => j j j j j j j j . empty substitution r r r r ---> j j j j j j j j *********** rule rl [file]: j => a . empty substitution j ---> a *********** rule rl [disc]: a => n . empty substitution a ---> n *********** rule rl [file]: j => a . empty substitution j ---> a *********** rule rl [borr]: a => b . empty substitution a ---> b *********** rule rl [ret]: b => a . empty substitution b ---> a *********** rule rl [disc]: a => n . empty substitution a ---> n *********** rule rl [req1]: n n => r r . empty substitution n n j j j j j j ---> j j j j j j r r *********** rule rl [file]: j => a . empty substitution j ---> a *********** rule rl [borr]: a => b . empty substitution a ---> b rewrites: 10 in -10ms cpu (0ms real) (~ rewrites/second) result Marking: b r r j j j j j ) set trace off .