*To*: kuecuek at rbg.informatik.tu-darmstadt.de*Subject*: Re: [isabelle] need help*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 07 Dec 2006 09:39:14 +0100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <200612061755.33852.kuecuek@rbg.informatik.tu-darmstadt.de>*References*: <200612061755.33852.kuecuek@rbg.informatik.tu-darmstadt.de>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

Tobias kuecuek at rbg.informatik.tu-darmstadt.de wrote:

hallo, i try to solve an equation but it is realy complex can anybody help me?if i try with numbers then i can show it with "auto" but if i use variablesthen i can not proof it.the equations below are giveny1 ^2 = x1 ^3 + a*x1 + b y2 ^2 = x2 ^ 3 + a*x2 + bandx3 = ((((y1 - y2) * ((x1 - x2) ^ nat (p -2 ))) mod p) ^ 2 - x1 - x2) mod p y3 = ((((y1 - y2) * ((x1 - x2) ^ nat (p -2 ))) mod p) * (x1 - x3) - y1) mod p and i must to show that y3^2 = x3^3 + a*x3 + bif you put the definitionof y3 and x3 in last equation you would see howcomplex it is :(can anybody give a trick to proof something like that? thanks a lot

**References**:**[isabelle] need help***From:*kuecuek

- Previous by Date: [isabelle] need help
- Next by Date: Re: [isabelle] BUG: poly-ml dumps core (polyml 4.1.4, Isabelle2005, AWE 0.4)
- Previous by Thread: [isabelle] need help
- Next by Thread: Re: [isabelle] need help
- Cl-isabelle-users December 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list