Re: [isabelle] need help

I am afraid there is no automation for reasoning involving "mod p" where p is not a numeral.


kuecuek at wrote:

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 variables then i can not proof it.

the equations below are given
y1 ^2 = x1 ^3 + a*x1 + b
y2 ^2 = x2 ^ 3 + a*x2 + b

x3 =  ((((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 + b

if you put the definitionof y3 and x3 in last equation you would see how complex it is :(

can anybody give a trick to proof something like that?

thanks a lot

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.