Certification Problem

Input (TPDB TRS_Standard/HirokawaMiddeldorp_04/t012)

The rewrite relation of the following TRS is considered.

minus(minus(x)) x (1)
minus(+(x,y)) *(minus(minus(minus(x))),minus(minus(minus(y)))) (2)
minus(*(x,y)) +(minus(minus(minus(x))),minus(minus(minus(y)))) (3)
f(minus(x)) minus(minus(minus(f(x)))) (4)

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.
minus#(+(x,y)) minus#(minus(minus(x))) (5)
minus#(+(x,y)) minus#(minus(x)) (6)
minus#(+(x,y)) minus#(x) (7)
minus#(+(x,y)) minus#(minus(minus(y))) (8)
minus#(+(x,y)) minus#(minus(y)) (9)
minus#(+(x,y)) minus#(y) (10)
minus#(*(x,y)) minus#(minus(minus(x))) (11)
minus#(*(x,y)) minus#(minus(x)) (12)
minus#(*(x,y)) minus#(x) (13)
minus#(*(x,y)) minus#(minus(minus(y))) (14)
minus#(*(x,y)) minus#(minus(y)) (15)
minus#(*(x,y)) minus#(y) (16)
f#(minus(x)) minus#(minus(minus(f(x)))) (17)
f#(minus(x)) minus#(minus(f(x))) (18)
f#(minus(x)) minus#(f(x)) (19)
f#(minus(x)) f#(x) (20)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.