Word destructors

[ReedOei]

With this feature, squares could be defined by:

T[i..j] = a^b & a = b 

which would expand into:

exists k1. i <= k1 & k1 < j & T[i..k1] = T[k1..j]

basically, we pick n - 1 (where n is the number of variables) indices in the range i..j.
Then we assign each word variable (e.g., a and b) to the corresponding index range.
Then whenever we refer to those variables again, we substitute in the corresponding index range

or:

Bordered factors:
T[i..j] = a^b^c & a = c