## 0 Replies - 889 Views - Last Post: 30 November 2015 - 09:23 AM

### #1 tease_bees Posted 30 November 2015 - 09:23 AM

The following code is on CafeOBJ
```mod* MONOID {
[ Elt ]
op e : -> Elt
op _*_ : Elt Elt -> Elt  { assoc id: e}
}

open  MONOID .
ops a b c : -> Elt .

```

At this stage assoicativity is held and everything is clear:

%MONOID> red (c * a) * b = c * (a * B ) .
_-- reduce in %MONOID : (((c * a) * B ) = (c * (a * B ))):Bool
(true):Bool
(0.0000 sec for parse, 0.0000 sec for 1 rewrites + 9 matches)

```eq [e1] : c * a = e .
eq [e2] : a * b = e .

```

When this equations are added I get the following:

%MONOID> red (c * a) * b = c * (a * B ) .
-- reduce in %MONOID : (((c * a) * B ) = (c * (a * B ))):Bool
(b = c):Bool
(0.0000 sec for parse, 0.0000 sec for 4 rewrites + 27 matches)

Looks like associativity is not held, no matter it is operator property... why this happens?

b == c is what I need to proove (which mathematically follows from given equations eq1,eq2 + associativity), but a far as I undersand the interperter tells me the opposite!..

damn! />/> is
```B)/>/>/>
```

This post has been edited by modi123_1: 30 November 2015 - 09:25 AM
Reason for edit:: fixed the B ) for you.

Is This A Good Question/Topic? 0

Page 1 of 1

 .related ul { list-style-type: circle; font-size: 12px; font-weight: bold; } .related li { margin-bottom: 5px; background-position: left 7px !important; margin-left: -35px; } .related h2 { font-size: 18px; font-weight: bold; } .related a { color: blue; }