April 2007 (under construction)
% loop axioms 1 * x = x. x * 1 = x. x * (x \ y) = y. x \ (x * y) = y. (x * y) / y = x. (x / y) * y = x. % axioms for a conjugacy closed loop ((x * y) / x) * (x * z) = x * (y * z) # label(LCC). (z * x) * (x \ (y * x)) = (z * y) * x # label(RCC). % theorem to prove x * (y * ((u * z) \ (z * u))) = (x * y) * ((u * z) \ (z * u)).(... include some comments about the problem ...)
basarab.pf(... include some comments about the use of proof sketches for this problem ...)
Here is another proof, derived from the preceding one, in which all demodulation (rewriting) steps are explicit, and the goal is derived directly. We call this a strictly-forward, demodulation-free (sfdf) proof.
basarab_sfdf.pfThe sfdf version of the proof was found using Otter.
newauto -f basarab_auto.in > basarab_auto.out