Certification Problem

Input (TPDB TRS_Standard/AotoYamada_05/022)

The rewrite relation of the following TRS is considered.

app(app(mapt,f),app(leaf,x)) app(leaf,app(f,x)) (1)
app(app(mapt,f),app(node,xs)) app(node,app(app(maptlist,f),xs)) (2)
app(app(maptlist,f),nil) nil (3)
app(app(maptlist,f),app(app(cons,x),xs)) app(app(cons,app(app(mapt,f),x)),app(app(maptlist,f),xs)) (4)

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.
app#(app(mapt,f),app(leaf,x)) app#(f,x) (5)
app#(app(mapt,f),app(leaf,x)) app#(leaf,app(f,x)) (6)
app#(app(mapt,f),app(node,xs)) app#(maptlist,f) (7)
app#(app(mapt,f),app(node,xs)) app#(app(maptlist,f),xs) (8)
app#(app(mapt,f),app(node,xs)) app#(node,app(app(maptlist,f),xs)) (9)
app#(app(maptlist,f),app(app(cons,x),xs)) app#(app(maptlist,f),xs) (10)
app#(app(maptlist,f),app(app(cons,x),xs)) app#(mapt,f) (11)
app#(app(maptlist,f),app(app(cons,x),xs)) app#(app(mapt,f),x) (12)
app#(app(maptlist,f),app(app(cons,x),xs)) app#(cons,app(app(mapt,f),x)) (13)
app#(app(maptlist,f),app(app(cons,x),xs)) app#(app(cons,app(app(mapt,f),x)),app(app(maptlist,f),xs)) (14)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.