Hello all,
Does anyone have an example of modelling a term rewriting system,
where you also prove properties like confluence (using critical pairs)?
I am about to do this, and I would much rather use "best practices"
rather than muddle my way through via re-inventing squarish wheels.
Jacques