Maude-help mailing list

[Marc Boyer <Marc.Boyer AT enseeiht.fr>]

Dear all,

here is a (very simplified version of) my problem.
A 'high level' equation hides a rule...

Let be the following module:
-------------------------------------------
mod BUG-CONV is
  sort S .
  op _ /\ _ : S S -> S .
  op _ comp _ : S S -> S .
  op _ conv _ : S S -> S .

  vars f g h : S .

  eq [compMin] : f comp ( g /\ h ) = ( f comp g ) /\ ( f comp h ) .
  rl [conv2min] : f conv g => f /\ g .

  ops x y z : -> S [ctor] .
endm
-------------------------------------------

This search is successfull
   search y conv z =>* y /\ z .
but this one is not
   search x comp ( y conv z ) =>* x comp ( y /\ z ) .

More strange (to me), if I hide (or set nonexec) the
equation [compMin], then, both search are successfull...

Any explanation ?

Regards,
  Marc
--
Marc Boyer     INPT - ENSEEIHT - Networks and Telecommunications Dep.
Assistant Professor                                          IRIT-IRT
Tel: 33  5.61.58.80.21                                2, rue Camichel
http://www.enseeiht.fr/~boyer/      31071 TOULOUSE Cedex 7  -- FRANCE