Certification Problem

Input (TPDB TRS_Standard/SK90/4.28)

The rewrite relation of the following TRS is considered.

f(x,nil) g(nil,x) (1)
f(x,g(y,z)) g(f(x,y),z) (2)
++(x,nil) x (3)
++(x,g(y,z)) g(++(x,y),z) (4)
null(nil) true (5)
null(g(x,y)) false (6)
mem(nil,y) false (7)
mem(g(x,y),z) or(=(y,z),mem(x,z)) (8)
mem(x,max(x)) not(null(x)) (9)
max(g(g(nil,x),y)) max'(x,y) (10)
max(g(g(g(x,y),z),u)) max'(max(g(g(x,y),z)),u) (11)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
f#(x,g(y,z)) f#(x,y) (12)
++#(x,g(y,z)) ++#(x,y) (13)
mem#(g(x,y),z) mem#(x,z) (14)
mem#(x,max(x)) null#(x) (15)
max#(g(g(g(x,y),z),u)) max#(g(g(x,y),z)) (16)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.