Anillo tal que $x^4=x$ % todo $x$es conmutativa

Question

Que $R$ ser un anillo tal que $x^4=x$ cada $x\in R$. ¿Este anillo es conmutativa?

Answer 1

Aquí es una observación interesante:

$2x=(x+x)=(x+x)^4=16x^4=16x$. Así $14x=0$.

También $3x=(3x)^4=81x^4=81x$. Así $78x=0$. Puesto que MCD $(78,14) =2$ obtenemos $2x=0$ % todos $x \in R$.

Ahora uno probablemente tiene que ver en % y $x+y=(x+y)^4$ $(x+y+z)=(x+y+z)^4$o $(x+y+1)=(x+y+1)^4$.

P.D. Realmente característica 2 también se obtiene la siguiente forma: $x=x^4=(-x)^4=-x$.

Answer 2

En mi anterior versión de esta respuesta, me dio un fichero automatizado de Prover9 prueba de este resultado el uso de un paso-a-paso. Resulta que esto es innecesario. Anteriormente, he utilizado el defecto Lexicográfica del Camino de Pedidos, mientras que la Knuth-Bendix de los Pedidos (assign(order, kbo).)es mucho más rápida para este problema (ref.), y podemos obtener una prueba:

============================== PROOF =================================

% Proof 1 at 46.52 (+ 0.36) seconds.
% Length of proof is 243.
% Level of proof is 45.
% Maximum clause weight is 35.
% Given clauses 639.

