Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

On Wednesday 01 February 2006 07:42, Marc Boyer wrote:
> 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...

The second seach fails because the target pattern

x comp ( y /\ z ) 

is not reduced wrt the equational part of your specification.

Steven