(*
	*** COMPUTATIONS USED IN MY 2007 PAPER - M. Q. RIECK *** 
*)

(* Overhead / Support Tools - Activate all of this *)

cSubs = {              (* System (1) solved for c's *) 
c1 -> (r2^2 + r3^2 - D1) / (2r2 r3),
c2 -> (r3^2 + r1^2 - D2) / (2r3 r1),
c3 -> (r1^2 + r2^2 - D3) / (2r1 r2)
};

r2RSubs = {          (*  R1 = r1^2, etc.  *)
r1 -> Sqrt[R1],
r2 -> Sqrt[R2], 
r3 -> Sqrt[R3] 
};

RSubs = {               (*  R1 = r1^2, etc.  *)
R1-> (x-x1)^2 + (y-y1)^2 + Z, 
R2-> (x-x2)^2 + (y-y2)^2 + Z, 
R3-> (x-x3)^2 + (y-y3)^2 + Z
};

DSubs = {              (*  D1 = d1^2, etc.  *)
D1-> (x2-x3)^2 + (y2-y3)^2,
D2-> (x3-x1)^2 + (y3-y1)^2,
D3-> (x1-x2)^2 + (y1-y2)^2
};

DRSubs = { 
D1 -> Expand[D1 /. DSubs],
D2 -> Expand[D2 /. DSubs],
D3 -> Expand[D3 /. DSubs],
R1 -> Expand[R1 /. RSubs],
R2 -> Expand[R2 /. RSubs],
R3 -> Expand[R3 /. RSubs]
};

tSubs = {       (*  Weierstrass substitutions  *)
x1-> (1-t1^2)/(1+t1^2), y1-> 2t1/(1+t1^2), 
x2-> (1-t2^2)/(1+t2^2), y2-> 2t2/(1+t2^2), 
x3-> (1-t3^2)/(1+t3^2), y3-> 2t3/(1+t3^2)
} ;
tSubsSp = {x1->((1-(t1^2))/(1+(t1^2))),y1->((2 t1)/(1+(t1^2))),x2->((1-(t2^2))/(1+(t2^2))),y2->((2 t2)/(1+(t2^2))),x3->((1-(t3^2))/(1+(t3^2))),y3->((2 t3)/(1+(t3^2))), 
t1->((t2+t3)/(-1+t2 t3))};     (*  t1 + t2 + t3 = t1 t2 t3 in special coordinate system  *)

untSubs = {
t1->y1/(1+x1),
t2->y2/(1+x2),
t3->y3/(1+x3)
} ;

ySubs = {           (*   x1^2 + y1^2 = 1, etc.  *)
y1^2 -> 1 - x1^2, 
y1^3 -> y1(1 - x1^2), 
y1^4 -> (1 - x1^2)^2, 
y1^5 -> y1(1 - x1^2)^2, 
y1^6 -> (1 - x1^2)^3, 
y1^7 -> y1(1 - x1^2)^3, 
y1^8 -> (1 - x1^2)^4, 
y1^9 -> y1(1 - x1^2)^4, 
y1^10 -> (1 - x1^2)^5, 
y1^11 -> y1(1 - x1^2)^5, 
y1^12 -> (1 - x1^2)^6, 
y1^13 -> y1(1 - x1^2)^6, 
y1^14 -> (1 - x1^2)^7, 
y1^15 -> y1(1 - x1^2)^7, 
y1^16 -> (1 - x1^2)^8, 
y2^2 -> 1 - x2^2, 
y2^3 -> y2(1 - x2^2), 
y2^4 -> (1 - x2^2)^2, 
y2^5 -> y2(1 - x2^2)^2, 
y2^6 -> (1 - x2^2)^3, 
y2^7 -> y2(1 - x2^2)^3, 
y2^8 -> (1 - x2^2)^4, 
y2^9 -> y2(1 - x2^2)^4, 
y2^10 -> (1 - x2^2)^5, 
y2^11 -> y2(1 - x2^2)^5, 
y2^12 -> (1 - x2^2)^6, 
y2^13 -> y2(1 - x2^2)^6, 
y2^14 -> (1 - x2^2)^7, 
y2^15 -> y2(1 - x2^2)^7, 
y2^16 -> (1 - x2^2)^8, 
y3^2 -> 1 - x3^2, 
y3^3 -> y3(1 - x3^2), 
y3^4 -> (1 - x3^2)^2, 
y3^5 -> y3(1 - x3^2)^2, 
y3^6 -> (1 - x3^2)^3, 
y3^7 -> y3(1 - x3^2)^3, 
y3^8 -> (1 - x3^2)^4,
y3^9 -> y3(1 - x3^2)^4, 
y3^10 -> (1 - x3^2)^5, 
y3^11 -> y3(1 - x3^2)^5, 
y3^12 -> (1 - x3^2)^6,
y3^13 -> y3(1 - x3^2)^6, 
y3^14 -> (1 - x3^2)^7, 
y3^15 -> y3(1 - x3^2)^7, 
y3^16 -> (1 - x3^2)^8
};

special = {        (*  Valid only in special coordinate system   *)
t3->(t2 +t3)/(t2 t3 - 1), 
x1 x2 x3-> 1+x1 y2 y3 + y1 x2 y3 + y1 y2 x3, 
y1 y2 y3-> y1 x2 x3 + x1 y2 x3 + x1 x2 y3,
y2 x3 -> -x2 y3 -  y1,
y2 y3 -> x2 x3 - x1, 
y1 x3 -> -x1 y3 -  y2,
y1 y3 -> x1 x3 - x2, 
y1 x2 -> -x1 y2 -  y3,
y1 y2 -> x1 x2 - x3 
}; 

ListDepth[list_] :=
If [ListQ[list], 
If [Length[list]==0, 
1, 
1+Max[Map[ListDepth,list]]],
0
] 

UnCoefficientList[list_, vars_] := Module[
{depth, powers,sum, i, len, var, vars2},
If[!ListQ[vars], 
Total[list * vars^(Range[Length[list]]-1)], 
depth = Length[vars]; 
If[depth ==0, 
list, 
If[depth==1, 
Total[list * vars[[1]]^(Range[Length[list]]-1)], 
sum = 0; 
len = Length[list];
var = vars[[1]]; 
vars2 = Delete[vars,1];
For[ i = 1, i≤len, i++, 
sum += UnCoefficientList[list[[i]], vars2] * var^(i-1)
];
sum
]
]
]
]

unXYΔSubs = {
 XH -> x1 + x2 + x3, 
 X1  ->  2x1 - x2 - x3 ,
 X2  ->  2x2 - x3 - x1 ,
 X3  ->  2x3 - x1 - x2 ,
 
 YH  -> y1 + y2 + y3 ,
 Y1  -> 2y1 - y2 - y3 ,
 Y2  -> 2y2 - y3 - y1 ,
 Y3  -> 2y3 - y1 - y2 , 

 Δ -> x1 y2 + x2 y3 + x3 y1 - x1 y3 - x2 y1 - x3 y2 
};


XYΔSubs = {
(*
x1-> (XH + Xp + Xm)/3, 
x2-> (XH + ω^2 Xp + ω Xm)/3, 
x3-> (XH + ω Xp + ω^2 Xm)/3, 
y1-> (YH + Yp + Ym)/3, 
y2-> (YH + ω^2 Yp + ω Ym)/3, 
y3-> (YH + ω Yp + ω^2 Ym)/3, 
*)

x1-> (XH + X1)/3, 
x2-> (XH + X2)/3, 
x3-> (XH + X3)/3, 
y1-> (YH + Y1)/3, 
y2-> (YH + Y2)/3, 
y3-> (YH + Y3)/3, 

X1^2 ->  ( (3X1-XH X1-3 YH Y1) + (9 - 6 XH + XH^2 - 3YH^2) ) / 2   ,
X1^3 ->  X1( (3X1-XH X1-3 YH Y1) + (9 - 6 XH + XH^2 - 3YH^2) ) / 2   ,
X1^4 ->  ( ( (3X1-XH X1-3 YH Y1) + (9 - 6 XH + XH^2 - 3YH^2) ) / 2  )^2  ,
X1^5 ->  X1 ( ( (3X1-XH X1-3 YH Y1) + (9 - 6 XH + XH^2 - 3YH^2) ) / 2  )^2  ,
X1^6 ->  ( ( (3X1-XH X1-3 YH Y1) + (9 - 6 XH + XH^2 - 3YH^2 ) / 2)  )^3  ,

X2^2 ->  (  (3X2-XH X2-3 YH Y2) + (9 - 6 XH + XH^2 - 3YH^2)  ) / 2   ,
X2^3 ->  X2  (  (3X2-XH X2-3 YH Y2) + (9 - 6 XH + XH^2 - 3YH^2)  ) / 2   ,
X2^4 ->  ( (  (3X2-XH X2-3 YH Y2) + (9 - 6 XH + XH^2 - 3YH^2)  ) / 2  )^2  ,
X2^5 ->  X2( (  (3X2-XH X2-3 YH Y2) + (9 - 6 XH + XH^2 - 3YH^2)  ) / 2  )^2  ,
X2^6 ->  ( (  (3X2-XH X2-3 YH Y2) + (9 - 6 XH + XH^2 - 3YH^2)  ) / 2  )^3  ,

X3^2 ->  (  (3X3-XH X3-3 YH Y3) + (9 - 6 XH + XH^2 - 3YH^2)  ) / 2   ,
X3^3 ->  X3  (  (3X3-XH X3-3 YH Y3) + (9 - 6 XH + XH^2 - 3YH^2)  ) / 2   ,
X3^4 ->  ( (  (3X3-XH X3-3 YH Y3) + (9 - 6 XH + XH^2 - 3YH^2)  ) / 2  )^2  ,
X3^5 ->  X3( (  (3X3-XH X3-3 YH Y3) + (9 - 6 XH + XH^2 - 3YH^2)  ) / 2  )^2  ,
X3^6 ->  ( (  (3X3-XH X3-3 YH Y3) + (9 - 6 XH + XH^2 - 3YH^2)  ) / 2 )^3  ,

X1 X2 -> (  2(3X3-XH X3-3 YH Y3) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1^2 X2 -> X1 (  2(3X3-XH X3-3 YH Y3) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1^3 X2 -> X1^2 (  2(3X3-XH X3-3 YH Y3) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1^4 X2 -> X1^3 (  2(3X3-XH X3-3 YH Y3) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1^5 X2 -> X1^4 (  2(3X3-XH X3-3 YH Y3) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1 X2^2 -> X2(  2(3X3-XH X3-3 YH Y3) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1 X2^3 -> X2^2(  2(3X3-XH X3-3 YH Y3) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1 X2^4 -> X2^3(  2(3X3-XH X3-3 YH Y3) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1 X2^5 -> X2^4(  2(3X3-XH X3-3 YH Y3) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1^2 X2^2 -> ( (  2(3X3-XH X3-3 YH Y3) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^2  , 
X1^3 X2^2 -> X1( (  2(3X3-XH X3-3 YH Y3) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^2  , 
X1^4 X2^2 -> X1^2( (  2(3X3-XH X3-3 YH Y3) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^2  , 
X1^2 X2^3 -> X2( (  2(3X3-XH X3-3 YH Y3) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^2  , 
X1^2 X2^4 -> X2^2( (  2(3X3-XH X3-3 YH Y3) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^2  , 
X1^3 X2^3 -> ( (  2(3X3-XH X3-3 YH Y3) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^3 , 

X1 X3 -> (  2(3X2-XH X2-3 YH Y2) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1^2 X3 -> X1 (  2(3X2-XH X2-3 YH Y2) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1^3 X3 -> X1^2 (  2(3X2-XH X2-3 YH Y2) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1^4 X3 -> X1^3 (  2(3X2-XH X2-3 YH Y2) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1^5 X3 -> X1^4 (  2(3X2-XH X2-3 YH Y2) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1 X3^2 -> X3(  2(3X2-XH X2-3 YH Y2) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1 X3^3 -> X3^2(  2(3X2-XH X2-3 YH Y2) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1 X3^4 -> X3^3(  2(3X2-XH X2-3 YH Y2) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1 X3^5 -> X3^4(  2(3X2-XH X2-3 YH Y2) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X1^2 X3^2 -> ( (  2(3X2-XH X2-3 YH Y2) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^2  , 
X1^3 X3^2 -> X1( (  2(3X2-XH X2-3 YH Y2) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^2  , 
X1^4 X3^2 -> X1^2( (  2(3X2-XH X2-3 YH Y2) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^2  , 
X1^2 X3^3 -> X3( (  2(3X2-XH X2-3 YH Y2) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^2  , 
X1^2 X3^4 -> X3^2( (  2(3X2-XH X2-3 YH Y2) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^2  , 
X1^3 X3^3 -> ( (  2(3X2-XH X2-3 YH Y2) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^3 , 

X2 X3 -> (  2(3X1-XH X1-3 YH Y1) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X2^2 X3 -> X2 (  2(3X1-XH X1-3 YH Y1) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X2^3 X3 -> X2^2 (  2(3X1-XH X1-3 YH Y1) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X2^4 X3 -> X2^3 (  2(3X1-XH X1-3 YH Y1) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X2^5 X3 -> X2^4 (  2(3X1-XH X1-3 YH Y1) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X2 X3^2 -> X3(  2(3X1-XH X1-3 YH Y1) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X2 X3^3 -> X3^2(  2(3X1-XH X1-3 YH Y1) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X2 X3^4 -> X3^3(  2(3X1-XH X1-3 YH Y1) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X2 X3^5 -> X3^4(  2(3X1-XH X1-3 YH Y1) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4  , 
X2^2 X3^2 -> ( (  2(3X1-XH X1-3 YH Y1) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^2  , 
X2^3 X3^2 -> X2( (  2(3X1-XH X1-3 YH Y1) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^2  , 
X2^4 X3^2 -> X2^2( (  2(3X1-XH X1-3 YH Y1) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^2  , 
X2^2 X3^3 -> X3( (  2(3X1-XH X1-3 YH Y1) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^2  , 
X2^2 X3^4 -> X3^2( (  2(3X1-XH X1-3 YH Y1) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^2  , 
X2^3 X3^3 -> ( (  2(3X1-XH X1-3 YH Y1) - (9 - 6 XH + XH^2 - 3YH^2)  ) / 4 )^3 , 

Y1^2 ->  (  -(3X1+3XH X1+YH Y1) + (9 + 6 XH -3 XH^2 +YH^2) ) / 2   ,
Y1^3 ->  Y1( -(3X1+3XH X1+YH Y1) + (9 + 6 XH -3 XH^2 +YH^2) ) / 2   ,
Y1^4 ->  (  ( -(3X1+3XH X1+YH Y1) + (9 + 6 XH -3 XH^2 +YH^2) ) / 2  )^2  ,
Y1^5 ->  Y1 ( ( -(3X1+3XH X1+YH Y1) + (9 + 6 XH -3 XH^2 +YH^2) ) / 2  )^2  ,
Y1^6 ->  (  ( -(3X1+3XH X1+YH Y1) + (9 + 6 XH -3 XH^2 +YH^2) )/2  )^3  ,

Y2^2 ->  (  -(3X2+3XH X2+YH Y2) + (9 + 6 XH -3 XH^2 +YH^2) ) / 2   ,
Y2^3 ->  Y2( -(3X2+3XH X2+YH Y2) + (9 + 6 XH -3 XH^2 +YH^2) ) / 2   ,
Y2^4 ->  (  ( -(3X2+3XH X2+YH Y2) + (9 + 6 XH -3 XH^2 +YH^2) ) / 2  )^2  ,
Y2^5 ->  Y2( ( -(3X2+3XH X2+YH Y2) + (9 + 6 XH -3 XH^2 +YH^2) ) / 2  )^2  ,
Y2^6 ->  (  ( -(3X2+3XH X2+YH Y2) + (9 + 6 XH -3 XH^2 +YH^2) )/2  )^3  ,

Y3^2 ->  (  -(3X3+3XH X3+YH Y3) + (9 + 6 XH -3 XH^2 +YH^2) ) / 2   ,
Y3^3 ->  Y3( -(3X3+3XH X3+YH Y3) + (9 + 6 XH -3 XH^2 +YH^2) ) / 2   ,
Y3^4 ->  (  ( -(3X3+3XH X3+YH Y3) + (9 + 6 XH -3 XH^2 +YH^2) ) / 2  )^2  ,
Y3^5 ->  Y3 ( ( -(3X3+3XH X3+YH Y3) + (9 + 6 XH -3 XH^2 +YH^2) ) / 2  )^2  ,
Y3^6 ->  (  ( -(3X3+3XH X3+YH Y3) + (9 + 6 XH -3 XH^2 +YH^2) )/2  )^3  ,

Y1 Y2 -> (  2*-(3X3+3XH X3+YH Y3) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y1^2 Y2 -> Y1 (  2*-(3X3+3XH X3+YH Y3) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y1^3 Y2 -> Y1^2 (  2*-(3X3+3XH X3+YH Y3) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y1^4 Y2 -> Y1^3 (  2*-(3X3+3XH X3+YH Y3) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y1^5 Y2 -> Y1^4 (  2*-(3X3+3XH X3+YH Y3) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4 , 
Y1 Y2^2 -> Y2(  2*-(3X3+3XH X3+YH Y3) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y1 Y2^3 -> Y2^2(  2*-(3X3+3XH X3+YH Y3) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y1 Y2^4 -> Y2^3(  2*-(3X3+3XH X3+YH Y3) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4 , 
Y1 Y2^5 -> Y2^4(  2*-(3X3+3XH X3+YH Y3) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4 , 
Y1^2 Y2^2 -> ( (  2*-(3X3+3XH X3+YH Y3) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^2  , 
Y1^3 Y2^2 -> Y1( (  2*-(3X3+3XH X3+YH Y3) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^2  , 
Y1^4 Y2^2 -> Y1^2( (  2*-(3X3+3XH X3+YH Y3) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^2  , 
Y1^2 Y2^3 -> Y2( (  2*-(3X3+3XH X3+YH Y3) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^2  , 
Y1^2 Y2^4 -> Y2^2( (  2*-(3X3+3XH X3+YH Y3) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^2  , 
Y1^3 Y2^3 -> ( (  2*-(3X3+3XH X3+YH Y3) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^3 , 

Y1 Y3 -> (  2*-(3X2+3XH X2+YH Y2) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y1^2 Y3 -> Y1 (  2*-(3X2+3XH X2+YH Y2) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y1^3 Y3 -> Y1^2 (  2*-(3X2+3XH X2+YH Y2) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y1^4 Y3 -> Y1^3 (  2*-(3X2+3XH X2+YH Y2) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y1^5 Y3 -> Y1^4 (  2*-(3X2+3XH X2+YH Y2) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4 , 
Y1 Y3^2 -> Y3(  2*-(3X2+3XH X2+YH Y2) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y1 Y3^3 -> Y3^2(  2*-(3X2+3XH X2+YH Y2) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y1 Y3^4 -> Y3^3(  2*-(3X2+3XH X2+YH Y2) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4 , 
Y1 Y3^5 -> Y3^4(  2*-(3X2+3XH X2+YH Y2) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4 , 
Y1^2 Y3^2 -> ( (  2*-(3X2+3XH X2+YH Y2) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^2  , 
Y1^3 Y3^2 -> Y1( (  2*-(3X2+3XH X2+YH Y2) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^2  , 
Y1^4 Y3^2 -> Y1^2( (  2*-(3X2+3XH X2+YH Y2) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^2  , 
Y1^2 Y3^3 -> Y3( (  2*-(3X2+3XH X2+YH Y2) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^2  , 
Y1^2 Y3^4 -> Y3^2( (  2*-(3X2+3XH X2+YH Y2) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^2  , 
Y1^3 Y3^3 -> ( (  2*-(3X2+3XH X2+YH Y2) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^3 , 

Y2 Y3 -> (  2*-(3X1+3XH X1+YH Y1) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y2^2 Y3 -> Y2 (  2*-(3X1+3XH X1+YH Y1) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y2^3 Y3 -> Y2^2 (  2*-(3X1+3XH X1+YH Y1) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y2^4 Y3 -> Y2^3 (  2*-(3X1+3XH X1+YH Y1) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y2^5 Y3 -> Y2^4 (  2*-(3X1+3XH X1+YH Y1) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4 , 
Y2 Y3^2 -> Y3(  2*-(3X1+3XH X1+YH Y1) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y2 Y3^3 -> Y3^2(  2*-(3X1+3XH X1+YH Y1) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4  , 
Y2 Y3^4 -> Y3^3(  2*-(3X1+3XH X1+YH Y1) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4 , 
Y2 Y3^5 -> Y3^4(  2*-(3X1+3XH X1+YH Y1) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4 , 
Y2^2 Y3^2 -> ( (  2*-(3X1+3XH X1+YH Y1) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^2  , 
Y2^3 Y3^2 -> Y2( (  2*-(3X1+3XH X1+YH Y1) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^2  , 
Y2^4 Y3^2 -> Y2^2( (  2*-(3X1+3XH X1+YH Y1) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^2  , 
Y2^2 Y3^3 -> Y3( (  2*-(3X1+3XH X1+YH Y1) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^2  , 
Y2^2 Y3^4 -> Y3^2( (  2*-(3X1+3XH X1+YH Y1) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^2  , 
Y2^3 Y3^3 -> ( (  2*-(3X1+3XH X1+YH Y1) - (9 + 6 XH-3 XH^2 +YH^2)  ) / 4)^3 , 

X1 Y1 -> ( (XH Y1+YH X1-3Y1) + 2(2XH YH + 3YH)  ) / 2  , 
X1^2 Y1 ->  X1( (XH Y1+YH X1-3Y1) + 2(2XH YH + 3YH)  ) / 2  , 
X1^3 Y1 ->  X1^2( (XH Y1+YH X1-3Y1) + 2(2XH YH + 3YH)  ) / 2  , 
X1^4 Y1 ->  X1^3( (XH Y1+YH X1-3Y1) + 2(2XH YH + 3YH)  ) / 2  , 
X1^5 Y1 ->  X1^4( (XH Y1+YH X1-3Y1) + 2(2XH YH + 3YH)  ) / 2  , 
X1 Y1^2 ->  Y1( (XH Y1+YH X1-3Y1) + 2(2XH YH + 3YH)  ) / 2  , 
X1 Y1^3 ->  Y1^2( (XH Y1+YH X1-3Y1) + 2(2XH YH + 3YH)  ) / 2  , 
X1 Y1^4 ->  Y1^3( (XH Y1+YH X1-3Y1) + 2(2XH YH + 3YH)  ) / 2  , 
X1 Y1^5 ->  Y1^4( (XH Y1+YH X1-3Y1) + 2(2XH YH + 3YH)  ) / 2  , 
X1^2 Y1^2 -> (  ( (XH Y1+YH X1-3Y1) + 2(2XH YH + 3YH)  ) / 2  )^2 , 
X1^3 Y1^2 -> X1(  ( (XH Y1+YH X1-3Y1) + 2(2XH YH + 3YH)  ) / 2  )^2 , 
X1^4 Y1^2 -> X1^2(  ( (XH Y1+YH X1-3Y1) + 2(2XH YH + 3YH)  ) / 2  )^2 , 
X1^2 Y1^3 -> Y1(  ( (XH Y1+YH X1-3Y1) + 2(2XH YH + 3YH)  ) / 2  )^2 , 
X1^2 Y1^4 -> Y1^2(  ( (XH Y1+YH X1-3Y1) + 2(2XH YH + 3YH)  ) / 2  )^2 , 
X1^3 Y1^3 -> (  ( (XH Y1+YH X1-3Y1) + 2(2XH YH + 3YH)  ) / 2  )^3 , 

X1 Y2 -> ( (XH Y3+YH X3-3Y3) - (2XH YH + 3YH)   +  3 Δ  ) / 2  , 
X1^2 Y2 ->  X1( (XH Y3+YH X3-3Y3) - (2XH YH + 3YH)   +  3 Δ  ) / 2  , 
X1^3 Y2 ->  X1^2( (XH Y3+YH X3-3Y3) - (2XH YH + 3YH)   +  3 Δ  ) / 2  , 
X1^4 Y2 ->  X1^3( (XH Y3+YH X3-3Y3) - (2XH YH + 3YH)   +  3 Δ  ) / 2  , 
X1^5 Y2 ->  X1^4( (XH Y3+YH X3-3Y3) - (2XH YH + 3YH)   +  3 Δ  ) / 2  , 
X1 Y2^2 ->  Y2( (XH Y3+YH X3-3Y3) - (2XH YH + 3YH)   +  3 Δ  ) / 2  , 
X1 Y2^3 ->  Y2^2( (XH Y3+YH X3-3Y3) - (2XH YH + 3YH)   +  3 Δ  ) / 2  , 
X1 Y2^4 ->  Y2^3( (XH Y3+YH X3-3Y3) - (2XH YH + 3YH)   +  3 Δ  ) / 2  , 
X1 Y2^5 ->  Y2^4( (XH Y3+YH X3-3Y3) - (2XH YH + 3YH)   +  3 Δ  ) / 2  , 
X1^2 Y2^2 -> (  ( (XH Y3+YH X3-3Y3) -(2XH YH + 3YH)   +  3 Δ  ) / 2  )^2 , 
X1^3 Y2^2 -> X1(  ( (XH Y3+YH X3-3Y3) - (2XH YH + 3YH)   +  3 Δ  ) / 2  )^2 , 
X1^4 Y2^2 -> X1^2(  ( (XH Y3+YH X3-3Y3) - (2XH YH + 3YH)   +  3 Δ  ) / 2  )^2 , 
X1^2 Y2^3 -> Y2(  ( (XH Y3+YH X3-3Y3) - (2XH YH + 3YH)   +  3 Δ  ) / 2  )^2 , 
X1^2 Y2^4 -> Y2^2(  ( (XH Y3+YH X3-3Y3) - (2XH YH + 3YH)   +  3 Δ  ) / 2  )^2 , 
X1^3 Y2^3 -> (  ( (XH Y3+YH X3-3Y3) - (2XH YH + 3YH)   +  3 Δ  ) / 2  )^3 , 

X1 Y3 -> ( (XH Y2+YH X2-3Y2) - (2XH YH + 3YH)  -  3 Δ ) / 2  , 
X1^2 Y3 ->  X1( (XH Y2+YH X2-3Y2) - (2XH YH + 3YH)  -  3 Δ  ) / 2  , 
X1^3 Y3 ->  X1^2( (XH Y2+YH X2-3Y2) - (2XH YH + 3YH)  -  3 Δ  ) / 2  , 
X1^4 Y3 ->  X1^3( (XH Y2+YH X2-3Y2) - (2XH YH + 3YH)   -  3 Δ ) / 2  , 
X1^5 Y3 ->  X1^4( (XH Y2+YH X2-3Y2) - (2XH YH + 3YH)   -  3 Δ ) / 2  , 
X1 Y3^2 ->  Y3( (XH Y2+YH X2-3Y2) - (2XH YH + 3YH)   -  3 Δ ) / 2  , 
X1 Y3^3 ->  Y3^2( (XH Y2+YH X2-3Y2) - (2XH YH + 3YH)   -  3 Δ ) / 2  , 
X1 Y3^4 ->  Y3^3( (XH Y2+YH X2-3Y2) - (2XH YH + 3YH)   -  3 Δ ) / 2  , 
X1 Y3^5 ->  Y3^4( (XH Y2+YH X2-3Y2) - (2XH YH + 3YH)   -  3 Δ ) / 2  , 
X1^2 Y3^2 -> (  ( (XH Y2+YH X2-3Y2) - (2XH YH + 3YH)   -  3 Δ ) / 2  )^2 , 
X1^3 Y3^2 -> X1(  ( (XH Y2+YH X2-3Y2) - (2XH YH + 3YH)   -  3 Δ ) / 2  )^2 , 
X1^4 Y3^2 -> X1^2(  ( (XH Y2+YH X2-3Y2) - (2XH YH + 3YH)   -  3 Δ ) / 2  )^2 , 
X1^2 Y3^3 -> Y3(  ( (XH Y2+YH X2-3Y2) - (2XH YH + 3YH)   -  3 Δ ) / 2  )^2 , 
X1^2 Y3^4 -> Y3^2(  ( (XH Y2+YH X2-3Y2) - (2XH YH + 3YH)   -  3 Δ ) / 2  )^2 , 
X1^3 Y3^3 -> (  ( (XH Y2+YH X2-3Y2) - (2XH YH + 3YH)   -  3 Δ ) / 2  )^3 , 

X2 Y1 -> ( (XH Y3+YH X3-3Y3) -(2XH YH + 3YH)    -  3 Δ  ) / 2  , 
X2^2 Y1 ->  X2( (XH Y3+YH X3-3Y3) -(2XH YH + 3YH)   -  3 Δ  ) / 2  , 
X2^3 Y1 ->  X2^2( (XH Y3+YH X3-3Y3) -(2XH YH + 3YH)   -  3 Δ   ) / 2  , 
X2^4 Y1 ->  X2^3( (XH Y3+YH X3-3Y3) -(2XH YH + 3YH)   -  3 Δ   ) / 2  , 
X2^5 Y1 ->  X2^4( (XH Y3+YH X3-3Y3) -(2XH YH + 3YH)   -  3 Δ   ) / 2  , 
X2 Y1^2 ->  Y1( (XH Y3+YH X3-3Y3) -(2XH YH + 3YH)   -  3 Δ   ) / 2  , 
X2 Y1^3 ->  Y1^2( (XH Y3+YH X3-3Y3) -(2XH YH + 3YH)   -  3 Δ  ) / 2  , 
X2 Y1^4 ->  Y1^3( (XH Y3+YH X3-3Y3) -(2XH YH + 3YH)   -  3 Δ   ) / 2  , 
X2 Y1^5 ->  Y1^4( (XH Y3+YH X3-3Y3) -(2XH YH + 3YH)   -  3 Δ   ) / 2  , 
X2^2 Y1^2 -> (  ( (XH Y3+YH X3-3Y3) -(2XH YH + 3YH)   -  3 Δ   ) / 2  )^2 , 
X2^3 Y1^2 -> X2(  ( (XH Y3+YH X3-3Y3) -(2XH YH + 3YH)   -  3 Δ   ) / 2  )^2 , 
X2^4 Y1^2 -> X2^2(  ( (XH Y3+YH X3-3Y3) -(2XH YH + 3YH)   -  3 Δ   ) / 2  )^2 , 
X2^2 Y1^3 -> Y1(  ( (XH Y3+YH X3-3Y3) -(2XH YH + 3YH)   -  3 Δ   ) / 2  )^2 , 
X2^2 Y1^4 -> Y1^2(  ( (XH Y3+YH X3-3Y3) -(2XH YH + 3YH)   -  3 Δ   ) / 2  )^2 , 
X2^3 Y1^3 -> (  ( (XH Y3+YH X3-3Y3) -(2XH YH + 3YH)    -  3 Δ  ) / 2  )^3 , 

X2 Y2 -> ( (XH Y2+YH X2-3Y2) +2 (2XH YH + 3YH)  ) / 2  , 
X2^2 Y2 ->  X2( (XH Y2+YH X2-3Y2) +2 (2XH YH + 3YH)  ) / 2  , 
X2^3 Y2 ->  X2^2( (XH Y2+YH X2-3Y2) +2 (2XH YH + 3YH)  ) / 2  , 
X2^4 Y2 ->  X2^3( (XH Y2+YH X2-3Y2) +2 (2XH YH + 3YH)  ) / 2  , 
X2^5 Y2 ->  X2^4( (XH Y2+YH X2-3Y2) +2 (2XH YH + 3YH)  ) / 2  , 
X2 Y2^2 ->  Y2( (XH Y2+YH X2-3Y2) +2 (2XH YH + 3YH)  ) / 2  , 
X2 Y2^3 ->  Y2^2( (XH Y2+YH X2-3Y2) +2 (2XH YH + 3YH)  ) / 2  , 
X2 Y2^4 ->  Y2^3( (XH Y2+YH X2-3Y2) +2 (2XH YH + 3YH)  ) / 2  , 
X2 Y2^5 ->  Y2^4( (XH Y2+YH X2-3Y2) +2 (2XH YH + 3YH)  ) / 2  , 
X2^2 Y2^2 -> (  ( (XH Y2+YH X2-3Y2) +2(2XH YH + 3YH)  ) / 2  )^2 , 
X2^3 Y2^2 -> X2(  ( (XH Y2+YH X2-3Y2) +2 (2XH YH + 3YH)  ) / 2  )^2 , 
X2^4 Y2^2 -> X2^2(  ( (XH Y2+YH X2-3Y2) +2 (2XH YH + 3YH)  ) / 2  )^2 , 
X2^2 Y2^3 -> Y2(  ( (XH Y2+YH X2-3Y2) +2 (2XH YH + 3YH)  ) / 2  )^2 , 
X2^2 Y2^4 -> Y2^2(  ( (XH Y2+YH X2-3Y2) +2 (2XH YH + 3YH)  ) / 2  )^2 , 
X2^3 Y2^3 -> (  ( (XH Y2+YH X2-3Y2) +2 (2XH YH + 3YH)  ) / 2  )^3 , 

X2 Y3 -> ( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)   +  3 Δ   ) / 2  , 
X2^2 Y3 ->  X2( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  +  3 Δ    ) / 2  , 
X2^3 Y3 ->  X2^2( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  +  3 Δ    ) / 2  , 
X2^4 Y3 ->  X2^3( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  +  3 Δ    ) / 2  , 
X2^5 Y3 ->  X2^4( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  +  3 Δ    ) / 2  , 
X2 Y3^2 ->  Y3( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  +  3 Δ    ) / 2  , 
X2 Y3^3 ->  Y3^2( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  +  3 Δ    ) / 2  , 
X2 Y3^4 ->  Y3^3( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  +  3 Δ    ) / 2  , 
X2 Y3^5 ->  Y3^4( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  +  3 Δ    ) / 2  , 
X2^2 Y3^2 -> (  ( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  +  3 Δ    ) / 2  )^2 , 
X2^3 Y3^2 -> X2(  ( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  +  3 Δ    ) / 2  )^2 , 
X2^4 Y3^2 -> X2^2(  ( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  +  3 Δ    ) / 2  )^2 , 
X2^2 Y3^3 -> Y3(  ( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  +  3 Δ    ) / 2  )^2 , 
X2^2 Y3^4 -> Y3^2(  ( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  +  3 Δ    ) / 2  )^2 , 
X2^3 Y3^3 -> (  ( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  +  3 Δ    ) / 2  )^3 , 

X3 Y1 -> ( (XH Y2+YH X2-3Y2) -(2XH YH + 3YH)   +  3 Δ   ) / 2  , 
X3^2 Y1 ->  X3( (XH Y2+YH X2-3Y2) -(2XH YH + 3YH)  +  3 Δ    ) / 2  , 
X3^3 Y1 ->  X3^2( (XH Y2+YH X2-3Y2) -(2XH YH + 3YH)  +  3 Δ    ) / 2  , 
X3^4 Y1 ->  X3^3( (XH Y2+YH X2-3Y2) -(2XH YH + 3YH)  +  3 Δ    ) / 2  , 
X3^5 Y1 ->  X3^4( (XH Y2+YH X2-3Y2) -(2XH YH + 3YH)  +  3 Δ    ) / 2  , 
X3 Y1^2 ->  Y1( (XH Y2+YH X2-3Y2) -(2XH YH + 3YH)  +  3 Δ    ) / 2  , 
X3 Y1^3 ->  Y1^2( (XH Y2+YH X2-3Y2) -(2XH YH + 3YH)  +  3 Δ    ) / 2  , 
X3 Y1^4 ->  Y1^3( (XH Y2+YH X2-3Y2) -(2XH YH + 3YH)  +  3 Δ    ) / 2  , 
X3 Y1^5 ->  Y1^4( (XH Y2+YH X2-3Y2) -(2XH YH + 3YH)  +  3 Δ    ) / 2  , 
X3^2 Y1^2 -> (  ( (XH Y2+YH X2-3Y2) -(2XH YH + 3YH)  +  3 Δ    ) / 2  )^2 , 
X3^3 Y1^2 -> X3(  ( (XH Y2+YH X2-3Y2) -(2XH YH + 3YH)  +  3 Δ    ) / 2  )^2 , 
X3^4 Y1^2 -> X3^2(  ( (XH Y2+YH X2-3Y2) -(2XH YH + 3YH)  +  3 Δ    ) / 2  )^2 , 
X3^2 Y1^3 -> Y1(  ( (XH Y2+YH X2-3Y2) -(2XH YH + 3YH)  +  3 Δ    ) / 2  )^2 , 
X3^2 Y1^4 -> Y1^2(  ( (XH Y2+YH X2-3Y2) - (2XH YH + 3YH)  +  3 Δ    ) / 2  )^2 , 
X3^3 Y1^3 -> (  ( (XH Y2+YH X2-3Y2) -(2XH YH + 3YH)  +  3 Δ    ) / 2  )^3 , 

X3 Y2 -> ( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  -  3 Δ    ) / 2  , 
X3^2 Y2 ->  X3( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  -  3 Δ    ) / 2  , 
X3^3 Y2 ->  X3^2( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  -  3 Δ    ) / 2  , 
X3^4 Y2 ->  X3^3( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  -  3 Δ    ) / 2  , 
X3^5 Y2 ->  X3^4( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  -  3 Δ    ) / 2  , 
X3 Y2^2 ->  Y2( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  -  3 Δ     ) / 2  , 
X3 Y2^3 ->  Y2^2( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  -  3 Δ    ) / 2  , 
X3 Y2^4 ->  Y2^3( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  -  3 Δ    ) / 2  , 
X3 Y2^5 ->  Y2^4( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  -  3 Δ    ) / 2  , 
X3^2 Y2^2 -> (  ( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  -  3 Δ     ) / 2  )^2 , 
X3^3 Y2^2 -> X3(  ( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  -  3 Δ    ) / 2  )^2 , 
X3^4 Y2^2 -> X3^2(  ( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  -  3 Δ    ) / 2  )^2 , 
X3^2 Y2^3 -> Y2(  ( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  -  3 Δ    ) / 2  )^2 , 
X3^2 Y2^4 -> Y2^2(  ( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  -  3 Δ    ) / 2  )^2 , 
X3^3 Y2^3 -> (  ( (XH Y1+YH X1-3Y1) - (2XH YH + 3YH)  -  3 Δ    ) / 2  )^3 , 

X3 Y3 -> ( (XH Y3+YH X3-3Y3) +2 (2XH YH + 3YH)  ) / 2  , 
X3^2 Y3 ->  X3( (XH Y3+YH X3-3Y3) +2 (2XH YH + 3YH)  ) / 2  , 
X3^3 Y3 ->  X3^2( (XH Y3+YH X3-3Y3) +2 (2XH YH + 3YH)  ) / 2  , 
X3^4 Y3 ->  X3^3( (XH Y3+YH X3-3Y3) +2 (2XH YH + 3YH)  ) / 2  , 
X3^5 Y3 ->  X3^4( (XH Y3+YH X3-3Y3) +2 (2XH YH + 3YH)  ) / 2  , 
X3 Y3^2 ->  Y3( (XH Y3+YH X3-3Y3) +2 (2XH YH + 3YH)  ) / 2  , 
X3 Y3^3 ->  Y3^2( (XH Y3+YH X3-3Y3) +2 (2XH YH + 3YH)  ) / 2  , 
X3 Y3^4 ->  Y3^3( (XH Y3+YH X3-3Y3) +2 (2XH YH + 3YH)  ) / 2  , 
X3 Y3^5 ->  Y3^4( (XH Y3+YH X3-3Y3) +2 (2XH YH + 3YH)  ) / 2  , 
X3^2 Y3^2 -> (  ( (XH Y3+YH X3-3Y3) +2(2XH YH + 3YH)  ) / 2  )^2 , 
X3^3 Y3^2 -> X3(  ( (XH Y3+YH X3-3Y3) +2 (2XH YH + 3YH)  ) / 2  )^2 , 
X3^4 Y3^2 -> X3^2(  ( (XH Y3+YH X3-3Y3) +2 (2XH YH + 3YH)  ) / 2  )^2 , 
X3^2 Y3^3 -> Y3(  ( (XH Y3+YH X3-3Y3) +2 (2XH YH + 3YH)  ) / 2  )^2 , 
X3^2 Y3^4 -> Y3^2(  ( (XH Y3+YH X3-3Y3) +2 (2XH YH + 3YH)  ) / 2  )^2 , 
X3^3 Y3^3 -> (  ( (XH Y3+YH X3-3Y3) +2 (2XH YH + 3YH)  ) / 2  )^3 ,

Δ^2 -> (1/4) (27-18 (XH^2)+8 (XH^3)-(XH^4)-18 (YH^2)-24 XH (YH^2)-2 (XH^2) (YH^2)-(YH^4)), 
Δ^3 -> Δ (1/4) (27-18 (XH^2)+8 (XH^3)-(XH^4)-18 (YH^2)-24 XH (YH^2)-2 (XH^2) (YH^2)-(YH^4)), 
Δ^4 -> ((1/4) (27-18 (XH^2)+8 (XH^3)-(XH^4)-18 (YH^2)-24 XH (YH^2)-2 (XH^2) (YH^2)-(YH^4)))^2 , 
Δ^5 -> Δ ((1/4) (27-18 (XH^2)+8 (XH^3)-(XH^4)-18 (YH^2)-24 XH (YH^2)-2 (XH^2) (YH^2)-(YH^4)))^2 , 
Δ^6 -> ((1/4) (27-18 (XH^2)+8 (XH^3)-(XH^4)-18 (YH^2)-24 XH (YH^2)-2 (XH^2) (YH^2)-(YH^4)))^3 , 
Δ^7 -> Δ ((1/4) (27-18 (XH^2)+8 (XH^3)-(XH^4)-18 (YH^2)-24 XH (YH^2)-2 (XH^2) (YH^2)-(YH^4)))^3 , 
Δ^8 -> ((1/4) (27-18 (XH^2)+8 (XH^3)-(XH^4)-18 (YH^2)-24 XH (YH^2)-2 (XH^2) (YH^2)-(YH^4)))^4 , 
Δ^9 -> Δ ((1/4) (27-18 (XH^2)+8 (XH^3)-(XH^4)-18 (YH^2)-24 XH (YH^2)-2 (XH^2) (YH^2)-(YH^4)))^4 ,
Δ^10 -> ((1/4) (27-18 (XH^2)+8 (XH^3)-(XH^4)-18 (YH^2)-24 XH (YH^2)-2 (XH^2) (YH^2)-(YH^4)))^5 , 

X1 Δ -> ( 2(3+2XH)YH(X3-X2)+ (9-6XH+XH^2-3YH^2) (Y2-Y3) ) / 6 , 

X1^2 Δ -> X1 ( 2(3+2XH)YH(X3-X2)+ (9-6XH+XH^2-3YH^2) (Y2-Y3) ) / 6 , 

X1^3 Δ -> X1^2 ( 2(3+2XH)YH(X3-X2)+ (9-6XH+XH^2-3YH^2) (Y2-Y3) ) / 6 , 

X1^4 Δ -> X1^3 ( 2(3+2XH)YH(X3-X2)+ (9-6XH+XH^2-3YH^2) (Y2-Y3) ) / 6 , 

X1^5 Δ -> X1^4 ( 2(3+2XH)YH(X3-X2)+ (9-6XH+XH^2-3YH^2) (Y2-Y3) ) / 6 , 

X1 Δ^2 ->  Δ( 2(3+2XH)YH(X3-X2)+ (9-6XH+XH^2-3YH^2) (Y2-Y3) ) / 6 , 

X1 Δ^3 ->  Δ^2( 2(3+2XH)YH(X3-X2)+ (9-6XH+XH^2-3YH^2) (Y2-Y3) ) / 6 , 

X1 Δ^4 ->  Δ^3( 2(3+2XH)YH(X3-X2)+ (9-6XH+XH^2-3YH^2) (Y2-Y3) ) / 6 , 

X1 Δ^5 ->  Δ^4( 2(3+2XH)YH(X3-X2)+ (9-6XH+XH^2-3YH^2) (Y2-Y3) ) / 6 , 

X1^2 Δ^2 -> ( ( 2(3+2XH)YH(X3-X2)+ (9-6XH+XH^2-3YH^2) (Y2-Y3) ) / 6  )^2 , 

X1^3 Δ^2 -> X1 ( ( 2(3+2XH)YH(X3-X2)+ (9-6XH+XH^2-3YH^2) (Y2-Y3) ) / 6  )^2 , 

X1^4 Δ^2 -> X1^2 ( ( 2(3+2XH)YH(X3-X2)+ (9-6XH+XH^2-3YH^2) (Y2-Y3) ) / 6  )^2 , 

X1^2 Δ^3 -> Δ ( ( 2(3+2XH)YH(X3-X2)+ (9-6XH+XH^2-3YH^2) (Y2-Y3) ) / 6  )^2 , 

X1^2 Δ^4 -> Δ^2 ( ( 2(3+2XH)YH(X3-X2)+ (9-6XH+XH^2-3YH^2) (Y2-Y3) ) / 6  )^2 , 

X1^3 Δ^3 -> ( ( 2(3+2XH)YH(X3-X2)+ (9-6XH+XH^2-3YH^2) (Y2-Y3) ) / 6  )^3 , 


X2 Δ -> ( 2(3+2XH)YH(X1-X3)+ (9-6XH+XH^2-3YH^2) (Y3-Y1) ) / 6 , 

X2^2 Δ -> X2 ( 2(3+2XH)YH(X1-X3)+ (9-6XH+XH^2-3YH^2) (Y3-Y1) ) / 6 , 

X2^3 Δ -> X2^2 ( 2(3+2XH)YH(X1-X3)+ (9-6XH+XH^2-3YH^2) (Y3-Y1) ) / 6 , 

X2^4 Δ -> X2^3 ( 2(3+2XH)YH(X1-X3)+ (9-6XH+XH^2-3YH^2) (Y3-Y1) ) / 6 , 

X2^5 Δ -> X2^4 ( 2(3+2XH)YH(X1-X3)+ (9-6XH+XH^2-3YH^2) (Y3-Y1) ) / 6 , 

X2 Δ^2 ->  Δ( 2(3+2XH)YH(X1-X3)+ (9-6XH+XH^2-3YH^2) (Y3-Y1) ) / 6 , 

X2 Δ^3 ->  Δ^2( 2(3+2XH)YH(X1-X3)+ (9-6XH+XH^2-3YH^2) (Y3-Y1) ) / 6 , 

X2 Δ^4 ->  Δ^3( 2(3+2XH)YH(X1-X3)+ (9-6XH+XH^2-3YH^2) (Y3-Y1) ) / 6 , 

X2 Δ^5 ->  Δ^4( 2(3+2XH)YH(X1-X3)+ (9-6XH+XH^2-3YH^2) (Y3-Y1) ) / 6 , 

X2^2 Δ^2 -> ( ( 2(3+2XH)YH(X1-X3)+ (9-6XH+XH^2-3YH^2) (Y3-Y1) ) / 6  )^2 , 

X2^3 Δ^2 -> X2 ( ( 2(3+2XH)YH(X1-X3)+ (9-6XH+XH^2-3YH^2) (Y3-Y1) ) / 6  )^2 , 

X2^4 Δ^2 -> X2^2 ( ( 2(3+2XH)YH(X1-X3)+ (9-6XH+XH^2-3YH^2) (Y3-Y1) ) / 6  )^2 , 

X2^2 Δ^3 -> Δ ( ( 2(3+2XH)YH(X1-X3)+ (9-6XH+XH^2-3YH^2) (Y3-Y1) ) / 6  )^2 , 

X2^2 Δ^4 -> Δ^2 ( ( 2(3+2XH)YH(X1-X3)+ (9-6XH+XH^2-3YH^2) (Y3-Y1) ) / 6  )^2 , 

X2^3 Δ^3 -> ( ( 2(3+2XH)YH(X1-X3)+ (9-6XH+XH^2-3YH^2) (Y3-Y1) ) / 6  )^3 , 


X3 Δ -> ( 2(3+2XH)YH(X2-X1)+ (9-6XH+XH^2-3YH^2) (Y1-Y2) ) / 6 , 

X3^2 Δ -> X3 ( 2(3+2XH)YH(X2-X1)+ (9-6XH+XH^2-3YH^2) (Y1-Y2) ) / 6 , 

X3^3 Δ -> X3^2 ( 2(3+2XH)YH(X2-X1)+ (9-6XH+XH^2-3YH^2) (Y1-Y2) ) / 6 , 

X3^4 Δ -> X3^3 ( 2(3+2XH)YH(X2-X1)+ (9-6XH+XH^2-3YH^2) (Y1-Y2) ) / 6 , 

X3^5 Δ -> X3^4 ( 2(3+2XH)YH(X2-X1)+ (9-6XH+XH^2-3YH^2) (Y1-Y2) ) / 6 , 

X3 Δ^2 ->  Δ( 2(3+2XH)YH(X2-X1)+ (9-6XH+XH^2-3YH^2) (Y1-Y2) ) / 6 , 

X3 Δ^3 ->  Δ^2( 2(3+2XH)YH(X2-X1)+ (9-6XH+XH^2-3YH^2) (Y1-Y2) ) / 6 , 

X3 Δ^4 ->  Δ^3( 2(3+2XH)YH(X2-X1)+ (9-6XH+XH^2-3YH^2) (Y1-Y2) ) / 6 , 

X3 Δ^5 ->  Δ^4( 2(3+2XH)YH(X2-X1)+ (9-6XH+XH^2-3YH^2) (Y1-Y2) ) / 6 , 

X3^2 Δ^2 -> ( ( 2(3+2XH)YH(X2-X1)+ (9-6XH+XH^2-3YH^2) (Y1-Y2) ) / 6  )^2 , 

X3^3 Δ^2 -> X3 ( ( 2(3+2XH)YH(X2-X1)+ (9-6XH+XH^2-3YH^2) (Y1-Y2) ) / 6  )^2 , 

X3^4 Δ^2 -> X3^2 ( ( 2(3+2XH)YH(X2-X1)+ (9-6XH+XH^2-3YH^2) (Y1-Y2) ) / 6  )^2 , 

X3^2 Δ^3 -> Δ ( ( 2(3+2XH)YH(X2-X1)+ (9-6XH+XH^2-3YH^2) (Y1-Y2) ) / 6  )^2 , 

X3^2 Δ^4 -> Δ^2 ( ( 2(3+2XH)YH(X2-X1)+ (9-6XH+XH^2-3YH^2) (Y1-Y2) ) / 6  )^2 , 

X3^3 Δ^3 -> ( ( 2(3+2XH)YH(X2-X1)+ (9-6XH+XH^2-3YH^2) (Y1-Y2) ) / 6  )^3 ,
 

Y1 Δ -> ( 2(3+2XH)YH(Y2-Y3)+ (9+6XH-3XH^2+YH^2) (X3-X2) ) / 6 , 

Y1^2 Δ -> Y1 ( 2(3+2XH)YH(Y2-Y3)+ (9+6XH-3XH^2+YH^2) (X3-X2) ) / 6 , 

Y1^3 Δ -> Y1^2 ( 2(3+2XH)YH(Y2-Y3)+ (9+6XH-3XH^2+YH^2) (X3-X2) ) / 6 , 

Y1^4 Δ -> Y1^3 ( 2(3+2XH)YH(Y2-Y3)+ (9+6XH-3XH^2+YH^2) (X3-X2) ) / 6 , 

Y1^5 Δ -> Y1^4 ( 2(3+2XH)YH(Y2-Y3)+ (9+6XH-3XH^2+YH^2) (X3-X2) ) / 6 , 

Y1 Δ^2 ->  Δ( 2(3+2XH)YH(Y2-Y3)+ (9+6XH-3XH^2+YH^2) (X3-X2) ) / 6 , 

Y1 Δ^3 ->  Δ^2( 2(3+2XH)YH(Y2-Y3)+ (9+6XH-3XH^2+YH^2) (X3-X2) ) / 6 , 

Y1 Δ^4 ->  Δ^3( 2(3+2XH)YH(Y2-Y3)+ (9+6XH-3XH^2+YH^2) (X3-X2) ) / 6 , 

Y1 Δ^5 ->  Δ^4( 2(3+2XH)YH(Y2-Y3)+ (9+6XH-3XH^2+YH^2) (X3-X2) ) / 6 , 

Y1^2 Δ^2 -> ( ( 2(3+2XH)YH(Y2-Y3)+ (9+6XH-3XH^2+YH^2) (X3-X2) ) / 6  )^2 , 

Y1^3 Δ^2 -> Y1 ( ( 2(3+2XH)YH(Y2-Y3)+ (9+6XH-3XH^2+YH^2) (X3-X2) ) / 6  )^2 , 

Y1^4 Δ^2 -> Y1^2 ( ( 2(3+2XH)YH(Y2-Y3)+ (9+6XH-3XH^2+YH^2) (X3-X2) ) / 6  )^2 , 

Y1^2 Δ^3 -> Δ ( ( 2(3+2XH)YH(Y2-Y3)+ (9+6XH-3XH^2+YH^2) (X3-X2) ) / 6  )^2 , 

Y1^2 Δ^4 -> Δ^2 ( ( 2(3+2XH)YH(Y2-Y3)+ (9+6XH-3XH^2+YH^2) (X3-X2) ) / 6  )^2 , 

Y1^3 Δ^3 -> ( ( 2(3+2XH)YH(Y2-Y3)+ (9+6XH-3XH^2+YH^2) (X3-X2) ) / 6  )^3 , 


Y2 Δ -> ( 2(3+2XH)YH(Y3-Y1)+ (9+6XH-3XH^2+YH^2) (X1-X3) ) / 6 , 

Y2^2 Δ -> Y2 ( 2(3+2XH)YH(Y3-Y1)+ (9+6XH-3XH^2+YH^2) (X1-X3) ) / 6 , 

Y2^3 Δ -> Y2^2 ( 2(3+2XH)YH(Y3-Y1)+ (9+6XH-3XH^2+YH^2) (X1-X3) ) / 6 , 

Y2^4 Δ -> Y2^3 ( 2(3+2XH)YH(Y3-Y1)+ (9+6XH-3XH^2+YH^2) (X1-X3) ) / 6 , 

Y2^5 Δ -> Y2^4 ( 2(3+2XH)YH(Y3-Y1)+ (9+6XH-3XH^2+YH^2) (X1-X3) ) / 6 , 

Y2 Δ^2 ->  Δ( 2(3+2XH)YH(Y3-Y1)+ (9+6XH-3XH^2+YH^2) (X1-X3) ) / 6 , 

Y2 Δ^3 ->  Δ^2( 2(3+2XH)YH(Y3-Y1)+ (9+6XH-3XH^2+YH^2) (X1-X3) ) / 6 , 

Y2 Δ^4 ->  Δ^3( 2(3+2XH)YH(Y3-Y1)+ (9+6XH-3XH^2+YH^2) (X1-X3) ) / 6 , 

Y2 Δ^5 ->  Δ^4( 2(3+2XH)YH(Y3-Y1)+ (9+6XH-3XH^2+YH^2) (X1-X3) ) / 6 , 

Y2^2 Δ^2 -> ( ( 2(3+2XH)YH(Y3-Y1)+ (9+6XH-3XH^2+YH^2) (X1-X3) ) / 6  )^2 , 

Y2^3 Δ^2 -> Y2 ( ( 2(3+2XH)YH(Y3-Y1)+ (9+6XH-3XH^2+YH^2) (X1-X3) ) / 6  )^2 , 

Y2^4 Δ^2 -> Y2^2 ( ( 2(3+2XH)YH(Y3-Y1)+ (9+6XH-3XH^2+YH^2) (X1-X3) ) / 6  )^2 , 

Y2^2 Δ^3 -> Δ ( ( 2(3+2XH)YH(Y3-Y1)+ (9+6XH-3XH^2+YH^2) (X1-X3) ) / 6  )^2 , 

Y2^2 Δ^4 -> Δ^2 ( ( 2(3+2XH)YH(Y3-Y1)+ (9+6XH-3XH^2+YH^2) (X1-X3) ) / 6  )^2 , 

Y2^3 Δ^3 -> ( ( 2(3+2XH)YH(Y3-Y1)+ (9+6XH-3XH^2+YH^2) (X1-X3) ) / 6  )^3 , 


Y3 Δ -> ( 2(3+2XH)YH(Y1-Y2)+ (9+6XH-3XH^2+YH^2) (X2-X1) ) / 6 , 

Y3^2 Δ -> Y3 ( 2(3+2XH)YH(Y1-Y2)+ (9+6XH-3XH^2+YH^2) (X2-X1) ) / 6 , 

Y3^3 Δ -> Y3^2 ( 2(3+2XH)YH(Y1-Y2)+ (9+6XH-3XH^2+YH^2) (X2-X1) ) / 6 , 

Y3^4 Δ -> Y3^3 ( 2(3+2XH)YH(Y1-Y2)+ (9+6XH-3XH^2+YH^2) (X2-X1) ) / 6 , 

Y3^5 Δ -> Y3^4 ( 2(3+2XH)YH(Y1-Y2)+ (9+6XH-3XH^2+YH^2) (X2-X1) ) / 6 , 

Y3 Δ^2 ->  Δ( 2(3+2XH)YH(Y1-Y2)+ (9+6XH-3XH^2+YH^2) (X2-X1) ) / 6 , 

Y3 Δ^3 ->  Δ^2( 2(3+2XH)YH(Y1-Y2)+ (9+6XH-3XH^2+YH^2) (X2-X1) ) / 6 , 

Y3 Δ^4 ->  Δ^3( 2(3+2XH)YH(Y1-Y2)+ (9+6XH-3XH^2+YH^2) (X2-X1) ) / 6 , 

Y3 Δ^5 ->  Δ^4( 2(3+2XH)YH(Y1-Y2)+ (9+6XH-3XH^2+YH^2) (X2-X1) ) / 6 , 

Y3^2 Δ^2 -> ( ( 2(3+2XH)YH(Y1-Y2)+ (9+6XH-3XH^2+YH^2) (X2-X1) ) / 6  )^2 , 

Y3^3 Δ^2 -> Y3 ( ( 2(3+2XH)YH(Y1-Y2)+ (9+6XH-3XH^2+YH^2) (X2-X1) ) / 6  )^2 , 

Y3^4 Δ^2 -> Y3^2 ( ( 2(3+2XH)YH(Y1-Y2)+ (9+6XH-3XH^2+YH^2) (X2-X1) ) / 6  )^2 , 

Y3^2 Δ^3 -> Δ ( ( 2(3+2XH)YH(Y1-Y2)+ (9+6XH-3XH^2+YH^2) (X2-X1) ) / 6  )^2 , 

Y3^2 Δ^4 -> Δ^2 ( ( 2(3+2XH)YH(Y1-Y2)+ (9+6XH-3XH^2+YH^2) (X2-X1) ) / 6  )^2 , 

Y3^3 Δ^3 -> ( ( 2(3+2XH)YH(Y1-Y2)+ (9+6XH-3XH^2+YH^2) (X2-X1) ) / 6  )^3 , 

Xp^2 ->(3Xm-XH Xm-3YH Ym)/2,
Xm^2 ->(3Xp-XH Xp-3YH Yp)/2,
Xp^3 -> Xp(3Xm-XH Xm-3YH Ym)/2,
Xm^3 -> Xm(3Xp-XH Xp-3YH Yp)/2,
Xp^4 -> ( (3Xm-XH Xm-3YH Ym)/2 )^2,
Xm^4 -> ( (3Xp-XH Xp-3YH Yp)/2 )^2,
Xp^5 -> Xp ((3Xm-XH Xm-3YH Ym)/2)^2,
Xm^5 -> Xm((3Xp-XH Xp-3YH Yp)/2)^2,
Xp^6 -> ((3Xm-XH Xm-3YH Ym)/2)^3,
Xm^6 -> ((3Xp-XH Xp-3YH Yp)/2)^3,

Yp^2 -> -(3Xm+YH Ym+3XH Xm)/2,
Ym^2 -> -(3Xp+YH Yp+3XH Xp)/2,
Yp^3 -> Yp * -(3Xm+YH Ym+3XH Xm)/2,
Ym^3 -> Ym * -(3Xp+YH Yp+3XH Xp)/2,
Yp^4 -> ( (3Xm+YH Ym+3XH Xm)/2 )^2 ,
Ym^4 -> ( (3Xp+YH Yp+3XH Xp)/2 )^2,
Yp^5 -> Yp( (3Xm+YH Ym+3XH Xm)/2 )^2 ,
Ym^5 -> Ym( (3Xp+YH Yp+3XH Xp)/2 )^2,
Yp^6 -> - ( (3Xm+YH Ym+3XH Xm)/2 )^3 ,
Ym^6 -> - ( (3Xp+YH Yp+3XH Xp)/2 )^3,

Xp Xm -> (9-6XH+XH^2-3YH^2)/4, 
Xm Xp -> (9-6XH+XH^2-3YH^2)/4,
Xp^2 Xm -> Xp (9-6XH+XH^2-3YH^2)/4, 
Xm^2 Xp -> Xm(9-6XH+XH^2-3YH^2)/4,
Xp Xm^2 -> Xm(9-6XH+XH^2-3YH^2)/4, 
Xm Xp^2 -> Xp(9-6XH+XH^2-3YH^2)/4,
Xp^3 Xm -> Xp^2 (9-6XH+XH^2-3YH^2)/4, 
Xm^3 Xp -> Xm^2(9-6XH+XH^2-3YH^2)/4,
Xp Xm^3 -> Xm^2(9-6XH+XH^2-3YH^2)/4, 
Xm Xp^3 -> Xp^2(9-6XH+XH^2-3YH^2)/4,
Xp^4 Xm -> Xp^3 (9-6XH+XH^2-3YH^2)/4, 
Xm^4 Xp -> Xm^3(9-6XH+XH^2-3YH^2)/4,
Xp Xm^4 -> Xm^3(9-6XH+XH^2-3YH^2)/4, 
Xm Xp^4 -> Xp^3(9-6XH+XH^2-3YH^2)/4,
Xp^5 Xm -> Xp^3 (9-6XH+XH^2-3YH^2)/4, 
Xm^5 Xp -> Xm^3(9-6XH+XH^2-3YH^2)/4,
Xp Xm^5 -> Xm^3(9-6XH+XH^2-3YH^2)/4, 
Xm Xp^5 -> Xp^3(9-6XH+XH^2-3YH^2)/4,
Xp^2 Xm^2 -> ( (9-6XH+XH^2-3YH^2)/4 )^2, 
Xm^2 Xp^2 -> ( (9-6XH+XH^2-3YH^2)/4 )^2,
Xp^3 Xm^2 -> Xp( (9-6XH+XH^2-3YH^2)/4 )^2, 
Xm^3 Xp^2 -> Xm( (9-6XH+XH^2-3YH^2)/4 )^2,
Xp^2 Xm^3 -> Xm( (9-6XH+XH^2-3YH^2)/4 )^2, 
Xm^2 Xp^3 -> Xp( (9-6XH+XH^2-3YH^2)/4 )^2,
Xp^4 Xm^2 -> Xp^2( (9-6XH+XH^2-3YH^2)/4 )^2, 
Xm^4 Xp^2 -> Xm^2( (9-6XH+XH^2-3YH^2)/4 )^2,
Xp^2 Xm^4 -> Xm^2( (9-6XH+XH^2-3YH^2)/4 )^2, 
Xm^2 Xp^4 -> Xp^2( (9-6XH+XH^2-3YH^2)/4 )^2,
Xp^3 Xm^3 -> ( (9-6XH+XH^2-3YH^2)/4 )^3, 
Xm^3 Xp^3 -> ( (9-6XH+XH^2-3YH^2)/4 )^3,

Yp Ym -> (9+6XH-3XH^2+YH^2)/4, 
Ym Yp -> (9+6XH-3XH^2+YH^2)/4,
Yp^2 Ym -> Yp (9+6XH-3XH^2+YH^2)/4, 
Ym^2 Yp -> Ym(9+6XH-3XH^2+YH^2)/4,
Yp Ym^2 -> Ym(9+6XH-3XH^2+YH^2)/4, 
Ym Yp^2 -> Yp(9+6XH-3XH^2+YH^2)/4,
Yp^3 Ym -> Yp^2 (9+6XH-3XH^2+YH^2)/4, 
Ym^3 Yp -> Ym^2(9+6XH-3XH^2+YH^2)/4,
Yp Ym^3 -> Ym^2(9+6XH-3XH^2+YH^2)/4, 
Ym Yp^3 -> Yp^2(9+6XH-3XH^2+YH^2)/4,
Yp^4 Ym -> Yp^3 (9+6XH-3XH^2+YH^2)/4, 
Ym^4 Yp -> Ym^3(9+6XH-3XH^2+YH^2)/4,
Yp Ym^4 -> Ym^3(9+6XH-3XH^2+YH^2)/4, 
Ym Yp^4 -> Yp^3(9+6XH-3XH^2+YH^2)/4,
Yp^5 Ym -> Yp^3 (9+6XH-3XH^2+YH^2)/4, 
Ym^5 Yp -> Ym^3(9+6XH-3XH^2+YH^2)/4,
Yp Ym^5 -> Ym^3(9+6XH-3XH^2+YH^2)/4, 
Ym Yp^5 -> Yp^3(9+6XH-3XH^2+YH^2)/4,
Yp^2 Ym^2 -> ( (9+6XH-3XH^2+YH^2)/4 )^2, 
Ym^2 Yp^2 -> ( (9+6XH-3XH^2+YH^2)/4 )^2,
Yp^3 Ym^2 -> Yp( (9+6XH-3XH^2+YH^2)/4 )^2, 
Ym^3 Yp^2 -> Ym( (9+6XH-3XH^2+YH^2)/4 )^2,
Yp^2 Ym^3 -> Ym( (9+6XH-3XH^2+YH^2)/4 )^2, 
Ym^2 Yp^3 -> Yp( (9+6XH-3XH^2+YH^2)/4 )^2,
Yp^4 Ym^2 -> Yp^2( (9+6XH-3XH^2+YH^2)/4 )^2, 
Ym^4 Yp^2 -> Ym^2( (9+6XH-3XH^2+YH^2)/4 )^2,
Yp^2 Ym^4 -> Ym^2( (9+6XH-3XH^2+YH^2)/4 )^2, 
Ym^2 Yp^4 -> Yp^2( (9+6XH-3XH^2+YH^2)/4 )^2,
Yp^3 Ym^3 -> ( (9+6XH-3XH^2+YH^2)/4 )^3, 
Ym^3 Yp^3 -> ( (9+6XH-3XH^2+YH^2)/4 )^3,

Xp Yp -> (XH Ym + YH Xm - 3Ym)/2, 
Yp Xp -> (XH Ym + YH Xm - 3Ym)/2, 
Xp^2 Yp -> Xp(XH Ym + YH Xm - 3Ym)/2, 
Yp^2 Xp -> Yp(XH Ym + YH Xm - 3Ym)/2, 
Xp^3 Yp -> Xp^2(XH Ym + YH Xm - 3Ym)/2, 
Yp^3 Xp -> Yp^2(XH Ym + YH Xm - 3Ym)/2, 
Xp^4 Yp -> Xp^3(XH Ym + YH Xm - 3Ym)/2, 
Yp^4 Xp -> Yp^3(XH Ym + YH Xm - 3Ym)/2, 
Xp^5 Yp -> Xp^4(XH Ym + YH Xm - 3Ym)/2, 
Yp^5 Xp -> Yp^4(XH Ym + YH Xm - 3Ym)/2, 
Xp Yp^2 -> Yp(XH Ym + YH Xm - 3Ym)/2, 
Yp Xp^2 -> Xp(XH Ym + YH Xm - 3Ym)/2, 
Xp Yp^3 -> Yp^2(XH Ym + YH Xm - 3Ym)/2, 
Yp Xp^3 -> Xp^2(XH Ym + YH Xm - 3Ym)/2, 
Xp Yp^4 -> Yp^3(XH Ym + YH Xm - 3Ym)/2, 
Yp Xp^4 -> Xp^3(XH Ym + YH Xm - 3Ym)/2, 
Xp Yp^5 -> Yp^4(XH Ym + YH Xm - 3Ym)/2, 
Yp Xp^5 -> Xp^4(XH Ym + YH Xm - 3Ym)/2, 
Xp^2 Yp^2 -> ( (XH Ym + YH Xm - 3Ym)/2 )^2, 
Yp^2 Xp^2 -> ( (XH Ym + YH Xm - 3Ym)/2 )^2, 
Xp^3 Yp^2 -> Xp( (XH Ym + YH Xm - 3Ym)/2 )^2, 
Yp^3 Xp^2 -> Yp( (XH Ym + YH Xm - 3Ym)/2 )^2, 
Xp^4 Yp^2 -> Xp^2( (XH Ym + YH Xm - 3Ym)/2 )^2, 
Yp^4 Xp^2 -> Yp^2( (XH Ym + YH Xm - 3Ym)/2 )^2, 
Xp^2 Yp^3 -> Yp( (XH Ym + YH Xm - 3Ym)/2 )^2, 
Yp^2 Xp^3 -> Xp( (XH Ym + YH Xm - 3Ym)/2 )^2, 
Xp^2 Yp^4 -> Yp^2( (XH Ym + YH Xm - 3Ym)/2 )^2, 
Yp^2 Xp^4 -> Xp^2( (XH Ym + YH Xm - 3Ym)/2 )^2, 
Xp^3 Yp^3 -> ( (XH Ym + YH Xm - 3Ym)/2 )^3, 
Yp^3 Xp^3 -> ( (XH Ym + YH Xm - 3Ym)/2 )^3, 

Xm Ym -> (XH Yp + YH Xp - 3Yp)/2, 
Ym Xm -> (XH Yp + YH Xp - 3Yp)/2, 
Xm^2 Ym -> Xm(XH Yp + YH Xp - 3Yp)/2, 
Ym^2 Xm -> Ym(XH Yp + YH Xp - 3Yp)/2, 
Xm^3 Ym -> Xm^2(XH Yp + YH Xp - 3Yp)/2, 
Ym^3 Xm -> Ym^2(XH Yp + YH Xp - 3Yp)/2, 
Xm^4 Ym -> Xm^3(XH Yp + YH Xp - 3Yp)/2, 
Ym^4 Xm -> Ym^3(XH Yp + YH Xp - 3Yp)/2, 
Xm^5 Ym -> Xm^4(XH Yp + YH Xp - 3Yp)/2, 
Ym^5 Xm -> Ym^4(XH Yp + YH Xp - 3Yp)/2, 
Xm Ym^2 -> Ym(XH Yp + YH Xp - 3Yp)/2, 
Ym Xm^2 -> Xm(XH Yp + YH Xp - 3Yp)/2, 
Xm Ym^3 -> Ym^2(XH Yp + YH Xp - 3Yp)/2, 
Ym Xm^3 -> Xm^2(XH Yp + YH Xp - 3Yp)/2, 
Xm Ym^4 -> Ym^3(XH Yp + YH Xp - 3Yp)/2, 
Ym Xm^4 -> Xm^3(XH Yp + YH Xp - 3Yp)/2, 
Xm Ym^5 -> Ym^4(XH Yp + YH Xp - 3Yp)/2, 
Ym Xm^5 -> Xm^4(XH Yp + YH Xp - 3Yp)/2, 
Xm^2 Ym^2 -> ( (XH Yp + YH Xp - 3Yp)/2 )^2, 
Ym^2 Xm^2 -> ( (XH Yp + YH Xp - 3Yp)/2 )^2, 
Xm^3 Ym^2 -> Xm( (XH Yp + YH Xp - 3Yp)/2 )^2, 
Ym^3 Xm^2 -> Ym( (XH Yp + YH Xp - 3Yp)/2 )^2, 
Xm^4 Ym^2 -> Xm^2( (XH Yp + YH Xp - 3Yp)/2 )^2, 
Ym^4 Xm^2 -> Ym^2( (XH Yp + YH Xp - 3Yp)/2 )^2, 
Xm^2 Ym^3 -> Ym( (XH Yp + YH Xp - 3Yp)/2 )^2, 
Ym^2 Xm^3 -> Xm( (XH Yp + YH Xp - 3Yp)/2 )^2, 
Xm^2 Ym^4 -> Ym^2( (XH Yp + YH Xp - 3Yp)/2 )^2, 
Ym^2 Xm^4 -> Xm^2( (XH Yp + YH Xp - 3Yp)/2 )^2, 
Xm^3 Ym^3 -> ( (XH Yp + YH Xp - 3Yp)/2 )^3, 
Ym^3 Xm^3 -> ( (XH Yp + YH Xp - 3Yp)/2 )^3, 


Xp Ym -> (2XH YH + 3YH + (ω^2-ω)Δ)/ 2, 
Ym Xp -> (2XH YH + 3YH + (ω^2-ω)Δ)/ 2, 
Xm Yp -> (2XH YH + 3YH + (ω-ω^2)Δ)/ 2, 
Yp Xm -> (2XH YH + 3YH + (ω-ω^2)Δ)/ 2, 
Ym Xp -> (2XH YH + 3YH + (ω^2-ω)Δ)/ 2, 
Xp Ym -> (2XH YH + 3YH + (ω^2-ω)Δ)/ 2, 
Yp Xm -> (2XH YH + 3YH + (ω-ω^2)Δ)/ 2, 
Xm Yp -> (2XH YH + 3YH + (ω-ω^2)Δ)/ 2, 

Δ^2 -> (1/4) (27-18 (XH^2)+8 (XH^3)-(XH^4)-18 (YH^2)-24 XH (YH^2)-2 (XH^2) (YH^2)-(YH^4)),
      
 Δ Xp -> (1/6)((1-ω) ω) (6 Xp YH+4 XH Xp YH-9 Yp+6 XH Yp-(XH^2) Yp+3 (YH^2) Yp) , 

        Δ Xm -> (1/6) ((1-ω) ω)(-6 Xm YH-4 XH Xm YH+9 Ym-6 XH Ym+(XH^2) Ym-3 (YH^2) Ym) , 

        Δ Yp -> (1/6) ((1-ω) ω)(9 Xp+6 XH Xp-3 (XH^2) Xp+Xp (YH^2)-6 YH Yp-4 XH YH Yp) , 

       Δ Ym -> (1/6) ((1-ω) ω)(-9 Xm-6 XH Xm+3 (XH^2) Xm-Xm (YH^2)+6 YH Ym+4 XH YH Ym)  

}  ;

tweak1 = {
X1-> - X2-X3,
Y1-> - Y2- Y3
};

tweak2 = {
X2-> - X3-X1,
Y2-> - Y3- Y1
};

tweak3 = {
X3-> - X1-X2,
Y3-> - Y1- Y2
};

XYΔReduce[e_] := Factor[Expand[Factor[Expand[Factor[Expand[e//. XYΔSubs]//. XYΔSubs] //. XYΔSubs]//. XYΔSubs]//. XYΔSubs]//. XYΔSubs]//. XYΔSubs

μνξSubs = {
x->((μ+XH ξ)/(1+ξ)), y->((ν+YH ξ)/(1+ξ)), z->(Sqrt[Z]), Z->(((1-(x^2)-(y^2)) (1-ξ))/(-2 ξ))
};

unμνξSubs = {
μ->((-2 x+2 (x^3)+2 x (y^2)+2 x Z+XH-(x^2) XH-(y^2) XH)/(-1+(x^2)+(y^2)+2 Z)),
ν->((-2 y+2 (x^2) y+2 (y^3)+2 y Z+YH-(x^2) YH-(y^2) YH)/(-1+(x^2)+(y^2)+2 Z)),
ξ->((-1+(x^2)+(y^2))/(-1+(x^2)+(y^2)+2 Z))
};

(* 
    Lemma 1 Check.  
    using Weierstrass Subtittuions. 
 t1 = Tan[ϕ1/2], x1 = Cos[ϕ1], y1 = Sin[ϕ1], etc. 
Since ϕ1+ϕ2+ϕ3 = 0, have t1 + t2 + t3 = t1 t2 t3.  
*)

tSubsSp

Factor[ {
x1 - (x2 x3 - y2 y3), 
x2 - (x3 x1 - y3 y1), 
x3 - (x1 x2 - y1 y2),
y1 + (x2 y3 + x3 y2), 
y2 + (x3 y1 + x1 y3), 
y3 + (x1 y2 + x2 y1), 
x1 x2 x3 - x1 y2 y3 - x2 y3 y1 - x3 y1 y2 - 1, 
y1 y2 y3 - y1 x2 x3 - y2 x3 x1 - y3 x1 x2
} //. tSubsSp]

(*     
    Lemma 2 Check.
*)

unXYΔSubs

Factor[Factor[{
(x1^2 + x2^2 + x3^2) - (1 + ((XH-1)^2-YH^2)/2), 
(y1^2 + y2^2 + y3^2) - (2 - ((XH-1)^2-YH^2)/2), 
(x2 x3 + x3 x1 + x1 x2)  -  (((XH+1)^2+YH^2)/4 - 1), 
(y2 y3 + y3 y1 + y1 y2)  -  (((XH-1)^2+YH^2)/4 - 1), 
(x1 y2+x1 y3+x2 y3+x2 y1+x3 y1+x3 y2)   +  YH, 
(x1 y1 + x2 y2 + x3 y3)  -  (XH+1)YH,
 x1 x2 x3  -  ((XH-1)^2 - YH^2)/4 , 
 y1 y2 y3  +  ((XH+1) YH)/2, 
(x1+1)(x2+1)(x3+1)  -   (XH+1)^2/2
} //. unXYΔSubs] //. tSubsSp]

(*   Lemma 3, Part (i) Check.   *)

Factor[Factor[{XH- x1, YH - y1}. {x2 -x3, y2-y3} //. unXYΔSubs] //. tSubsSp]

(*   Lemma 3, Part (ii) Check.   *)

DSubs

Factor[Factor[Factor[{
D1 D2 D3 / 16, 
(1-x2 x3-y2 y3)(1-x3 x1-y3 y1)(1-x1 x2-y1 y2) / 2,   (* TYPO IN PAPER *) 
(2D2 D3+2D3 D1+2D1 D2-D1^2-D2^2-D3^2) / 16, 
(x1 y2+x2 y3+x3 y1-x1 y3-x2 y1-x3 y2)^2 / 4, 
((x1-x2)(x2-x3)(x3-x1) / YH )^2 , 
((y1-y2)(y2-y3)(y3-y1) / (XH+1))^2, 
(27 + 8XH(XH^2-3YH^2)-(XH^2+YH^2)(XH^2+YH^2+18)) / 16 
} /. DSubs] //. unXYΔSubs] //. tSubsSp]

Factor[{%[[1]]/%[[2]],%[[2]]/%[[3]],%[[3]]/%[[4]],%[[4]]/%[[5]],%[[5]]/%[[6]],%[[6]]/%[[7]]}]

(* Lemma 4 Check. *)

list = { 
X1^2, 
X2 X3, 
Y1^2, 
Y2 Y3, 
X1 Y1, 
X2 Y3, 
X3 Y2, 
X1 Δ, 
Y1 Δ, 
Δ^2 
}

Factor[list] /. XYΔSubs

{
(1/2) (9+3 X1-6 XH-X1 XH+(XH^2)-3 Y1 YH-3 (YH^2)),
(1/4) (-9+6 XH-(XH^2)+3 (YH^2)+2 (3 X1-X1 XH-3 Y1 YH)),
(1/2) (9-3 X1+6 XH-3 X1 XH-3 (XH^2)-Y1 YH+(YH^2)),
(1/4) (-9-6 XH+3 (XH^2)-(YH^2)+2 (-3 X1-3 X1 XH-Y1 YH)),
(1/2) (-3 Y1+XH Y1+X1 YH+2 (3 YH+2 XH YH)),
(1/2) (-3 Y1+XH Y1-3 YH+X1 YH-2 XH YH+3 Δ),
(1/2) (-3 Y1+XH Y1-3 YH+X1 YH-2 XH YH-3 Δ),
(1/6) (2 (-X2+X3) (3+2 XH) YH+(Y2-Y3) (9-6 XH+(XH^2)-3 (YH^2))),
(1/6) (2 (3+2 XH) (Y2-Y3) YH+(-X2+X3) (9+6 XH-3 (XH^2)+(YH^2))),
(1/4) (27-18 (XH^2)+8 (XH^3)-(XH^4)-18 (YH^2)-24 XH (YH^2)-2 (XH^2) (YH^2)-(YH^4))
}

list1 = Factor[ list /. unXYΔSubs]

list2 = Factor[list1 //. tSubsSp]

list3 = Factor[XYΔReduce[list1] /. tweak3]

list4 = Factor[ list3 /. unXYΔSubs]

list5 = Factor[list4 //. tSubsSp]

Factor[list2 - list5]

(* Lemma 5 Check. *)

H = 1-c1^2-c2^2-c3^2+2 c1 c2 c3    (*  H = η^2  *)

Factor[Factor[Factor[Factor[Factor[  { 
D1 - ( (x2-x3)^2+(y2-y3)^2 ), 
D1 - 2(1-x2 x3 - y2 y3), 
R1 - (1 - 2(x1 x+y1 y) + x^2+y^2+z^2), 
(R2+R3-D1) / 2 - ((x-x2)(x-x3)+(y-y2)(y-y3)+z^2),         (* TYPO IN PAPER *) 
4 R1 R2 R3 H - D1 D2 D3 z^2,
4 R1 R2 R3 c1^2 - R1(R2+R3-D1)^2  , 
8 R1 R2 R3 c1 c2 c3  -  (R2+R3-D1)(R3+R1-D2)(R1+R2-D3) , 
c1^2 / H  -  R1(R2+R3-D1)^2 / (D1 D2 D3 z^2) , 
c1 c2 c3 / H  -  (R2+R3-D1)(R3+R1-D2)(R1+R2-D3) / (2D1 D2 D3 z^2) 
}  /. cSubs ] /. r2RSubs] /. DRSubs] /. Z->z^2] /. tSubsSp]

(*  Lemma 6 Check.  *)

Factor[Factor[Factor[Factor[  { 
x1 - (XH+X1)/3, 
y1 - (YH+Y1)/3, 
(1-x1)y1  -  ((3-XH)Y1 - YH X1- 2 XH YH) / 6, 
(1+x1) x1  -  ((3+XH)X1 - YH Y1 + XH^2 - YH^2 + 3) / 6 , 
 D1  -  ((9-XH^2-YH^2) + 2(XH X1+YH Y1))/ 3 , 
 R1  -  (1+x^2+y^2+z^2 - 2((XH+X1)x+(YH+Y1)y)/3 ) , 
 (R2 + R3 - D1)    -  (2(x^2+y^2+z^2)-1 + (2(X1-2XH)x+2(Y1-2YH)y+(XH^2+YH^2-2XH X1-2YH Y1))/3) 
}  /. DRSubs] /. Z->z^2] /. unXYΔSubs ] //. tSubsSp]

(*  Lemma 7 Check.  *)

Factor[ XYΔReduce[Factor[Factor[  { 
R1 R2 R3 
}  /. DRSubs] /. Z->z^2]] /. tweak3]

Factor[CoefficientList[% , {z,y,x}]]

{
{
{
{1,-2 XH,2 XH+(XH^2)+(YH^2),-2 (1+(XH^2)-(YH^2)),2 XH+(XH^2)+(YH^2),-2 XH,1},
{-2 YH,-4 YH,4 XH YH,-4 YH,-2 YH,0,0},
{-2 XH+(XH^2)+(YH^2),-2 (-3+(XH^2)-(YH^2)),2 ((XH^2)+(YH^2)),-4 XH,3,0,0},
{4 XH YH,-4 YH,-4 YH,0,0,0,0},
{-2 XH+(XH^2)+(YH^2),-2 XH,3,0,0,0,0},
{-2 YH,0,0,0,0,0,0},
{1,0,0,0,0,0,0}
},{
{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0}
},{
{3,-4 XH,3+2 XH+(XH^2)+(YH^2),-4 XH,3,0,0},
{-4 YH,-4 YH,-4 YH,0,0,0,0},
{3-2 XH+(XH^2)+(YH^2),-4 XH,6,0,0,0,0},
{-4 YH,0,0,0,0,0,0},
{3,0,0,0,0,0,0},
{0,0,0,0,0,0,0},{0,0,0,0,0,0,0}
},{
{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0}
},{
{3,-2 XH,3,0,0,0,0},
{-2 YH,0,0,0,0,0,0},
{3,0,0,0,0,0,0},
{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0}
},{
{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0}
},{
{1,0,0,0,0,0,0},
{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0}}
}
}

Factor[ XYΔReduce[Factor[Factor[  { 
(R2+R3-D1)(R3+R1-D2)(R1+R2-D3) 
}  /. DRSubs] /. Z->z^2]] /. tweak3]

Factor[CoefficientList[% , {z,y,x}]]

{
{
{
{-1+4 (XH^2)-4 (XH^3)+(XH^4)+4 (YH^2)+12 XH (YH^2)+2 (XH^2) (YH^2)+(YH^4),-2 (-XH+(XH^2)-(YH^2)) (-5+(XH^2)+(YH^2)),9-8 XH-18 (XH^2)+8 (XH^3)+(XH^4)-10 (YH^2)-8 XH (YH^2)+2 (XH^2) (YH^2)+(YH^4),-2 (-1-15 XH+5 (XH^2)+3 (XH^3)-3 (YH^2)+3 XH (YH^2)),2 (-9+2 XH+7 (XH^2)+3 (YH^2)),-16 XH,8},
{2 (1+2 XH) YH (-5+(XH^2)+(YH^2)),-8 YH (-2+2 XH+(XH^2)+(YH^2)),-2 YH (-15-8 XH+3 (XH^2)+3 (YH^2)),8 (-1+2 XH) YH,-16 YH,0,0},{9+8 XH-10 (XH^2)+(XH^4)-18 (YH^2)-16 XH (YH^2)+2 (XH^2) (YH^2)+(YH^4),-2 (3-15 XH+(XH^2)+3 (XH^3)-7 (YH^2)+3 XH (YH^2)),4 (-9+5 (XH^2)+5 (YH^2)),-32 XH,24,0,0},
{-2 YH (-15-8 XH+3 (XH^2)+3 (YH^2)),8 (-1+2 XH) YH,-32 YH,0,0,0,0},
{2 (-9-2 XH+3 (XH^2)+7 (YH^2)),-16 XH,24,0,0,0,0},
{-16 YH,0,0,0,0,0,0},
{8,0,0,0,0,0,0}
},{
{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0}
},{
{2 (3-5 (XH^2)+2 (XH^3)-5 (YH^2)-6 XH (YH^2)),-4 (-7 XH+2 (XH^2)+(XH^3)-2 (YH^2)+XH (YH^2)),2 (-15+2 XH+9 (XH^2)+5 (YH^2)),-32 XH,24,0,0},
{-4 YH (-7-4 XH+(XH^2)+(YH^2)),8 (-1+2 XH) YH,-32 YH,0,0,0,0},
{2 (-15-2 XH+5 (XH^2)+9 (YH^2)),-32 XH,48,0,0,0,0},
{-32 YH,0,0,0,0,0,0},
{24,0,0,0,0,0,0},
{0,0,0,0,0,0,0},{0,0,0,0,0,0,0}
},{
{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0}
},{
{4 (-3+(XH^2)+(YH^2)),-16 XH,24,0,0,0,0},
{-16 YH,0,0,0,0,0,0},
{24,0,0,0,0,0,0},
{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0}
},{
{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0}
},{
{8,0,0,0,0,0,0},
{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0},{0,0,0,0,0,0,0}}
}
}

(*  Lemma 8 Check.  *)

Factor[Factor[ Factor[ Factor[ (α+β c1 c2 c3+γ1 c1^2+γ2 c2^2+γ3 c3^2) / H /. cSubs] /. r2RSubs] /. DRSubs] /. Z->z^2]

{Numerator[%], Denominator[%]}

Factor[CoefficientList[%, z]]

{Length[%[[1]]], Length[%[[2]]]}

Factor[ %%[[1]][[7]] z^4 / %%[[2]][[3]] ]

Factor[ XYΔReduce[ (((x2 y1-x3 y1-x1 y2+x3 y2+x1 y3-x2 y3))^2) /. DSubs] /. tweak3]

Factor[ XYΔReduce[ D1 D2 D3 / 4 /. DSubs] /. tweak3]

Factor[%%-%]

(*  Lemma 9 Check.  *)

Factor[Factor[ Factor[ Factor[ (β (c1 c2 c3-1)+γ1 (c1^2-1)+γ2 (c2^2-1)+γ3 (c3^2-1)) / H /. cSubs] /. r2RSubs] /. DRSubs] /. Z->z^2]

{Numerator[%], Denominator[%]}

Factor[CoefficientList[%, z]]

{Length[%[[1]]], Length[%[[2]]]}

ratio = Factor[ Factor[ %%[[1]][[5]] z^2 / %%[[2]][[3]] ] /. ySubs]

ratio2 = Factor[Factor[Factor[ -4 ( ( (9-XH^2-YH^2)/2) β + D1 γ1 + D2 γ2 + D3 γ3 ) z^2  / (D1 D2 D3)  /. unXYΔSubs] /. DSubs] //. ySubs]

Factor[%%/%]

Factor[% /.tSubsSp]

(*   Lemma 11 Check.  *)

ι = 3-x2 x3-x3 x1-x1 x2-y2 y3-y3 y1-y1 y2

Factor[Factor[2 ι - D1 - D2 - D3 /. DSubs] //. ySubs]

(* So H is of form (4) and satisfies (5) *)

LL =  (2/H) ((1-x1)y1(c1^2-1)+(1-x2)y2(c2^2-1)+(1-x3)y3(c3^2-1)+(y1+y2+y3)(1-c1 c2 c3))

Factor[CoefficientList[Numerator[%],{c3,c2,c1}]]

Factor[Factor[Factor[%[[2]][[2]][[2]] ι + %[[1]][[1]][[3]] D1  + %[[1]][[3]][[1]] D2  + %[[3]][[1]][[1]] D3] /. DSubs] //. tSubsSp]

RR = (2/H) ((1+x1)x1(c1^2-1)+(1+x2)x2(c2^2-1)+(1+x3)x3(c3^2-1)+(1+x1+x2+x3)(1-c1 c2 c3))

Factor[CoefficientList[Numerator[%],{c3,c2,c1}]]

Factor[Factor[Factor[%[[2]][[2]][[2]] ι + %[[1]][[1]][[3]] D1  + %[[1]][[3]][[1]] D2  + %[[3]][[1]][[1]] D3] /. DSubs] //. tSubsSp]

(*   Theorem 1 Check.  *)

H = 1-c1^2-c2^2-c3^2+2 c1 c2 c3    (*  H = η^2  *)

LL =  (2/H) ((1-x1)y1(c1^2-1)+(1-x2)y2(c2^2-1)+(1-x3)y3(c3^2-1)+(y1+y2+y3)(1-c1 c2 c3))

RR = (2/H) ((1+x1)x1(c1^2-1)+(1+x2)x2(c2^2-1)+(1+x3)x3(c3^2-1)+(1+x1+x2+x3)(1-c1 c2 c3))

Factor[Factor[Factor[Factor[Factor[Factor[Factor[Factor[ LL /. cSubs] /. r2RSubs] /. DRSubs] //. tSubsSp] /. untSubs] //. ySubs] //. ySubs]/. Z->z^2]

Factor[ XYΔReduce[ % ] /. tweak3]

{Numerator[%], Denominator[%]}

Factor[CoefficientList[%[[1]], z]]

LLL = UnCoefficientList[ % , z] / z^2

Factor[Factor[Factor[Factor[Factor[Factor[Factor[Factor[  RR  /. cSubs] /. r2RSubs] /. DRSubs] //. tSubsSp] /. untSubs] //. ySubs] //. ySubs]/. Z->z^2]

Factor[ XYΔReduce[ % ] /. tweak3]

{Numerator[%], Denominator[%]}

Factor[CoefficientList[%[[1]], z]]

RRR = UnCoefficientList[ % , z] / z^2

(*  Corollary 1 Check.  *)

Factor[ H * ((1+x3)LL + y3 RR + 2(1+x3)y3)/(y1-y2)]

Factor[Factor[CoefficientList[%, {c3,c2,c1}]] //. special]

Factor[% //. tSubsSp]

%[[1]]

Factor[D1(1-c2^2)-D2(1-c1^2) /. DSubs]

Factor[Factor[Factor[CoefficientList[%, {c3,c2,c1}]]//. ySubs]//.special]

Factor[% //. tSubsSp]

%[[1]]

Factor[%%%%%-%]

Factor[ ((1+x3)LLL + y3 RRR + 2(1+x3)y3)/(y1-y2) /. unXYΔSubs]

Factor[% //. tSubsSp]

Factor[
2(1+x3)y3/(y1-y2) +  (y3/(y1-y2))(y^2-(x-1)^2)  +  ((1+x3)/(y1-y2))(2(x+1)y)  +
( (1+2x3)y3/(y1-y2) - (y3/(y1-y2))(y^2-x^2 ) - ((1+x3)/(y1-y2))(2x y) + 
(2(x1+x2)x3/(y1-y2)) y  - (2(x1+x2)y3/(y1-y2)) x  ) (1-x^2-y^2)/z^2
]

Factor[% //. tSubsSp]

Factor[ %%%-% ]

temp  =  Factor[ Factor[ Factor[ 

2(1+x3)* {(1-x1)y1,(1-x2)y2,(1-x3)y3,-(y1+y2+y3)} + 

2y3  * {(1+x1)x1,(1+x2)x2,(1+x3)x3,-(1+x1+x2+x3)} + 

2(1+x3)y3 {-1,-1,-1,2} 

] //. ySubs]//. ySubs]

Factor[Factor[(y1-y2){D2, -D1, 0, 0} /. DSubs //. ySubs]//. ySubs]

Factor[temp - % //. tSubsSp]

Factor[temp - 
2{
y1-y3-x1 y1-x3 y3+x1 y3+x3 y1+x1^2 y3-x1 x3 y1,
y2-y3-x2 y2-x3 y3+x2 y3+x3 y2+x2^2 y3-x2 x3 y2,
0,
-(y1+y2+x1 y3+x2 y3+x3 y1+x3 y2) 
} ]

A3 = (  (y1+y2-y3)((y+y3)^2 -(x+x3)^2)- 
        2(1+x1+x2+x3)(x+x3)(y+y3)  )   / 
                    (-y1+y2+y3+2x1 y2)

B3 = (x1-x2)(1+2x3)/2    +  
 
      (  (y3-y1-y2)((y-(y1+y2)/2)^2 - (x-(x1+x2)/2)^2)   +   
       2(1+x1+x2+x3)(x-(x1+x2)/2)(y-(y1+y2)/2)   )      / 
                  (-y1+y2+y3+2x1 y2)

T3 = Factor[Factor[Factor[Factor[Factor[A3+B3(1-x^2-y^2)/z^2] //. ySubs]//. ySubs]//.special]//.special]

TT3 = Factor[Factor[Factor[Factor[Factor[Factor[Factor[ (D1(1-c2^2)-D2(1-c1^2))/H /. cSubs] /. r2RSubs] /. DRSubs /. Z->z^2] //.ySubs]//.ySubs]//.special]//.special]

Factor[Factor[T3-TT3]//. tSubsSp]

TTT3 = Factor[((1+x3)LLL + y3 RRR + 2(1+x3)y3)/(y1-y2)  /. unXYΔSubs]

Factor[Factor[T3-TTT3]//. tSubsSp]

{Numerator[T3],Denominator[T3]}

Factor[ % /. (y1-y2-2 x1 y2-y3) -> (2(1+x1)(1+x2)(y1-y2))/(1+x1+x2+x3) ]

T30 = Factor[%[[1]]/%[[2]]]

Factor[Factor[T3-T30]//. tSubsSp]

Factor[Factor[TTT3-T30]//. tSubsSp]

thing1 =
(1+x1+x2+x3) (4 y+4 x y-4 (x^2) y-4 (x^3) y+4 x x1 y-4 (x^3) x1 y-4 (x1^2) y+4 (x^2) (x1^2) y+4 x x2 y-4 (x^3) x2 y-4 (x2^2) y+4 (x^2) (x2^2) y-4 x3 y+4 x x3 y+4 (x^2) x3 y-4 (x^3) x3 y-4 x1 x3 y+4 (x^2) x1 x3 y-4 x2 x3 y+4 (x^2) x2 x3 y-4 (y^3)-4 x (y^3)-4 x x1 (y^3)+4 (x1^2) (y^3)-4 x x2 (y^3)+4 (x2^2) (y^3)+4 x3 (y^3)-4 x x3 (y^3)+4 x1 x3 (y^3)+4 x2 x3 (y^3)-2 y1+4 (x^2) y1-2 (x^4) y1-4 x1 y1-4 x x1 y1+4 (x^2) x1 y1+4 (x^3) x1 y1-2 (x1^2) y1+2 (x^2) (x1^2) y1-4 x1 x2 y1+4 (x^2) x1 x2 y1+3 (x2^2) y1-3 (x^2) (x2^2) y1+4 x1 (y^2) y1+4 x x1 (y^2) y1+2 (x1^2) (y^2) y1+4 x1 x2 (y^2) y1-3 (x2^2) (y^2) y1+2 (y^4) y1-14 y2+16 (x^2) y2-2 (x^4) y2+14 (x1^2) y2-14 (x^2) (x1^2) y2-4 x2 y2-4 x x2 y2+4 (x^2) x2 y2+4 (x^3) x2 y2+x1 x2 y2-(x^2) x1 x2 y2+10 (x2^2) y2-10 (x^2) (x2^2) y2-16 x1 x2 x3 y2+16 (x^2) x1 x2 x3 y2+12 (y^2) y2-14 (x1^2) (y^2) y2+4 x2 (y^2) y2+4 x x2 (y^2) y2-x1 x2 (y^2) y2-10 (x2^2) (y^2) y2+16 x1 x2 x3 (y^2) y2+2 (y^4) y2+12 (y1^2) y2-12 (x^2) (y1^2) y2-12 (y^2) (y1^2) y2-2 y3+4 x y3-4 (x^3) y3+2 (x^4) y3-2 x1 y3+4 x x1 y3+2 (x^2) x1 y3-4 (x^3) x1 y3-x2 y3+4 x x2 y3+(x^2) x2 y3-4 (x^3) x2 y3-8 x1 x2 y3+8 (x^2) x1 x2 y3-4 (x1^2) x2 y3+4 (x^2) (x1^2) x2 y3-4 x1 (x2^2) y3+4 (x^2) x1 (x2^2) y3+2 x1 x3 y3-2 (x^2) x1 x3 y3-2 x2 x3 y3+2 (x^2) x2 x3 y3+4 (y^2) y3-4 x (y^2) y3+2 x1 (y^2) y3-4 x x1 (y^2) y3+x2 (y^2) y3-4 x x2 (y^2) y3+8 x1 x2 (y^2) y3+4 (x1^2) x2 (y^2) y3+4 x1 (x2^2) (y^2) y3-2 x1 x3 (y^2) y3+2 x2 x3 (y^2) y3-2 (y^4) y3+8 x2 y1 y2 y3-8 (x^2) x2 y1 y2 y3-8 x2 (y^2) y1 y2 y3-4 y (z^2)-4 x y (z^2)-4 x1 y (z^2)-4 x x1 y (z^2)-4 x2 y (z^2)-4 x x2 y (z^2)-4 x3 y (z^2)-4 x x3 y (z^2)+2 y1 (z^2)+4 x y1 (z^2)-2 (x^2) y1 (z^2)-4 (x3^2) y1 (z^2)+2 (y^2) y1 (z^2)+2 y2 (z^2)+4 x y2 (z^2)-2 (x^2) y2 (z^2)-4 (x3^2) y2 (z^2)+2 (y^2) y2 (z^2)-2 y3 (z^2)-4 x y3 (z^2)+2 (x^2) y3 (z^2)-4 x3 y3 (z^2)-4 x1 x3 y3 (z^2)-4 x2 x3 y3 (z^2)-2 (y^2) y3 (z^2))

thing2 = 
4 (1+x1) (1+x2) (y+2 x y-(x^2) y-2 (x^3) y-x1 y+(x^2) x1 y-x2 y+(x^2) x2 y+2 x x3 y-2 (x^3) x3 y-x1 x3 y+(x^2) x1 x3 y-x2 x3 y+(x^2) x2 x3 y-(x3^2) y+(x^2) (x3^2) y-(y^3)-2 x (y^3)+x1 (y^3)+x2 (y^3)-2 x x3 (y^3)+x1 x3 (y^3)+x2 x3 (y^3)+(x3^2) (y^3)-y1-x y1+(x^2) y1+(x^3) y1-x3 y1-x x3 y1+(x^2) x3 y1+(x^3) x3 y1+(y^2) y1+x (y^2) y1+x3 (y^2) y1+x x3 (y^2) y1-y2-x y2+(x^2) y2+(x^3) y2-x3 y2-x x3 y2+(x^2) x3 y2+(x^3) x3 y2+(y^2) y2+x (y^2) y2+x3 (y^2) y2+x x3 (y^2) y2-y3+(x^4) y3-x1 y3+x x1 y3+(x^2) x1 y3-(x^3) x1 y3-x2 y3+x x2 y3+(x^2) x2 y3-(x^3) x2 y3-2 x3 y3+2 (x^2) x3 y3+2 (y^2) y3+x1 (y^2) y3-x x1 (y^2) y3+x2 (y^2) y3-x x2 (y^2) y3+2 x3 (y^2) y3-(y^4) y3-y y1 y3+(x^2) y y1 y3+(y^3) y1 y3-y y2 y3+(x^2) y y2 y3+(y^3) y2 y3-y (y3^2)+(x^2) y (y3^2)+(y^3) (y3^2)-2 y (z^2)-2 x y (z^2)-2 x3 y (z^2)-2 x x3 y (z^2)-y3 (z^2)-2 x y3 (z^2)+(x^2) y3 (z^2)-2 x3 y3 (z^2)-(y^2) y3 (z^2))

Factor[XYΔReduce[thing1]//. tweak3]

Factor[XYΔReduce[thing2] //. tweak3]

Factor[%%-%]

list1 = Factor[CoefficientList[thing1, {z,y,x}]]

list2 = Factor[CoefficientList[thing2, {z,y,x}]]

Factor[ list1-list2 //. tSubsSp]

Factor[XYΔReduce[list1]//. tweak3]

Factor[XYΔReduce[list2]//. tweak3]

Factor[%%-%]

(* Lemma 12 Check.  *)

deltoid = (L^2 + (R+1)^2)^2 + 8(R+1)((R+1)^2 - 3L^2) + 18(L^2+(R+1)^2) - 27

Factor[deltoid /. {L -> 2(x+1)y, R-> y^2-(x-1)^2}]

Factor[(x^2+y^2-1)^2 ((x^2+y^2)^2 + 8x(3y^2-x^2) + 18(x^2+y^2) - 27) ]

Factor[%%/%]

LLL

RRR

Factor[ y(LLL-2(x+1)y) - (x+1)(RRR - y^2 + (x-1)^2) ]

Factor[Factor[deltoid /. {L ->LLL, R-> RRR}] /. z->Sqrt[Z]]

(* Lemma 13 Check.  *)

p[XH_,YH_,x_,y_,Z_] := ((x^4)-4 (x^5)+4 (x^6)+4 (x^7)-10 (x^8)+4 (x^9)+4 (x^10)-4 (x^11)+(x^12)-4 (x^3) XH+16 (x^4) XH-16 (x^5) XH-16 (x^6) XH+40 (x^7) XH-16 (x^8) XH-16 (x^9) XH+16 (x^10) XH-4 (x^11) XH+6 (x^2) (XH^2)-24 (x^3) (XH^2)+24 (x^4) (XH^2)+24 (x^5) (XH^2)-60 (x^6) (XH^2)+24 (x^7) (XH^2)+24 (x^8) (XH^2)-24 (x^9) (XH^2)+6 (x^10) (XH^2)-4 x (XH^3)+16 (x^2) (XH^3)-16 (x^3) (XH^3)-16 (x^4) (XH^3)+40 (x^5) (XH^3)-16 (x^6) (XH^3)-16 (x^7) (XH^3)+16 (x^8) (XH^3)-4 (x^9) (XH^3)+(XH^4)-4 x (XH^4)+4 (x^2) (XH^4)+4 (x^3) (XH^4)-10 (x^4) (XH^4)+4 (x^5) (XH^4)+4 (x^6) (XH^4)-4 (x^7) (XH^4)+(x^8) (XH^4)+2 (x^2) (y^2)+8 (x^3) (y^2)-24 (x^4) (y^2)-4 (x^5) (y^2)+32 (x^6) (y^2)-16 (x^8) (y^2)-4 (x^9) (y^2)+6 (x^10) (y^2)-4 x XH (y^2)-24 (x^2) XH (y^2)+64 (x^3) XH (y^2)+8 (x^4) XH (y^2)-72 (x^5) XH (y^2)-8 (x^6) XH (y^2)+32 (x^7) XH (y^2)+24 (x^8) XH (y^2)-20 (x^9) XH (y^2)+2 (XH^2) (y^2)+24 x (XH^2) (y^2)-56 (x^2) (XH^2) (y^2)+36 (x^4) (XH^2) (y^2)+24 (x^5) (XH^2) (y^2)-8 (x^6) (XH^2) (y^2)-48 (x^7) (XH^2) (y^2)+26 (x^8) (XH^2) (y^2)-8 (XH^3) (y^2)+16 x (XH^3) (y^2)-8 (x^2) (XH^3) (y^2)+16 (x^3) (XH^3) (y^2)-24 (x^4) (XH^3) (y^2)-16 (x^5) (XH^3) (y^2)+40 (x^6) (XH^3) (y^2)-16 (x^7) (XH^3) (y^2)+4 x (XH^4) (y^2)-12 (x^2) (XH^4) (y^2)+8 (x^3) (XH^4) (y^2)+8 (x^4) (XH^4) (y^2)-12 (x^5) (XH^4) (y^2)+4 (x^6) (XH^4) (y^2)+(y^4)+12 x (y^4)+36 (x^2) (y^4)-20 (x^3) (y^4)-36 (x^4) (y^4)-24 (x^5) (y^4)-8 (x^6) (y^4)+24 (x^7) (y^4)+15 (x^8) (y^4)-8 XH (y^4)-48 x XH (y^4)+32 (x^2) XH (y^4)-8 (x^3) XH (y^4)+40 (x^4) XH (y^4)+64 (x^5) XH (y^4)-32 (x^6) XH (y^4)-40 (x^7) XH (y^4)+16 (XH^2) (y^4)-24 x (XH^2) (y^4)+60 (x^2) (XH^2) (y^4)-24 (x^3) (XH^2) (y^4)-72 (x^4) (XH^2) (y^4)+44 (x^6) (XH^2) (y^4)+8 (XH^3) (y^4)-24 x (XH^3) (y^4)+16 (x^3) (XH^3) (y^4)+24 (x^4) (XH^3) (y^4)-24 (x^5) (XH^3) (y^4)-2 (XH^4) (y^4)+4 x (XH^4) (y^4)+4 (x^2) (XH^4) (y^4)-12 (x^3) (XH^4) (y^4)+6 (x^4) (XH^4) (y^4)-12 x (y^6)-80 (x^2) (y^6)-32 (x^3) (y^6)+48 (x^4) (y^6)+56 (x^5) (y^6)+20 (x^6) (y^6)+8 XH (y^6)+104 x XH (y^6)+40 (x^2) XH (y^6)-32 (x^3) XH (y^6)-80 (x^4) XH (y^6)-40 (x^5) XH (y^6)-36 (XH^2) (y^6)-24 x (XH^2) (y^6)-24 (x^2) (XH^2) (y^6)+48 (x^3) (XH^2) (y^6)+36 (x^4) (XH^2) (y^6)+8 (XH^3) (y^6)+16 x (XH^3) (y^6)-8 (x^2) (XH^3) (y^6)-16 (x^3) (XH^3) (y^6)-4 x (XH^4) (y^6)+4 (x^2) (XH^4) (y^6)-2 (y^8)-12 x (y^8)+36 (x^2) (y^8)+44 (x^3) (y^8)+15 (x^4) (y^8)+8 XH (y^8)-48 x XH (y^8)-48 (x^2) XH (y^8)-20 (x^3) XH (y^8)+16 (XH^2) (y^8)+24 x (XH^2) (y^8)+14 (x^2) (XH^2) (y^8)-8 (XH^3) (y^8)-4 x (XH^3) (y^8)+(XH^4) (y^8)+12 x (y^10)+6 (x^2) (y^10)-8 XH (y^10)-4 x XH (y^10)+2 (XH^2) (y^10)+(y^12)-4 (x^2) y YH-8 (x^3) y YH+32 (x^4) y YH+8 (x^5) y YH-56 (x^6) y YH+8 (x^7) y YH+32 (x^8) y YH-8 (x^9) y YH-4 (x^10) y YH+8 x XH y YH+24 (x^2) XH y YH-80 (x^3) XH y YH-24 (x^4) XH y YH+144 (x^5) XH y YH-24 (x^6) XH y YH-80 (x^7) XH y YH+24 (x^8) XH y YH+8 (x^9) XH y YH-4 (XH^2) y YH-24 x (XH^2) y YH+64 (x^2) (XH^2) y YH+24 (x^3) (XH^2) y YH-120 (x^4) (XH^2) y YH+24 (x^5) (XH^2) y YH+64 (x^6) (XH^2) y YH-24 (x^7) (XH^2) y YH-4 (x^8) (XH^2) y YH+8 (XH^3) y YH-16 x (XH^3) y YH-8 (x^2) (XH^3) y YH+32 (x^3) (XH^3) y YH-8 (x^4) (XH^3) y YH-16 (x^5) (XH^3) y YH+8 (x^6) (XH^3) y YH-4 (y^3) YH-40 x (y^3) YH-96 (x^2) (y^3) YH+48 (x^3) (y^3) YH+152 (x^4) (y^3) YH+56 (x^5) (y^3) YH-32 (x^6) (y^3) YH-64 (x^7) (y^3) YH-20 (x^8) (y^3) YH+24 XH (y^3) YH+112 x XH (y^3) YH-48 (x^2) XH (y^3) YH-96 (x^3) XH (y^3) YH-72 (x^4) XH (y^3) YH-48 (x^5) XH (y^3) YH+96 (x^6) XH (y^3) YH+32 (x^7) XH (y^3) YH-32 (XH^2) (y^3) YH+24 x (XH^2) (y^3) YH-48 (x^2) (XH^2) (y^3) YH+48 (x^3) (XH^2) (y^3) YH+96 (x^4) (XH^2) (y^3) YH-72 (x^5) (XH^2) (y^3) YH-16 (x^6) (XH^2) (y^3) YH-8 (XH^3) (y^3) YH+32 x (XH^3) (y^3) YH-16 (x^2) (XH^3) (y^3) YH-32 (x^3) (XH^3) (y^3) YH+24 (x^4) (XH^3) (y^3) YH+40 x (y^5) YH+216 (x^2) (y^5) YH+88 (x^3) (y^5) YH-160 (x^4) (y^5) YH-144 (x^5) (y^5) YH-40 (x^6) (y^5) YH-24 XH (y^5) YH-240 x XH (y^5) YH-72 (x^2) XH (y^5) YH+144 (x^3) XH (y^5) YH+144 (x^4) XH (y^5) YH+48 (x^5) XH (y^5) YH+72 (XH^2) (y^5) YH+24 x (XH^2) (y^5) YH-72 (x^3) (XH^2) (y^5) YH-24 (x^4) (XH^2) (y^5) YH-8 (XH^3) (y^5) YH-16 x (XH^3) (y^5) YH+24 (x^2) (XH^3) (y^5) YH+8 (y^7) YH+40 x (y^7) YH-96 (x^2) (y^7) YH-128 (x^3) (y^7) YH-40 (x^4) (y^7) YH-24 XH (y^7) YH+112 x XH (y^7) YH+96 (x^2) XH (y^7) YH+32 (x^3) XH (y^7) YH-32 (XH^2) (y^7) YH-24 x (XH^2) (y^7) YH-16 (x^2) (XH^2) (y^7) YH+8 (XH^3) (y^7) YH-40 x (y^9) YH-20 (x^2) (y^9) YH+24 XH (y^9) YH+8 x XH (y^9) YH-4 (XH^2) (y^9) YH-4 (y^11) YH+2 (x^2) (YH^2)-8 (x^4) (YH^2)+12 (x^6) (YH^2)-8 (x^8) (YH^2)+2 (x^10) (YH^2)-4 x XH (YH^2)+16 (x^3) XH (YH^2)-24 (x^5) XH (YH^2)+16 (x^7) XH (YH^2)-4 (x^9) XH (YH^2)+2 (XH^2) (YH^2)-8 (x^2) (XH^2) (YH^2)+12 (x^4) (XH^2) (YH^2)-8 (x^6) (XH^2) (YH^2)+2 (x^8) (XH^2) (YH^2)+6 (y^2) (YH^2)+48 x (y^2) (YH^2)+88 (x^2) (y^2) (YH^2)-48 (x^3) (y^2) (YH^2)-180 (x^4) (y^2) (YH^2)-48 (x^5) (y^2) (YH^2)+72 (x^6) (y^2) (YH^2)+48 (x^7) (y^2) (YH^2)+14 (x^8) (y^2) (YH^2)-24 XH (y^2) (YH^2)-80 x XH (y^2) (YH^2)+24 (x^2) XH (y^2) (YH^2)+144 (x^3) XH (y^2) (YH^2)+24 (x^4) XH (y^2) (YH^2)-48 (x^5) XH (y^2) (YH^2)-24 (x^6) XH (y^2) (YH^2)-16 (x^7) XH (y^2) (YH^2)+16 (XH^2) (y^2) (YH^2)-24 (x^2) (XH^2) (y^2) (YH^2)+8 (x^6) (XH^2) (y^2) (YH^2)-48 x (y^4) (YH^2)-204 (x^2) (y^4) (YH^2)-96 (x^3) (y^4) (YH^2)+168 (x^4) (y^4) (YH^2)+144 (x^5) (y^4) (YH^2)+36 (x^6) (y^4) (YH^2)+24 XH (y^4) (YH^2)+168 x XH (y^4) (YH^2)+48 (x^2) XH (y^4) (YH^2)-144 (x^3) XH (y^4) (YH^2)-72 (x^4) XH (y^4) (YH^2)-24 (x^5) XH (y^4) (YH^2)-36 (XH^2) (y^4) (YH^2)+24 (x^2) (XH^2) (y^4) (YH^2)+12 (x^4) (XH^2) (y^4) (YH^2)-12 (y^6) (YH^2)-48 x (y^6) (YH^2)+88 (x^2) (y^6) (YH^2)+144 (x^3) (y^6) (YH^2)+44 (x^4) (y^6) (YH^2)+24 XH (y^6) (YH^2)-80 x XH (y^6) (YH^2)-72 (x^2) XH (y^6) (YH^2)-16 (x^3) XH (y^6) (YH^2)+16 (XH^2) (y^6) (YH^2)+8 (x^2) (XH^2) (y^6) (YH^2)+48 x (y^8) (YH^2)+26 (x^2) (y^8) (YH^2)-24 XH (y^8) (YH^2)-4 x XH (y^8) (YH^2)+2 (XH^2) (y^8) (YH^2)+6 (y^10) (YH^2)-4 y (YH^3)-24 x y (YH^3)-32 (x^2) y (YH^3)+24 (x^3) y (YH^3)+72 (x^4) y (YH^3)+24 (x^5) y (YH^3)-32 (x^6) y (YH^3)-24 (x^7) y (YH^3)-4 (x^8) y (YH^3)+8 XH y (YH^3)+16 x XH y (YH^3)-8 (x^2) XH y (YH^3)-32 (x^3) XH y (YH^3)-8 (x^4) XH y (YH^3)+16 (x^5) XH y (YH^3)+8 (x^6) XH y (YH^3)+24 x (y^3) (YH^3)+80 (x^2) (y^3) (YH^3)+48 (x^3) (y^3) (YH^3)-64 (x^4) (y^3) (YH^3)-72 (x^5) (y^3) (YH^3)-16 (x^6) (y^3) (YH^3)-8 XH (y^3) (YH^3)-32 x XH (y^3) (YH^3)-16 (x^2) XH (y^3) (YH^3)+32 (x^3) XH (y^3) (YH^3)+24 (x^4) XH (y^3) (YH^3)+8 (y^5) (YH^3)+24 x (y^5) (YH^3)-32 (x^2) (y^5) (YH^3)-72 (x^3) (y^5) (YH^3)-24 (x^4) (y^5) (YH^3)-8 XH (y^5) (YH^3)+16 x XH (y^5) (YH^3)+24 (x^2) XH (y^5) (YH^3)-24 x (y^7) (YH^3)-16 (x^2) (y^7) (YH^3)+8 XH (y^7) (YH^3)-4 (y^9) (YH^3)+(YH^4)+4 x (YH^4)+4 (x^2) (YH^4)-4 (x^3) (YH^4)-10 (x^4) (YH^4)-4 (x^5) (YH^4)+4 (x^6) (YH^4)+4 (x^7) (YH^4)+(x^8) (YH^4)-4 x (y^2) (YH^4)-12 (x^2) (y^2) (YH^4)-8 (x^3) (y^2) (YH^4)+8 (x^4) (y^2) (YH^4)+12 (x^5) (y^2) (YH^4)+4 (x^6) (y^2) (YH^4)-2 (y^4) (YH^4)-4 x (y^4) (YH^4)+4 (x^2) (y^4) (YH^4)+12 (x^3) (y^4) (YH^4)+6 (x^4) (y^4) (YH^4)+4 x (y^6) (YH^4)+4 (x^2) (y^6) (YH^4)+(y^8) (YH^4)-8 (x^3) Z+16 (x^4) Z+12 (x^5) Z-44 (x^6) Z+16 (x^7) Z+24 (x^8) Z-20 (x^9) Z+4 (x^10) Z+24 (x^2) XH Z-48 (x^3) XH Z-36 (x^4) XH Z+132 (x^5) XH Z-48 (x^6) XH Z-72 (x^7) XH Z+60 (x^8) XH Z-12 (x^9) XH Z-24 x (XH^2) Z+48 (x^2) (XH^2) Z+36 (x^3) (XH^2) Z-132 (x^4) (XH^2) Z+48 (x^5) (XH^2) Z+72 (x^6) (XH^2) Z-60 (x^7) (XH^2) Z+12 (x^8) (XH^2) Z+8 (XH^3) Z-16 x (XH^3) Z-12 (x^2) (XH^3) Z+44 (x^3) (XH^3) Z-16 (x^4) (XH^3) Z-24 (x^5) (XH^3) Z+20 (x^6) (XH^3) Z-4 (x^7) (XH^3) Z+24 x (y^2) Z+32 (x^2) (y^2) Z-24 (x^3) (y^2) Z-60 (x^4) (y^2) Z-16 (x^5) (y^2) Z+24 (x^6) (y^2) Z+20 (x^8) (y^2) Z-24 XH (y^2) Z-48 x XH (y^2) Z-24 (x^2) XH (y^2) Z+120 (x^3) XH (y^2) Z+72 (x^4) XH (y^2) Z-72 (x^5) XH (y^2) Z+24 (x^6) XH (y^2) Z-48 (x^7) XH (y^2) Z+16 (XH^2) (y^2) Z+68 x (XH^2) (y^2) Z-88 (x^2) (XH^2) (y^2) Z-64 (x^3) (XH^2) (y^2) Z+80 (x^4) (XH^2) (y^2) Z-52 (x^5) (XH^2) (y^2) Z+40 (x^6) (XH^2) (y^2) Z-20 (XH^3) (y^2) Z+28 x (XH^3) (y^2) Z+8 (x^2) (XH^3) (y^2) Z-32 (x^3) (XH^3) (y^2) Z+28 (x^4) (XH^3) (y^2) Z-12 (x^5) (XH^3) (y^2) Z+16 (y^4) Z-36 x (y^4) Z-180 (x^2) (y^4) Z-80 (x^3) (y^4) Z+120 (x^4) (y^4) Z+120 (x^5) (y^4) Z+40 (x^6) (y^4) Z+44 XH (y^4) Z+180 x XH (y^4) Z+128 (x^2) XH (y^4) Z-120 (x^3) XH (y^4) Z-160 (x^4) XH (y^4) Z-72 (x^5) XH (y^4) Z-52 (XH^2) (y^4) Z-112 x (XH^2) (y^4) Z+40 (x^2) (XH^2) (y^4) Z+76 (x^3) (XH^2) (y^4) Z+48 (x^4) (XH^2) (y^4) Z+24 (XH^3) (y^4) Z-8 x (XH^3) (y^4) Z-4 (x^2) (XH^3) (y^4) Z-12 (x^3) (XH^3) (y^4) Z-36 (y^6) Z-48 x (y^6) Z+136 (x^2) (y^6) Z+160 (x^3) (y^6) Z+40 (x^4) (y^6) Z+8 XH (y^6) Z-120 x XH (y^6) Z-152 (x^2) XH (y^6) Z-48 (x^3) XH (y^6) Z+32 (XH^2) (y^6) Z+68 x (XH^2) (y^6) Z+24 (x^2) (XH^2) (y^6) Z-12 (XH^3) (y^6) Z-4 x (XH^3) (y^6) Z+16 (y^8) Z+60 x (y^8) Z+20 (x^2) (y^8) Z-28 XH (y^8) Z-12 x XH (y^8) Z+4 (XH^2) (y^8) Z+4 (y^10) Z-48 x y YH Z-48 (x^2) y YH Z+96 (x^3) y YH Z+60 (x^4) y YH Z-24 (x^5) y YH Z-24 (x^7) y YH Z-12 (x^8) y YH Z+48 XH y YH Z+64 x XH y YH Z-88 (x^2) XH y YH Z-64 (x^3) XH y YH Z-16 (x^4) XH y YH Z-16 (x^5) XH y YH Z+56 (x^6) XH y YH Z+16 (x^7) XH y YH Z-16 (XH^2) y YH Z-8 x (XH^2) y YH Z+4 (x^2) (XH^2) y YH Z+40 (x^3) (XH^2) y YH Z+16 (x^4) (XH^2) y YH Z-32 (x^5) (XH^2) y YH Z-4 (x^6) (XH^2) y YH Z-48 (y^3) YH Z+64 x (y^3) YH Z+360 (x^2) (y^3) YH Z+112 (x^3) (y^3) YH Z-240 (x^4) (y^3) YH Z-200 (x^5) (y^3) YH Z-48 (x^6) (y^3) YH Z-88 XH (y^3) YH Z-256 x XH (y^3) YH Z-32 (x^2) XH (y^3) YH Z+160 (x^3) XH (y^3) YH Z+168 (x^4) XH (y^3) YH Z+48 (x^5) XH (y^3) YH Z+52 (XH^2) (y^3) YH Z+40 x (XH^2) (y^3) YH Z-16 (x^2) (XH^2) (y^3) YH Z-64 (x^3) (XH^2) (y^3) YH Z-12 (x^4) (XH^2) (y^3) YH Z+108 (y^5) YH Z+136 x (y^5) YH Z-288 (x^2) (y^5) YH Z-328 (x^3) (y^5) YH Z-72 (x^4) (y^5) YH Z-16 XH (y^5) YH Z+176 x XH (y^5) YH Z+168 (x^2) XH (y^5) YH Z+48 (x^3) XH (y^5) YH Z-32 (XH^2) (y^5) YH Z-32 x (XH^2) (y^5) YH Z-12 (x^2) (XH^2) (y^5) YH Z-48 (y^7) YH Z-152 x (y^7) YH Z-48 (x^2) (y^7) YH Z+56 XH (y^7) YH Z+16 x XH (y^7) YH Z-4 (XH^2) (y^7) YH Z-12 (y^9) YH Z+24 x (YH^2) Z+16 (x^2) (YH^2) Z-52 (x^3) (YH^2) Z-28 (x^4) (YH^2) Z+32 (x^5) (YH^2) Z+8 (x^6) (YH^2) Z-4 (x^7) (YH^2) Z+4 (x^8) (YH^2) Z-24 XH (YH^2) Z-16 x XH (YH^2) Z+52 (x^2) XH (YH^2) Z+28 (x^3) XH (YH^2) Z-32 (x^4) XH (YH^2) Z-8 (x^5) XH (YH^2) Z+4 (x^6) XH (YH^2) Z-4 (x^7) XH (YH^2) Z+48 (y^2) (YH^2) Z-20 x (y^2) (YH^2) Z-232 (x^2) (y^2) (YH^2) Z-96 (x^3) (y^2) (YH^2) Z+160 (x^4) (y^2) (YH^2) Z+116 (x^5) (y^2) (YH^2) Z+24 (x^6) (y^2) (YH^2) Z+44 XH (y^2) (YH^2) Z+76 x XH (y^2) (YH^2) Z-24 (x^2) XH (y^2) (YH^2) Z-64 (x^3) XH (y^2) (YH^2) Z-20 (x^4) XH (y^2) (YH^2) Z-12 (x^5) XH (y^2) (YH^2) Z-108 (y^4) (YH^2) Z-128 x (y^4) (YH^2) Z+200 (x^2) (y^4) (YH^2) Z+244 (x^3) (y^4) (YH^2) Z+48 (x^4) (y^4) (YH^2) Z+8 XH (y^4) (YH^2) Z-56 x XH (y^4) (YH^2) Z-52 (x^2) XH (y^4) (YH^2) Z-12 (x^3) XH (y^4) (YH^2) Z+48 (y^6) (YH^2) Z+124 x (y^6) (YH^2) Z+40 (x^2) (y^6) (YH^2) Z-28 XH (y^6) (YH^2) Z-4 x XH (y^6) (YH^2) Z+12 (y^8) (YH^2) Z-16 y (YH^3) Z-8 x y (YH^3) Z+52 (x^2) y (YH^3) Z+40 (x^3) y (YH^3) Z-32 (x^4) y (YH^3) Z-32 (x^5) y (YH^3) Z-4 (x^6) y (YH^3) Z+36 (y^3) (YH^3) Z+40 x (y^3) (YH^3) Z-48 (x^2) (y^3) (YH^3) Z-64 (x^3) (y^3) (YH^3) Z-12 (x^4) (y^3) (YH^3) Z-16 (y^5) (YH^3) Z-32 x (y^5) (YH^3) Z-12 (x^2) (y^5) (YH^3) Z-4 (y^7) (YH^3) Z+18 (x^2) (Z^2)+12 (x^3) (Z^2)-78 (x^4) (Z^2)+24 (x^5) (Z^2)+54 (x^6) (Z^2)-36 (x^7) (Z^2)+6 (x^8) (Z^2)-36 x XH (Z^2)-24 (x^2) XH (Z^2)+156 (x^3) XH (Z^2)-48 (x^4) XH (Z^2)-108 (x^5) XH (Z^2)+72 (x^6) XH (Z^2)-12 (x^7) XH (Z^2)+18 (XH^2) (Z^2)+12 x (XH^2) (Z^2)-78 (x^2) (XH^2) (Z^2)+24 (x^3) (XH^2) (Z^2)+54 (x^4) (XH^2) (Z^2)-36 (x^5) (XH^2) (Z^2)+6 (x^6) (XH^2) (Z^2)+18 (y^2) (Z^2)-36 x (y^2) (Z^2)-156 (x^2) (y^2) (Z^2)-48 (x^3) (y^2) (Z^2)+126 (x^4) (y^2) (Z^2)+36 (x^5) (y^2) (Z^2)+24 (x^6) (y^2) (Z^2)+24 XH (y^2) (Z^2)+156 x XH (y^2) (Z^2)+96 (x^2) XH (y^2) (Z^2)-168 (x^3) XH (y^2) (Z^2)-48 (x^4) XH (y^2) (Z^2)-36 (x^5) XH (y^2) (Z^2)-46 (XH^2) (y^2) (Z^2)-40 x (XH^2) (y^2) (Z^2)+60 (x^2) (XH^2) (y^2) (Z^2)+8 (x^3) (XH^2) (y^2) (Z^2)+14 (x^4) (XH^2) (y^2) (Z^2)-78 (y^4) (Z^2)-72 x (y^4) (Z^2)+186 (x^2) (y^4) (Z^2)+180 (x^3) (y^4) (Z^2)+36 (x^4) (y^4) (Z^2)+16 XH (y^4) (Z^2)-124 x XH (y^4) (Z^2)-152 (x^2) XH (y^4) (Z^2)-36 (x^3) XH (y^4) (Z^2)+22 (XH^2) (y^4) (Z^2)+44 x (XH^2) (y^4) (Z^2)+10 (x^2) (XH^2) (y^4) (Z^2)+50 (y^6) (Z^2)+108 x (y^6) (Z^2)+24 (x^2) (y^6) (Z^2)-32 XH (y^6) (Z^2)-12 x XH (y^6) (Z^2)+2 (XH^2) (y^6) (Z^2)+6 (y^8) (Z^2)-36 y YH (Z^2)+48 x y YH (Z^2)+156 (x^2) y YH (Z^2)-84 (x^4) y YH (Z^2)-24 (x^5) y YH (Z^2)-12 (x^6) y YH (Z^2)-24 XH y YH (Z^2)-64 x XH y YH (Z^2)-16 (x^2) XH y YH (Z^2)+48 (x^3) XH y YH (Z^2)+32 (x^4) XH y YH (Z^2)+8 (x^5) XH y YH (Z^2)+156 (y^3) YH (Z^2)+128 x (y^3) YH (Z^2)-248 (x^2) (y^3) YH (Z^2)-208 (x^3) (y^3) YH (Z^2)-36 (x^4) (y^3) YH (Z^2)-16 XH (y^3) YH (Z^2)+80 x XH (y^3) YH (Z^2)+64 (x^2) XH (y^3) YH (Z^2)+16 (x^3) XH (y^3) YH (Z^2)-100 (y^5) YH (Z^2)-184 x (y^5) YH (Z^2)-36 (x^2) (y^5) YH (Z^2)+32 XH (y^5) YH (Z^2)+8 x XH (y^5) YH (Z^2)-12 (y^7) YH (Z^2)+18 (YH^2) (Z^2)-12 x (YH^2) (Z^2)-46 (x^2) (YH^2) (Z^2)+8 (x^3) (YH^2) (Z^2)+18 (x^4) (YH^2) (Z^2)-4 (x^5) (YH^2) (Z^2)+2 (x^6) (YH^2) (Z^2)-78 (y^2) (YH^2) (Z^2)-56 x (y^2) (YH^2) (Z^2)+84 (x^2) (y^2) (YH^2) (Z^2)+72 (x^3) (y^2) (YH^2) (Z^2)+10 (x^4) (y^2) (YH^2) (Z^2)+50 (y^4) (YH^2) (Z^2)+76 x (y^4) (YH^2) (Z^2)+14 (x^2) (y^4) (YH^2) (Z^2)+6 (y^6) (YH^2) (Z^2)-72 (x^2) (Z^3)+12 (x^3) (Z^3)+52 (x^4) (Z^3)-28 (x^5) (Z^3)+4 (x^6) (Z^3)+72 x XH (Z^3)-12 (x^2) XH (Z^3)-52 (x^3) XH (Z^3)+28 (x^4) XH (Z^3)-4 (x^5) XH (Z^3)-72 (y^2) (Z^3)-36 x (y^2) (Z^3)+104 (x^2) (y^2) (Z^3)+56 (x^3) (y^2) (Z^3)+12 (x^4) (y^2) (Z^3)+12 XH (y^2) (Z^3)-52 x XH (y^2) (Z^3)-48 (x^2) XH (y^2) (Z^3)-8 (x^3) XH (y^2) (Z^3)+52 (y^4) (Z^3)+84 x (y^4) (Z^3)+12 (x^2) (y^4) (Z^3)-12 XH (y^4) (Z^3)-4 x XH (y^4) (Z^3)+4 (y^6) (Z^3)+72 y YH (Z^3)+24 x y YH (Z^3)-52 (x^2) y YH (Z^3)-8 (x^3) y YH (Z^3)-4 (x^4) y YH (Z^3)-52 (y^3) YH (Z^3)-72 x (y^3) YH (Z^3)-8 (x^2) (y^3) YH (Z^3)-4 (y^5) YH (Z^3)-27 (Z^4)+18 (x^2) (Z^4)-8 (x^3) (Z^4)+(x^4) (Z^4)+18 (y^2) (Z^4)+24 x (y^2) (Z^4)+2 (x^2) (y^2) (Z^4)+(y^4) (Z^4))

Factor[p[0,0,x,y,Z]]

( (x^2+y^2)^2+8x(3y^2-x^2)+18(x^2+y^2)-27) Z^4+

4( (x^2+y^2)^3+7 x (3y^2-x^2)(x^2+y^2)+13 (x^2+y^2)^2+3 x (x^2-3 y^2)-18 (x^2+y^2) ) Z^3 +
 2( 3 (x^2+y^2)^4+18 x (3 y^2-x^2) (x^2+y^2)^2+(3 x^2+y^2) (9 x^4+18 x^2 y^2+25 y^4)+12 x (x^2-3 y^2) (x^2+y^2)-39 (x^2+y^2)^2+6 x (x^2-3 y^2)+9 (x^2+y^2) )Z^2  +
 4(x^2+y^2-1)( (x^2+y^2)^4-5 x (x^2-3 y^2) (x^2+y^2)^2+(7 x^6+3 x^4 y^2+33 x^2 y^4+5 y^6)-x (x^2-3 y^2) (x^2+y^2)-6 x y^2-4(x^2+y^2)^2+2 x^3 )Z + 

(x^2+y^2-1)^2 ((x^2+y^2)^2+2 x (3 y^2-x^2)+(x^2+y^2))^2

Factor[%%-%]

(*  Lemma 14 Check.  *)

Factor[{c1^2, c2^2, c3^2, c1 c2 c3} /. cSubs]

{Numerator[%], Denominator[%]}

Factor[ % /. {r1^2->R1,r2^2->R2,r3^2->R3,-D1+(r2^2)+(r3^2)->R1bar,-D2+(r1^2)+(r3^2)->R2bar,-D3+(r1^2)+(r2^2)->R3bar} ]

Factor[ %[[1]]/%[[2]] ]

Factor[Factor[Factor[{ r1^2,r2^2,r3^2,-D1+(r2^2)+(r3^2),-D2+(r1^2)+(r3^2),-D3+(r1^2)+(r2^2) }  /. r2RSubs] /. DRSubs]//. ySubs]

Factor[% /. {x->0,y->0}]

Factor[XYΔReduce[%] /. tweak3]

list = Delete[%, {{1},{2}}]

newlist = Factor[  XYΔReduce[ { list[[1]], list[[2]]+list[[3]]+list[[4]], list[[3]]list[[4]]+list[[4]]list[[2]]+list[[2]]list[[3]], list[[2]]list[[3]]list[[4]] }  ]  /. tweak3]

{
1+Z,

-3+(XH^2)+(YH^2)+6 Z,

3-5 (XH^2)+2 (XH^3)-5 (YH^2)-6 XH (YH^2)-12 Z+4 (XH^2) Z+4 (YH^2) Z+12 (Z^2),

-1+4 (XH^2)-4 (XH^3)+(XH^4)+4 (YH^2)+12 XH (YH^2)+2 (XH^2) (YH^2)+(YH^4)+6 Z-10 (XH^2) Z+4 (XH^3) Z-10 (YH^2) Z-12 XH (YH^2) Z-12 (Z^2)+4 (XH^2) (Z^2)+4 (YH^2) (Z^2)+8 (Z^3)
}

(* Poly's are scaled differently in paper - will change there *)

{Q0, Q1, Q2, Q3} - %

GroebnerBasis[ {-1+Q0-Z,3+Q1-(XH^2)-(YH^2)-6 Z,-3+Q2+5 (XH^2)-2 (XH^3)+5 (YH^2)+6 XH (YH^2)+12 Z-4 (XH^2) Z-4 (YH^2) Z-12 (Z^2),1+Q3-4 (XH^2)+4 (XH^3)-(XH^4)-4 (YH^2)-12 XH (YH^2)-2 (XH^2) (YH^2)-(YH^4)-6 Z+10 (XH^2) Z-4 (XH^3) Z+10 (YH^2) Z+12 XH (YH^2) Z+12 (Z^2)-4 (XH^2) (Z^2)-4 (YH^2) (Z^2)-8 (Z^3)}, {Z,YH,XH,Q3,Q2,Q1,Q0}]

poly = %[[1]]

(* 
   This generates ideal of polynomials in Q0, Q1, Q2, Q3 
  (independent of XH and YH) such that substitutions yield zero. 
*)

(* 
     Theorem 2 Check.
  Mathematica becomes overwhelmed trying to compute the 
   multi-polynomial resultant. 
  Let us here start instead by obtaining the discriminant
   of the quartic. Start with Grunert's system: 
*)

p1 = r2^2 + r3^2 - 2r2 r3 c1 - D1 
p2 = r3^2 + r1^2 - 2r3 r1 c2 - D2
p3 = r1^2 + r2^2 - 2r1 r2 c3 - D3

p4 = Factor[Resultant[p1,p2,r3]]

p5 = Factor[Factor[Resultant[p3, p4, r2]] /. r1->Sqrt[R1]]

Factor[CoefficientList[p5, {c3,c2,c1}]]

quarticDiscriminant = Factor[Discriminant[p5, R1]]

quarticDiscriminant0 = Factor[quarticDiscriminant / (16777216 (((-1+(c1^2)+(c2^2)-2 c1 c2 c3+(c3^2)))^2) ((((c1^2) D1+(c2^2) D1-2 c1 c2 c3 D1-(c1^2) D2-(c2^2) D2+2 c1 c2 c3 D2+(c1^2) D3-(c2^2) D3))^2) ((((c1^2) D1-2 c1 c2 c3 D1+(c3^2) D1+(c1^2) D2-(c3^2) D2-(c1^2) D3+2 c1 c2 c3 D3-(c3^2) D3))^2) (((-(c2^2) D1+(c3^2) D1-(c2^2) D2+2 c1 c2 c3 D2-(c3^2) D2+(c2^2) D3-2 c1 c2 c3 D3+(c3^2) D3))^2) ) ]

Factor[CoefficientList[quarticDiscriminant0, {c3,c2,c1}]]

Factor[Factor[% /. DRSubs] //. tSubsSp]

quarticDiscriminant00 = Factor[UnCoefficientList[ % , {c3,c2,c1}]]

(* Now compute formula in theorem, and compare *)

deltoid

Factor[Factor[Factor[ deltoid /. {L ->LL, R-> RR}] //. ySubs] //. ySubs]

Factor[Factor[Factor[CoefficientList[Numerator[%], {c3,c2,c1}]]//. ySubs] //. ySubs]

Factor[% //. tSubsSp]

discriminantGrunert = Factor[UnCoefficientList[ % , {c3,c2,c1}]]

quarticDiscriminant00

Factor[%% / %]

(* 
    Up to a scalar multiple, the quantity in Theorem 2 ("discriminantGrunert") 
   equals the "big factor" in the discriminant of the quartic polynomial (in R1). 
  The other factors vanish in the "flat case" (z = 0) and in the "altitude 
    plane case," and these do NOT correspond to repeated solutions to the 
   Grunert system, only to repeated roots of the quartic polynomial.  
  Now, what about the degree of the discriminant to Gruenert's system? 
*)

{num,den} = {Numerator[discriminantGrunert],Denominator[discriminantGrunert]}

coeffs = Factor[CoefficientList[num, {c3,c2,c1}]]

Length[coeffs]

Factor[coeffs[[5]][[5]][[5]] / den]

Factor[Factor[ Δ^2 /. unXYΔSubs ] //. tSubsSp]

Factor[%%/%]

(*
    coeffs[[5]][[5]][[5]] is the coefficient of c1^4 c2^4 c3^4, 
    which is a degree-12 monomial. No higher degree monomials are 
  possible since discriminant is a fourth degree polynomial in 
  polynomials that are linear in c1^2, c2^2, c3^2 and c1 c2 c3. 
*)

(*  Lemma 15 Check.  *)

μνξSubs

unμνξSubs

Factor[{x,y,Z} /. μνξSubs]

Factor[{x,y,Z} //. μνξSubs]

Factor[ % /. unμνξSubs ]

Factor[ {μ,ν,ξ} //. unμνξSubs ]

Factor[ % //. μνξSubs ]

(* 
     Corollary 2 Check.
*)

{LLL, RRR}

{LLLμνξ, RRRμνξ}  = Factor[ % //. μνξSubs]

(* 
    Lemma 16 Check.   
 TYPO IN PAPER - forgot to square denominator in proof in paper
*)

Factor[ μ^2 + ν^2 - 1 //. unμνξSubs ]

Factor[ 
(x^2+y^2-1)(4(x^2+y^2+Z)^2+4(1+XH x+YH y)(1-x^2-y^2-Z)+(1-XH^2-YH^2)(1-x^2-y^2)- 4 )/ (x^2+y^2+2Z-1)^2
]

Factor[%%-%]

long = (1-5 (x^2)+4 (x^4)+4 x XH-4 (x^3) XH-(XH^2)+(x^2) (XH^2)-5 (y^2)+8 (x^2) (y^2)-4 x XH (y^2)+(XH^2) (y^2)+4 (y^4)+4 y YH-4 (x^2) y YH-4 (y^3) YH-(YH^2)+(x^2) (YH^2)+(y^2) (YH^2)-4 Z+8 (x^2) Z-4 x XH Z+8 (y^2) Z-4 y YH Z+4 (Z^2))

Factor[D[ long, Z]]

Factor[8 Z + 8(x-XH/4)^2+8(y-YH/4)^2 -(XH^2+YH^2+8)/2]

Factor[%%-%]

Factor[long /. Z->4]

Factor[Φ^2 - Ψ^2 - 4*(XH^2 + YH^2 - 1) /. {
 Φ -> 2*((x - XH/4)^2 + (y - YH/4)^2) + (XH^2 + YH^2 + 54)/8, 
    Ψ -> XH*x + YH*y - (XH^2 + YH^2 + 3)/4
}]

Factor[%%-%]

(* 
     Lemma 17 Check.
*)

trigSubs = {
  Cos[4ϕ] -> Cos[2ϕ]^2 - Sin[2ϕ]^2, 
  Sin[4ϕ] -> 2 Cos[2ϕ]Sin[2ϕ], 
  Cos[2ϕ] -> Cos[ϕ]^2 - Sin[ϕ]^2, 
  Sin[2ϕ] -> 2 Cos[ϕ]Sin[ϕ], 
  ((Sin[ϕ])^2) -> 1 -  ((Cos[ϕ])^2), 
  ((Sin[ϕ])^3) -> Sin[ϕ](1 -  ((Cos[ϕ])^2)), 
  ((Sin[ϕ])^4) -> (1 -  ((Cos[ϕ])^2))^2, 
  ((Sin[ϕ])^5) -> Sin[ϕ](1 -  ((Cos[ϕ])^2))^2, 
  ((Sin[ϕ])^6) -> (1 -  ((Cos[ϕ])^2))^3 
}

Factor[ 
Factor[ 

(  Cos[2ϕ]  (2(1+μ)ν)  +  Sin[2ϕ](ν^2-(μ-1)^2)  ) - 

( 2 (Cos[ϕ] (μ+ Cos[4ϕ])+ Sin[ϕ] (ν+ Sin[4ϕ])) *(-Sin[ϕ](μ+ Cos[4ϕ])+ Cos[ϕ] (ν+ Sin[4ϕ])) - 4Cos[2ϕ]^2  Sin[2ϕ] ) 

  //. trigSubs]  //.  trigSubs]

(* 
     Lemma 18 Check.
*)

LLL

RRR

Factor[ 
Factor[ 

( Cos[2ϕ]LLLμνξ +Sin[2ϕ]RRRμνξ ) -   

( ( ( Cos[ϕ] (μ+  Cos[4ϕ])+ Sin[ϕ] (ν+ Sin[4ϕ]))(-Sin[ϕ] (μ+  Cos[4ϕ])+ Cos[ϕ] (ν+ Sin[4ϕ]))  - ( Cos[ϕ] (XH+  Cos[4ϕ])+ Sin[ϕ] (YH+ Sin[4ϕ])) (-Sin[ϕ] (XH+  Cos[4ϕ])+ Cos[ϕ](YH+ Sin[4ϕ])) ξ^2  )(2 / (1-ξ^2))  -   4 Cos[2ϕ]^2 Sin[2ϕ] ) 

  //. trigSubs]  //.  trigSubs]

(* 
     Lemma 22 Check.
*)

μt = ( 2μ0 + 2(- Sin[2ϕ] + μ0(1-Sin[2ϕ])+ ν0  Cos[2ϕ])t + (- Cos[4ϕ]- Sin[2ϕ] + μ0(1-Sin[2ϕ])+ ν0  Cos[2ϕ]) t^2 ) / (2 (1+t))

νt = ( 2 ν0 + 2(- Cos[2ϕ] + μ0 Cos[2ϕ]+ν0 (1+Sin[2ϕ])) t + (- Sin[4ϕ]- Cos[2ϕ] + μ0  Cos[2ϕ]+ν0(1+Sin[2ϕ]))t^2 ) / (2 (1+t))

Ξt  =  (  4 (μ0^2+ν0^2-1)  t +

 2(-3-2μ0 Sin[2ϕ]+ μ0^2(3-2Sin[2ϕ])- 2 ν0 Cos[2ϕ]+4μ0 ν0 Cos[2ϕ] +ν0^2(3+2Sin[2ϕ]))  t^2 + 

4( μ0(Sin[2ϕ]-1)(2Sin[2ϕ]+1) +  μ0^2(1-Sin[2ϕ]) - ν0 Cos[2ϕ] (2Sin[2ϕ]+1) +2μ0 ν0 Cos[2ϕ]+ν0^2(1+Sin[2ϕ]))  t^3 + 

((1- Sin[2ϕ])(1+2Sin[2ϕ])^2 - 2μ0(1- Sin[2ϕ])(1+2Sin[2ϕ]) + μ0^2 (1- Sin[2ϕ]) - 2 ν0 Cos[2ϕ] (1+2Sin[2ϕ]) + 2μ0 ν0 Cos[2ϕ]+ν0^2(1+ Sin[2ϕ]) )t^4 )  / 

(2κ (1+t)^2)

Factor[Factor[ 
2(μt+1)νt - (2(μ0+1)ν0 + κ Cos[2ϕ] Ξt) 
  //. trigSubs]  //.  trigSubs]

Factor[Factor[ 
νt^2 -(μt-1)^2  - ( ν0^2 -(μ0-1)^2 + κ Sin[2ϕ] Ξt) 
  //. trigSubs]  //.  trigSubs]

(* 
     Lemma 23 Check.
*)

MatrixForm[ M = {{ν,-μ-1},{μ-1,ν}} ]

MatrixForm[ v = {{ 2(XH+1)YH- 2(μ+1)ν }, {YH^2-(XH-1)^2-ν^2+(μ-1)^2}}]

M.v

(*
    That equals  2(μ^2+ν^2-1)(1-Ξ)((( (Overscript[μ, •]) / (Overscript[Ξ, •]) , (Overscript[ν, •]) / (Overscript[Ξ, •]) ))^T)  =  
   2(μ^2+ν^2-1)(1-ξ^2)((( (Overscript[μ, •]) / 2ξ(Overscript[ξ, •]) , (Overscript[ν, •]) / 2ξ(Overscript[ξ, •]) ))^T) , 
    so the following is ((( (Overscript[μ, •]) / (Overscript[ξ, •]) , (Overscript[ν, •]) / (Overscript[ξ, •]) , 1 ))^T) . 
*)

MatrixForm[Append[ ξ M.v  / ((μ^2+ν^2-1)(1-ξ^2)), {1} ]]

(*
    which is proportional to ((( (Overscript[μ, •]) , (Overscript[ν, •]) , (Overscript[ξ, •]) ))^T) and also to the following:
*)

MatrixForm[ V = Factor[Append[ ξ  M.v ,  {((μ^2+ν^2-1)(1-ξ^2))}]]]

(* From paper: *)

MatrixForm[  { { ( ( (XH-1)^2-YH^2)(μ+1)+ 2(XH+1)YH ν - (μ+1)((μ-1)^2+ν^2) ) ξ }  ,
 { ( 2(XH+1)YH(μ-1)+ (YH^2-(XH-1)^2)ν  -ν( ν^2 +(μ-1)(μ+3)) ) ξ } ,
{(μ^2+ν^2-1)(1- ξ^2) } } ]

Factor[V - %]

(* 
     Lemma 24 Check.
*)

Factor[{x, y, Z} //. μνξSubs]

J = Factor[Transpose[ { D[%,μ], D[%,ν], D[%,ξ] } ]]

V

Factor[ J.V ]

Factor[% /. unμνξSubs]

MatrixForm[  W = Factor[ %  (((-1+(x^2)+(y^2)+2 Z))^2) /   (2(-1+(x^2)+(y^2)+Z)) ]]

(* That is proportional to ( (Overscript[x, •]), (Overscript[y, •]), (Overscript[Z, •]) ) *)

poly = Factor[(1-7 (x^2)-2 (x^3)+8 (x^4)+6 x XH+4 (x^2) XH-10 (x^3) XH-(XH^2)-2 x (XH^2)+3 (x^2) (XH^2)-7 (y^2)+6 x (y^2)+16 (x^2) (y^2)-4 XH (y^2)-10 x XH (y^2)+3 (XH^2) (y^2)+8 (y^4)+6 y YH-8 x y YH-10 (x^2) y YH+4 XH y YH-10 (y^3) YH-(YH^2)+2 x (YH^2)+3 (x^2) (YH^2)+3 (y^2) (YH^2)-4 Z+12 (x^2) Z-8 x XH Z+12 (y^2) Z-8 y YH Z+4 (Z^2)) /. Z->z^2]

(* From paper (CORRECTED): *)

p = Factor[
1-XH^2-YH^2+2(YH^2-XH^2+3XH)x +(3XH^2+3YH^2+4XH-7)x^2-2(1+5XH)x^3+ 8 x^4+ 2(3+2XH)YH y-8YH x y-10 YH x^2 y +(3XH^2+3YH^2-4XH-7)y^2+2(3-5XH) x y^2 + 16 x^2 y^2-10 YH y^3+8 y^4-4 z^2-8XH x z^2+12 x^2 z^2- 8YH y z^2+12 y^2 z^2+4 z^4
]

Factor[poly-p]

Clear[p]

p[XH_,YH_,x_,y_,Z_] := 1-7 (x^2)-2 (x^3)+8 (x^4)+6 x XH+4 (x^2) XH-10 (x^3) XH-(XH^2)-2 x (XH^2)+3 (x^2) (XH^2)-7 (y^2)+6 x (y^2)+16 (x^2) (y^2)-4 XH (y^2)-10 x XH (y^2)+3 (XH^2) (y^2)+8 (y^4)+6 y YH-8 x y YH-10 (x^2) y YH+4 XH y YH-10 (y^3) YH-(YH^2)+2 x (YH^2)+3 (x^2) (YH^2)+3 (y^2) (YH^2)-4 Z+12 (x^2) Z-8 x XH Z+12 (y^2) Z-8 y YH Z+4 (Z^2)

Factor[D[p[XH,YH,x,y,Z],Z]]

Factor[ 8Z + 12((x-XH/3)^2+(y-YH/3)^2-(3+XH^2+YH^2)/9)]

Factor[%%-%]

Factor[8 Z - 12(3+9)/9]

Q[u_,v_] := 8((u^2+v^2)^2 + u v^2)

q[XH_,YH_,x_,y_] := Q[x-(1+5XH)/16, y-5YH/16]

Factor[p[XH,YH,x,y,Z]- q[XH,YH,x,y]]

r[XH_,YH_,x_,y_,Z_] := 4Z^2 + 12x^2 Z + 12 y^2 Z - 8XH x Z - 8YH y Z - 4Z

Factor[ p[XH,YH,x,y,Z] -  q[XH,YH,x,y] - r[XH,YH,x,y,Z] ]

s[XH_,YH_,x_,y_] := (1/8192)(8191+64 x-58880 (x^2)-20 XH+50112 x XH+17408 (x^2) XH-8342 (XH^2)-11584 x (XH^2)-13824 (x^2) (XH^2)-500 (XH^3)+8000 x (XH^3)-625 (XH^4)-53760 (y^2)-17408 XH (y^2)+11776 (XH^2) (y^2)+46912 y YH-34816 x y YH+23168 XH y YH-51200 x XH y YH+8000 (XH^2) y YH-7842 (YH^2)+11584 x (YH^2)+11776 (x^2) (YH^2)+1500 XH (YH^2)+8000 x XH (YH^2)-1250 (XH^2) (YH^2)-13824 (y^2) (YH^2)+8000 y (YH^3)-625 (YH^4))

r[XH_,YH_,x_,y_,Z_] := 4Z^2 + 12x^2 Z + 12 y^2 Z - 8XH x Z - 8YH y Z - 4Z  + s[XH, YH, x, y]

r[XH,YH,x,y,Z]

Clear[u,v]

Q[u,v]

first = Factor[D[Q[u,v], u]]

second = Factor[D[Q[u,v], v]]

Factor[Resultant[first, second, v]]

Factor[{first,second} /. u->-1/6]

Q[-1/6, 1/Sqrt[18]]

(* 
    That is the least value of Q[u,v] and so least value of q[XH,YH,x,y] too.
 Now consider r[XH,YH,x,y,Z] which needs to be > 1/54 when Z ≥ 9. 
*)

Factor[r[XH,YH,x,y,9]]

first = Factor[D[r[XH,YH,x,y,9],x]]

second = Factor[D[r[XH,YH,x,y,9],y]]

Factor[Resultant[first,second,y]]

x0 = Factor[ x /. Solve[Numerator[%]==0, x][[1]]]

Factor[{first,second} /. x->x0]

y0 = Factor[ y /. Solve[(-41886384 y-5440 XH y+126048 (XH^2) y-27200 (XH^3) y+9936 (XH^4) y+13683045 YH-8812 XH YH-15170 (XH^2) YH+10324 (XH^3) YH-2875 (XH^4) YH+118048 y (YH^2)+81600 XH y (YH^2)+19872 (XH^2) y (YH^2)-12670 (YH^3)-25876 XH (YH^3)-5750 (XH^2) (YH^3)+9936 y (YH^4)-2875 (YH^5))==0, y][[1]]]

Factor[r[XH,YH,x0,y0,9]]

(*
    That is the minimum value of r[XH,YH,x,y,9] for fixed XY and YH.
*)

{num, den} = {Numerator[%], Denominator[%]}

polarSubs = { 
XH -> ρ Cos[ω], YH->  ρ Sin[ω], 
Sin[ω]^2 -> 1-Cos[ω]^2, 
Sin[ω]^3 -> Sin[ω](1-Cos[ω]^2), 
Sin[ω]^4 -> (1-Cos[ω]^2)^2, 
Sin[ω]^5 -> Sin[ω](1-Cos[ω]^2)^2, 
Sin[ω]^6 -> (1-Cos[ω]^2)^3,
Sin[ω]^7 -> Sin[ω](1-Cos[ω]^2)^3, 
Sin[ω]^8 -> (1-Cos[ω]^2)^4
}

Factor[ {num, den} //. polarSubs ]

{numPolar, denPolar} = Factor[ - % /. Cos[ω]-> χ ]

Expand[denPolar]

(* lower bound on denPolar  *)

21445828608-60440576 (3^2)-5087232 (3^4)+2785280 (-3)-41779200 (3^3)-4096000 (3^2)+55705600 (-3^3)

(* upper bound on denPolar  *)

21445828608-60440576 (0)-5087232 (0)+2785280 (3)-41779200 (-3^3)-4096000 (0)+55705600 (3^3)

Expand[numPolar]

(* lower bound on numPolar *)

6197841846567-270144022668 (3^2)+585260050 (0)+55321476 (0)-330625 (3^8)+807334704 (-3)+6949989152 (-3^3)+439735024 (-3^5)-7176000 (3^7)-1186409352 (3^2)+50495184 (0)-37399400 (3^6)-9310310016 (3^3)-589707072 (3^5)+9568000 (-3^7)-3292080 (3^4)+99026400 (0)+4840000 (-3^5)-66017600 (3^6)

(* lower bound on numPolar/denPolar *)

N[ 2948641317306 / 24086274048 ]

(* 
   So r[XH,YH,x,y,9] is at least this big, and so too is 
 r[XH,YH,x,y,Z] for all Z ≥ 9. 
*)