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

*To*: pvs-help@csl.sri.com*Subject*: infix-problem*From*: "Thomas J. Fuchs" <thomas.fuchs@kuk-marine.at>*Date*: Sat, 6 Jan 2001 20:18:08 +0100*Importance*: Normal

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

- Prev by Date:
**problems with writing strategies for PVS** - Next by Date:
**Re: infix-problem** - Prev by thread:
**Defining help functions for strategies** - Next by thread:
**Re: infix-problem** - Index(es):