Sharing of introduced variables

[Stef De Pooter]

When unnesting terms we want to be able to introduce only one variable for a term reoccurring several times in the same formula (or rule). Currently, for every occurrence a new variable is introduced.

When unnesting term //Color(t,x)// in the following theory, two different variables are introduced. {{{ theory T1 : V { { Edges(Color(t,x),Color(t,y)) <- Edge(t,x,y) & Color(t,x) < Color(t,y). Edges(Color(t,y),Color(t,x)) <- Edge(t,x,y) & Color(t,y) < Color(t,x). } ! t c : ?1 n : Color(t,n) = c. } }}}

While we would like to end up with a theory that looks more like this: {{{ theory T2 : V { { Edges(ctx,cty) <- ctx = Color(t,x) & cty = Color(t,y) & Edge(t,x,y) & ctx < cty. Edges(cty,ctx) <- ctx = Color(t,x) & cty = Color(t,y) & Edge(t,x,y) & cty < ctx. } ! t c : ?1 n : Color(t,n) = c. } }}}