with(RegularChains):
with(ChainTools):
with(MatrixTools):
with(ConstructibleSetTools):
with(ParametricSystemTools):
with(SemiAlgebraicSetTools):
with(FastArithmeticTools):
R := PolynomialRing([x,y,z,a,b]):
sys := [a*x^2+b*x+c]:
N := []:
P := [a]: 
H := [x,y,z]:
dec := RealTriangularize(sys,N,P,H,R):
Display(dec, R);

how to write : a <> 0 and (some x)(a*x^2+b*x+c) for quantifier elimination in maple?

is RealTriangularize parameters are after quantifier elimination or it accept quantifer expression?

if not, how to input above statement into real or lazy triangularize and expect return b^2 + 4*a*c;

with(RegularChains):
with(ChainTools):
with(MatrixTools):
with(ConstructibleSetTools):
with(ParametricSystemTools):
with(SemiAlgebraicSetTools):
with(FastArithmeticTools):
R := PolynomialRing([x,y,z,a,b]):
sys := [x^2 + y^2 - x*y - 1 = 0, y^2 + z^2 - y*z - a^2 = 0, z^2 + x^2 - x*z - b^2 = 0,x > 0, y > 0, z > 0, a - 1 >= 0, b-a >= 0, a+1-b > 0]:

dec := RealTriangularize(sys,R): # very slow
Display(dec, R);

dec := LazyRealTriangularize(sys,R): # it is faster
dec2 := value(dec): # very slow
value(dec2); 

find a , b to satisfy sys have real solution

expect  one of solution is below, but above function are very slow, load a very time still no result, where is wrong?

R1 = a^2+a+1-b^2;
R1 = a^2-1+b-b^2;

[R1 > 0, R2 > 0]

LeadingTerm(y^2-x^2/y, plex(x, y));
 

(in Groebner:-LeadingTerm) the input is not polynomial in, {x, y}

how to do when fraction in it ?

it return error

Buchberger function same as Basis function then how to make it as solver function?

is it the newly added y(y-1) be used in solver to find x ?

i find eliminate without y*(y-1) same solution as adding y*(y-1)

why premas and Reduce are different for calculating remainder h?

where is wrong in commented L and S polynomials ? LCM wrong?

with(Groebner):
with(ListTools):
with(combinat):

premas := proc(P,A, PRing)
local R, i, x;
R := P;
i := nops(A);
while i <> 0 do
 x := MainVariable(A[i], PRing);
 R := prem(R, A[i],x);
 i := i - 1:
od:
return R:
end proc:

Buchberger := proc(Fparam, PRing)
#Fparam := [x*y-x, -y+x^2]:
F := MakeUnique(Fparam):
GG := choose(F, 2):
G := F:
while GG <> [] do
f := GG[1][1]:
g := GG[1][2]:
GG := [seq(GG[i], i=2..nops(GG))]:
#L := lcm(TrailingTerm(f, PRing)[2],TrailingTerm(g, PRing)[2]):
#S := simplify(L/LeadingTerm(f, PRing)[2]*f - L/LeadingTerm(g, PRing)[2]*g);
S := SPolynomial(f, g, PRing);
#print("S",S);
#print("G",G);
# S reduce to G modulo h
#h := premas(S, G, PolynomialRing([x, y, z]));
h := Reduce(S, G, PRing, 'h');
#print("h",h);
if h = 0 then
h := []:
end if:
if h <> [] then
 GG := [op(GG), [SelectFirst(G), h]]:
 G := [op(G), h]:
end if:
od:
return G:
end proc:
sol := Buchberger([x*y-x, -y+x^2], plex(x, y));
factor(sol[nops(sol)]);
eliminate(sol,[x,y]);
eliminate([x*y-x, -y+x^2],[x,y]);
sol := Basis([x*y-x, -y+x^2], plex(x, y));
solve([x*y-x, -y+x^2]);
 

pointset := [A, [0,0], B, [0,v_B], C, [u_C, v_C], D, [x_D, y_D], O, [x_O, y_O]];
for i from 1 to nops(pointset)/2 do
print(i, i+1);
pointset[i] := pointset[i+1];
od:
how to Make A := [0,0] instead of pointset[1]