:: POLYEQ_4 semantic presentation

REAL is set

K6(REAL) is set

K6(NAT) is set
K6(NAT) is set
K7(NAT,REAL) is set
K6(K7(NAT,REAL)) is set

delta (b,a,x) is complex real ext-real Element of REAL
sqrt (delta (b,a,x)) is complex real ext-real Element of REAL
(- a) + (sqrt (delta (b,a,x))) is complex real ext-real set
((- a) + (sqrt (delta (b,a,x)))) / (2 * b) is complex real ext-real set
(- a) - (sqrt (delta (b,a,x))) is complex real ext-real set
((- a) - (sqrt (delta (b,a,x)))) / (2 * b) is complex real ext-real set

(4 * b) * x is complex real ext-real set
(a ^2) - ((4 * b) * x) is complex real ext-real set
sqrt ((a ^2) - ((4 * b) * x)) is complex real ext-real set
(- a) + (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set

((- a) + (sqrt ((a ^2) - ((4 * b) * x)))) / (2 * b) is complex real ext-real set
- ((4 * b) * x) is complex real ext-real set
- (- ((4 * b) * x)) is complex real ext-real set

(a ^2) + (- ((4 * b) * x)) is complex real ext-real set

- (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
- (- a) is complex real ext-real set
(- (sqrt ((a ^2) - ((4 * b) * x)))) + (- a) is complex real ext-real set
(- (- a)) + (- a) is complex real ext-real set
(- a) - (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
((- a) - (sqrt ((a ^2) - ((4 * b) * x)))) / (2 * b) is complex real ext-real set

4 * (b * x) is complex real ext-real set
- ((4 * b) * x) is complex real ext-real set
- (- ((4 * b) * x)) is complex real ext-real set

(a ^2) + (- ((4 * b) * x)) is complex real ext-real set

sqrt ((a ^2) - ((4 * b) * x)) is complex real ext-real set

(0 + a) + (- a) is complex real ext-real set
(- a) + (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
((- a) + (sqrt ((a ^2) - ((4 * b) * x)))) / (2 * b) is complex real ext-real set
- (- a) is complex real ext-real set
0 + (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set

(sqrt ((a ^2) - ((4 * b) * x))) + a is complex real ext-real set
- ((sqrt ((a ^2) - ((4 * b) * x))) + a) is complex real ext-real set
- (- ((sqrt ((a ^2) - ((4 * b) * x))) + a)) is complex real ext-real set
(- a) - (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
((- a) - (sqrt ((a ^2) - ((4 * b) * x)))) / (2 * b) is complex real ext-real set

delta (b,a,x) is complex real ext-real Element of REAL
sqrt (delta (b,a,x)) is complex real ext-real Element of REAL
(- a) + (sqrt (delta (b,a,x))) is complex real ext-real set
((- a) + (sqrt (delta (b,a,x)))) / (2 * b) is complex real ext-real set
(- a) - (sqrt (delta (b,a,x))) is complex real ext-real set
((- a) - (sqrt (delta (b,a,x)))) / (2 * b) is complex real ext-real set

(4 * b) * x is complex real ext-real set
(a ^2) - ((4 * b) * x) is complex real ext-real set
- ((4 * b) * x) is complex real ext-real set
- (- ((4 * b) * x)) is complex real ext-real set

(a ^2) + (- ((4 * b) * x)) is complex real ext-real set

sqrt ((a ^2) - ((4 * b) * x)) is complex real ext-real set
a + (- a) is complex real ext-real set
0 + (a + (- a)) is complex real ext-real set
(- a) + (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
((- a) + (sqrt ((a ^2) - ((4 * b) * x)))) / (2 * b) is complex real ext-real set
a + (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set

- (a + (sqrt ((a ^2) - ((4 * b) * x)))) is complex real ext-real set
- (- (a + (sqrt ((a ^2) - ((4 * b) * x))))) is complex real ext-real set
(- a) - (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
((- a) - (sqrt ((a ^2) - ((4 * b) * x)))) / (2 * b) is complex real ext-real set
sqrt ((a ^2) - ((4 * b) * x)) is complex real ext-real set

(- a) + (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set

((- a) + (sqrt ((a ^2) - ((4 * b) * x)))) / (2 * b) is complex real ext-real set

4 * (b * x) is complex real ext-real set
- ((4 * b) * x) is complex real ext-real set
- (- ((4 * b) * x)) is complex real ext-real set

(a ^2) + (- ((4 * b) * x)) is complex real ext-real set

(0 + a) + (- a) is complex real ext-real set
a + (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
- (a + (sqrt ((a ^2) - ((4 * b) * x)))) is complex real ext-real set
(- a) - (sqrt ((a ^2) - ((4 * b) * x))) is complex real ext-real set
((- a) - (sqrt ((a ^2) - ((4 * b) * x)))) / (2 * b) is complex real ext-real set

delta (b,x,a) is complex real ext-real Element of REAL
sqrt (delta (b,x,a)) is complex real ext-real Element of REAL
(- x) + (sqrt (delta (b,x,a))) is complex real ext-real set
((- x) + (sqrt (delta (b,x,a)))) / (2 * b) is complex real ext-real set
(- x) - (sqrt (delta (b,x,a))) is complex real ext-real set
((- x) - (sqrt (delta (b,x,a)))) / (2 * b) is complex real ext-real set

(4 * b) * a is complex real ext-real set
- ((4 * b) * a) is complex real ext-real set

(x ^2) + (- ((4 * b) * a)) is complex real ext-real set

(x ^2) - ((4 * b) * a) is complex real ext-real set
sqrt ((x ^2) - ((4 * b) * a)) is complex real ext-real set

(- ((4 * b) * a)) + (x ^2) is complex real ext-real set

- (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
- (- (sqrt ((x ^2) - ((4 * b) * a)))) is complex real ext-real set

(- (sqrt ((x ^2) - ((4 * b) * a)))) + (- x) is complex real ext-real set
(- x) - (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
(- x) + (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set

(0 + x) + (- x) is complex real ext-real set
((- x) + (sqrt ((x ^2) - ((4 * b) * a)))) / (2 * b) is complex real ext-real set
x + (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
- (x + (sqrt ((x ^2) - ((4 * b) * a)))) is complex real ext-real set
- (- (x + (sqrt ((x ^2) - ((4 * b) * a))))) is complex real ext-real set
(- x) - (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
((- x) - (sqrt ((x ^2) - ((4 * b) * a)))) / (2 * b) is complex real ext-real set
(sqrt ((x ^2) - ((4 * b) * a))) + (- x) is complex real ext-real set
(sqrt (delta (b,x,a))) + (- x) is complex real ext-real set

(4 * b) * 0 is complex real ext-real set
(4 * b) * a is complex real ext-real set
- ((4 * b) * a) is complex real ext-real set

(x ^2) + (- ((4 * b) * a)) is complex real ext-real set

(x ^2) - ((4 * b) * a) is complex real ext-real set
sqrt ((x ^2) - ((4 * b) * a)) is complex real ext-real set

(- ((4 * b) * a)) + (x ^2) is complex real ext-real set

- (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
- (- (sqrt ((x ^2) - ((4 * b) * a)))) is complex real ext-real set

(- (sqrt ((x ^2) - ((4 * b) * a)))) + (- x) is complex real ext-real set
(- x) - (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
(- x) + (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set

(0 + x) + (- x) is complex real ext-real set
((- x) + (sqrt ((x ^2) - ((4 * b) * a)))) / (2 * b) is complex real ext-real set
x + (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
- (x + (sqrt ((x ^2) - ((4 * b) * a)))) is complex real ext-real set
- (- (x + (sqrt ((x ^2) - ((4 * b) * a))))) is complex real ext-real set
(- x) - (sqrt ((x ^2) - ((4 * b) * a))) is complex real ext-real set
((- x) - (sqrt ((x ^2) - ((4 * b) * a)))) / (2 * b) is complex real ext-real set
(sqrt ((x ^2) - ((4 * b) * a))) + (- x) is complex real ext-real set
(sqrt (delta (b,x,a))) + (- x) is complex real ext-real set

- (x -root a) is complex real ext-real set

(- b) |^ x is complex real ext-real set
x -root ((- b) |^ x) is complex real ext-real set
- 1 is non zero complex real ext-real non positive V33() set
(- 1) * (x -root a) is complex real ext-real set
(- 1) * (- b) is complex real ext-real set

- (b / a) is complex real ext-real set

Polynom (a,b,0,x) is complex real ext-real Element of REAL

a * (x ^2) is complex real ext-real set

(a * (x ^2)) + (b * x) is complex real ext-real set
((a * (x ^2)) + (b * x)) + 0 is complex real ext-real set

(a * x) + b is complex real ext-real set
((a * x) + b) + 0 is complex real ext-real set
(((a * x) + b) + 0) * x is complex real ext-real set

((a * x) + b) + (- b) is complex real ext-real set

(- b) / a is complex real ext-real set

Polynom (a,0,0,b) is complex real ext-real Element of REAL

a * (b ^2) is complex real ext-real set

(a * (b ^2)) + (0 * b) is complex real ext-real set
((a * (b ^2)) + (0 * b)) + 0 is complex real ext-real set

delta (a,b,x) is complex real ext-real Element of REAL
sqrt (delta (a,b,x)) is complex real ext-real Element of REAL
(- b) + (sqrt (delta (a,b,x))) is complex real ext-real set
((- b) + (sqrt (delta (a,b,x)))) / (2 * a) is complex real ext-real set
(- b) - (sqrt (delta (a,b,x))) is complex real ext-real set
((- b) - (sqrt (delta (a,b,x)))) / (2 * a) is complex real ext-real set

Polynom (a,b,x,(y |^ q)) is complex real ext-real Element of REAL
q -root (((- b) + (sqrt (delta (a,b,x)))) / (2 * a)) is complex real ext-real set
q -root (((- b) - (sqrt (delta (a,b,x)))) / (2 * a)) is complex real ext-real set

delta (a,b,x) is complex real ext-real Element of REAL
sqrt (delta (a,b,x)) is complex real ext-real Element of REAL
(- b) + (sqrt (delta (a,b,x))) is complex real ext-real set
((- b) + (sqrt (delta (a,b,x)))) / (2 * a) is complex real ext-real set
(- b) - (sqrt (delta (a,b,x))) is complex real ext-real set
((- b) - (sqrt (delta (a,b,x)))) / (2 * a) is complex real ext-real set

Polynom (a,b,x,(y |^ q)) is complex real ext-real Element of REAL
q -root (((- b) + (sqrt (delta (a,b,x)))) / (2 * a)) is complex real ext-real set
- (q -root (((- b) + (sqrt (delta (a,b,x)))) / (2 * a))) is complex real ext-real set
q -root (((- b) - (sqrt (delta (a,b,x)))) / (2 * a)) is complex real ext-real set
- (q -root (((- b) - (sqrt (delta (a,b,x)))) / (2 * a))) is complex real ext-real set

- (b / a) is complex real ext-real set

Polynom (a,b,0,(x |^ y)) is complex real ext-real Element of REAL
y -root (- (b / a)) is complex real ext-real set

- (b / a) is complex real ext-real set

Polynom (a,b,0,(x |^ y)) is complex real ext-real Element of REAL
y -root (- (b / a)) is complex real ext-real set
- (y -root (- (b / a))) is complex real ext-real set

(a |^ 3) + (b |^ 3) is complex real ext-real set

(a ^2) - (a * b) is complex real ext-real set

((a ^2) - (a * b)) + (b ^2) is complex real ext-real set
(a + b) * (((a ^2) - (a * b)) + (b ^2)) is complex real ext-real set

(a |^ 5) + (b |^ 5) is complex real ext-real set
(a |^ 3) * b is complex real ext-real set
(a |^ 4) - ((a |^ 3) * b) is complex real ext-real set

(a |^ 2) * (b |^ 2) is complex real ext-real set
((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2)) is complex real ext-real set
a * (b |^ 3) is complex real ext-real set
(((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2))) - (a * (b |^ 3)) is complex real ext-real set

((((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2))) - (a * (b |^ 3))) + (b |^ 4) is complex real ext-real set
(a + b) * (((((a |^ 4) - ((a |^ 3) * b)) + ((a |^ 2) * (b |^ 2))) - (a * (b |^ 3))) + (b |^ 4)) is complex real ext-real set
(a |^ 4) * a is complex real ext-real set
b * (a |^ 4) is complex real ext-real set
((a |^ 4) * a) + (b * (a |^ 4)) is complex real ext-real set
0 * (a |^ 4) is complex real ext-real set
(((a |^ 4) * a) + (b * (a |^ 4))) + (0 * (a |^ 4)) is complex real ext-real set
((a |^ 3) * b) * (a + b) is complex real ext-real set
((((a |^ 4) * a) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b)) is complex real ext-real set
((a |^ 2) * (b |^ 2)) * (a + b) is complex real ext-real set
(((((a |^ 4) * a) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b)) is complex real ext-real set
(a * (b |^ 3)) * (a + b) is complex real ext-real set
((((((a |^ 4) * a) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b)) is complex real ext-real set
(b |^ 4) * (a + b) is complex real ext-real set
(((((((a |^ 4) * a) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b))) + ((b |^ 4) * (a + b)) is complex real ext-real set

(a |^ 4) * (a |^ 1) is complex real ext-real set
((a |^ 4) * (a |^ 1)) + (b * (a |^ 4)) is complex real ext-real set
(((a |^ 4) * (a |^ 1)) + (b * (a |^ 4))) + (0 * (a |^ 4)) is complex real ext-real set
((((a |^ 4) * (a |^ 1)) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b)) is complex real ext-real set
(((((a |^ 4) * (a |^ 1)) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b)) is complex real ext-real set
((((((a |^ 4) * (a |^ 1)) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b)) is complex real ext-real set
(((((((a |^ 4) * (a |^ 1)) + (b * (a |^ 4))) + (0 * (a |^ 4))) - (((a |^ 3) * b) * (a + b))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b))) + ((b |^ 4) * (a + b)) is complex real ext-real set

a |^ (4 + 1) is complex real ext-real Element of REAL
(a |^ (4 + 1)) + (b * (a |^ 4)) is complex real ext-real set
(a + b) + 0 is complex real ext-real set
((a |^ 3) * b) * ((a + b) + 0) is complex real ext-real set
((a |^ (4 + 1)) + (b * (a |^ 4))) - (((a |^ 3) * b) * ((a + b) + 0)) is complex real ext-real set
(((a |^ (4 + 1)) + (b * (a |^ 4))) - (((a |^ 3) * b) * ((a + b) + 0))) + (((a |^ 2) * (b |^ 2)) * (a + b)) is complex real ext-real set
((((a |^ (4 + 1)) + (b * (a |^ 4))) - (((a |^ 3) * b) * ((a + b) + 0))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b)) is complex real ext-real set
(((((a |^ (4 + 1)) + (b * (a |^ 4))) - (((a |^ 3) * b) * ((a + b) + 0))) + (((a |^ 2) * (b |^ 2)) * (a + b))) - ((a * (b |^ 3)) * (a + b))) + ((b |^ 4) * (a + b)) is complex real ext-real set
(a |^ 5) + (b * (a |^ 4)) is complex real ext-real set
a * (a |^ 3) is complex real ext-real set
(a * (a |^ 3)) * b is complex real ext-real set
b * ((a |^ 3) * b) is complex real ext-real set
((a * (a |^ 3)) * b) + (b * ((a |^ 3) * b)) is complex real ext-real set
((a |^ 5) + (b * (a |^ 4))) - (((a * (a |^ 3)) * b) + (b * ((a |^ 3) * b))) is complex real ext-real set
a * ((a |^ 2) * (b |^ 2)) is complex real ext-real set
b * ((a |^ 2) * (b |^ 2)) is complex real ext-real set
(a * ((a |^ 2) * (b |^ 2))) + (b * ((a |^ 2) * (b |^ 2))) is complex real ext-real set
(((a |^ 5) + (b * (a |^ 4))) - (((a * (a |^ 3)) * b) + (b * ((a |^ 3) * b)))) + ((a * ((a |^ 2) * (b |^ 2))) + (b * ((a |^ 2) * (b |^ 2)))) is complex real ext-real set
a * (a * (b |^ 3)) is complex real ext-real set
b * (a * (b |^ 3)) is complex real ext-real set
(a * (a * (b |^ 3))) + (b * (a * (b |^ 3))) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a * (a |^ 3)) * b) + (b * ((a |^ 3) * b)))) + ((a * ((a |^ 2) * (b |^ 2))) + (b * ((a |^ 2) * (b |^ 2))))) - ((a * (a * (b |^ 3))) + (b * (a * (b |^ 3)))) is complex real ext-real set
a * (b |^ 4) is complex real ext-real set
b * (b |^ 4) is complex real ext-real set
(a * (b |^ 4)) + (b * (b |^ 4)) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a * (a |^ 3)) * b) + (b * ((a |^ 3) * b)))) + ((a * ((a |^ 2) * (b |^ 2))) + (b * ((a |^ 2) * (b |^ 2))))) - ((a * (a * (b |^ 3))) + (b * (a * (b |^ 3))))) + ((a * (b |^ 4)) + (b * (b |^ 4))) is complex real ext-real set
(a |^ 4) * b is complex real ext-real set
(b * b) * (a |^ 3) is complex real ext-real set
((a |^ 4) * b) + ((b * b) * (a |^ 3)) is complex real ext-real set
((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3))) is complex real ext-real set
(a |^ 2) * a is complex real ext-real set
((a |^ 2) * a) * (b |^ 2) is complex real ext-real set
b * (b |^ 2) is complex real ext-real set
(b * (b |^ 2)) * (a |^ 2) is complex real ext-real set
(((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2)) is complex real ext-real set
(((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + ((((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2))) is complex real ext-real set
(a * a) * (b |^ 3) is complex real ext-real set
b * (b |^ 3) is complex real ext-real set
(b * (b |^ 3)) * a is complex real ext-real set
((a * a) * (b |^ 3)) + ((b * (b |^ 3)) * a) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + ((((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b * (b |^ 3)) * a)) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + ((((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b * (b |^ 3)) * a))) + ((a * (b |^ 4)) + (b * (b |^ 4))) is complex real ext-real set
(b |^ 4) * a is complex real ext-real set
((a * a) * (b |^ 3)) + ((b |^ 4) * a) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + ((((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a)) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + ((((a |^ 2) * a) * (b |^ 2)) + ((b * (b |^ 2)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b * (b |^ 4))) is complex real ext-real set

a |^ (2 + 1) is complex real ext-real Element of REAL
(a |^ (2 + 1)) * (b |^ 2) is complex real ext-real set
(b |^ 2) * b is complex real ext-real set
((b |^ 2) * b) * (a |^ 2) is complex real ext-real set
((a |^ (2 + 1)) * (b |^ 2)) + (((b |^ 2) * b) * (a |^ 2)) is complex real ext-real set
(((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ (2 + 1)) * (b |^ 2)) + (((b |^ 2) * b) * (a |^ 2))) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ (2 + 1)) * (b |^ 2)) + (((b |^ 2) * b) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a)) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ (2 + 1)) * (b |^ 2)) + (((b |^ 2) * b) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b * (b |^ 4))) is complex real ext-real set
(a |^ 3) * (b |^ 2) is complex real ext-real set
b |^ (2 + 1) is complex real ext-real Element of REAL
(b |^ (2 + 1)) * (a |^ 2) is complex real ext-real set
((a |^ 3) * (b |^ 2)) + ((b |^ (2 + 1)) * (a |^ 2)) is complex real ext-real set
(((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ (2 + 1)) * (a |^ 2))) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ (2 + 1)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a)) is complex real ext-real set
(b |^ 4) * b is complex real ext-real set
(a * (b |^ 4)) + ((b |^ 4) * b) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ (2 + 1)) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + ((b |^ 4) * b)) is complex real ext-real set
(b |^ 3) * (a |^ 2) is complex real ext-real set
((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)) is complex real ext-real set
(((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2))) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a)) is complex real ext-real set
b |^ (4 + 1) is complex real ext-real Element of REAL
(a * (b |^ 4)) + (b |^ (4 + 1)) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ (4 + 1))) is complex real ext-real set

(b |^ 1) * b is complex real ext-real set
((b |^ 1) * b) * (a |^ 3) is complex real ext-real set
((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)) is complex real ext-real set
((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3))) is complex real ext-real set
(((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2))) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a)) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - (((a * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ (4 + 1))) is complex real ext-real set
(a |^ 1) * a is complex real ext-real set
((a |^ 1) * a) * (b |^ 3) is complex real ext-real set
(((a |^ 1) * a) * (b |^ 3)) + ((b |^ 4) * a) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - ((((a |^ 1) * a) * (b |^ 3)) + ((b |^ 4) * a)) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + (((b |^ 1) * b) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - ((((a |^ 1) * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ (4 + 1))) is complex real ext-real set

b |^ (1 + 1) is complex real ext-real Element of REAL
(b |^ (1 + 1)) * (a |^ 3) is complex real ext-real set
((a |^ 4) * b) + ((b |^ (1 + 1)) * (a |^ 3)) is complex real ext-real set
((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b |^ (1 + 1)) * (a |^ 3))) is complex real ext-real set
(((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b |^ (1 + 1)) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2))) is complex real ext-real set
((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b |^ (1 + 1)) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - ((((a |^ 1) * a) * (b |^ 3)) + ((b |^ 4) * a)) is complex real ext-real set
(a * (b |^ 4)) + (b |^ 5) is complex real ext-real set
(((((a |^ 5) + (b * (a |^ 4))) - (((a |^ 4) * b) + ((b |^ (1 + 1)) * (a |^ 3)))) + (((a |^ 3) * (b |^ 2)) + ((b |^ 3) * (a |^ 2)))) - ((((a |^ 1) * a) * (b |^ 3)) + ((b |^ 4) * a))) + ((a * (b |^ 4)) + (b |^ 5)) is complex real ext-real set
(a |^ 2) * (b |^ 3) is complex real ext-real set
(a |^ 5) + ((a |^ 2) * (b |^ 3)) is complex real ext-real set
((a |^ 2) * (b |^ 3)) + (a * (b |^ 4)) is complex real ext-real set
((a |^ 5) + ((a |^ 2) * (b |^ 3))) - (((a |^ 2) * (b |^ 3)) + (a * (b |^ 4))) is complex real ext-real set
(((a |^ 5) + ((a |^ 2) * (b |^ 3))) - (((a |^ 2) * (b |^ 3)) + (a * (b |^ 4)))) + ((a * (b |^ 4)) + (b |^ 5)) is complex real ext-real set
(((a ^2) - (a * b)) + (b ^2)) * (a + b) is complex real ext-real set
(a ^2) * a is complex real ext-real set
b * (a ^2) is complex real ext-real set
((a ^2) * a) + (b * (a ^2)) is complex real ext-real set
a * (a * b) is complex real ext-real set
b * (a * b) is complex real ext-real set
(a * (a * b)) + (b * (a * b)) is complex real ext-real set
(((a ^2) * a) + (b * (a ^2))) - ((a * (a * b)) + (b * (a * b))) is complex real ext-real set
a * (b ^2) is complex real ext-real set
b * (b ^2) is complex real ext-real set
(a * (b ^2)) + (b * (b ^2)) is complex real ext-real set

((a * (b ^2)) + (b * (b ^2))) + (0 * (b ^2)) is complex real ext-real set
((((a ^2) * a) + (b * (a ^2))) - ((a * (a * b)) + (b * (a * b)))) + (((a * (b ^2)) + (b * (b ^2))) + (0 * (b ^2))) is complex real ext-real set
(a |^ 3) + (b * (a ^2)) is complex real ext-real set
((a |^ 3) + (b * (a ^2))) - ((a * (a * b)) + (b * (a * b))) is complex real ext-real set
(((a |^ 3) + (b * (a ^2))) - ((a * (a * b)) + (b * (a * b)))) + ((a * (b ^2)) + (b * (b ^2))) is complex real ext-real set
(a ^2) * b is complex real ext-real set
(b * b) * a is complex real ext-real set
((a ^2) * b) + ((b * b) * a) is complex real ext-real set
((a |^ 3) + (b * (a ^2))) - (((a ^2) * b) + ((b * b) * a)) is complex real ext-real set
(a * (b ^2)) + (b |^ 3) is complex real ext-real set
(((a |^ 3) + (b * (a ^2))) - (((a ^2) * b) + ((b * b) * a))) + ((a * (b ^2)) + (b |^ 3)) is complex real ext-real set
- 1 is non zero complex real ext-real non positive V33() set

3 * (a ^2) is complex real ext-real set

(2 * a) * b is complex real ext-real set
(b ^2) - ((2 * a) * b) is complex real ext-real set
((b ^2) - ((2 * a) * b)) - (3 * (a ^2)) is complex real ext-real set

sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))) is complex real ext-real set
(a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2)))) is complex real ext-real set
((a - b) + (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) is complex real ext-real set
(a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2)))) is complex real ext-real set
((a - b) - (sqrt (((b ^2) - ((2 * a) * b)) - (3 * (a ^2))))) / (2 * a) is complex real ext-real set

Polynom (a,b,b,a,x) is complex real ext-real Element of REAL

a * (x |^ 3) is complex real ext-real set

b * (x ^2) is complex real ext-real set
(a * (x |^ 3)) + (b * (x ^2)) is complex real ext-real set

((a * (x |^ 3)) + (b * (x ^2))) + (b * x) is complex real ext-real set
(((a * (x |^ 3)) + (b * (x ^2))) + (b * x)) + a is complex real ext-real set
(x |^ 3) + 1 is complex real ext-real set
((x |^ 3) + 1) * a is complex real ext-real set
(x ^2) + x is complex real ext-real set
((x ^2) + x) + 0 is complex real ext-real set
(((x ^2) + x) + 0) * b is complex real ext-real set
(((x |^ 3) + 1) * a) + ((((x ^2) + x) + 0) * b) is complex real ext-real set

(x |^ 3) + (1 to_power 3) is complex real ext-real set
((x |^ 3) + (1 to_power 3)) * a is complex real ext-real set

(x + 1) * x is complex real ext-real set
((x + 1) * x) * b is complex real ext-real set
(((x |^ 3) + (1 to_power 3)) * a) + (((x + 1) * x) * b) is complex real ext-real set

(x ^2) - (x * 1) is complex real ext-real set

((x ^2) - (x * 1)) + (1 ^2) is complex real ext-real set
(x + 1) * (((x ^2) - (x * 1)) + (1 ^2)) is complex real ext-real set
((x + 1) * (((x ^2) - (x * 1)) + (1 ^2))) * a is complex real ext-real set
(((x + 1) * (((x ^2) - (x * 1)) + (1 ^2))) * a) + (((x + 1) * x) * b) is complex real ext-real set
(x ^2) * a is complex real ext-real set

((x ^2) * a) - (x * a) is complex real ext-real set

(((x ^2) * a) - (x * a)) + (x * b) is complex real ext-real set
((((x ^2) * a) - (x * a)) + (x * b)) + a is complex real ext-real set
(((((x ^2) * a) - (x * a)) + (x * b)) + a) * (x + 1) is complex real ext-real set
a * (x ^2) is complex real ext-real set
(a - b) * x is complex real ext-real set
(a * (x ^2)) - ((a - b) * x) is complex real ext-real set
((a * (x ^2)) - ((a - b) * x)) + a is complex real ext-real set

(- a) + b is complex real ext-real set
delta (a,((- a) + b),a) is complex real ext-real set
((- a) + b) ^2 is complex real ext-real set
((- a) + b) * ((- a) + b) is complex real ext-real set

(4 * a) * a is complex real ext-real set
(((- a) + b) ^2) - ((4 * a) * a) is complex real ext-real set
4 - 1 is complex real ext-real V33() set
- (4 - 1) is complex real ext-real V33() set
(- (4 - 1)) * (a ^2) is complex real ext-real set
((b ^2) - ((2 * a) * b)) + ((- (4 - 1)) * (a ^2)) is complex real ext-real set
((- a) + b) * x is complex real ext-real set
(a * (x ^2)) + (((- a) + b) * x) is complex real ext-real set
((a * (x ^2)) + (((- a) + b) * x)) + a is complex real ext-real set
Polynom (a,((- a) + b),a,x) is set
- ((- a) + b) is complex real ext-real set
sqrt (delta (a,((- a) + b),a)) is complex real ext-real set
(- ((- a) + b)) + (sqrt (delta (a,((- a) + b),a))) is complex real ext-real set
((- ((- a) + b)) + (sqrt (delta (a,((- a) + b),a)))) / (2 * a) is complex real ext-real set
(- ((- a) + b)) - (sqrt (delta (a,((- a) + b),a))) is complex real ext-real set
((- ((- a) + b)) - (sqrt (delta (a,((- a) + b),a)))) / (2 * a) is complex real ext-real set
a * (x ^2) is complex real ext-real set
(a - b) * x is complex real ext-real set
(a * (x ^2)) - ((a - b) * x) is complex real ext-real set
((a * (x ^2)) - ((a - b) * x)) + a is complex real ext-real set
a * (x ^2) is complex real ext-real set
(a - b) * x is complex real ext-real set
(a * (x ^2)) - ((a - b) * x) is complex real ext-real set
((a * (x ^2)) - ((a - b) * x)) + a is complex real ext-real set
a is complex set
m is complex set
m |^ 5 is complex set
a * (m |^ 5) is complex set
b is complex set
m |^ 4 is complex set
b * (m |^ 4) is complex set
(a * (m |^ 5)) + (b * (m |^ 4)) is complex set
x is complex set
m |^ 3 is complex set
x * (m |^ 3) is complex set
((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3)) is complex set
y is complex set
m ^2 is complex set
m * m is complex set
y * (m ^2) is complex set
(((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2)) is complex set
q is complex set
q * m is complex set
((((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2))) + (q * m) is complex set
n is complex set
(((((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2))) + (q * m)) + n is complex set
a is complex set
b is complex set
x is complex set
y is complex set
q is complex set
n is complex set
m is complex set
(a,b,x,y,q,n,m) is set
m |^ 5 is complex set
a * (m |^ 5) is complex set
m |^ 4 is complex set
b * (m |^ 4) is complex set
(a * (m |^ 5)) + (b * (m |^ 4)) is complex set
m |^ 3 is complex set
x * (m |^ 3) is complex set
((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3)) is complex set
m ^2 is complex set
m * m is complex set
y * (m ^2) is complex set
(((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2)) is complex set
q * m is complex set
((((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2))) + (q * m) is complex set
(((((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2))) + (q * m)) + n is complex set

(a,b,x,y,q,n,m) is complex set

a * (m |^ 5) is complex real ext-real set

b * (m |^ 4) is complex real ext-real set
(a * (m |^ 5)) + (b * (m |^ 4)) is complex real ext-real set

x * (m |^ 3) is complex real ext-real set
((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3)) is complex real ext-real set

y * (m ^2) is complex real ext-real set
(((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2)) is complex real ext-real set

((((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2))) + (q * m) is complex real ext-real set
(((((a * (m |^ 5)) + (b * (m |^ 4))) + (x * (m |^ 3))) + (y * (m ^2))) + (q * m)) + n is complex real ext-real set

5 * (a ^2) is complex real ext-real set

(2 * a) * b is complex real ext-real set
(b ^2) + ((2 * a) * b) is complex real ext-real set
((b ^2) + ((2 * a) * b)) + (5 * (a ^2)) is complex real ext-real set

(4 * a) * x is complex real ext-real set
(((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * x) is complex real ext-real set
sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * x)) is complex real ext-real set
(a - b) + (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * x))) is complex real ext-real set
((a - b) + (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * x)))) / (2 * a) is complex real ext-real set
(a - b) - (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * x))) is complex real ext-real set
((a - b) - (sqrt ((((b ^2) + ((2 * a) * b)) + (5 * (a ^2))) - ((4 * a) * x)))) / (2 * a) is complex real ext-real set

(a,b,x,x,b,a,y) is complex real ext-real set

a * (y |^ 5) is complex real ext-real set

b * (y |^ 4) is complex real ext-real set
(a * (y |^ 5)) + (b * (y |^ 4)) is complex real ext-real set

x * (y |^ 3) is complex real ext-real set
((a * (y |^ 5)) + (b * (y |^ 4))) + (x * (y |^ 3)) is complex real ext-real set

x * (y ^2) is complex real ext-real set
(((a * (y |^ 5)) + (b * (y |^ 4))) + (x * (y |^ 3))) + (x * (y ^2)) is complex real ext-real set

((((a * (y |^ 5)) + (b * (y |^ 4))) + (x * (y |^ 3))) + (x * (y ^2))) + (b * y) is complex real ext-real set
(((((a * (y |^ 5)) + (b * (y |^ 4))) + (x * (y |^ 3))) + (x * (y ^2))) + (b * y)) + a is complex real ext-real set

delta (1,(- q),1) is complex real ext-real set
sqrt (delta (1,(- q),1)) is complex real ext-real set
q + (sqrt (delta (1,(- q),1))) is complex real ext-real set
(q + (sqrt (delta (1,(- q),1)))) / 2 is complex real ext-real set

delta (1,(- n),1) is complex real ext-real set
sqrt (delta (1,(- n),1)) is complex real ext-real set
n + (sqrt (delta (1,(- n),1))) is complex real ext-real set
(n + (sqrt (delta (1,(- n),1)))) / 2 is complex real ext-real set
q - (sqrt (delta (1,(- q),1))) is complex real ext-real set
(q - (sqrt (delta (1,(- q),1)))) / 2 is complex real ext-real set
n - (sqrt (delta (1,(- n),1))) is complex real ext-real set
(n - (sqrt (delta (1,(- n),1)))) / 2 is complex real ext-real set

(y |^ 5) + 1 is complex real ext-real set
((y |^ 5) + 1) * a is complex real ext-real set

(y |^ 4) + y is complex real ext-real set
((y |^ 4) + y) + 0 is complex real ext-real set
(((y |^ 4) + y) + 0) * b is complex real ext-real set
(((y |^ 5) + 1) * a) + ((((y |^ 4) + y) + 0) * b) is complex real ext-real set

x * (y |^ 3) is complex real ext-real set

x * (y ^2) is complex real ext-real set
(x * (y |^ 3)) + (x * (y ^2)) is complex real ext-real set

((x * (y |^ 3)) + (x * (y ^2))) + (0 * x) is complex real ext-real set
((((y |^ 5) + 1) * a) + ((((y |^ 4) + y) + 0) * b)) + (((x * (y |^ 3)) + (x * (y ^2))) + (0 * x)) is complex real ext-real set

(y |^ 5) + (1 |^ 5) is complex real ext-real set
((y |^ 5) + (1 |^ 5)) * a is complex real ext-real set

y |^ (3 + 1) is complex real ext-real Element of REAL
(y |^ (3 + 1)) + y is complex real ext-real set
((y |^ (3 + 1)) + y) * b is