Certification Problem

Input (TPDB TRS_Standard/AotoYamada_05/016)

The rewrite relation of the following TRS is considered.

app(app(neq,0),0) → false (1)
app(app(neq,0),app(s,y)) → true (2)
app(app(neq,app(s,x)),0) → true (3)
app(app(neq,app(s,x)),app(s,y)) → app(app(neq,x),y) (4)
app(app(filter,f),nil) → nil (5)
app(app(filter,f),app(app(cons,y),ys)) → app(app(app(filtersub,app(f,y)),f),app(app(cons,y),ys)) (6)
app(app(app(filtersub,true),f),app(app(cons,y),ys)) → app(app(cons,y),app(app(filter,f),ys)) (7)
app(app(app(filtersub,false),f),app(app(cons,y),ys)) → app(app(filter,f),ys) (8)
nonzero → app(filter,app(neq,0)) (9)

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(neq,app(s,x)),app(s,y)) → app#(neq,x) (10)
app#(app(neq,app(s,x)),app(s,y)) → app#(app(neq,x),y) (11)
app#(app(filter,f),app(app(cons,y),ys)) → app#(f,y) (12)
app#(app(filter,f),app(app(cons,y),ys)) → app#(filtersub,app(f,y)) (13)
app#(app(filter,f),app(app(cons,y),ys)) → app#(app(filtersub,app(f,y)),f) (14)
app#(app(filter,f),app(app(cons,y),ys)) → app#(app(app(filtersub,app(f,y)),f),app(app(cons,y),ys)) (15)
app#(app(app(filtersub,true),f),app(app(cons,y),ys)) → app#(filter,f) (16)
app#(app(app(filtersub,true),f),app(app(cons,y),ys)) → app#(app(filter,f),ys) (17)
app#(app(app(filtersub,true),f),app(app(cons,y),ys)) → app#(app(cons,y),app(app(filter,f),ys)) (18)
app#(app(app(filtersub,false),f),app(app(cons,y),ys)) → app#(filter,f) (19)
app#(app(app(filtersub,false),f),app(app(cons,y),ys)) → app#(app(filter,f),ys) (20)
nonzero# → app#(neq,0) (21)
nonzero# → app#(filter,app(neq,0)) (22)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.