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, r5, r7, r9, r10, r11, r12 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: flatwith_2#_A(x1,x2) = x1 + x2 + 3 leaf_1_A(x1) = x1 + 2 app#_A(x1,x2) = x1 + x2 + 3 flatwithsub_1_A(x1) = x1 + 2 flatwithsub_2#_A(x1,x2) = x1 + x2 + 3 cons_2_A(x1,x2) = x1 + x2 + 2 node_1_A(x1) = x1 + 2 flatwith_1_A(x1) = x1 + 2 app_A(x1,x2) = x2 + 3 append_0_A() = 2 append_1_A(x1) = 1 cons_0_A() = 2 cons_1_A(x1) = 1 flatwith_0_A() = 1 flatwithsub_0_A() = 1 leaf_0_A() = 1 node_0_A() = 1 append_2_A(x1,x2) = x1 + x2 + 4 nil_0_A() = 1 base order 2: precedence: app# > flatwith_2# > flatwithsub_2# = append_2 > node_1 = cons_0 > node_0 > cons_2 > leaf_1 > app = append_0 = leaf_0 = nil_0 > flatwithsub_1 = flatwith_1 = append_1 = cons_1 > flatwith_0 = flatwithsub_0 partial status: pi(flatwith_2#) = [] pi(leaf_1) = [1] pi(app#) = [2] pi(flatwithsub_1) = [1] pi(flatwithsub_2#) = [1] pi(cons_2) = [1] pi(node_1) = [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) = [] pi(append_2) = [] pi(nil_0) = [] The following rules are removed: p1 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: app#(flatwithsub_1(x1),y) -> flatwithsub_2#(x1,y) 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: {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 r1, r2, r3, r4, r5, r7, r9, r10, r11, r12 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: flatwithsub_2#_A(x1,x2) = x2 cons_2_A(x1,x2) = x1 + x2 + 2 flatwith_2#_A(x1,x2) = x2 node_1_A(x1) = x1 + 2 app_A(x1,x2) = x1 + x2 + 3 append_0_A() = 1 append_1_A(x1) = x1 + 2 append_2_A(x1,x2) = x1 + x2 + 3 cons_0_A() = 2 cons_1_A(x1) = x1 + 1 flatwith_0_A() = 1 flatwith_1_A(x1) = x1 + 3 flatwithsub_0_A() = 1 flatwithsub_1_A(x1) = x1 + 2 leaf_0_A() = 3 leaf_1_A(x1) = x1 + 2 node_0_A() = 1 nil_0_A() = 1 base order 2: precedence: append_2 > flatwith_2# = node_1 = flatwithsub_1 > flatwithsub_0 = node_0 > app > flatwithsub_2# = cons_2 = append_1 = flatwith_1 > append_0 = cons_1 = flatwith_0 = leaf_1 > cons_0 = leaf_0 = nil_0 partial status: pi(flatwithsub_2#) = [] pi(cons_2) = [2] pi(flatwith_2#) = [2] pi(node_1) = [1] pi(app) = [1] pi(append_0) = [] pi(append_1) = [1] pi(append_2) = [] pi(cons_0) = [] pi(cons_1) = [1] pi(flatwith_0) = [] pi(flatwith_1) = [1] pi(flatwithsub_0) = [] pi(flatwithsub_1) = [1] pi(leaf_0) = [] pi(leaf_1) = [1] pi(node_0) = [] pi(nil_0) = [] 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)) -> flatwith_2#(f,x) p2: 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: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: flatwithsub_2#(f,cons_2(x,xs)) -> flatwith_2#(f,x) p2: 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 r1, r3, r5, r7, r10, r11, r12 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: flatwithsub_2#_A(x1,x2) = x2 cons_2_A(x1,x2) = x1 + x2 + 4 flatwith_2#_A(x1,x2) = x2 node_1_A(x1) = x1 + 2 app_A(x1,x2) = x2 + 3 append_0_A() = 2 append_1_A(x1) = 1 cons_0_A() = 2 cons_1_A(x1) = 1 flatwith_0_A() = 2 flatwith_1_A(x1) = 1 flatwithsub_0_A() = 2 flatwithsub_1_A(x1) = 1 node_0_A() = 1 append_2_A(x1,x2) = x1 + x2 + 5 nil_0_A() = 1 base order 2: precedence: cons_0 = nil_0 > cons_1 = flatwithsub_0 > app = append_0 = flatwith_0 = flatwithsub_1 = node_0 = append_2 > append_1 > cons_2 = node_1 = flatwith_1 > flatwithsub_2# = flatwith_2# partial status: pi(flatwithsub_2#) = [2] pi(cons_2) = [] pi(flatwith_2#) = [2] pi(node_1) = [] 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(node_0) = [] pi(append_2) = [] pi(nil_0) = [] The following rules are removed: p1 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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: (no SCCs) -- 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, r10, r11, r12 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: append_2#_A(x1,x2) = x1 + x2 cons_2_A(x1,x2) = x1 + x2 + 4 app_A(x1,x2) = x2 + 3 append_0_A() = 2 append_1_A(x1) = 1 cons_0_A() = 2 cons_1_A(x1) = 1 flatwith_0_A() = 2 flatwith_1_A(x1) = 1 flatwithsub_0_A() = 2 flatwithsub_1_A(x1) = 1 node_0_A() = 1 node_1_A(x1) = x1 + 2 append_2_A(x1,x2) = x1 + x2 + 5 nil_0_A() = 1 base order 2: precedence: cons_0 = append_2 > append_2# = cons_1 > cons_2 > app = append_0 = flatwith_0 = flatwithsub_0 = nil_0 > append_1 = flatwith_1 = flatwithsub_1 = node_1 > node_0 partial status: pi(append_2#) = [1, 2] pi(cons_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(node_0) = [] pi(node_1) = [] pi(append_2) = [] pi(nil_0) = [] The following rules are removed: p1 Then no dependency pair remains.