Certification Problem

Input (TPDB TRS_Standard/Rubio_04/gcd)

The rewrite relation of the following TRS is considered.

minus(X,s(Y)) pred(minus(X,Y)) (1)
minus(X,0) X (2)
pred(s(X)) X (3)
le(s(X),s(Y)) le(X,Y) (4)
le(s(X),0) false (5)
le(0,Y) true (6)
gcd(0,Y) 0 (7)
gcd(s(X),0) s(X) (8)
gcd(s(X),s(Y)) if(le(Y,X),s(X),s(Y)) (9)
if(true,s(X),s(Y)) gcd(minus(X,Y),s(Y)) (10)
if(false,s(X),s(Y)) gcd(minus(Y,X),s(X)) (11)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Switch to Innermost Termination

The TRS is overlay and locally confluent:

10

Hence, it suffices to show innermost termination in the following.

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
minus#(X,s(Y)) pred#(minus(X,Y)) (12)
minus#(X,s(Y)) minus#(X,Y) (13)
le#(s(X),s(Y)) le#(X,Y) (14)
gcd#(s(X),s(Y)) if#(le(Y,X),s(X),s(Y)) (15)
gcd#(s(X),s(Y)) le#(Y,X) (16)
if#(true,s(X),s(Y)) gcd#(minus(X,Y),s(Y)) (17)
if#(true,s(X),s(Y)) minus#(X,Y) (18)
if#(false,s(X),s(Y)) gcd#(minus(Y,X),s(X)) (19)
if#(false,s(X),s(Y)) minus#(Y,X) (20)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.