Piotr Rudnicki wrote:
>
> I do not know about biggest terms but if we remove every second step and
> then recursively run RELITER we may save even more.
You might be right. But look to an example (ASYMPT_1, line 807): To prove (^2
substituted for d253, and * for d249)
A5: ((k+1)+1)^2 = (k+1)^2 + 2*(k+1)*1 + 1 by SQUARE_1:59,63
.= (k+1)^2 + (2*(k+1) + 1) by AXIOMS:13
.= (k+1)^2 + (2*k+2*1 + 1) by AXIOMS:18
.= (k+1)^2 + (2*k+(2 + 1)) by AXIOMS:13;
you use 18 steps (instead of 4). RELITERS reports 11 errors (first attach.) and
routine enhancement with RELITERS shorten the Iterative Equality to 10, (second
attach.). So I would like to have something more efficient.
The problem is with the first step, of course. Why
A5: ((k+1)+1)^2 = (k+(1+1))^2 by AXIOMS:13
.= (k+2)^2
....
if you need (k+1)^2 anyway. So if the proof (or rather the author) goes astray, a
simplistic approach with RELITERS is not enough.
> Sure - but where to find the hand: do not count on mine.
I do not intend.
> The problem is interesting as it involves only equality of terms and
> I am sure that in the rewriting literature there will be plenty to
> learn from.
Do it.
Andrzej
Attachment:
It.1
Description: application/unknown-content-type-1_auto_file
Attachment:
It.2
Description: application/unknown-content-type-2_auto_file