[Termination tools] small hard string termination problem

[Juergen Giesl]

Dear all,

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:

If one enters the example in the format

  [X]
  1(0(1(X))) -> 0(0(0(X)))
  0(0(0(X))) -> 1(1(1(X))

the web interface only tries the innermost instead of the full termination proof.
This is different if one uses the WST-format:

(VAR X)
(RULES
1(0(1(X))) -> 0(0(0(X)))
0(0(0(X))) -> 1(1(1(X)))
)

Here, the web interface times out after 1 minute.)


Best Regards
Juergen