Write the rewriting background + confluence bits

[codyroux]

WIP for some of the rewriting bits. Needs feedback and polish.

[teorth]

Thanks for writing this. I was wondering if one could supply a simple example of a rewriting system to illustrate the concepts. Not every concept needs an example (we can defer to the cited references and/or the blueprint for an in depth discussion), but perhaps one or two examples, preferably related to an equational law, would be helpful.

[codyroux]

Sure! I can do the KB completion for the theory of groups. That's usually a crowd pleaser.

Not sure I know how to do the 1 equation version though.

[teorth]

That's probably good enough. Even just a single example can help correct any misconceptions that a reader may have if they misread the definition somehow.

[codyroux]

Wait no I have a better example 😄 : The equation x * (y * x) = y (equation 14), the completion of this as a rewrite rule solves the Putnam problem I now see is associated to it. That's kind of cute!

[teorth]

Looks good to merge now!