1 x * y = y * x # label(non_clause) # label(goal).  [goal].
2 (x + y) + z = x + (y + z).  [assumption].
3 x + y = y + x.  [assumption].
4 x + 0 = x.  [assumption].
5 0 + x = x.  [assumption].
6 x + -x = 0.  [assumption].
8 x * (y + z) = (x * y) + (x * z).  [assumption].
9 (x * y) + (x * z) = x * (y + z).  [copy(8),flip(a)].
10 (x + y) * z = (x * z) + (y * z).  [assumption].
11 (x * y) + (z * y) = (x + z) * y.  [copy(10),flip(a)].
12 (x * y) * z = x * (y * z).  [assumption].
13 x * (x * (x * x)) = x.  [assumption].
14 c2 * c1 != c1 * c2.  [deny(1)].
15 x + (y + z) = y + (x + z).  [para(3(a,1),2(a,1,1)),rewrite([2(2)])].
16 x + (-x + y) = y.  [para(6(a,1),2(a,1,1)),rewrite([5(2)]),flip(a)].
18 -x + (y + x) = y.  [para(6(a,1),2(a,2,2)),rewrite([3(3),4(5)])].
20 (x * y) + ((x * z) + u) = (x * (y + z)) + u.  [para(9(a,1),2(a,1,1)),flip(a)].
21 (x * y) + ((z * y) + u) = ((x + z) * y) + u.  [para(11(a,1),2(a,1,1)),flip(a)].
22 (x + x) * y = x * (y + y).  [para(11(a,1),9(a,1))].
23 (x * (y * z)) + (u * z) = ((x * y) + u) * z.  [para(12(a,1),11(a,1,1))].
24 (x * y) + (z * (u * y)) = (x + (z * u)) * y.  [para(12(a,1),11(a,1,2))].
25 x * ((x * (x * x)) + y) = x + (x * y).  [para(13(a,1),9(a,1,1)),flip(a)].
26 x * (y + (x * (x * x))) = x + (x * y).  [para(13(a,1),9(a,1,2)),rewrite([3(2)]),flip(a)].
27 (x + y) * (x * (x * x)) = x + (y * (x * (x * x))).  [para(13(a,1),11(a,1,1)),flip(a)].
29 x * (x * (x * (x * y))) = x * y.  [para(13(a,1),12(a,1,1)),rewrite([12(4),12(3)]),flip(a)].
30 x * (y * (x * (y * (x * (y * (x * y)))))) = x * y.  [para(13(a,1),12(a,1)),rewrite([12(5),12(6)]),flip(a)].
31 x + (y + -x) = y.  [para(6(a,1),15(a,1,2)),rewrite([4(2)]),flip(a)].
32 (x * y) + (z + (x * u)) = z + (x * (y + u)).  [para(9(a,1),15(a,1,2)),flip(a)].
36 --x = x.  [para(6(a,1),16(a,1,2)),rewrite([4(2)]),flip(a)].
39 -(x * y) + (x * (z + y)) = x * z.  [para(9(a,1),18(a,1,2))].
43 x + -(x + y) = -y.  [para(18(a,1),18(a,1,2)),rewrite([3(3)])].
49 x + (y + (z + -x)) = y + z.  [para(2(a,1),31(a,1,2))].
58 (x * y) + -(x * (y + z)) = -(x * z).  [para(9(a,1),43(a,1,2,1))].
66 (x * (y + z)) + (u * z) = (x * y) + ((x + u) * z).  [para(11(a,1),20(a,1,2)),flip(a)].
73 0 * (x + x) = 0 * x.  [para(4(a,1),22(a,1,1)),flip(a)].
74 (x + x) * 0 = x * 0.  [para(4(a,1),22(a,2,2))].
98 0 * (x + (x + y)) = 0 * (x + y).  [para(73(a,1),9(a,1,1)),rewrite([9(5),2(6)]),flip(a)].
105 (x + (x + y)) * 0 = (x + y) * 0.  [para(74(a,1),11(a,1,1)),rewrite([11(5),2(5)]),flip(a)].
114 ((x + y) * z) + (y * u) = (x * z) + (y * (z + u)).  [para(9(a,1),21(a,1,2)),flip(a)].
116 (x * y) + ((z * (u * y)) + w) = ((x + (z * u)) * y) + w.  [para(12(a,1),21(a,1,2,1))].
119 -(x * y) + ((x + z) * y) = z * y.  [para(21(a,1),31(a,1)),rewrite([3(5)])].
143 x * ((x * (x * (x * y))) + z) = x * (y + z).  [para(29(a,1),9(a,1,1)),rewrite([9(3)]),flip(a)].
144 x * (y + (x * (x * (x * z)))) = x * (y + z).  [para(29(a,1),9(a,1,2)),rewrite([9(3)]),flip(a)].
146 x * (y * (x * (y * (x * (y * (x * (y * z))))))) = x * (y * z).  [para(29(a,1),12(a,1)),rewrite([12(2),12(6),12(7),12(8)]),flip(a)].
154 (x + (x * y)) * z = x * (z + (y * z)).  [para(23(a,1),9(a,1)),rewrite([3(2),3(5)])].
155 (x * (y * (z * u))) + (w * u) = ((x * (y * z)) + w) * u.  [para(12(a,1),23(a,1,1,2))].
156 (x * (y * z)) + (u * (w * z)) = ((x * y) + (u * w)) * z.  [para(12(a,1),23(a,1,2))].
157 ((x * y) + z) * (y * (y * y)) = (x * y) + (z * (y * (y * y))).  [para(13(a,1),23(a,1,1,2)),flip(a)].
158 ((x * x) + y) * (x * x) = x + (y * (x * x)).  [para(13(a,1),23(a,1,1)),flip(a)].
159 (x * (y * z)) + (u + (w * z)) = u + (((x * y) + w) * z).  [para(23(a,1),15(a,1,2)),flip(a)].
173 (x * (y * z)) + (u * (y * (y * (y * z)))) = ((x * y) + u) * (y * (y * (y * z))).  [para(29(a,1),23(a,1,1,2))].
174 ((x * x) + y) * (x * (x * z)) = (x * z) + (y * (x * (x * z))).  [para(29(a,1),23(a,1,1)),flip(a)].
178 0 * 0 = 0 * x.  [para(6(a,1),98(a,1,2,2)),rewrite([4(3),6(5)]),flip(a)].
191 0 * 0 = 0.  [para(178(a,1),13(a,1,2,2)),rewrite([178(5,R),178(5,R)])].
193 0 * x = 0.  [para(178(a,2),22(a,2)),rewrite([4(3),191(5)])].
198 x * 0 = 0.  [para(6(a,1),105(a,1,1,2)),rewrite([4(2),6(4),193(5)])].
199 (x * y) + (z * (u * (w * y))) = (x + (z * (u * w))) * y.  [para(12(a,1),24(a,1,2,2))].
200 (x + (y * z)) * (z * (z * z)) = ((x * (z * z)) + y) * z.  [para(13(a,1),24(a,1,2,2)),rewrite([155(5)]),flip(a)].
201 (x + (y * y)) * (y * y) = y + (x * (y * y)).  [para(13(a,1),24(a,1,2)),rewrite([3(3)]),flip(a)].
202 (x * y) + (z + (u * (w * y))) = z + ((x + (u * w)) * y).  [para(24(a,1),15(a,1,2)),flip(a)].
215 (x + (y * y)) * (y * (y * z)) = (y + (x * (y * y))) * z.  [para(29(a,1),24(a,1,2)),rewrite([3(5),199(5)]),flip(a)].
216 ((x * x) + y) * (x * (x * z)) = (x + (y * (x * x))) * z.  [back_rewrite(174),rewrite([199(10)])].
217 ((x * y) + z) * (y * (y * (y * u))) = (x + (z * (y * y))) * (y * u).  [back_rewrite(173),rewrite([199(7)]),flip(a)].
218 ((x * y) + z) * (y * (y * y)) = (x + (z * (y * y))) * y.  [back_rewrite(157),rewrite([199(10)])].
225 -(x * y) = x * -y.  [para(18(a,1),39(a,1,2,2)),rewrite([3(5),58(5)])].
242 (x * -y) + ((x + z) * y) = z * y.  [back_rewrite(119),rewrite([225(2)])].
247 x * (x * (x * -x)) = -x.  [para(13(a,1),225(a,1,1)),rewrite([225(4),225(3)]),flip(a)].
256 x * (y * (x * (y * (x * (y * (x * -y)))))) = x * -y.  [para(247(a,1),12(a,1)),rewrite([225(2),225(6),12(7),12(8)]),flip(a)].
257 -x * (-x * (-x * x)) = x.  [para(36(a,1),247(a,1,2,2,2)),rewrite([36(8)])].
268 x * (x * ((x * x) + y)) = x + (x * (x * y)).  [para(9(a,1),25(a,1,2))].
272 x * (((x * (x * x)) + y) * z) = (x + (x * y)) * z.  [para(25(a,1),12(a,1,1)),flip(a)].
305 x * (-y * (x * (-y * (x * (-y * (x * y)))))) = x * y.  [para(225(a,1),257(a,1,1)),rewrite([225(4),225(6),12(8),12(9),12(10)])].
326 -x * y = x * -y.  [para(6(a,1),242(a,1,2,1)),rewrite([193(4),3(4),5(4)]),flip(a)].
348 x * -y = x * y.  [back_rewrite(305),rewrite([326(5),225(4),326(7),225(6),225(5),225(4),36(3),326(7),225(6),225(5),225(4),225(3),225(2),256(8)])].
369 -x = x.  [back_rewrite(247),rewrite([348(2),13(3)]),flip(a)].
399 x + (y + (z + x)) = y + z.  [back_rewrite(49),rewrite([369(1)])].
401 x + (y + x) = y.  [back_rewrite(31),rewrite([369(1)])].
402 x + (x + y) = y.  [back_rewrite(16),rewrite([369(1)])].
403 x + x = 0.  [back_rewrite(6),rewrite([369(1)])].
405 x * (x * (y + (x * x))) = x + (x * (x * y)).  [para(9(a,1),26(a,1,2))].
408 x * ((y + (x * (x * x))) * z) = (x + (x * y)) * z.  [para(26(a,1),12(a,1,1)),flip(a)].
412 x + ((x * y) + (z * (u * (y + (x * (x * x)))))) = ((z * u) + x) * (y + (x * (x * x))).  [para(26(a,1),23(a,1,2)),rewrite([3(8),2(8)])].
414 x * ((y + (x * x)) * x) = x + (x * (y * x)).  [para(24(a,1),26(a,1,2))].
416 x + ((y * (x * (x * x))) + ((x + y) * z)) = (x + y) * ((x * (x * x)) + z).  [para(27(a,1),9(a,1,1)),rewrite([2(7)])].
422 (x + (y * (x * (x * x)))) * z = (x + y) * (x * (x * (x * z))).  [para(27(a,1),12(a,1,1)),rewrite([12(9),12(8)])].
444 (x + (x * y)) * (y * z) = x * (y * (z + (y * z))).  [para(9(a,1),154(a,2,2))].
449 (x + (x * y)) * (z * u) = x * ((z + (y * z)) * u).  [para(154(a,1),12(a,1,1)),rewrite([12(4)]),flip(a)].
451 (x + (x * (y * z))) * u = x * (u + (y * (z * u))).  [para(12(a,1),154(a,2,2,2))].
564 (x * y) + ((z + x) * u) = (z * u) + (x * (y + u)).  [para(11(a,1),32(a,1,2))].
566 ((x + y) * z) + (x * u) = (y * z) + (x * (z + u)).  [para(32(a,1),21(a,1)),flip(a)].
602 x * (x * ((x * (x * y)) + z)) = x * (y + (x * z)).  [para(9(a,1),143(a,1,2))].
636 x * (x * (y + (x * (x * z)))) = x * ((x * y) + z).  [para(9(a,1),144(a,1,2))].
805 ((x + y) * z) + (x * u) = (x * (u + z)) + (y * z).  [para(66(a,2),3(a,1)),flip(a)].
839 (x * (y + z)) + ((u + x) * z) = (x * y) + (u * z).  [para(401(a,1),66(a,2,2,1))].
931 x * (y + ((z + (x * x)) * x)) = x + (x * (y + (z * x))).  [para(414(a,1),9(a,1,2)),rewrite([15(5),9(4)]),flip(a)].
933 x * ((y + (x * x)) * (x * z)) = (x + (x * (y * x))) * z.  [para(414(a,1),12(a,1,1)),rewrite([12(8)]),flip(a)].
940 (x + (y * (z + (y * y)))) * y = y + ((x + (y * z)) * y).  [para(414(a,1),24(a,1,2)),rewrite([15(5),24(4)]),flip(a)].
997 ((x + y) * z) + (y * (u + z)) = (x * z) + (y * u).  [para(401(a,1),114(a,2,2,2))].
998 (x * y) + ((z + x) * u) = (z * y) + ((z + x) * (y + u)).  [para(402(a,1),114(a,1,1,1))].
1233 (x + (x * (x * x))) * x = x + (x * x).  [para(272(a,1),414(a,1)),rewrite([12(7),12(6),13(7)])].
1248 (x + (x * (x * x))) * (x * y) = (x + (x * x)) * y.  [para(1233(a,1),12(a,1,1)),flip(a)].
1256 (x + (x * (x * x))) * (y + (x * y)) = x * ((x + (x * x)) * y).  [para(1233(a,1),154(a,1,1,2)),rewrite([3(6),15(6),2(5),9(4),402(5),12(4)]),flip(a)].
1876 (x + (x * x)) * (y + (x * y)) = (x + (x * (x * x))) * y.  [para(1233(a,1),444(a,1,1,2)),rewrite([3(6),15(6),2(5),9(4),402(5),12(5),933(5),1248(11)]),flip(a)].
2110 (x + (x * (x * x))) * ((y + (x * y)) * z) = x * ((x + (x * x)) * (y * z)).  [para(1233(a,1),449(a,1,1,2)),rewrite([3(6),15(6),2(5),9(4),402(5),12(5)]),flip(a)].
7294 ((x * (x * x)) + y) * x = x + (y * x).  [para(13(a,1),155(a,1,1)),flip(a)].
7299 ((x * (x * x)) + y) * (x * z) = (x + (y * x)) * z.  [para(29(a,1),155(a,1,1)),rewrite([24(4)]),flip(a)].
7543 (x + (x * (y * (y * y)))) * y = 0.  [para(7294(a,1),408(a,1,2)),rewrite([12(3),12(2),144(5),403(1),198(2)]),flip(a)].
7634 (x + (x * (y * (y * y)))) * (y * z) = 0.  [para(7543(a,1),12(a,1,1)),rewrite([193(2)]),flip(a)].
7788 x * (y + (y * (x * (x * x)))) = 0.  [para(7634(a,1),30(a,1,2,2,2,2,2)),rewrite([198(10),198(10),198(6),198(6),198(2)]),flip(a)].
7809 x * ((y + (y * (x * (x * x)))) * z) = 0.  [para(7634(a,1),146(a,1,2,2,2,2,2)),rewrite([198(10),198(10),198(6),198(6),198(2)]),flip(a)].
7963 x * (y + ((y * (x * (x * x))) + z)) = x * z.  [para(7788(a,1),9(a,1,1)),rewrite([5(3),2(6)]),flip(a)].
7968 x * (y * (z + (z * (x * (x * x))))) = 0.  [para(12(a,1),7788(a,1,2,2)),rewrite([9(6)])].
8032 x * (y * (z + (x * (x * (x * z))))) = 0.  [para(154(a,1),7809(a,1,2)),rewrite([12(3),12(2)])].
8122 (x + (x * (y * (y * y)))) * (z * y) = 0.  [para(7809(a,1),7968(a,1,2,2,2)),rewrite([4(6)])].
8399 x * ((y + (z * (z * (z * y)))) * z) = 0.  [para(8122(a,1),449(a,1)),rewrite([12(4),12(3)]),flip(a)].
8445 (x + (y * (y * (y * x)))) * y = 0.  [para(8399(a,1),13(a,1,2,2)),rewrite([198(12),198(7)]),flip(a)].
8493 (x + (y * (y * (y * x)))) * (z * y) = 0.  [para(8399(a,1),8032(a,1,2,2,2,2)),rewrite([198(10),4(6)])].
8495 (x + ((y * (y * (y * x))) + z)) * y = z * y.  [para(8445(a,1),11(a,1,1)),rewrite([5(3),2(6)]),flip(a)].
8498 (x + (y * (y * (y * x)))) * (y * z) = 0.  [para(8445(a,1),12(a,1,1)),rewrite([193(2)]),flip(a)].
8583 (x + (y * (y * (y * x)))) * (z * (u * y)) = 0.  [para(12(a,1),8493(a,1,2))].
9132 (x + (y + (z * (z * (z * (x + y)))))) * (z * u) = 0.  [para(2(a,1),8498(a,1,1))].
9199 (x * (x * (x * (y * z)))) + (y * (x * u)) = x * (x * (x * (y * (z + (x * u))))).  [para(8498(a,1),839(a,1,2)),rewrite([12(6),12(5),12(4),3(8),5(8),12(10),12(9),12(8)]),flip(a)].
9862 x * (y + (y * ((x * (x * x)) + z))) = x * (y * z).  [para(9(a,1),7963(a,1,2,2))].
9875 x * (y * (x * (x * x))) = x * y.  [para(403(a,1),7963(a,1,2,2)),rewrite([4(2)]),flip(a)].
9876 x * (y + (z * (x * (x * x)))) = x * (z + y).  [para(401(a,1),7963(a,1,2,2)),flip(a)].
9877 x * ((y * (x * (x * x))) + z) = x * (y + z).  [para(402(a,1),7963(a,1,2,2)),flip(a)].
9878 x * (y + (z + (u * (x * (x * x))))) = x * (u + (y + z)).  [para(399(a,1),7963(a,1,2,2)),flip(a)].
9946 x * (y * (z + (x * (x * x)))) = x * (y + (y * z)).  [para(564(a,2),7963(a,1,2,2)),rewrite([9878(8),15(4),2(3),402(4)]),flip(a)].
10001 x * (y * (x * (x * (x * z)))) = x * (y * z).  [para(9875(a,1),12(a,1,1)),rewrite([12(2),12(6),12(5),12(4)]),flip(a)].
10003 x * (y * (z * (x * (x * x)))) = x * (y * z).  [para(12(a,1),9875(a,1,2))].
10009 (x + (y * z)) * (y * (y * y)) = (x * (y * (y * y))) + (y * z).  [para(9875(a,1),24(a,1,2)),flip(a)].
10077 x * (y * (x * (y * (x * (y * x))))) = x * (y * (y * y)).  [para(9875(a,1),146(a,1,2,2,2,2,2))].
10274 (x + (y * ((z + (u * u)) * u))) * u = (x * u) + (y * (u + (z * (u * u)))).  [para(201(a,1),199(a,1,2,2)),flip(a)].
10415 (x + (y * (z * u))) * (z * (z * z)) = (x * (z * (z * z))) + (y * (z * u)).  [para(9875(a,1),199(a,1,2,2)),flip(a)].
10416 (x + (y * (z * y))) * (y * y) = (x * (y * y)) + (y * z).  [para(9875(a,1),199(a,1,2)),flip(a)].
10973 (x * (y * (y * y))) + (y * (y * (y * x))) = 0.  [para(8445(a,1),200(a,2)),rewrite([12(6),12(5),12(4),12(3),12(2),9875(4),10009(7)])].
10988 x * (((y * (x * x)) + z) * x) = x * (y + (z * x)).  [para(200(a,1),9875(a,1,2))].
11257 x * (x * (x * (y * x))) = y * x.  [para(403(a,1),8495(a,1,1,2)),rewrite([4(2),12(5),12(4),12(3)]),flip(a)].
11259 ((x * (x * (x * y))) + z) * x = (y + z) * x.  [para(402(a,1),8495(a,1,1,2)),flip(a)].
11383 (x + (((y * (y * y)) + z) * x)) * y = z * (x * y).  [para(155(a,1),8495(a,1,1,2)),rewrite([12(8)])].
11436 x * (y + (x * (x * (z * x)))) = (x * y) + (z * x).  [para(11257(a,1),9(a,1,2)),flip(a)].
11439 x * (x * (x * (y * (x * z)))) = y * (x * z).  [para(11257(a,1),12(a,1,1)),rewrite([12(2),12(6),12(5),12(4)]),flip(a)].
11441 x * (x * (x * (y * (z * x)))) = y * (z * x).  [para(12(a,1),11257(a,1,2,2,2)),rewrite([12(7)])].
11446 (x + (y * z)) * (z * (z * (u * z))) = ((x * (z * z)) + y) * (u * z).  [para(11257(a,1),24(a,1,2,2)),rewrite([155(7)]),flip(a)].
11550 (x + (y * (y * (z * (z * (z * (y * x))))))) * (z * y) = 0.  [para(11257(a,1),8493(a,1,2)),rewrite([12(10),12(9),12(8),12(11),12(10),12(9),11439(8),12(9),12(8),12(7),10001(8)])].
12710 ((x + y) * (z * (x * (x * x)))) + (x * u) = (x * (z + u)) + (y * (z * (x * (x * x)))).  [para(9876(a,1),805(a,2,1))].
12715 (x * (y + z)) + ((u + x) * (y * (x * (x * x)))) = (x * z) + (u * (y * (x * (x * x)))).  [para(9876(a,1),839(a,1,1))].
12726 ((x + y) * (z * (y * (y * y)))) + (y * (z + u)) = (x * (z * (y * (y * y)))) + (y * u).  [para(9876(a,1),997(a,1,2))].
12837 ((x + y) * (z * (x * (x * x)))) + (x * u) = (y * (z * (x * (x * x)))) + (x * (z + u)).  [para(9877(a,1),566(a,2,2))].
12904 x * (y * (z * (x * (x * (x * u))))) = x * (y * (z * u)).  [para(12(a,1),10001(a,1,2)),rewrite([12(8)])].
12906 (x * (y * (z * u))) + (w * (z * (y * (y * (y * u))))) = ((x * y) + w) * (z * (y * (y * (y * u)))).  [para(10001(a,1),23(a,1,1,2))].
12912 (x + y) * (z * ((x + y) * ((x + y) * (x + (y * (x * (x * x))))))) = (x + y) * (z * (x * (x * x))).  [para(27(a,1),10001(a,1,2,2,2,2))].
12923 x * (y * (z + (x * (x * (x * u))))) = x * (y * (z + u)).  [para(144(a,1),10001(a,1,2,2,2,2)),rewrite([10001(6)]),flip(a)].
12934 x * (y * (x * (x * ((x + (x * z)) * u)))) = x * (y * (((x * (x * x)) + z) * u)).  [para(272(a,1),10001(a,1,2,2,2,2))].
12980 x * (y * (x * (x * (z + (x * u))))) = x * (y * ((x * (x * z)) + u)).  [para(602(a,1),10001(a,1,2,2,2))].
12987 x * (y * (x * (y * (x * (y * (x * z)))))) = x * (y * (y * (y * z))).  [para(10001(a,1),146(a,1,2,2,2,2,2))].
13027 x * ((y + (x * (z * (x * (z * (x * (z * y))))))) * z) = 0.  [para(8583(a,1),10001(a,1,2)),rewrite([198(2),12(5),12(6),12(7)]),flip(a)].
13083 x * (y * (z * (u * (x * (x * x))))) = x * (y * (z * u)).  [para(12(a,1),10003(a,1,2,2))].
13089 (x * (y * (z * (z * z)))) + (z * (u * y)) = (x + (z * u)) * (y * (z * (z * z))).  [para(10003(a,1),24(a,1,2))].
13439 x * (y * (y * y)) = y * (y * (y * x)).  [para(10973(a,1),401(a,1,2)),rewrite([3(5),5(5)]),flip(a)].
13460 x * (y * (y * (y * z))) = y * (y * (y * (x * z))).  [para(10973(a,1),66(a,2,2,1)),rewrite([12(5),12(4),12(3),12(9),12(8),12(7),3(10),9199(10),12923(7),401(2),12(8),12(7),12(6),193(10),3(10),5(10)]),flip(a)].
13517 (x * (y * (y * y))) + (y * z) = y * ((y * (y * x)) + z).  [para(13439(a,2),9(a,1,1))].
13548 (x + y) * ((x + y) * (x + (y * (x * (x * x))))) = x * (x * (x * ((x + y) * ((x + y) * (x + y))))).  [para(27(a,1),13439(a,2,2,2)),rewrite([12(8),12(7)]),flip(a)].
13574 (x + (y * (x * x))) * x = x * (x + (x * (x * y))).  [para(268(a,1),13439(a,2,2)),rewrite([216(5)])].
13623 (x + y) * (x * (x * (x * z))) = x * (x * (x * ((y + x) * z))).  [para(13439(a,2),408(a,2,1,2)),rewrite([9(5),9(3),12(4),12(3),422(10)]),flip(a)].
13848 x * (y * (z * (z * (z * (x * (x * x)))))) = x * (z * (z * (z * y))).  [para(13439(a,1),10003(a,2,2)),rewrite([12(5),12(4)])].
13863 (x + (y * z)) * (y * (y * y)) = y * ((y * (y * x)) + z).  [back_rewrite(10009),rewrite([13517(10)])].
13885 (x + y) * (z * (x * (x * x))) = x * (x * (x * ((y + x) * z))).  [back_rewrite(12912),rewrite([13548(9),13848(11),13623(5)]),flip(a)].
14123 (x * (y * (z * (z * z)))) + (z * (y + u)) = z * ((z * (z * ((x + z) * y))) + u).  [back_rewrite(12837),rewrite([13885(5),9(7)]),flip(a)].
14124 (x * (y + z)) + (u * (y * (x * (x * x)))) = x * ((x * (x * ((u + x) * y))) + z).  [back_rewrite(12710),rewrite([13885(5),9(7)]),flip(a)].
14224 (x * (y * (z * (z * z)))) + (z * u) = z * ((z * (z * (x * y))) + u).  [back_rewrite(12726),rewrite([14123(8),3(2),401(2)]),flip(a)].
14226 (x * y) + (z * (u * (x * (x * x)))) = x * ((x * (x * (z * u))) + y).  [back_rewrite(12715),rewrite([14124(8),3(2),401(2)]),flip(a)].
14262 (x + (y * z)) * (u * (y * (y * y))) = y * (((y * (y * x)) + z) * u).  [back_rewrite(13089),rewrite([14224(7),155(5)]),flip(a)].
14429 x * (((x * (x * y)) + z) * x) = (y + (x * z)) * x.  [para(9(a,1),11259(a,1,1)),rewrite([12(5)])].
14684 (x + (y * (x * x))) * (z + (x * (x * u))) = (y + (x * x)) * (x * ((x * z) + u)).  [para(636(a,1),215(a,1,2)),flip(a)].
14786 (x + (y * (x * x))) * (x * z) = x * ((x + (x * (x * y))) * z).  [para(13439(a,2),215(a,1,2)),rewrite([14262(6),3(3)]),flip(a)].
14838 x * (x * ((x + (x * y)) * (x * z))) = (x + (y * x)) * z.  [para(272(a,1),11439(a,1,2,2)),rewrite([7299(11)])].
15052 x * (y * (x * (y * (x * (y * y))))) = x * (x * (x * y)).  [para(13439(a,2),11441(a,1,2,2,2)),rewrite([12(7),10003(7),12(5),12(6)])].
16018 ((x * y) + z) * (u * (y * (y * (y * w)))) = (x + (z * (u * (y * (u * (y * u)))))) * (y * (u * w)).  [para(23(a,1),217(a,1,1)),rewrite([12(7),12(8),12(9),12(10),12987(9),12(11),12(12),12(15)])].
16020 (x + (((y * z) + u) * z)) * (z * (z * w)) = (y + ((x + (u * z)) * z)) * (z * w).  [para(217(a,1),24(a,1,2)),rewrite([23(9),202(5)]),flip(a)].
16999 (x + (((y * z) + u) * z)) * (z * z) = (y + ((x + (u * z)) * z)) * z.  [para(218(a,1),24(a,1,2)),rewrite([23(7),202(5)]),flip(a)].
17991 (x + (y * x)) * (x * x) = x * (x * (x + (x * y))).  [para(7299(a,1),13439(a,1)),rewrite([25(8)])].
20339 x * (y * (z + (z * ((x * (x * x)) + u)))) = x * (y * (z * u)).  [para(12(a,1),9862(a,1,2,2)),rewrite([9(7),12(9)])].
20347 x * (y * ((x * (x * x)) + y)) = (x + (x * y)) * y.  [para(9862(a,1),154(a,2)),rewrite([25(4),402(3),12(5),272(10)])].
20738 x * (y * (y + (x * (x * x)))) = (x + (x * y)) * y.  [para(9946(a,2),154(a,2)),flip(a)].
21673 x * ((y + (((z * x) + u) * x)) * x) = x * (z + ((y + (u * x)) * x)).  [para(159(a,1),10988(a,1,2,1))].
21795 (x + (y + (((z * (z * z)) + u) * (x + y)))) * z = u * ((x + y) * z).  [para(2(a,1),11383(a,1,1))].
22013 (x + (y * x)) * y = (y + (y * (y * y))) * (x * y).  [para(11436(a,1),451(a,2)),rewrite([3(9),24(9)]),flip(a)].
23566 ((x * y) + z) * (u * (y * (y * (y * w)))) = (x + (z * (y * y))) * (y * (u * w)).  [para(13460(a,2),199(a,1,2,2)),rewrite([12906(9)])].
23724 (x + (y * (z * (u * (z * (u * z)))))) * (u * (z * w)) = (x + (y * (u * u))) * (u * (z * w)).  [back_rewrite(16018),rewrite([23566(7)]),flip(a)].
23995 (x * (y * z)) + (z * (z + (z * (z * u)))) = ((x * y) + (z + (u * (z * z)))) * z.  [para(13574(a,1),23(a,1,2))].
24414 x * (((x * (x * y)) + z) * (x * u)) = (y + (x * z)) * (x * u).  [para(14429(a,1),12(a,1,1)),rewrite([12(4),12(9)]),flip(a)].
24599 (x + (y * y)) * (y * (y + (y * y))) = y + ((y + (x * (y + (y * y)))) * y).  [para(13574(a,1),416(a,1,2,2)),rewrite([12(5),12(4),13(3),23995(7),15(5),9(4),3(12),14684(13),3(10)]),flip(a)].
24923 x * (y * (((x * (x * x)) + y) * z)) = (x + (x * y)) * (y * z).  [para(20347(a,1),12(a,1,1)),rewrite([12(4),12(9)]),flip(a)].
25111 (x + (x * y)) * (y + (x * (x * x))) = x + (x * (y * y)).  [para(20738(a,1),412(a,1,2,2)),rewrite([11(5),402(3),12(2),3(5)]),flip(a)].
25390 (x + (x * x)) * (y * x) = y * (x * (x + (x * x))).  [para(22013(a,2),13439(a,2,2,2)),rewrite([14684(11),3(8),24599(10),940(9),402(9),2110(8),17991(5),405(5),26(5),12(4),2110(14),14786(13),2110(12),933(10),408(10)]),flip(a)].
25416 (x + (x * (x * x))) * (y + (y * (x * x))) = (y + (x * y)) * x.  [para(22013(a,2),9862(a,2)),rewrite([14684(13),3(10),24599(12),940(11),402(11),2110(10),17991(7),405(7),26(7),3(6),402(6)])].
25444 (x + (x * x)) * (y * x) = y * ((x + (x * x)) * x).  [para(22013(a,2),13460(a,2,2,2)),rewrite([13574(10),26(10),1256(9),414(7),25416(7),2110(14),14786(13),2110(12),933(10),408(10)]),flip(a)].
26061 (x + (x * y)) * (y * y) = y * ((x + (y * x)) * y).  [para(9875(a,1),25390(a,1,2)),rewrite([12(10),12(9),12(8),9875(7),9(8),9(6),9(4),12(7),12(6),12(5),14838(6),12(17),12(16),12(15),9875(14),9(15),9(13),9(11),12(13),12(12),12(11),12980(10),20347(9),12934(11),24923(10)]),flip(a)].
26098 x * ((x + (x * x)) * ((x + (x * (x * x))) * y)) = y * (x + (x * x)).  [para(25390(a,2),13439(a,1,2,2)),rewrite([12(9),414(9),25111(9),12(7),25111(6),26(4),12(13),12(14),933(14),2110(13),933(11),12(11)]),flip(a)].
26176 (x + (x * x)) * (y + (y * (x * x))) = y * (x * (x + (x * x))).  [para(25390(a,1),9862(a,2)),rewrite([1876(9),13574(8),26(8),1876(7),13574(6),26(6),3(5),402(5)])].
26449 (x + (x * x)) * (y * (x + (x * x))) = y * (x + (x * x)).  [para(25444(a,2),13439(a,1,2,2)),rewrite([12(9),26061(9),414(9),26176(9),405(7),12(7),26(6),1876(5),13574(4),26(4),12(13),12(14),933(13),12(14),26098(13)]),flip(a)].
26578 (x + (x * x)) * y = y * (x + (x * x)).  [para(25444(a,2),20347(a,2)),rewrite([12(10),931(9),20339(10),27(5),12(4),13(3),10274(11),9(11),402(9),14262(9),3(6),408(8)]),flip(a)].
26672 (x * y) + (y * (z + (z * z))) = (x + (z + (z * z))) * y.  [para(26578(a,1),11(a,1,2))].
26673 x * (y + (y * y)) = y * (x + (y * x)).  [para(26578(a,1),11(a,2)),rewrite([12(3),9(4)]),flip(a)].
26725 (x + (x * x)) * (y + (z * (x + (x * x)))) = (x + (x * x)) * (y + z).  [para(26578(a,1),144(a,1,2,2,2,2)),rewrite([26449(10),26449(8)])].
26859 (x + (x * x)) * (y + ((x + (x * x)) * z)) = (x + (x * x)) * (y + z).  [para(26578(a,1),602(a,2,2,2)),rewrite([602(13),26725(14)])].
27111 (x + (x * y)) * y = y * (x + (y * x)).  [para(26578(a,2),9862(a,1)),rewrite([2(11),21795(12),7294(4),272(8)]),flip(a)].
27820 (x * (y + (x * y))) + (z * x) = (y + ((y * x) + z)) * x.  [para(27111(a,1),11(a,1,1)),rewrite([2(8)])].
27822 (x + (x * y)) * (y * z) = y * ((x + (y * x)) * z).  [para(27111(a,1),12(a,1,1)),rewrite([12(4)]),flip(a)].
28041 (x + (y * (x + (y * x)))) * (y + (y * y)) = 0.  [para(26673(a,1),27111(a,1,1,2)),rewrite([26859(14),403(10),198(11)])].
28298 (x + (x * x)) * (y + (x * (y + (x * y)))) = 0.  [para(28041(a,1),26578(a,2))].
28363 (x + (y * (x + (y * x)))) * ((y + (y * y)) * z) = 0.  [para(28298(a,1),9132(a,1,1,2,2,2,2)),rewrite([198(9),198(7),3(5),5(5)])].
31439 (x + (y * (x + (y * x)))) * (y + (y * (y * y))) = 0.  [para(158(a,1),28363(a,1,2)),rewrite([12(3),12(5),636(5),3(2),12(7),13(7)])].
37695 x * (y + (((y * x) + (x * y)) * x)) = y * x.  [para(31439(a,1),998(a,2,2)),rewrite([12(4),13863(11),15(9),3(8),9(8),9(10),15(8),3(7),27820(7),15(4),402(5),3(9),5(9)])].
37721 x * (y + ((y + (x * (y * x))) * x)) = y * (x * x).  [para(11(a,1),37695(a,1,2)),rewrite([12(2),156(5),21673(7),12(2),12(8)])].
37722 x * ((y + (((y * x) + (x * y)) * x)) * z) = y * (x * z).  [para(37695(a,1),12(a,1,1)),rewrite([12(2)]),flip(a)].
37942 x * ((y + ((y + (x * (y * x))) * x)) * z) = y * (x * (x * z)).  [para(37721(a,1),12(a,1,1)),rewrite([12(3),12(2)]),flip(a)].
43797 (x + ((y + (z * (u * z))) * z)) * z = ((x + (y * z)) * z) + (z * u).  [para(10416(a,1),24(a,1,2)),rewrite([116(6)]),flip(a)].
43804 (x + ((x + (y * z)) * y)) * (y * y) = y * (((x + (y * x)) * y) + z).  [para(27822(a,1),10416(a,2,1)),rewrite([2(5),24(4),9(12)])].
44721 ((x * x) + (y * (x * (y * (x * y))))) * (y * x) = 0.  [para(10077(a,1),11550(a,1,1,2,2,2,2,2)),rewrite([13083(10),14226(9),12(10),24414(10)])].
44779 x * (((x * x) + (y * (x * (y * (x * y))))) * y) = 0.  [para(10077(a,1),44721(a,1,2)),rewrite([12(11),12(10),12(9),12(8),12(7),10077(6),9875(4),12(16),12(15),12(14),12(13),12(12),15052(16),12(15),12(14),12(13),12(12),12(11),12904(11),9875(9),23724(15),3(8),14262(12),14224(9),12(9),14429(9)])].
46495 x * (y * ((x * x) + (y * (x * (y * (x * y)))))) = 0.  [para(44779(a,1),13027(a,1,2,1,2,2,2,2,2)),rewrite([198(14),198(8),198(8),198(2),4(2)])].
46810 x * ((y * y) + (x * (y * (x * (y * x))))) = 0.  [para(46495(a,1),13439(a,2,2,2)),rewrite([12(10),10415(9),12(4),13(3),198(9),198(9)])].
46856 x * ((x * (x * (y * y))) + (y * (x * (y * x)))) = 0.  [para(46810(a,1),13439(a,2,2,2)),rewrite([13863(9),198(10),198(10)])].
47125 (x * (x * (y * y))) + (y * (x * (y * x))) = 0.  [para(46856(a,1),13439(a,2,2,2)),rewrite([10415(10),12(6),12(5),12(4),10003(5),198(9),198(9)])].
47157 x * (y * (x * y)) = y * (y * (x * x)).  [para(47125(a,1),401(a,1,2)),rewrite([3(5),5(5)])].
47247 x * (x * (y * (x * (y * x)))) = x * (y * y).  [para(47157(a,2),29(a,1,2,2))].
47365 x * (x * (y * (y * (x * x)))) = y * (x * y).  [para(47157(a,1),13439(a,2,2,2)),rewrite([12(5),12(4),9875(4)]),flip(a)].
47370 x * (x * (y * (x * (x * (y * x))))) = x * (y * (x * y)).  [para(47157(a,2),11439(a,1,2)),rewrite([12(3),12(5),12(9)])].
47501 (x + ((x + (y * (x * y))) * y)) * (y * x) = x * (y * (x * y)).  [para(37695(a,1),47157(a,1,2,2)),rewrite([37722(8),16999(15),12(10),43797(14),27111(11),3(13),9(13),402(11),16020(11),12(5)]),flip(a)].
47504 (x + (((x * y) + (y * x)) * y)) * (x * y) = x * (y * (y * (x * (y * y)))).  [para(37721(a,1),47157(a,1,2,2)),rewrite([37942(9),43804(17),3(15),11(15),402(13),12(12),11446(14),15(11),156(10)]),flip(a)].
47604 x * (x * (y * (x * (y * (x * z))))) = x * (y * (y * z)).  [para(47247(a,1),12(a,1,1)),rewrite([12(3),12(2),12(8),12(7),12(6),12(5)]),flip(a)].
47676 x * (x * (y * (y * (x * (x * z))))) = y * (x * (y * z)).  [para(47365(a,1),12(a,1,1)),rewrite([12(3),12(2),12(8),12(7),12(6),12(5)]),flip(a)].
47700 x * (y * (x * (x * (y * x)))) = y * (x * y).  [para(47365(a,1),11441(a,1,2,2,2)),rewrite([12(12),12(11),12(10),12(13),12(12),12(11),47676(11),47370(9),12(8),12(7),12(6),47676(8),47365(10)])].
47751 x * (y * (y * (x * (y * y)))) = y * (x * x).  [para(37695(a,1),47365(a,2,2)),rewrite([16999(12),12(7),43797(11),27111(8),3(10),9(10),402(8),16020(8),12(2),47501(7),47247(5),47504(9)]),flip(a)].
47784 x * (y * (x * (y * (x * (x * (y * y)))))) = x * (x * (y * (x * x))).  [para(47247(a,1),47365(a,2,2)),rewrite([12(10),12(9),12(8),12(7),9875(8),12(8),12(7),12(6),12(5),47604(9),47247(5),12(11),12(10),12(9),12(8)]),flip(a)].
47804 x * (y * (x * (x * (y * (x * z))))) = y * (x * (y * z)).  [para(47700(a,1),12(a,1,1)),rewrite([12(3),12(2),12(8),12(7),12(6),12(5)]),flip(a)].
47868 x * (y * y) = y * (y * x).  [para(47700(a,1),37695(a,1,2,2,1,2)),rewrite([12(9),12(8),12(7),12(6),47751(9),156(9),12(9),155(10),15(6),3(5),9(5),26672(5),402(3),12(2),12(4),12(3),11441(5),12(7),12(6),12(5),12(4),47751(7)]),flip(a)].
47889 x * (y * (x * (y * (x * x)))) = y * (x * y).  [para(47700(a,1),47157(a,1,2,2)),rewrite([12(7),12(6),12(5),12(4),47604(6),9875(4),47868(12),47700(11),12(10),12(9),12(8),12(7),47804(8)]),flip(a)].
47894 x * (x * (y * (x * x))) = y * x.  [para(47247(a,1),47700(a,2,2)),rewrite([12(9),12(8),12(7),12(6),47889(9),12(9),12(8),12(7),12(6),11439(5),47700(5),11257(4),12(8),12(7),12(6),12(5),47784(8)]),flip(a)].
47896 x * y = y * x.  [para(47700(a,1),47700(a,2,2)),rewrite([12(9),12(8),12(7),12(6),47894(8),12(9),12(8),12(7),12(6),11441(5),12904(6),9875(4),12(8),12(7),12(6),12(5),47604(7),9875(5)])].
47897 $F.  [resolve(47896,a,14,a)].

============================== end of proof ==========================