Here is a question that Stephen Bloom asked
me to place on this list. You may reply to
him at bloom@....

Are there charaterization theorems for models
of balanced, regular equations? (Sometimes
these are called super regular equations.)

An equation s=t is balanced, and regular if
var(s)=var(t) and no variable
appears more than once in each list, where

v(s)=s, if s is a variable and

v( f(t1,...tk) ) is the concatenation
v(t1) v(t2) ... v(tk), where f is a function symbol of rank k.

So, for example,
x.(y.z) = (x.y).z
is regular and balanced, but
x.y = y.x
is not. The ordering of the variables counts.