Maude-help mailing list

[<hcantunc AT gmail.com>]

Hello,

I am wondering if there's a way to define commutativity as an ordinary
equation.
I am trying to define the conditional commutativity as shown below. I do not
think it's possible to use the 'comm' attribute in this case but I couldn't
figure out a way to define it as an ordinary equation without causing non-
termination.


sorts P F N Z .

op one : -> Z [ctor] .
op _(_<--_) : P F N -> Z [ctor prec 40] .
op _._ : Z Z -> Z [ctor assoc id: one prec 41] .

var P1 P2 : P .
var F1 F2 : F .
var N1 N2 : N .

ceq P1(F1 <-- N1) . P1(F2 <-- N2) = P1(F2 <-- N2) . P1(F1 <-- N1) if F1 =/=
F2 .



Thank you.