Certification Problem

Input (TPDB TRS_Standard/Zantema_05/z26)

The rewrite relation of the following TRS is considered.

a(a(f(x,y))) f(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) (1)
f(a(x),a(y)) a(f(x,y)) (2)
f(b(x),b(y)) b(f(x,y)) (3)

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.
a#(a(f(x,y))) f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) (4)
a#(a(f(x,y))) a#(b(a(b(a(x))))) (5)
a#(a(f(x,y))) a#(b(a(x))) (6)
a#(a(f(x,y))) a#(x) (7)
a#(a(f(x,y))) a#(b(a(b(a(y))))) (8)
a#(a(f(x,y))) a#(b(a(y))) (9)
a#(a(f(x,y))) a#(y) (10)
f#(a(x),a(y)) a#(f(x,y)) (11)
f#(a(x),a(y)) f#(x,y) (12)
f#(b(x),b(y)) f#(x,y) (13)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.