[Termination tools] small hard string termination problem

[Salvador Lucas]

Hi,

Juergen Giesl wrote:

> thanks for Johannes for the nice example and for Salvador
> for the nice solution with AProVE.
>
> However, note that AProVE only proved INNERMOST termination
> of this example. This can indeed easily be verified by AProVE.
> But whether the TRS is terminating remains unclear.
>
> (This indicates a small strange behavior of AProVE's web interface
> which has to be fixed. This strange behavior
> doesn't happen in the downloadable version of AProVE: 

Yes, I already noticed that the downloadable version of AProVE does
not prove the termination of the example, but I thought that the Web
vesion was implementing something which is not implemented in the
other one (in particular, I was using version 1.0h which is not the
most recent one).

Best,

Salvador.

>