// file to verify in SINGULAR (http://www.singular.uni-kl.de)
// computation in Example 1.8, Theorem 1.17 and Appendix
// C. Hillar L.H. Lim, Most tensor problems are NP-hard
//

ring r = 0,(a_1,a_2,a_3,b_1,b_2,b_3,c_1,c_2,c_3,d_1,d_2,d_3),dp;

poly F1 = a_1*a_2*a_3+c_1*c_2*c_3-2; 
poly F2 = a_1*a_3*b_2+c_1*c_3*d_2; 
poly F3 = a_2*a_3*b_1+c_2*c_3*d_1; 
poly F4 = a_3*b_1*b_2+c_3*d_1*d_2+4; 
poly F5 = a_1*a_2*b_3+c_1*c_2*d_3; 
poly F6 = a_1*b_2*b_3+c_1*d_2*d_3+4; 
poly F7 = a_2*b_1*b_3+c_2*d_1*d_3-4; 
poly F8 = b_1*b_2*b_3+d_1*d_2*d_3;

ideal I = F1,F2,F3,F4,F5,F6,F7,F8;

std(I);

poly g = 2*c_2^2 - d_2^2;
poly h = c_1*d_2*d_3 + 2;

lift(I,g);
lift(I,h);

// we will now show how to express g = 2*c_2^2 - d_2^2 and 
// h = c_1*d_2*d_3 + 2  as a polynomial linear combination of 
// polynomials in F.  Thus g,h are consequences of F.

poly G1 = -1/8*b_1*b_2*b_3*c_2*d_2+1/8*a_2*b_1*b_3*d_2^2;
poly G2 = 1/8*b_1*b_2*b_3*c_2^2-1/8*a_2*b_1*b_3*c_2*d_2;
poly G3 = -1/2*c_2*d_2;
poly G4 = 1/2*c_2^2;
poly G5 = 1/8*a_3*b_1*b_2*c_2*d_2-1/8*a_2*a_3*b_1*d_2^2;
poly G6 = -1/8*a_3*b_1*b_2*c_2^2+1/8*a_2*a_3*b_1*c_2*d_2;
poly G7 = 1/4*d_2^2;
poly G8 = -1/4*c_2*d_2;

// should show up as 2*c_2^2 - d_2^2
F1*G1 + F2*G2 + F3*G3 + F4*G4 + F5*G5 + F6*G6 + F7*G7 + F8*G8;

poly H1 = 0; 
poly H2 = (1/32)*b_1*b_2*b_3*c_2*d_1*d_3-(1/32)*a_2*b_1*b_3*d_1*d_2*d_3; 
poly H3 = -(1/32)*b_1*b_2*b_3*c_1*d_2*d_3+(1/32)*a_1*b_2*b_3*d_1*d_2*d_3; 
poly H4 = -(1/32)*a_1*b_2*b_3*c_2*d_1*d_3+(1/32)*a_2*b_1*b_3*c_1*d_2*d_3; 
poly H5 = -(1/8)*b_1*b_2*b_3; 
poly H6 = 1/2; 
poly H7 = (1/8)*a_1*b_2*b_3-(1/8)*c_1*d_2*d_3; 
poly H8 = (1/8)*c_1*c_2*d_3;

// should show up as h = c_1*d_2*d_3 + 2
F1*H1 + F2*H2 + F3*H3 + F4*H4 + F5*H5 + F6*H6 + F7*H7 + F8*H8;