todo
Working (I think) normal Knuth-Bendix completion