Let $R$ be a ring such that $x^4=x$ for every $x\in R$. Is this ring commutative?
Ring such that $x^4=x$ for all $x$ is commutative
-
0The$n=4$case appears in Herstein as well, actually; IIRC, it appears earlier. From what I recall of the solution, it's slightly easier than the$n=3$case. – 2011-10-29
3 Answers
Here's an old post of mine from Yahoo! Answers:
First, note $-x = (-x)^4 = x^4 = x$, so $x+x = 0$ for any $x$ in $R$. Then $(x^2+x)^2 = x^2 + x + x^3 + x^3 = x^2+x$. Thus $x^2+x$ is idempotent, and it is easy to see idempotent elements are central in this ring. [I give a proof of this at the end.]
Now let $x=a+b$, where $a$ and $b$ are arbitrary. From above, for any $c$ in $R$, $c(x^2 + x) = (x^2 + x)c$, and expanding this out and cancelling terms we get $c(ab + ba) = (ab + ba)c$. Setting $c=a$, we get, after cancelling again, $a^2b = ba^2$. Thus, for any $x$ in $R$, $x^2$ is central. Then of course $x = (x^2+x)-x^2$ is central.
To prove that idempotents are central, first note that if $xy=0$, then $yx = (yx)^4 = y (xy)(xy)(xy)x = 0$. So now if $z^2 = z$, then $z(y - zy) = 0$, so $(y-zy)z = 0$, or $yz = zyz$. Similarly, $(yz - y)z = 0$, so $z(yz-y) = 0$, or $zy = zyz$. Thus $yz = zy$.
-
0@Jonathan: While I agree this seems somewhat opaque, this is a natural way of beginning to prove the much stronger version of this theorem (Jacobson's theorem): look at idempotents, and the differences between them. – 2013-05-14
Here is an interesting observation:
$2x=(x+x)=(x+x)^4=16x^4=16x$. Thus $14x=0$.
Also $3x=(3x)^4=81x^4=81x$. Thus $78x=0$. Since gcd $(78,14) =2$ we get $2x=0$ for all $x \in R$.
Now one probably needs to look at $x+y=(x+y)^4$ and probably $(x+y+z)=(x+y+z)^4$ or $(x+y+1)=(x+y+1)^4$.
P.S. Actually characteristic 2 is also obtained the following way: $x=x^4=(-x)^4=-x$.
-
4What proved this answer to get eight upvotes? (Well, nine minus one from me.) That $2=0$ in $R$ is almost trivial, but from here to a full proof is a long, long way. – 2013-07-28
In my previous version of this answer, I gave an automated Prover9 proof of this result using a step-by-step approach. It turns out that this is unnecessary. Previously, I used the default Lexicographic Path Ordering, whereas the Knuth-Bendix Ordering (assign(order, kbo).
)is much faster for this problem (ref.), and we can obtain a proof:
============================== 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 ==========================
-
1What are you trying to say with this? Are you proving the result by using a computer program? – 2013-07-28