Maude-help mailing list

[Paco Durán <duran AT lcc.uma.es>]

Operators with the nonexec attribute are ignored for rewriting 
(https://urldefense.com/v3/__http://maude.lcc.uma.es/maude31-manual-html/maude-manualch4.html*x19-590004.5.3__;Iw!!DZ3fjg!taNfjmIqt_LJqF8OZZ9TPSNJuTtpL2C83jY5mcnBFP3NzB6MgH9oZqcGEo4l5XsCkH-g6jLpB47j$
 ). You can use the attribute, but it wouldn't have the behavior I think you 
expect. And if you leave the eq without the attribute you clearly get into a 
non-terminating spec. 

Best,

Francisco



> On 12 Jun 2021, at 14:45, Petar 
> <paradzik42 AT gmail.com>
>  wrote:
> 
> Dear All,
> 
> I understand that Maude considers attributes like [comm] and [assoc] when
> doing rewriting modulo an equational theory. Is it possible to do a rewrite
> modulo equation with [nonexec] attribute? For example, I would like to do a
> rewrite modulo "eq exp(exp(g:Msg,x:Msg), y:Msg) = 
> exp(exp(g:Msg,y:Msg),x:Msg)
> [nonexec] ." (commutative exponents).
> 
> Thanks!
> 
> Regards,
> Petar