On 2016-01-28 17:42, Sergei Meshveliani wrote: > Probably, the term b + b is normalized here according to the > equations of the domain (universal algebra ?) of XorRingSolver. > And it is normalized to `false', and this makes it a proof. > Right? There is a discussion in the paper that I referenced (Section 4). -- /NAD