Re: [isabelle] need help
I am afraid there is no automation for reasoning involving "mod p" where
p is not a numeral.
kuecuek at rbg.informatik.tu-darmstadt.de 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