Lines Matching refs:a3
478 a3 : 'a;
502 let a3 = e.a3 in
504 a1 * a3 + & 2 * a4`;
513 let a3 = e.a3 in
515 a3 ** 2 + & 4 * a6`;
527 let a3 = e.a3 in
530 a1 ** 2 * a6 + & 4 * a2 * a6 - a1 * a3 * a4 + a2 * a3 ** 2 - a4 ** 2`;
554 e.a3 IN e.field.carrier /\
567 let a3 = e.a3 in
573 (y ** 2 * z + a1 * x * y * z + a3 * y * z ** 2 =
594 let a3 = e.a3 in
598 let y = ~y1 - a1 * x1 - a3 in
613 let a3 = e.a3 in
618 let d = & 2 * y1 + a1 * x1 + a3 in
622 let m = (~(x1 ** 3) + a4 * x1 + & 2 * a6 - a3 * y1) / d in
624 let y = ~(l + a1) * x - m - a3 in
641 let a3 = e.a3 in
654 let y = ~(l + a1) * x - m - a3 in
694 ``!e :: Curve. e.a3 IN e.field.carrier``,
834 let a3 = e.a3 in
837 (y2 = y1) \/ (y2 = ~(y1 + a1 * x1 + a3))``,
922 let a3 = e.a3 in
924 let y = ~(y1 + a1 * x1 + a3 * z1) in
992 let a3 = e.a3 in
995 y ** 2 + a1 * x * y + a3 * y =
1057 (field_mult e.field e.a3 y)