YES We show the termination of the TRS R: app(app(append(),nil()),ys) -> ys app(app(append(),app(app(cons(),x),xs)),ys) -> app(app(cons(),x),app(app(append(),xs),ys)) app(app(flatwith(),f),app(leaf(),x)) -> app(app(cons(),app(f,x)),nil()) app(app(flatwith(),f),app(node(),xs)) -> app(app(flatwithsub(),f),xs) app(app(flatwithsub(),f),nil()) -> nil() app(app(flatwithsub(),f),app(app(cons(),x),xs)) -> app(app(append(),app(app(flatwith(),f),x)),app(app(flatwithsub(),f),xs)) Instead we prove termination of the uncurried system: app(append_0(),y) -> append_1(y) app(append_1(x1),y) -> append_2(x1,y) app(cons_0(),y) -> cons_1(y) app(cons_1(x1),y) -> cons_2(x1,y) app(flatwith_0(),y) -> flatwith_1(y) app(flatwith_1(x1),y) -> flatwith_2(x1,y) app(flatwithsub_0(),y) -> flatwithsub_1(y) app(flatwithsub_1(x1),y) -> flatwithsub_2(x1,y) app(leaf_0(),y) -> leaf_1(y) app(node_0(),y) -> node_1(y) append_2(nil_0(),ys) -> ys append_2(cons_2(x,xs),ys) -> cons_2(x,append_2(xs,ys)) flatwith_2(f,leaf_1(x)) -> cons_2(app(f,x),nil_0()) flatwith_2(f,node_1(xs)) -> flatwithsub_2(f,xs) flatwithsub_2(f,nil_0()) -> nil_0() flatwithsub_2(f,cons_2(x,xs)) -> append_2(flatwith_2(f,x),flatwithsub_2(f,xs)) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: app#(append_1(x1),y) -> append_2#(x1,y) p2: app#(flatwith_1(x1),y) -> flatwith_2#(x1,y) p3: app#(flatwithsub_1(x1),y) -> flatwithsub_2#(x1,y) p4: append_2#(cons_2(x,xs),ys) -> append_2#(xs,ys) p5: flatwith_2#(f,leaf_1(x)) -> app#(f,x) p6: flatwith_2#(f,node_1(xs)) -> flatwithsub_2#(f,xs) p7: flatwithsub_2#(f,cons_2(x,xs)) -> append_2#(flatwith_2(f,x),flatwithsub_2(f,xs)) p8: flatwithsub_2#(f,cons_2(x,xs)) -> flatwith_2#(f,x) p9: flatwithsub_2#(f,cons_2(x,xs)) -> flatwithsub_2#(f,xs) and R consists of: r1: app(append_0(),y) -> append_1(y) r2: app(append_1(x1),y) -> append_2(x1,y) r3: app(cons_0(),y) -> cons_1(y) r4: app(cons_1(x1),y) -> cons_2(x1,y) r5: app(flatwith_0(),y) -> flatwith_1(y) r6: app(flatwith_1(x1),y) -> flatwith_2(x1,y) r7: app(flatwithsub_0(),y) -> flatwithsub_1(y) r8: app(flatwithsub_1(x1),y) -> flatwithsub_2(x1,y) r9: app(leaf_0(),y) -> leaf_1(y) r10: app(node_0(),y) -> node_1(y) r11: append_2(nil_0(),ys) -> ys r12: append_2(cons_2(x,xs),ys) -> cons_2(x,append_2(xs,ys)) r13: flatwith_2(f,leaf_1(x)) -> cons_2(app(f,x),nil_0()) r14: flatwith_2(f,node_1(xs)) -> flatwithsub_2(f,xs) r15: flatwithsub_2(f,nil_0()) -> nil_0() r16: flatwithsub_2(f,cons_2(x,xs)) -> append_2(flatwith_2(f,x),flatwithsub_2(f,xs)) The estimated dependency graph contains the following SCCs: {p2, p3, p5, p6, p8, p9} {p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: flatwith_2#(f,leaf_1(x)) -> app#(f,x) p2: app#(flatwithsub_1(x1),y) -> flatwithsub_2#(x1,y) p3: flatwithsub_2#(f,cons_2(x,xs)) -> flatwithsub_2#(f,xs) p4: flatwithsub_2#(f,cons_2(x,xs)) -> flatwith_2#(f,x) p5: flatwith_2#(f,node_1(xs)) -> flatwithsub_2#(f,xs) p6: app#(flatwith_1(x1),y) -> flatwith_2#(x1,y) and R consists of: r1: app(append_0(),y) -> append_1(y) r2: app(append_1(x1),y) -> append_2(x1,y) r3: app(cons_0(),y) -> cons_1(y) r4: app(cons_1(x1),y) -> cons_2(x1,y) r5: app(flatwith_0(),y) -> flatwith_1(y) r6: app(flatwith_1(x1),y) -> flatwith_2(x1,y) r7: app(flatwithsub_0(),y) -> flatwithsub_1(y) r8: app(flatwithsub_1(x1),y) -> flatwithsub_2(x1,y) r9: app(leaf_0(),y) -> leaf_1(y) r10: app(node_0(),y) -> node_1(y) r11: append_2(nil_0(),ys) -> ys r12: append_2(cons_2(x,xs),ys) -> cons_2(x,append_2(xs,ys)) r13: flatwith_2(f,leaf_1(x)) -> cons_2(app(f,x),nil_0()) r14: flatwith_2(f,node_1(xs)) -> flatwithsub_2(f,xs) r15: flatwithsub_2(f,nil_0()) -> nil_0() r16: flatwithsub_2(f,cons_2(x,xs)) -> append_2(flatwith_2(f,x),flatwithsub_2(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: flatwith_2#_A(x1,x2) = max{0, x1 - 30, x2 - 11} leaf_1_A(x1) = x1 + 10 app#_A(x1,x2) = max{0, x1 - 30, x2 - 1} flatwithsub_1_A(x1) = max{29, x1 + 27} flatwithsub_2#_A(x1,x2) = max{0, x1 - 30, x2 - 9} cons_2_A(x1,x2) = max{4, x1 - 2, x2 + 1} node_1_A(x1) = max{10, x1 + 2} flatwith_1_A(x1) = x1 + 27 flatwith_2#!_A(x1,x2) = max{5, x1 - 2, x2 - 66} leaf_1!_A(x1) = max{4, x1 - 58} app#!_A(x1,x2) = max{5, x1 - 28, x2 - 57} flatwithsub_1!_A(x1) = 1 flatwithsub_2#!_A(x1,x2) = max{5, x1 - 2, x2 - 64} cons_2!_A(x1,x2) = max{0, x1 - 59, x2 - 63} node_1!_A(x1) = max{4, x1 - 10} flatwith_1!_A(x1) = max{4, x1 - 11} 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: flatwith_2#_A(x1,x2) = max{0, x1 - 3, x2 - 17} leaf_1_A(x1) = x1 + 16 app#_A(x1,x2) = max{0, x1 - 3, x2 - 1} flatwithsub_1_A(x1) = x1 + 2 flatwithsub_2#_A(x1,x2) = max{0, x1 - 3, x2 - 15} cons_2_A(x1,x2) = max{5, x1 - 1, x2 + 1} node_1_A(x1) = x1 + 2 flatwith_1_A(x1) = x1 + 2 flatwith_2#!_A(x1,x2) = max{7, x1 - 21, x2 - 8} leaf_1!_A(x1) = max{2, x1 - 56} app#!_A(x1,x2) = max{8, x1 - 22, x2 - 5} flatwithsub_1!_A(x1) = max{2, x1 - 20} flatwithsub_2#!_A(x1,x2) = max{7, x1 - 21, x2 - 6} cons_2!_A(x1,x2) = max{3, x1 - 50, x2 - 18} node_1!_A(x1) = max{6, x1 - 16} flatwith_1!_A(x1) = 6 partial status: pi(flatwith_2#) = [] pi(leaf_1) = [1] pi(app#) = [] pi(flatwithsub_1) = [] pi(flatwithsub_2#) = [] pi(cons_2) = [1, 2] pi(node_1) = [1] pi(flatwith_1) = [1] The following rules are removed: p2, p6 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: flatwith_2#(f,leaf_1(x)) -> app#(f,x) p2: flatwithsub_2#(f,cons_2(x,xs)) -> flatwithsub_2#(f,xs) p3: flatwithsub_2#(f,cons_2(x,xs)) -> flatwith_2#(f,x) p4: flatwith_2#(f,node_1(xs)) -> flatwithsub_2#(f,xs) and R consists of: r1: app(append_0(),y) -> append_1(y) r2: app(append_1(x1),y) -> append_2(x1,y) r3: app(cons_0(),y) -> cons_1(y) r4: app(cons_1(x1),y) -> cons_2(x1,y) r5: app(flatwith_0(),y) -> flatwith_1(y) r6: app(flatwith_1(x1),y) -> flatwith_2(x1,y) r7: app(flatwithsub_0(),y) -> flatwithsub_1(y) r8: app(flatwithsub_1(x1),y) -> flatwithsub_2(x1,y) r9: app(leaf_0(),y) -> leaf_1(y) r10: app(node_0(),y) -> node_1(y) r11: append_2(nil_0(),ys) -> ys r12: append_2(cons_2(x,xs),ys) -> cons_2(x,append_2(xs,ys)) r13: flatwith_2(f,leaf_1(x)) -> cons_2(app(f,x),nil_0()) r14: flatwith_2(f,node_1(xs)) -> flatwithsub_2(f,xs) r15: flatwithsub_2(f,nil_0()) -> nil_0() r16: flatwithsub_2(f,cons_2(x,xs)) -> append_2(flatwith_2(f,x),flatwithsub_2(f,xs)) The estimated dependency graph contains the following SCCs: {p2, p3, p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: flatwithsub_2#(f,cons_2(x,xs)) -> flatwithsub_2#(f,xs) p2: flatwithsub_2#(f,cons_2(x,xs)) -> flatwith_2#(f,x) p3: flatwith_2#(f,node_1(xs)) -> flatwithsub_2#(f,xs) and R consists of: r1: app(append_0(),y) -> append_1(y) r2: app(append_1(x1),y) -> append_2(x1,y) r3: app(cons_0(),y) -> cons_1(y) r4: app(cons_1(x1),y) -> cons_2(x1,y) r5: app(flatwith_0(),y) -> flatwith_1(y) r6: app(flatwith_1(x1),y) -> flatwith_2(x1,y) r7: app(flatwithsub_0(),y) -> flatwithsub_1(y) r8: app(flatwithsub_1(x1),y) -> flatwithsub_2(x1,y) r9: app(leaf_0(),y) -> leaf_1(y) r10: app(node_0(),y) -> node_1(y) r11: append_2(nil_0(),ys) -> ys r12: append_2(cons_2(x,xs),ys) -> cons_2(x,append_2(xs,ys)) r13: flatwith_2(f,leaf_1(x)) -> cons_2(app(f,x),nil_0()) r14: flatwith_2(f,node_1(xs)) -> flatwithsub_2(f,xs) r15: flatwithsub_2(f,nil_0()) -> nil_0() r16: flatwithsub_2(f,cons_2(x,xs)) -> append_2(flatwith_2(f,x),flatwithsub_2(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: flatwithsub_2#_A(x1,x2) = max{0, x1 - 1, x2 - 7} cons_2_A(x1,x2) = max{6, x1 - 1, x2 + 4} flatwith_2#_A(x1,x2) = max{0, x1 - 1, x2 - 10} node_1_A(x1) = x1 + 3 flatwithsub_2#!_A(x1,x2) = max{1, x2 - 2} cons_2!_A(x1,x2) = max{0, x2 - 23} flatwith_2#!_A(x1,x2) = max{3, x2 - 4} node_1!_A(x1) = max{0, x1 - 21} 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: flatwithsub_2#_A(x1,x2) = max{0, x1 - 1, x2 - 17} cons_2_A(x1,x2) = max{16, x1 - 1, x2 + 1} flatwith_2#_A(x1,x2) = max{0, x1 - 1, x2 - 18} node_1_A(x1) = x1 + 2 flatwithsub_2#!_A(x1,x2) = max{18, x1 + 1, x2 + 2} cons_2!_A(x1,x2) = max{5, x1 - 24} flatwith_2#!_A(x1,x2) = max{4, x1 - 1, x2 - 3} node_1!_A(x1) = max{7, x1 - 18} partial status: pi(flatwithsub_2#) = [2] pi(cons_2) = [1, 2] pi(flatwith_2#) = [2] pi(node_1) = [1] The following rules are removed: p1, p2, p3 Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: append_2#(cons_2(x,xs),ys) -> append_2#(xs,ys) and R consists of: r1: app(append_0(),y) -> append_1(y) r2: app(append_1(x1),y) -> append_2(x1,y) r3: app(cons_0(),y) -> cons_1(y) r4: app(cons_1(x1),y) -> cons_2(x1,y) r5: app(flatwith_0(),y) -> flatwith_1(y) r6: app(flatwith_1(x1),y) -> flatwith_2(x1,y) r7: app(flatwithsub_0(),y) -> flatwithsub_1(y) r8: app(flatwithsub_1(x1),y) -> flatwithsub_2(x1,y) r9: app(leaf_0(),y) -> leaf_1(y) r10: app(node_0(),y) -> node_1(y) r11: append_2(nil_0(),ys) -> ys r12: append_2(cons_2(x,xs),ys) -> cons_2(x,append_2(xs,ys)) r13: flatwith_2(f,leaf_1(x)) -> cons_2(app(f,x),nil_0()) r14: flatwith_2(f,node_1(xs)) -> flatwithsub_2(f,xs) r15: flatwithsub_2(f,nil_0()) -> nil_0() r16: flatwithsub_2(f,cons_2(x,xs)) -> append_2(flatwith_2(f,x),flatwithsub_2(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: append_2#_A(x1,x2) = 0 cons_2_A(x1,x2) = max{4, x1 - 1, x2 - 6} append_2#!_A(x1,x2) = max{0, x1 - 32} cons_2!_A(x1,x2) = max{2, x1 - 27, x2 - 31} 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: append_2#_A(x1,x2) = 0 cons_2_A(x1,x2) = max{5, x1 - 5, x2 - 5} append_2#!_A(x1,x2) = max{0, x1 - 37} cons_2!_A(x1,x2) = max{3, x1 - 31, x2 - 36} partial status: pi(append_2#) = [1] pi(cons_2) = [2] The following rules are removed: p1 Then no dependency pair remains.