Certification Problem

Input (TPDB TRS_Standard/Various_04/10)

The rewrite relation of the following TRS is considered.

+(0,y) y (1)
+(s(x),y) s(+(x,y)) (2)
++(nil,ys) ys (3)
++(:(x,xs),ys) :(x,++(xs,ys)) (4)
sum(:(x,nil)) :(x,nil) (5)
sum(:(x,:(y,xs))) sum(:(+(x,y),xs)) (6)
sum(++(xs,:(x,:(y,ys)))) sum(++(xs,sum(:(x,:(y,ys))))) (7)
-(x,0) x (8)
-(0,s(y)) 0 (9)
-(s(x),s(y)) -(x,y) (10)
quot(0,s(y)) 0 (11)
quot(s(x),s(y)) s(quot(-(x,y),s(y))) (12)
length(nil) 0 (13)
length(:(x,xs)) s(length(xs)) (14)
hd(:(x,xs)) x (15)
avg(xs) quot(hd(sum(xs)),length(xs)) (16)

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.
sum#(:(x,:(y,xs))) sum#(:(+(x,y),xs)) (17)
length#(:(x,xs)) length#(xs) (18)
avg#(xs) sum#(xs) (19)
sum#(++(xs,:(x,:(y,ys)))) sum#(:(x,:(y,ys))) (20)
avg#(xs) quot#(hd(sum(xs)),length(xs)) (21)
avg#(xs) hd#(sum(xs)) (22)
avg#(xs) length#(xs) (23)
sum#(++(xs,:(x,:(y,ys)))) sum#(++(xs,sum(:(x,:(y,ys))))) (24)
-#(s(x),s(y)) -#(x,y) (25)
quot#(s(x),s(y)) -#(x,y) (26)
sum#(:(x,:(y,xs))) +#(x,y) (27)
+#(s(x),y) +#(x,y) (28)
sum#(++(xs,:(x,:(y,ys)))) ++#(xs,sum(:(x,:(y,ys)))) (29)
++#(:(x,xs),ys) ++#(xs,ys) (30)
quot#(s(x),s(y)) quot#(-(x,y),s(y)) (31)

1.1 Dependency Graph Processor

The dependency pairs are split into 7 components.