Certification Problem

Input (TPDB TRS_Standard/HirokawaMiddeldorp_04/t001)

The rewrite relation of the following TRS is considered.

-(x,0) x (1)
-(s(x),s(y)) -(x,y) (2)
*(x,0) 0 (3)
*(x,s(y)) +(*(x,y),x) (4)
if(true,x,y) x (5)
if(false,x,y) y (6)
odd(0) false (7)
odd(s(0)) true (8)
odd(s(s(x))) odd(x) (9)
half(0) 0 (10)
half(s(0)) 0 (11)
half(s(s(x))) s(half(x)) (12)
if(true,x,y) true (13)
if(false,x,y) false (14)
pow(x,y) f(x,y,s(0)) (15)
f(x,0,z) z (16)
f(x,s(y),z) if(odd(s(y)),f(x,y,*(x,z)),f(*(x,x),half(s(y)),z)) (17)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
-#(s(x),s(y)) -#(x,y) (18)
*#(x,s(y)) *#(x,y) (19)
odd#(s(s(x))) odd#(x) (20)
half#(s(s(x))) half#(x) (21)
pow#(x,y) f#(x,y,s(0)) (22)
f#(x,s(y),z) if#(odd(s(y)),f(x,y,*(x,z)),f(*(x,x),half(s(y)),z)) (23)
f#(x,s(y),z) odd#(s(y)) (24)
f#(x,s(y),z) f#(x,y,*(x,z)) (25)
f#(x,s(y),z) *#(x,z) (26)
f#(x,s(y),z) f#(*(x,x),half(s(y)),z) (27)
f#(x,s(y),z) *#(x,x) (28)
f#(x,s(y),z) half#(s(y)) (29)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.