[Termtools] strange proof

[Zantema, H.]

> Jörg Endrullis notes that this proof is at least incomplete:
http://www.lri.fr/~marche/termination-competition/2007/webform.cgi?command=viewres&file=srs-standard.db&tool=torpa&prob=SRS.Gebhardt.02.srs


This is strange, on my computer the output is correct, see below. It is always found in at most 20 seconds, and sometimes an alternative proof is found using nested labelling. This latter proof is found in a fraction of a second.

            Best regards, Hans Zantema.

_________________________________________________________
Dr Hans Zantema            
Technische Universiteit Eindhoven, Department of Computer Science 
P.O. Box 513, 5600 MB Eindhoven, The Netherlands 
e-mail: H.Zantema at tue.nl, homepage: www.win.tue.nl/~hzantema
office: Hoofdgebouw room 6.73, tel: (040)2472749




YES
TORPA version 1.7 is applied to
0 0 0 0  -> 0 0 0 1 ,
1 0 0 1  -> 0 1 0 0 ,
[CG] Reversed dependency pair transformation:
  0 0 0 0  ->= 1 0 0 0 
  1 0 0 1  ->= 0 0 1 0 
  #0 0 0 0  -> #1 0 0 0 
  #0 0 0 0  -> #0 0 0 
  #0 0 0 0  -> #0 0 
  #0 0 0 0  -> #0 
  #1 0 0 1  -> #0 0 1 0 
  #1 0 0 1  -> #0 1 0 
  #1 0 0 1  -> #1 0 
  #1 0 0 1  -> #0 
[A] Choose polynomial interpretation   0 1 #0 #1: lambda x.x+1
remove: #0 0 0 0  -> #0 0 0 
remove: #0 0 0 0  -> #0 0 
remove: #0 0 0 0  -> #0 
remove: #1 0 0 1  -> #0 1 0 
remove: #1 0 0 1  -> #1 0 
remove: #1 0 0 1  -> #0 
Remaining rules:
    0 0 0 0  ->= 1 0 0 0 
    1 0 0 1  ->= 0 0 1 0 
    #0 0 0 0  -> #1 0 0 0 
    #1 0 0 1  -> #0 0 1 0 
[A] Choose quasi-periodic interpretation:
[0](0) = 4
[0](1) = 5
[0](2) = 8
[0](3) = 8
[0](4) = 8
[0](x+5) = [0](x)+5
[1](0) = 6
[1](1) = 6
[1](2) = 6
[1](3) = 6
[1](4) = 9
[1](x+5) = [1](x)+5
[#0](0) = 0
[#0](1) = 1
[#0](2) = 1
[#0](3) = 1
[#0](4) = 1
[#0](x+5) = [#0](x)+5
[#1](0) = 1
[#1](1) = 1
[#1](2) = 1
[#1](3) = 1
[#1](4) = 6
[#1](x+5) = [#1](x)+5
remove: #1 0 0 1  -> #0 0 1 0 
remaining rules:
0 0 0 0  ->= 1 0 0 0 
1 0 0 1  ->= 0 0 1 0 
#0 0 0 0  -> #1 0 0 0 
[A] Choose polynomial interpretation   #0: lambda x.x+1,  rest identity
remove: #0 0 0 0  -> #1 0 0 0 
Relatively terminating since no strict rules remain.