YES We show the termination of the TRS R: app(app(app(compose(),f),g),x) -> app(g,app(f,x)) app(reverse(),l) -> app(app(reverse2(),l),nil()) app(app(reverse2(),nil()),l) -> l app(app(reverse2(),app(app(cons(),x),xs)),l) -> app(app(reverse2(),xs),app(app(cons(),x),l)) app(hd(),app(app(cons(),x),xs)) -> x app(tl(),app(app(cons(),x),xs)) -> xs last() -> app(app(compose(),hd()),reverse()) init() -> app(app(compose(),reverse()),app(app(compose(),tl()),reverse())) Instead we prove termination of the uncurried system: app(compose_0(),y) -> compose_1(y) app(compose_1(x1),y) -> compose_2(x1,y) app(compose_2(x1,x2),y) -> compose_3(x1,x2,y) app(cons_0(),y) -> cons_1(y) app(cons_1(x1),y) -> cons_2(x1,y) app(hd_0(),y) -> hd_1(y) app(reverse_0(),y) -> reverse_1(y) app(reverse2_0(),y) -> reverse2_1(y) app(reverse2_1(x1),y) -> reverse2_2(x1,y) app(tl_0(),y) -> tl_1(y) compose_3(f,g,x) -> app(g,app(f,x)) reverse_1(l) -> reverse2_2(l,nil_0()) reverse2_2(nil_0(),l) -> l reverse2_2(cons_2(x,xs),l) -> reverse2_2(xs,cons_2(x,l)) hd_1(cons_2(x,xs)) -> x tl_1(cons_2(x,xs)) -> xs last_0() -> compose_2(hd_0(),reverse_0()) init_0() -> compose_2(reverse_0(),compose_2(tl_0(),reverse_0())) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: app#(compose_2(x1,x2),y) -> compose_3#(x1,x2,y) p2: app#(hd_0(),y) -> hd_1#(y) p3: app#(reverse_0(),y) -> reverse_1#(y) p4: app#(reverse2_1(x1),y) -> reverse2_2#(x1,y) p5: app#(tl_0(),y) -> tl_1#(y) p6: compose_3#(f,g,x) -> app#(g,app(f,x)) p7: compose_3#(f,g,x) -> app#(f,x) p8: reverse_1#(l) -> reverse2_2#(l,nil_0()) p9: reverse2_2#(cons_2(x,xs),l) -> reverse2_2#(xs,cons_2(x,l)) and R consists of: r1: app(compose_0(),y) -> compose_1(y) r2: app(compose_1(x1),y) -> compose_2(x1,y) r3: app(compose_2(x1,x2),y) -> compose_3(x1,x2,y) r4: app(cons_0(),y) -> cons_1(y) r5: app(cons_1(x1),y) -> cons_2(x1,y) r6: app(hd_0(),y) -> hd_1(y) r7: app(reverse_0(),y) -> reverse_1(y) r8: app(reverse2_0(),y) -> reverse2_1(y) r9: app(reverse2_1(x1),y) -> reverse2_2(x1,y) r10: app(tl_0(),y) -> tl_1(y) r11: compose_3(f,g,x) -> app(g,app(f,x)) r12: reverse_1(l) -> reverse2_2(l,nil_0()) r13: reverse2_2(nil_0(),l) -> l r14: reverse2_2(cons_2(x,xs),l) -> reverse2_2(xs,cons_2(x,l)) r15: hd_1(cons_2(x,xs)) -> x r16: tl_1(cons_2(x,xs)) -> xs r17: last_0() -> compose_2(hd_0(),reverse_0()) r18: init_0() -> compose_2(reverse_0(),compose_2(tl_0(),reverse_0())) The estimated dependency graph contains the following SCCs: {p1, p6, p7} {p9} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: app#(compose_2(x1,x2),y) -> compose_3#(x1,x2,y) p2: compose_3#(f,g,x) -> app#(f,x) p3: compose_3#(f,g,x) -> app#(g,app(f,x)) and R consists of: r1: app(compose_0(),y) -> compose_1(y) r2: app(compose_1(x1),y) -> compose_2(x1,y) r3: app(compose_2(x1,x2),y) -> compose_3(x1,x2,y) r4: app(cons_0(),y) -> cons_1(y) r5: app(cons_1(x1),y) -> cons_2(x1,y) r6: app(hd_0(),y) -> hd_1(y) r7: app(reverse_0(),y) -> reverse_1(y) r8: app(reverse2_0(),y) -> reverse2_1(y) r9: app(reverse2_1(x1),y) -> reverse2_2(x1,y) r10: app(tl_0(),y) -> tl_1(y) r11: compose_3(f,g,x) -> app(g,app(f,x)) r12: reverse_1(l) -> reverse2_2(l,nil_0()) r13: reverse2_2(nil_0(),l) -> l r14: reverse2_2(cons_2(x,xs),l) -> reverse2_2(xs,cons_2(x,l)) r15: hd_1(cons_2(x,xs)) -> x r16: tl_1(cons_2(x,xs)) -> xs r17: last_0() -> compose_2(hd_0(),reverse_0()) r18: init_0() -> compose_2(reverse_0(),compose_2(tl_0(),reverse_0())) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16 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!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: app#_A(x1,x2) = x1 + x2 compose_2_A(x1,x2) = x1 + x2 + 2 compose_3#_A(x1,x2,x3) = x1 + x2 + x3 + 1 app_A(x1,x2) = x1 + x2 + 1 compose_0_A() = 1 compose_1_A(x1) = x1 + 1 compose_3_A(x1,x2,x3) = x1 + x2 + x3 + 2 cons_0_A() = 1 cons_1_A(x1) = x1 + 1 cons_2_A(x1,x2) = x1 + x2 + 1 hd_0_A() = 1 hd_1_A(x1) = x1 reverse_0_A() = 1 reverse_1_A(x1) = x1 + 1 reverse2_0_A() = 1 reverse2_1_A(x1) = x1 + 1 reverse2_2_A(x1,x2) = x1 + x2 tl_0_A() = 1 tl_1_A(x1) = x1 nil_0_A() = 1 app#!_A(x1,x2) = 6 compose_2!_A(x1,x2) = x1 + 5 compose_3#!_A(x1,x2,x3) = 6 app!_A(x1,x2) = x1 + 7 compose_0!_A() = 0 compose_1!_A(x1) = 6 compose_3!_A(x1,x2,x3) = x1 + x2 + 8 cons_0!_A() = 0 cons_1!_A(x1) = 1 cons_2!_A(x1,x2) = 2 hd_0!_A() = 0 hd_1!_A(x1) = 1 reverse_0!_A() = 4 reverse_1!_A(x1) = 3 reverse2_0!_A() = 0 reverse2_1!_A(x1) = 1 reverse2_2!_A(x1,x2) = 2 tl_0!_A() = 0 tl_1!_A(x1) = 1 nil_0!_A() = 0 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: app#_A(x1,x2) = max{0, x1 - 5, x2 - 20} compose_2_A(x1,x2) = max{x1 + 4, x2} compose_3#_A(x1,x2,x3) = max{0, x1 - 2, x2 - 5, x3 - 20} app_A(x1,x2) = max{19, x1 + 14, x2} compose_0_A = 5 compose_1_A(x1) = max{5, x1} compose_3_A(x1,x2,x3) = max{19, x1 + 14, x2 + 14, x3} cons_0_A = 5 cons_1_A(x1) = max{5, x1 - 4} cons_2_A(x1,x2) = max{11, x1 + 1, x2} hd_0_A = 0 hd_1_A(x1) = max{15, x1 - 1} reverse_0_A = 4 reverse_1_A(x1) = max{19, x1} reverse2_0_A = 7 reverse2_1_A(x1) = max{5, x1 - 5} reverse2_2_A(x1,x2) = max{10, x1, x2} tl_0_A = 4 tl_1_A(x1) = max{19, x1} nil_0_A = 1 app#!_A(x1,x2) = max{1, x1 - 1} compose_2!_A(x1,x2) = max{8, x1 + 6, x2 - 4} compose_3#!_A(x1,x2,x3) = max{x1 + 2, x2 - 1} app!_A(x1,x2) = max{3, x1 - 6} compose_0!_A = 5 compose_1!_A(x1) = x1 + 5 compose_3!_A(x1,x2,x3) = max{9, x1 - 1, x2 - 5} cons_0!_A = 1 cons_1!_A(x1) = max{4, x1 - 1} cons_2!_A(x1,x2) = max{0, x1 - 11} hd_0!_A = 8 hd_1!_A(x1) = max{4, x1 - 1} reverse_0!_A = 6 reverse_1!_A(x1) = max{5, x1 - 1} reverse2_0!_A = 1 reverse2_1!_A(x1) = 2 reverse2_2!_A(x1,x2) = max{4, x1 - 12, x2 - 13} tl_0!_A = 5 tl_1!_A(x1) = max{4, x1 - 1} nil_0!_A = 0 partial status: pi(app#) = [] pi(compose_2) = [1, 2] pi(compose_3#) = [] pi(app) = [1, 2] pi(compose_0) = [] pi(compose_1) = [1] pi(compose_3) = [1, 2, 3] pi(cons_0) = [] pi(cons_1) = [1] pi(cons_2) = [1, 2] pi(hd_0) = [] pi(hd_1) = [1] pi(reverse_0) = [] pi(reverse_1) = [1] pi(reverse2_0) = [] pi(reverse2_1) = [1] pi(reverse2_2) = [1, 2] pi(tl_0) = [] pi(tl_1) = [1] pi(nil_0) = [] The following rules are removed: p2 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: app#(compose_2(x1,x2),y) -> compose_3#(x1,x2,y) p2: compose_3#(f,g,x) -> app#(g,app(f,x)) and R consists of: r1: app(compose_0(),y) -> compose_1(y) r2: app(compose_1(x1),y) -> compose_2(x1,y) r3: app(compose_2(x1,x2),y) -> compose_3(x1,x2,y) r4: app(cons_0(),y) -> cons_1(y) r5: app(cons_1(x1),y) -> cons_2(x1,y) r6: app(hd_0(),y) -> hd_1(y) r7: app(reverse_0(),y) -> reverse_1(y) r8: app(reverse2_0(),y) -> reverse2_1(y) r9: app(reverse2_1(x1),y) -> reverse2_2(x1,y) r10: app(tl_0(),y) -> tl_1(y) r11: compose_3(f,g,x) -> app(g,app(f,x)) r12: reverse_1(l) -> reverse2_2(l,nil_0()) r13: reverse2_2(nil_0(),l) -> l r14: reverse2_2(cons_2(x,xs),l) -> reverse2_2(xs,cons_2(x,l)) r15: hd_1(cons_2(x,xs)) -> x r16: tl_1(cons_2(x,xs)) -> xs r17: last_0() -> compose_2(hd_0(),reverse_0()) r18: init_0() -> compose_2(reverse_0(),compose_2(tl_0(),reverse_0())) The estimated dependency graph contains the following SCCs: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: app#(compose_2(x1,x2),y) -> compose_3#(x1,x2,y) p2: compose_3#(f,g,x) -> app#(g,app(f,x)) and R consists of: r1: app(compose_0(),y) -> compose_1(y) r2: app(compose_1(x1),y) -> compose_2(x1,y) r3: app(compose_2(x1,x2),y) -> compose_3(x1,x2,y) r4: app(cons_0(),y) -> cons_1(y) r5: app(cons_1(x1),y) -> cons_2(x1,y) r6: app(hd_0(),y) -> hd_1(y) r7: app(reverse_0(),y) -> reverse_1(y) r8: app(reverse2_0(),y) -> reverse2_1(y) r9: app(reverse2_1(x1),y) -> reverse2_2(x1,y) r10: app(tl_0(),y) -> tl_1(y) r11: compose_3(f,g,x) -> app(g,app(f,x)) r12: reverse_1(l) -> reverse2_2(l,nil_0()) r13: reverse2_2(nil_0(),l) -> l r14: reverse2_2(cons_2(x,xs),l) -> reverse2_2(xs,cons_2(x,l)) r15: hd_1(cons_2(x,xs)) -> x r16: tl_1(cons_2(x,xs)) -> xs r17: last_0() -> compose_2(hd_0(),reverse_0()) r18: init_0() -> compose_2(reverse_0(),compose_2(tl_0(),reverse_0())) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15, r16 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!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: app#_A(x1,x2) = x1 + x2 compose_2_A(x1,x2) = x1 + x2 + 3 compose_3#_A(x1,x2,x3) = x1 + x2 + x3 + 1 app_A(x1,x2) = x1 + x2 + 1 compose_0_A() = 3 compose_1_A(x1) = x1 + 4 compose_3_A(x1,x2,x3) = x1 + x2 + x3 + 2 cons_0_A() = 2 cons_1_A(x1) = x1 + 3 cons_2_A(x1,x2) = x1 + x2 + 1 hd_0_A() = 4 hd_1_A(x1) = x1 reverse_0_A() = 5 reverse_1_A(x1) = x1 + 1 reverse2_0_A() = 3 reverse2_1_A(x1) = x1 + 4 reverse2_2_A(x1,x2) = x1 + x2 tl_0_A() = 4 tl_1_A(x1) = x1 nil_0_A() = 1 app#!_A(x1,x2) = 0 compose_2!_A(x1,x2) = x1 + 3 compose_3#!_A(x1,x2,x3) = x1 + 1 app!_A(x1,x2) = x1 + x2 compose_0!_A() = 0 compose_1!_A(x1) = 1 compose_3!_A(x1,x2,x3) = x1 + x2 + x3 + 2 cons_0!_A() = 0 cons_1!_A(x1) = 1 cons_2!_A(x1,x2) = 2 hd_0!_A() = 0 hd_1!_A(x1) = 1 reverse_0!_A() = 5 reverse_1!_A(x1) = x1 + 4 reverse2_0!_A() = 0 reverse2_1!_A(x1) = 1 reverse2_2!_A(x1,x2) = x1 + 3 tl_0!_A() = 0 tl_1!_A(x1) = 1 nil_0!_A() = 0 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: app#_A(x1,x2) = max{0, x1 - 15, x2 - 22} compose_2_A(x1,x2) = max{14, x1 + 1, x2} compose_3#_A(x1,x2,x3) = max{0, x1 - 14, x2 - 15, x3 - 22} app_A(x1,x2) = max{21, x1 + 6, x2} compose_0_A = 0 compose_1_A(x1) = max{7, x1 - 5} compose_3_A(x1,x2,x3) = max{21, x1 + 6, x2 + 6, x3} cons_0_A = 0 cons_1_A(x1) = max{7, x1 - 5} cons_2_A(x1,x2) = max{20, x1, x2} hd_0_A = 3 hd_1_A(x1) = max{10, x1} reverse_0_A = 3 reverse_1_A(x1) = max{19, x1} reverse2_0_A = 5 reverse2_1_A(x1) = max{12, x1} reverse2_2_A(x1,x2) = max{19, x1, x2} tl_0_A = 2 tl_1_A(x1) = max{9, x1} nil_0_A = 1 app#!_A(x1,x2) = max{2, x1 - 17, x2 - 22} compose_2!_A(x1,x2) = max{9, x1 - 4} compose_3#!_A(x1,x2,x3) = max{1, x1 - 17} app!_A(x1,x2) = max{x1 + 4, x2 + 7} compose_0!_A = 1 compose_1!_A(x1) = 8 compose_3!_A(x1,x2,x3) = max{x1 + 29, x2 + 29, x3 + 29} cons_0!_A = 2 cons_1!_A(x1) = max{1, x1 - 1} cons_2!_A(x1,x2) = max{2, x1 - 1} hd_0!_A = 9 hd_1!_A(x1) = max{8, x1 - 1} reverse_0!_A = 7 reverse_1!_A(x1) = x1 + 6 reverse2_0!_A = 1 reverse2_1!_A(x1) = 8 reverse2_2!_A(x1,x2) = max{5, x1 + 3} tl_0!_A = 1 tl_1!_A(x1) = max{0, x1 - 1} nil_0!_A = 0 partial status: pi(app#) = [1] pi(compose_2) = [1, 2] pi(compose_3#) = [1, 2] pi(app) = [1, 2] pi(compose_0) = [] pi(compose_1) = [1] pi(compose_3) = [1, 2, 3] pi(cons_0) = [] pi(cons_1) = [1] pi(cons_2) = [1, 2] pi(hd_0) = [] pi(hd_1) = [1] pi(reverse_0) = [] pi(reverse_1) = [1] pi(reverse2_0) = [] pi(reverse2_1) = [1] pi(reverse2_2) = [1, 2] pi(tl_0) = [] pi(tl_1) = [1] pi(nil_0) = [] The following rules are removed: p1, p2 Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: reverse2_2#(cons_2(x,xs),l) -> reverse2_2#(xs,cons_2(x,l)) and R consists of: r1: app(compose_0(),y) -> compose_1(y) r2: app(compose_1(x1),y) -> compose_2(x1,y) r3: app(compose_2(x1,x2),y) -> compose_3(x1,x2,y) r4: app(cons_0(),y) -> cons_1(y) r5: app(cons_1(x1),y) -> cons_2(x1,y) r6: app(hd_0(),y) -> hd_1(y) r7: app(reverse_0(),y) -> reverse_1(y) r8: app(reverse2_0(),y) -> reverse2_1(y) r9: app(reverse2_1(x1),y) -> reverse2_2(x1,y) r10: app(tl_0(),y) -> tl_1(y) r11: compose_3(f,g,x) -> app(g,app(f,x)) r12: reverse_1(l) -> reverse2_2(l,nil_0()) r13: reverse2_2(nil_0(),l) -> l r14: reverse2_2(cons_2(x,xs),l) -> reverse2_2(xs,cons_2(x,l)) r15: hd_1(cons_2(x,xs)) -> x r16: tl_1(cons_2(x,xs)) -> xs r17: last_0() -> compose_2(hd_0(),reverse_0()) r18: init_0() -> compose_2(reverse_0(),compose_2(tl_0(),reverse_0())) 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!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: reverse2_2#_A(x1,x2) = x1 + x2 cons_2_A(x1,x2) = x1 + x2 + 2 reverse2_2#!_A(x1,x2) = x1 + 4 cons_2!_A(x1,x2) = x1 + 3 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: reverse2_2#_A(x1,x2) = max{0, x1 - 11, x2 - 11} cons_2_A(x1,x2) = max{10, x1 - 9, x2} reverse2_2#!_A(x1,x2) = max{x1 + 17, x2 + 8} cons_2!_A(x1,x2) = 6 partial status: pi(reverse2_2#) = [] pi(cons_2) = [] The following rules are removed: p1 Then no dependency pair remains.