Certification Problem

Input (TPDB TRS_Standard/AProVE_07/kabasci04)

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,any(y))) (8)
gcd(s(x),s(y)) gcd(minus(max(x,y),min(x,y)),s(min(x,y))) (9)
any(s(x)) s(s(any(x))) (10)
any(x) x (11)

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) (12)
max#(s(x),s(y)) max#(x,y) (13)
minus#(s(x),s(y)) minus#(x,any(y)) (14)
minus#(s(x),s(y)) any#(y) (15)
gcd#(s(x),s(y)) gcd#(minus(max(x,y),min(x,y)),s(min(x,y))) (16)
gcd#(s(x),s(y)) minus#(max(x,y),min(x,y)) (17)
gcd#(s(x),s(y)) max#(x,y) (18)
gcd#(s(x),s(y)) min#(x,y) (19)
any#(s(x)) any#(x) (20)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.