[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: RELITERS


Piotr Rudnicki wrote:

> ...
> It only indicates that a utility which actually removes superflous
> steps in iterative equalities is needed.
>

What strategy do you propose?

Let us look to an example (I have substitued  *  for d249):

Lm10:
 2 to_power 4 = 16
proof
 thus 2 to_power 4 = 2 to_power (2+2)
                  .= (2 to_power 2)*(2 to_power 2) by POWER:32
::>                                                 *746
                  .= 4*4 by Lm8
::>                       *746
                  .= 16;
 thus thesis;
end;

One may remove the second step or the third one, but not both. In general if we
got consecutive errors we
may remove odd steps or even steps, but maybe something a bit smarter may be
used (removing steps wiht biggest terms?).

On the other hand the lemma should be written as:

Lm10:
 2 to_power (2+2) = 4*4 by Lm8,POWER:32;

So it is btter to correct the text by hand.

Regards,
Andrzej Trybulec