YES We show the termination of the TRS R: app(app(|:|(),app(app(|:|(),x),y)),z) -> app(app(|:|(),x),app(app(|:|(),y),z)) app(app(|:|(),app(app(+(),x),y)),z) -> app(app(+(),app(app(|:|(),x),z)),app(app(|:|(),y),z)) app(app(|:|(),z),app(app(+(),x),app(f,y))) -> app(app(|:|(),app(app(g(),z),y)),app(app(+(),x),a())) app(app(map(),f),nil()) -> nil() app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs)) app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs) app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs)) app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: app#(app(|:|(),app(app(|:|(),x),y)),z) -> app#(app(|:|(),x),app(app(|:|(),y),z)) p2: app#(app(|:|(),app(app(|:|(),x),y)),z) -> app#(app(|:|(),y),z) p3: app#(app(|:|(),app(app(|:|(),x),y)),z) -> app#(|:|(),y) p4: app#(app(|:|(),app(app(+(),x),y)),z) -> app#(app(+(),app(app(|:|(),x),z)),app(app(|:|(),y),z)) p5: app#(app(|:|(),app(app(+(),x),y)),z) -> app#(+(),app(app(|:|(),x),z)) p6: app#(app(|:|(),app(app(+(),x),y)),z) -> app#(app(|:|(),x),z) p7: app#(app(|:|(),app(app(+(),x),y)),z) -> app#(|:|(),x) p8: app#(app(|:|(),app(app(+(),x),y)),z) -> app#(app(|:|(),y),z) p9: app#(app(|:|(),app(app(+(),x),y)),z) -> app#(|:|(),y) p10: app#(app(|:|(),z),app(app(+(),x),app(f,y))) -> app#(app(|:|(),app(app(g(),z),y)),app(app(+(),x),a())) p11: app#(app(|:|(),z),app(app(+(),x),app(f,y))) -> app#(|:|(),app(app(g(),z),y)) p12: app#(app(|:|(),z),app(app(+(),x),app(f,y))) -> app#(app(g(),z),y) p13: app#(app(|:|(),z),app(app(+(),x),app(f,y))) -> app#(g(),z) p14: app#(app(|:|(),z),app(app(+(),x),app(f,y))) -> app#(app(+(),x),a()) p15: app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(cons(),app(f,x)),app(app(map(),f),xs)) p16: app#(app(map(),f),app(app(cons(),x),xs)) -> app#(cons(),app(f,x)) p17: app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) p18: app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) p19: app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs) p20: app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(filter2(),app(f,x)),f),x) p21: app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(filter2(),app(f,x)),f) p22: app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(filter2(),app(f,x)) p23: app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) p24: app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(cons(),x),app(app(filter(),f),xs)) p25: app#(app(app(app(filter2(),true()),f),x),xs) -> app#(cons(),x) p26: app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs) p27: app#(app(app(app(filter2(),true()),f),x),xs) -> app#(filter(),f) p28: app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs) p29: app#(app(app(app(filter2(),false()),f),x),xs) -> app#(filter(),f) and R consists of: r1: app(app(|:|(),app(app(|:|(),x),y)),z) -> app(app(|:|(),x),app(app(|:|(),y),z)) r2: app(app(|:|(),app(app(+(),x),y)),z) -> app(app(+(),app(app(|:|(),x),z)),app(app(|:|(),y),z)) r3: app(app(|:|(),z),app(app(+(),x),app(f,y))) -> app(app(|:|(),app(app(g(),z),y)),app(app(+(),x),a())) r4: app(app(map(),f),nil()) -> nil() r5: app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs)) r6: app(app(filter(),f),nil()) -> nil() r7: app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs) r8: app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs)) r9: app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs) The estimated dependency graph contains the following SCCs: {p17, p18, p19, p23, p26, p28} {p1, p2, p6, p8} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(f,x) p2: app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs) p3: app#(app(filter(),f),app(app(cons(),x),xs)) -> app#(app(app(app(filter2(),app(f,x)),f),x),xs) p4: app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs) p5: app#(app(map(),f),app(app(cons(),x),xs)) -> app#(app(map(),f),xs) p6: app#(app(map(),f),app(app(cons(),x),xs)) -> app#(f,x) and R consists of: r1: app(app(|:|(),app(app(|:|(),x),y)),z) -> app(app(|:|(),x),app(app(|:|(),y),z)) r2: app(app(|:|(),app(app(+(),x),y)),z) -> app(app(+(),app(app(|:|(),x),z)),app(app(|:|(),y),z)) r3: app(app(|:|(),z),app(app(+(),x),app(f,y))) -> app(app(|:|(),app(app(g(),z),y)),app(app(+(),x),a())) r4: app(app(map(),f),nil()) -> nil() r5: app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs)) r6: app(app(filter(),f),nil()) -> nil() r7: app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs) r8: app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs)) r9: app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs) The set of usable rules consists of (no rules) Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: lexicographic combination of reduction triples: 1. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: app#_A(x1,x2) = 0 app_A(x1,x2) = 14 filter_A = 9 cons_A = 10 filter2_A = 19 false_A = 22 true_A = 15 map_A = 10 app#!_A(x1,x2) = 0 app!_A(x1,x2) = max{0, x1 - 12} filter!_A = 3 cons!_A = 0 filter2!_A = 0 false!_A = 0 true!_A = 4 map!_A = 1 2. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: app#_A(x1,x2) = 0 app_A(x1,x2) = x2 + 3 filter_A() = 2 cons_A() = 7 filter2_A() = 2 false_A() = 1 true_A() = 5 map_A() = 2 app#!_A(x1,x2) = 1 app!_A(x1,x2) = 4 filter!_A() = 5 cons!_A() = 2 filter2!_A() = 3 false!_A() = 0 true!_A() = 6 map!_A() = 5 partial status: pi(app#) = [2] pi(app) = [1, 2] pi(filter) = [] pi(cons) = [] pi(filter2) = [] pi(false) = [] pi(true) = [] pi(map) = [] The following rules are removed: p1, p3, p5, p6 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: app#(app(app(app(filter2(),false()),f),x),xs) -> app#(app(filter(),f),xs) p2: app#(app(app(app(filter2(),true()),f),x),xs) -> app#(app(filter(),f),xs) and R consists of: r1: app(app(|:|(),app(app(|:|(),x),y)),z) -> app(app(|:|(),x),app(app(|:|(),y),z)) r2: app(app(|:|(),app(app(+(),x),y)),z) -> app(app(+(),app(app(|:|(),x),z)),app(app(|:|(),y),z)) r3: app(app(|:|(),z),app(app(+(),x),app(f,y))) -> app(app(|:|(),app(app(g(),z),y)),app(app(+(),x),a())) r4: app(app(map(),f),nil()) -> nil() r5: app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs)) r6: app(app(filter(),f),nil()) -> nil() r7: app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs) r8: app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs)) r9: app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs) The estimated dependency graph contains the following SCCs: (no SCCs) -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: app#(app(|:|(),app(app(|:|(),x),y)),z) -> app#(app(|:|(),x),app(app(|:|(),y),z)) p2: app#(app(|:|(),app(app(+(),x),y)),z) -> app#(app(|:|(),y),z) p3: app#(app(|:|(),app(app(+(),x),y)),z) -> app#(app(|:|(),x),z) p4: app#(app(|:|(),app(app(|:|(),x),y)),z) -> app#(app(|:|(),y),z) and R consists of: r1: app(app(|:|(),app(app(|:|(),x),y)),z) -> app(app(|:|(),x),app(app(|:|(),y),z)) r2: app(app(|:|(),app(app(+(),x),y)),z) -> app(app(+(),app(app(|:|(),x),z)),app(app(|:|(),y),z)) r3: app(app(|:|(),z),app(app(+(),x),app(f,y))) -> app(app(|:|(),app(app(g(),z),y)),app(app(+(),x),a())) r4: app(app(map(),f),nil()) -> nil() r5: app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs)) r6: app(app(filter(),f),nil()) -> nil() r7: app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs) r8: app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs)) r9: app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs) The set of usable rules consists of (no rules) Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: trivial reduction triple (T x T, T x T, Φ) base order 2: lexicographic combination of reduction triples: 1. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: app#_A(x1,x2) = 0 app_A(x1,x2) = max{x1 - 15, x2 + 34} |:|_A = 30 +_A = 10 app#!_A(x1,x2) = max{1, x1 - 11} app!_A(x1,x2) = max{49, x1 - 31} |:|!_A = 56 +!_A = 49 2. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: app#_A(x1,x2) = 0 app_A(x1,x2) = 0 |:|_A() = 4 +_A() = 2 app#!_A(x1,x2) = 8 app!_A(x1,x2) = x1 + 2 |:|!_A() = 7 +!_A() = 4 partial status: pi(app#) = [] pi(app) = [] pi(|:|) = [] pi(+) = [] The following rules are removed: p1, p2, p3, p4 Then no dependency pair remains.