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 r1, r3, r4, r5, r7, r9, r10 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: flatwith_2#_A(x1,x2) = x1 + 3 leaf_1_A(x1) = max{0, x1 - 21} app#_A(x1,x2) = max{2, x1} flatwithsub_1_A(x1) = x1 + 3 flatwithsub_2#_A(x1,x2) = x1 + 3 cons_2_A(x1,x2) = max{8, x1 - 25, x2 - 13} node_1_A(x1) = max{9, x1 - 21} flatwith_1_A(x1) = max{6, x1 + 4} app_A(x1,x2) = max{24, x1 - 7, x2 + 5} append_0_A = 5 append_1_A(x1) = max{6, x1 - 1} cons_0_A = 14 cons_1_A(x1) = max{6, x1 - 1} flatwith_0_A = 5 flatwithsub_0_A = 1 leaf_0_A = 6 node_0_A = 8 base order 2: precedence: flatwith_0 > flatwith_1 > app > app# = flatwithsub_1 = node_1 > flatwith_2# = flatwithsub_2# > cons_2 = cons_1 = flatwithsub_0 = node_0 > leaf_1 = append_1 = cons_0 > append_0 = leaf_0 partial status: pi(flatwith_2#) = [1] pi(leaf_1) = [] pi(app#) = [1] pi(flatwithsub_1) = [1] pi(flatwithsub_2#) = [1] pi(cons_2) = [] pi(node_1) = [] pi(flatwith_1) = [1] pi(app) = [] pi(append_0) = [] pi(append_1) = [] pi(cons_0) = [] pi(cons_1) = [] pi(flatwith_0) = [] pi(flatwithsub_0) = [] pi(leaf_0) = [] pi(node_0) = [] The following rules are removed: p2 -- 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) p5: 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 estimated dependency graph contains the following SCCs: {p1, p2, p3, p4, p5} -- 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#(flatwith_1(x1),y) -> flatwith_2#(x1,y) p3: flatwith_2#(f,node_1(xs)) -> flatwithsub_2#(f,xs) p4: flatwithsub_2#(f,cons_2(x,xs)) -> flatwith_2#(f,x) p5: 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 set of usable rules consists of r3, r7, r10 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: flatwith_2#_A(x1,x2) = max{3, x1 - 1} leaf_1_A(x1) = max{26, x1 - 23} app#_A(x1,x2) = max{1, x1 - 3} flatwith_1_A(x1) = x1 + 6 node_1_A(x1) = max{9, x1 - 23} flatwithsub_2#_A(x1,x2) = max{3, x1 - 1} cons_2_A(x1,x2) = max{11, x1 - 20, x2 - 16} app_A(x1,x2) = max{10, x1 - 7, x2 - 2} cons_0_A = 5 cons_1_A(x1) = max{6, x1 - 13} flatwithsub_0_A = 6 flatwithsub_1_A(x1) = max{8, x1 - 9} node_0_A = 8 base order 2: precedence: flatwithsub_1 > app# = flatwith_1 > flatwith_2# = flatwithsub_2# = app > node_1 = cons_2 = flatwithsub_0 > leaf_1 = cons_1 = node_0 > cons_0 partial status: pi(flatwith_2#) = [] pi(leaf_1) = [] pi(app#) = [] pi(flatwith_1) = [1] pi(node_1) = [] pi(flatwithsub_2#) = [] pi(cons_2) = [] pi(app) = [] pi(cons_0) = [] pi(cons_1) = [] pi(flatwithsub_0) = [] pi(flatwithsub_1) = [] pi(node_0) = [] The following rules are removed: p1 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: app#(flatwith_1(x1),y) -> flatwith_2#(x1,y) p2: flatwith_2#(f,node_1(xs)) -> flatwithsub_2#(f,xs) p3: flatwithsub_2#(f,cons_2(x,xs)) -> flatwith_2#(f,x) p4: 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, p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: flatwith_2#(f,node_1(xs)) -> flatwithsub_2#(f,xs) p2: flatwithsub_2#(f,cons_2(x,xs)) -> flatwithsub_2#(f,xs) p3: flatwithsub_2#(f,cons_2(x,xs)) -> flatwith_2#(f,x) 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 r1, r3, r5, r7 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: flatwith_2#_A(x1,x2) = max{1, x2 - 26} node_1_A(x1) = x1 + 34 flatwithsub_2#_A(x1,x2) = max{7, x2 + 4} cons_2_A(x1,x2) = max{7, x1 - 25, x2 + 4} app_A(x1,x2) = max{6, x1 - 3, x2 - 21} append_0_A = 1 append_1_A(x1) = max{2, x1 - 22} cons_0_A = 2 cons_1_A(x1) = max{1, x1 - 22} flatwith_0_A = 1 flatwith_1_A(x1) = max{2, x1 - 22} flatwithsub_0_A = 5 flatwithsub_1_A(x1) = 4 base order 2: precedence: cons_2 = cons_0 > flatwithsub_2# > flatwith_2# = node_1 > app = flatwithsub_0 > append_1 = cons_1 = flatwith_1 = flatwithsub_1 > append_0 = flatwith_0 partial status: pi(flatwith_2#) = [] pi(node_1) = [1] pi(flatwithsub_2#) = [2] pi(cons_2) = [2] pi(app) = [] pi(append_0) = [] pi(append_1) = [] pi(cons_0) = [] pi(cons_1) = [] pi(flatwith_0) = [] pi(flatwith_1) = [] pi(flatwithsub_0) = [] pi(flatwithsub_1) = [] The following rules are removed: p1 -- SCC decomposition. 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) 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: {p1} -- 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) 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 r1, r3, r5, r7, r9, r10 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: flatwithsub_2#_A(x1,x2) = max{17, x1 + 1, x2 + 12} cons_2_A(x1,x2) = max{x1 - 11, x2 + 5} app_A(x1,x2) = max{8, x1 - 9, x2 - 5} append_0_A = 7 append_1_A(x1) = max{8, x1 - 5} cons_0_A = 8 cons_1_A(x1) = max{0, x1 - 12} flatwith_0_A = 1 flatwith_1_A(x1) = max{2, x1 - 6} flatwithsub_0_A = 7 flatwithsub_1_A(x1) = max{8, x1 - 5} leaf_0_A = 8 leaf_1_A(x1) = max{2, x1 - 17} node_0_A = 8 node_1_A(x1) = max{0, x1 - 20} base order 2: precedence: flatwithsub_2# = app > cons_2 = append_0 = flatwith_1 = node_0 > append_1 = cons_1 = flatwith_0 = flatwithsub_1 = leaf_1 = node_1 > cons_0 = flatwithsub_0 = leaf_0 partial status: pi(flatwithsub_2#) = [2] pi(cons_2) = [2] pi(app) = [] pi(append_0) = [] pi(append_1) = [] pi(cons_0) = [] pi(cons_1) = [] pi(flatwith_0) = [] pi(flatwith_1) = [] pi(flatwithsub_0) = [] pi(flatwithsub_1) = [] pi(leaf_0) = [] pi(leaf_1) = [] pi(node_0) = [] pi(node_1) = [] The following rules are removed: p1 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 r1, r3, r5, r7, r9, r10 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: append_2#_A(x1,x2) = max{27, x1 + 14, x2 + 1} cons_2_A(x1,x2) = max{x1 - 7, x2 + 13} app_A(x1,x2) = max{6, x1 - 5, x2 - 1} append_0_A = 3 append_1_A(x1) = max{4, x1 - 2} cons_0_A = 3 cons_1_A(x1) = max{4, x1 - 6} flatwith_0_A = 3 flatwith_1_A(x1) = max{4, x1 - 1} flatwithsub_0_A = 2 flatwithsub_1_A(x1) = max{3, x1 - 2} leaf_0_A = 1 leaf_1_A(x1) = max{2, x1 - 2} node_0_A = 1 node_1_A(x1) = max{2, x1 - 2} base order 2: precedence: append_2# > cons_2 > app = append_0 > append_1 = cons_1 = flatwith_1 = flatwithsub_1 = leaf_1 = node_1 > cons_0 = flatwith_0 = flatwithsub_0 = leaf_0 = node_0 partial status: pi(append_2#) = [1] pi(cons_2) = [2] pi(app) = [] pi(append_0) = [] pi(append_1) = [] pi(cons_0) = [] pi(cons_1) = [] pi(flatwith_0) = [] pi(flatwith_1) = [] pi(flatwithsub_0) = [] pi(flatwithsub_1) = [] pi(leaf_0) = [] pi(leaf_1) = [] pi(node_0) = [] pi(node_1) = [] The following rules are removed: p1 Then no dependency pair remains.