[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

infix-problem



Dear PVS-Experts!

We have to solve the following problem:

* ...... binary operation
e ...... neutral element
x,y,z .. arbitrary element

x * e = x
e * x = x
x * x = e
x * ( y * z ) = ( x * y ) = z

We have to prove:  x * y = y * x

We tried to convert the probelm into PVS: 
_______________________________________

bsp: THEORY

BEGIN

element: TYPE+

x,y,z: VAR element
a,b,e: element
*: [element,element -> element]

bsp: THEOREM

(FORALL x: x*e=x) AND
(FORALL x: e*x=x) AND
(FORALL x: x*x=e) AND
(FORALL x,y,z: x*(y*z)=(x*y)) AND
(FORALL x,y,z: (x*y)=z)
=> a*b=b*a

END bsp
____________________________________

We started with (skosimp*) which did fine,
but then we used (grind) and ended up in a
dead end.

We would be obliged if anyone could help us.

Thanks again,
		Thomas Fuchs
		Martin Grabner
		Marc Klostermann