I made some progress with the noncommutative version. Basically, instead
of using let rules for *, as in the commutative case, I use let rules
for . which is inherently noncommutative. The session below (I deleted
some erroneous lines, and also edited the answer using spaces instead of
tabs to place the exponents) shows some satisfactory results, but D13 shows
that it can't simplify y0.(x1^3*y1) even if it knows y0.(x1*y1)=(x1*y0).y1.
(C1) let([y1.y1,2*y0],gleep);
<2>
(D1) Y1 --> 2 y0
(C2) let([y0.y1,y1],gleep);
(D2) y0 . Y1 --> Y1
(C3) let([y1.y0,y0],gleep);
(D3) Y1 . y0 --> y0
(C4) let([y0.y0,y0],gleep);
<2>
(D4) y0 --> y0
(C5) letsimp((y0+y1)^^2,gleep);
<2>
(D5) (Y1 + y0)
(C6) letsimp((y0+y1).(y0+y1),gleep);
<2>
(D6) (Y1 + y0)
(C7) expand(%);
<2> <2>
(D7) Y1 . y0 + Y1 + y0 . Y1 + y0
(C8) letsimp(%,gleep);
(D8) Y1 + 4 y0
(C9) letsimp(expand((y0+y1)^^2),gleep);
(D9) Y1 + 4 y0
(C11) letsimp(expand((x1*y1).(x3*y0)),gleep);
(D11) x1 Y1 . x3 y0
(C12) let([y0.(x1*y1),x1*y0.y1],gleep);
(D12) y0 . x1 Y1 --> x1 (y0 . Y1)
(C13) letsimp(y0.(x1^3*y1),gleep);
3
(D13) y0 . x1 Y1
--
Ignorantly,
Allan Adler
* Disclaimer: I am a guest and *not* a member of the MIT CSAIL. My actions and
* comments do not reflect in any way on MIT. Also, I am nowhere near Boston.