On Dec 17, 2022, at 10:17 AM, Benjamin Redelings <benjamin.redelings@gmail.com> wrote:

But supposing I do get there, I'm curious if there are some papers on term-rewriting that would be helpful to set the context? The OutsideIn paper mentions Kapur (1997) "Shostak's congruence closure as completion" in support of the flattening idea.

I'm not aware of any, but I think looking for some is a good idea. For better or worse, the current approach was freshly invented; looking for prior art might have yielded something better.