Maude-help mailing list

[Roberto Bruttomesso <roberto.bruttomesso AT gmail.com>]

Hello,

I'm trying to use the nice CRC tool of maude to check one
specification of mine. The problem is that I need to express
conditional statements, like

rd( wr( x, i, e ), j ) = rd( x, j )             if i > j .

however I cannot define i, j to be Nat and use the predefined _>_
operator. So I tried to define it myself using a successor function
and so on. However
I cannot specify that the relation is transitive, and I get a critical pair

The following critical pairs cannot be joined:
  ccp for 8 and 6a
    rd(wr(wr(#1:ARRAY,I:INDEX,E:ELEM),#2:INDEX,#3:ELEM),J:INDEX)
    = rd(wr(#1:ARRAY,#2:INDEX,#3:ELEM),J:INDEX)
    if I:INDEX > J:INDEX = true /\ #2:INDEX > I:INDEX = true .

which could actually be joined since I > J and #2 > I implies #2 > J,
and a rule more would be triggered.

Defining something like

ceq N > M if N > L and L > M .

does not seem to help.

Is there a way around ?

Thanks in advance !

Roberto

-- 
Roberto Bruttomesso, PhD - http://tinyurl.com/r0b3r70