Maude> (rew test1 .)

Rewrite in RBP : test1 . 
Result Configuration :
< a : Node | nbs : nbs ( b , c ) , 
             nbsstates : nbsStates ( nbState( a , b , passive ) , 
                                     nbState( a , c , passive ) ) ,  
             seqNos : seqNos( seqNo ( a , 1 ) , 
                              seqNo ( b , 0 ) ,  
                              seqNo ( c , 0 ) ) ,  
             parents : parent( a , a ) ,			    
             states : states( state( a , passive ) , 
                              state( b , passive ) ,  
                              state( c , passive ) ) >  


< b : Node | nbs : nbs ( a , c ) , 
             nbsstates : nbsStates ( nbstate ( a , a , passive ) ,  
                                     nbstate ( a , c , passive ) ) ,  
             seqNos : seqNos ( seqNo ( a , 1 ) ,  
                               seqNo ( b , 0 ) ,  
                               seqNo ( c , 0 ) ) , 
             parents : parent (a , a ) ,
             states : states ( state ( a , passive ) ,  
                               state ( b , passive ) ,  
                               state ( c , passive ) ) >

< c : Node | nbs : nbs ( a , b ) , 
             nbsstates : nbsStates ( nbstate ( a , a , passive ) ,  
                                     nbstate ( a , b , passive ) ) ,  
             seqNos : seqNos ( seqNo ( a , 1 ) ,  
                               seqNo ( b , 0 ) ,  
                               seqNo ( c , 0 ) ) , 
             parents : parent ( a , a ) , 
             states : states ( state ( a , passive ) ,  
                               state ( b , passive ) ,  
                               state ( c , passive ) ) > 


Maude> (rew test2 .)

Rewrite in RBP : test2 . 
Result Configuration : 
< b : Node | nbs : nbs ( a , c ) , 
             nbsstates : nbsStates ( nbstate ( a , a , passive ) ,  
                                     nbstate ( a , c , passive ) ,  
                                     nbstate ( b , c , passive ) ,  
                                     nbstate ( c , a , passive ) ,  
                                     nbstate ( c , c , passive ) ) ,  
             seqNos : seqNos ( seqNo ( a , 0 ) ,  
                               seqNo ( b , 0 ) ,  
                               seqNo ( c , 0 ) ) ,  
             parents : mtparents ,
             states : states ( state ( a , passive ) ,  
                               state ( b , passive ) ,  
                               state ( c , passive ) ) >
 
< c : Node | nbs : nbs ( a , b ) , 
             nbsstates : nbsStates ( nbstate ( a , a , passive ) ,  
                                     nbstate ( a , b , passive ) ,  
                                     nbstate ( b , a , passive ) ,  
                                     nbstate ( b , b , passive ) , 
                                     nbState ( c , b , passive ) ) ,
             seqNos : seqNos ( seqNo ( a , 0 ) ,  
                               seqNo ( b , 0 ) ,
                               seqNo ( c , 0 ) ) ,  
	     parents : mtparents , 
             states : states ( state ( a , passive ) , 
                               state ( b , passive ) ,  
                               state ( c , passive ) ) > 



Maude> (rew test3 .)

Rewrite in RBP : test3 . 
Result Configuration : 
< a : Node | nbs : mtnbs , 
             nbsstates : mtnbsStates ,  
             seqNos : seqNos ( seqNo ( a , 0 ) ,  
                               seqNo ( b , 0 ) ) ,   
             parents : mtparents ,
             states : states ( state ( a , passive ) ,  
                               state ( b , passive ) ) > 

< b : Node | nbs : c , 
             nbsstates : nbsStates ( nbstate ( a , c , passive ) ,  
                                     nbstate ( b , c , passive ) ,
                                     nbstate ( c , c , passive ) ) ,  
             seqNos : seqNos ( seqNo ( a , 0 ) ,  
                               seqNo ( b , 0 ) ,  
                               seqNo ( c , 0 ) ) , 
             parents : mtparents , 
             states : states ( state ( a , passive ) ,  
                               state ( b , passive ) ,  
                               state ( c , passive ) ) >

 <c : Node | nbs : b , 
             nbsstates : nbsStates ( nbstate ( b , b , passive ) ,  
                                     nbstate ( c , b , passive ) ) , 
             seqNos : seqNos ( seqNo ( b , 0 ) ,  
                               seqNo ( c , 0 ) ) ,
             parents : mtparents ,  
             states : states ( state ( b , passive ) , 
                               state ( c , passive ) ) >