Certification Problem

Input (TPDB TRS_Standard/AProVE_07/kabasci05)

The rewrite relation of the following TRS is considered.

min(x,0) 0 (1)
min(0,y) 0 (2)
min(s(x),s(y)) s(min(x,y)) (3)
max(x,0) x (4)
max(0,y) y (5)
max(s(x),s(y)) s(max(x,y)) (6)
minus(x,0) x (7)
minus(s(x),s(y)) s(minus(x,y)) (8)
gcd(s(x),s(y)) gcd(minus(max(x,y),min(x,transform(y))),s(min(x,y))) (9)
transform(x) s(s(x)) (10)
transform(cons(x,y)) cons(cons(x,x),x) (11)
transform(cons(x,y)) y (12)
transform(s(x)) s(s(transform(x))) (13)
cons(x,y) y (14)
cons(x,cons(y,s(z))) cons(y,x) (15)
cons(cons(x,z),s(y)) transform(x) (16)

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.
min#(s(x),s(y)) min#(x,y) (17)
max#(s(x),s(y)) max#(x,y) (18)
minus#(s(x),s(y)) minus#(x,y) (19)
gcd#(s(x),s(y)) gcd#(minus(max(x,y),min(x,transform(y))),s(min(x,y))) (20)
gcd#(s(x),s(y)) minus#(max(x,y),min(x,transform(y))) (21)
gcd#(s(x),s(y)) max#(x,y) (22)
gcd#(s(x),s(y)) min#(x,transform(y)) (23)
gcd#(s(x),s(y)) transform#(y) (24)
gcd#(s(x),s(y)) min#(x,y) (25)
transform#(cons(x,y)) cons#(cons(x,x),x) (26)
transform#(cons(x,y)) cons#(x,x) (27)
transform#(s(x)) transform#(x) (28)
cons#(x,cons(y,s(z))) cons#(y,x) (29)
cons#(cons(x,z),s(y)) transform#(x) (30)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.