本日のC.A.D.

? f(x)=x^3+3*x^2-9*x;
? g=strjoin(["y<x,x<a",concat([f(x),">",((x-y)*f(a)+(a-x)*f(y))/(a-y)])],",")
%2 = "y<x,x<a,x^3+3*x^2-9*x>(y^2+(a+3)*y+(a^2+3*a-9))*x+(-a*y^2+(-a^2-3*a)*y)"
? tst12([all,all],[a,x,y],(f1,f2,f3)->imp(f1*f2,f3),g);Ans()
 *** using Lazard's method (MPP17).
[y,2]
[x,2]
[a,1]
time = 68 ms.
3 13(0,2) 36(0,6) 
 *** combined adjacent 35 cells.
1[a <= [a+1,1],true,true]
time = 5 ms.

? tst12([ex],[a,b,c,t],andx,"a^2+b^2+c^2=(t+2-a)^2+(t+2-b)^2+(t-c)^2,a^2+b^2+c^2=(2-a)^2+(1-b)^2+c^2,a^2+b^2+c^2=(1-a)^2+(2-b)^2+c^2");Ans(1)
 *** using Lazard's method (MPP17).
[t,1]
[c,1]
[b,3]
[a,3]
time = 76 ms.
7 43(0,6) 5(14,0) 4(4,0) 
 *** combined adjacent 2 cells.
1[a = [6*a-5,1],b = [6*b-5,1],c <= [9*c^2-42*c+13,1] or [9*c^2-42*c+13,2] <= c,true]
time = 14 ms.

? tst12([ex,ex,all,all],[a,m,x,y,X,Y],(f1,f2,f3,f4,f5,f6,f7)->f1*f2*f3*f4*imp(f5*f6,f7),"0<a,(2*x-1)*(x-1)<=0,(y-a)*(y-2*a)<=0,x*y*m==x^2+y^2-x^2*y^2,(2*X-1)*(X-1)<=0,(Y-a)*(Y-2*a)<=0,X*Y*m<=X^2+Y^2-X^2*Y^2",17);Ans(1)
 *** using Lazard's method (BM20) with realrad.
-7
[Y,3]
-7,-7
[X,7]
-7
[y,3]
-7,-7
[x,7]
-7,-7,-7,-7,-7,-7,-7,-7,-7
[m,15]
[a,29]
time = 289 ms.
53 2107(4,100) 9027(572,1899) 3321(1480,1992) 60201(770,2823) 5819(17390,10230) 
 *** combined adjacent 5816 cells.
1[[a,1] < a <= [20*a^2-1,2],m = [-12*a^2+4*m*a-1,1],true,true,true,true]
2[[20*a^2-1,2] < a < [8*a^2-1,2],m = [16*a^2+(m^2-4),2],true,true,true,true]
3[[8*a^2-1,2] <= a,m = [2*m*a-1,1],true,true,true,true]
time = 37,798 ms.

https://www.ssken.gr.jp/MAINSITE/event/2015/20150828-hpcf/lecture-01/SSKEN_hpcf2015_anai_presentation.pdf
https://www.jstage.jst.go.jp/article/pjsai/JSAI2013/0/JSAI2013_2A42/_pdf