Yes. I first tried things like this, too. I also tried term rewrite rules, and some of these were quite close. For example, AB → A*(B+1) or AB → A*(B+A) or AB → A*(B+index) led to some close misses (the question was which to expand first, so which associativity, I also considered expanding smaller first) but failed with later expansions. Took me half an hour to figure out that the index was not additive or multiplicative but the exponent base.
Yes. I first tried things like this, too. I also tried term rewrite rules, and some of these were quite close. For example, AB → A*(B+1) or AB → A*(B+A) or AB → A*(B+index) led to some close misses (the question was which to expand first, so which associativity, I also considered expanding smaller first) but failed with later expansions. Took me half an hour to figure out that the index was not additive or multiplicative but the exponent base.