// This is the correct way to
// design and verify a 2-bit GF multiplier
// over the finite field F_4
ring r = (2, X), 
(A, B, Z, Z_1,a_0, a_1, b_0, b_1, s_0, s_1, s_2, s_3, r_0, z_0, z_1,
t), 
lp; 

// degree-2 irreducible poly
minpoly = X2+X+1;

ideal J = 
A+a_0 + a_1*X,
B + b_0 + b_1*X,
Z + z_0 + z_1*X,
s_0 + a_0*b_0, //AND gate
s_1 + a_0*b_1, //AND gate
// BUG: s_1 + a_0 +b_1,
// AND gate replaced by XOR
s_2 + a_1*b_0, //AND gate
s_3 + a_1*b_1, //AND gate
r_0 + s_1 + s_2, //XOR gate
z_0 + s_0 + s_3, //XOR
z_1 + r_0 + s_3, // XOR

//Spec poly
Z_1 - A*B,

//miter
t*(Z - Z_1)-1;



ideal J0 =
A^4 - A,
B^4 - B,
Z^4 - Z,
Z_1^4 - Z_1,
t^4 - t,
a_0^2 - a_0,
a_1^2 - a_1,
b_0^2 - b_0,
b_1^2 - b_1,
s_0^2 - s_0,
s_1^2 - s_1,
s_2^2 - s_2,
s_3^2 - s_3,
r_0^2 - r_0,
z_0^2 - z_0,
z_1^2 - z_1;


groebner(J+J0);