Maude-help mailing list

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

Hi,

Perhaps you can consider some type of order. If F is a total order with an op 
< you could do:

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

Best,

Francisco

> On 26 Oct 2019, at 09:02, 
> hcantunc AT gmail.com
>  wrote:
> 
> 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.

Attachment: smime.p7s
Description: S/MIME cryptographic signature