Certification Problem

Input (TPDB TRS_Innermost/Applicative_AG01_innermost/#4.13)

The rewrite relation of the following TRS is considered.

app(app(app(f,0),1),x) app(app(app(f,x),x),x) (1)
app(app(app(f,x),y),z) 2 (2)
0 2 (3)
1 2 (4)
app(app(app(g,x),x),y) y (5)
app(app(app(g,x),y),y) x (6)
app(app(map,fun),nil) nil (7)
app(app(map,fun),app(app(cons,x),xs)) app(app(cons,app(fun,x)),app(app(map,fun),xs)) (8)
app(app(filter,fun),nil) nil (9)
app(app(filter,fun),app(app(cons,x),xs)) app(app(app(app(filter2,app(fun,x)),fun),x),xs) (10)
app(app(app(app(filter2,true),fun),x),xs) app(app(cons,x),app(app(filter,fun),xs)) (11)
app(app(app(app(filter2,false),fun),x),xs) app(app(filter,fun),xs) (12)
The evaluation strategy is innermost.

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.
app#(app(app(f,0),1),x) app#(app(app(f,x),x),x) (13)
app#(app(app(f,0),1),x) app#(app(f,x),x) (14)
app#(app(app(f,0),1),x) app#(f,x) (15)
app#(app(map,fun),app(app(cons,x),xs)) app#(app(cons,app(fun,x)),app(app(map,fun),xs)) (16)
app#(app(map,fun),app(app(cons,x),xs)) app#(cons,app(fun,x)) (17)
app#(app(map,fun),app(app(cons,x),xs)) app#(fun,x) (18)
app#(app(map,fun),app(app(cons,x),xs)) app#(app(map,fun),xs) (19)
app#(app(filter,fun),app(app(cons,x),xs)) app#(app(app(app(filter2,app(fun,x)),fun),x),xs) (20)
app#(app(filter,fun),app(app(cons,x),xs)) app#(app(app(filter2,app(fun,x)),fun),x) (21)
app#(app(filter,fun),app(app(cons,x),xs)) app#(app(filter2,app(fun,x)),fun) (22)
app#(app(filter,fun),app(app(cons,x),xs)) app#(filter2,app(fun,x)) (23)
app#(app(filter,fun),app(app(cons,x),xs)) app#(fun,x) (24)
app#(app(app(app(filter2,true),fun),x),xs) app#(app(cons,x),app(app(filter,fun),xs)) (25)
app#(app(app(app(filter2,true),fun),x),xs) app#(cons,x) (26)
app#(app(app(app(filter2,true),fun),x),xs) app#(app(filter,fun),xs) (27)
app#(app(app(app(filter2,true),fun),x),xs) app#(filter,fun) (28)
app#(app(app(app(filter2,false),fun),x),xs) app#(app(filter,fun),xs) (29)
app#(app(app(app(filter2,false),fun),x),xs) app#(filter,fun) (30)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.