Certification Problem

Input (TPDB TRS_Standard/Strategy_removed_AG01/#4.29)

The rewrite relation of the following TRS is considered.

even(0) true (1)
even(s(0)) false (2)
even(s(s(x))) even(x) (3)
half(0) 0 (4)
half(s(s(x))) s(half(x)) (5)
plus(0,y) y (6)
plus(s(x),y) s(plus(x,y)) (7)
times(0,y) 0 (8)
times(s(x),y) if_times(even(s(x)),s(x),y) (9)
if_times(true,s(x),y) plus(times(half(s(x)),y),times(half(s(x)),y)) (10)
if_times(false,s(x),y) plus(y,times(x,y)) (11)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
times#(s(x),y) even#(s(x)) (12)
if_times#(true,s(x),y) plus#(times(half(s(x)),y),times(half(s(x)),y)) (13)
if_times#(true,s(x),y) times#(half(s(x)),y) (14)
half#(s(s(x))) half#(x) (15)
even#(s(s(x))) even#(x) (16)
if_times#(true,s(x),y) times#(half(s(x)),y) (14)
if_times#(true,s(x),y) half#(s(x)) (17)
plus#(s(x),y) plus#(x,y) (18)
if_times#(false,s(x),y) plus#(y,times(x,y)) (19)
times#(s(x),y) if_times#(even(s(x)),s(x),y) (20)
if_times#(true,s(x),y) half#(s(x)) (17)
if_times#(false,s(x),y) times#(x,y) (21)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.