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, 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: model-based reduction triple (=A, >=A!, >A!): finite algebra: carrier: {0,1} interpretations: flatwith_2#_A(0,0) = 0 flatwith_2#_A(0,1) = 0 flatwith_2#_A(1,0) = 0 flatwith_2#_A(1,1) = 0 leaf_1_A(0) = 0 leaf_1_A(1) = 0 app#_A(0,0) = 0 app#_A(0,1) = 0 app#_A(1,0) = 0 app#_A(1,1) = 0 flatwithsub_1_A(0) = 0 flatwithsub_1_A(1) = 0 flatwithsub_2#_A(0,0) = 0 flatwithsub_2#_A(0,1) = 0 flatwithsub_2#_A(1,0) = 0 flatwithsub_2#_A(1,1) = 0 cons_2_A(0,0) = 0 cons_2_A(0,1) = 1 cons_2_A(1,0) = 0 cons_2_A(1,1) = 1 node_1_A(0) = 0 node_1_A(1) = 1 flatwith_1_A(0) = 0 flatwith_1_A(1) = 0 app_A(0,0) = 0 app_A(0,1) = 1 app_A(1,0) = 0 app_A(1,1) = 0 append_0_A = 1 append_1_A(0) = 0 append_1_A(1) = 0 append_2_A(0,0) = 0 append_2_A(0,1) = 1 append_2_A(1,0) = 0 append_2_A(1,1) = 1 cons_0_A = 1 cons_1_A(0) = 0 cons_1_A(1) = 0 flatwith_0_A = 1 flatwith_2_A(0,0) = 0 flatwith_2_A(0,1) = 1 flatwith_2_A(1,0) = 0 flatwith_2_A(1,1) = 1 flatwithsub_0_A = 1 flatwithsub_2_A(0,0) = 0 flatwithsub_2_A(0,1) = 1 flatwithsub_2_A(1,0) = 0 flatwithsub_2_A(1,1) = 1 leaf_0_A = 1 node_0_A = 0 nil_0_A = 0 flatwith_2#!_A(0,0) = 1 flatwith_2#!_A(0,1) = 1 flatwith_2#!_A(1,0) = 1 flatwith_2#!_A(1,1) = 1 leaf_1!_A(0) = 0 leaf_1!_A(1) = 0 app#!_A(0,0) = 1 app#!_A(0,1) = 1 app#!_A(1,0) = 0 app#!_A(1,1) = 0 flatwithsub_1!_A(0) = 0 flatwithsub_1!_A(1) = 0 flatwithsub_2#!_A(0,0) = 1 flatwithsub_2#!_A(0,1) = 1 flatwithsub_2#!_A(1,0) = 1 flatwithsub_2#!_A(1,1) = 1 cons_2!_A(0,0) = 0 cons_2!_A(0,1) = 0 cons_2!_A(1,0) = 0 cons_2!_A(1,1) = 0 node_1!_A(0) = 0 node_1!_A(1) = 0 flatwith_1!_A(0) = 0 flatwith_1!_A(1) = 0 app!_A(0,0) = 1 app!_A(0,1) = 1 app!_A(1,0) = 1 app!_A(1,1) = 1 append_0!_A = 0 append_1!_A(0) = 0 append_1!_A(1) = 0 append_2!_A(0,0) = 0 append_2!_A(0,1) = 0 append_2!_A(1,0) = 0 append_2!_A(1,1) = 0 cons_0!_A = 1 cons_1!_A(0) = 0 cons_1!_A(1) = 0 flatwith_0!_A = 0 flatwith_2!_A(0,0) = 1 flatwith_2!_A(0,1) = 1 flatwith_2!_A(1,0) = 1 flatwith_2!_A(1,1) = 1 flatwithsub_0!_A = 1 flatwithsub_2!_A(0,0) = 1 flatwithsub_2!_A(0,1) = 1 flatwithsub_2!_A(1,0) = 1 flatwithsub_2!_A(1,1) = 1 leaf_0!_A = 0 node_0!_A = 0 nil_0!_A = 1 partial status: pi(flatwith_2#) = [1, 2] pi(leaf_1) = [1] pi(app#) = [1, 2] pi(flatwithsub_1) = [1] pi(flatwithsub_2#) = [1, 2] pi(cons_2) = [1, 2] pi(node_1) = [1] pi(flatwith_1) = [1] pi(app) = [1, 2] pi(append_0) = [] pi(append_1) = [1] pi(append_2) = [1, 2] pi(cons_0) = [] pi(cons_1) = [1] pi(flatwith_0) = [] pi(flatwith_2) = [1, 2] pi(flatwithsub_0) = [] pi(flatwithsub_2) = [1, 2] pi(leaf_0) = [] 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: 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, 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: model-based reduction triple (=A, >=A!, >A!): finite algebra: carrier: {0,1} interpretations: flatwithsub_2#_A(0,0) = 0 flatwithsub_2#_A(0,1) = 0 flatwithsub_2#_A(1,0) = 0 flatwithsub_2#_A(1,1) = 0 cons_2_A(0,0) = 0 cons_2_A(0,1) = 1 cons_2_A(1,0) = 0 cons_2_A(1,1) = 1 flatwith_2#_A(0,0) = 0 flatwith_2#_A(0,1) = 0 flatwith_2#_A(1,0) = 0 flatwith_2#_A(1,1) = 0 node_1_A(0) = 0 node_1_A(1) = 1 app_A(0,0) = 1 app_A(0,1) = 1 app_A(1,0) = 0 app_A(1,1) = 1 append_0_A = 0 append_1_A(0) = 1 append_1_A(1) = 1 append_2_A(0,0) = 0 append_2_A(0,1) = 1 append_2_A(1,0) = 0 append_2_A(1,1) = 1 cons_0_A = 0 cons_1_A(0) = 1 cons_1_A(1) = 1 flatwith_0_A = 0 flatwith_1_A(0) = 1 flatwith_1_A(1) = 1 flatwith_2_A(0,0) = 0 flatwith_2_A(0,1) = 1 flatwith_2_A(1,0) = 0 flatwith_2_A(1,1) = 1 flatwithsub_0_A = 0 flatwithsub_1_A(0) = 1 flatwithsub_1_A(1) = 1 flatwithsub_2_A(0,0) = 0 flatwithsub_2_A(0,1) = 1 flatwithsub_2_A(1,0) = 0 flatwithsub_2_A(1,1) = 1 leaf_0_A = 0 leaf_1_A(0) = 1 leaf_1_A(1) = 1 node_0_A = 1 nil_0_A = 1 flatwithsub_2#!_A(0,0) = 0 flatwithsub_2#!_A(0,1) = 0 flatwithsub_2#!_A(1,0) = 0 flatwithsub_2#!_A(1,1) = 0 cons_2!_A(0,0) = 0 cons_2!_A(0,1) = 0 cons_2!_A(1,0) = 0 cons_2!_A(1,1) = 0 flatwith_2#!_A(0,0) = 0 flatwith_2#!_A(0,1) = 0 flatwith_2#!_A(1,0) = 0 flatwith_2#!_A(1,1) = 0 node_1!_A(0) = 0 node_1!_A(1) = 0 app!_A(0,0) = 1 app!_A(0,1) = 1 app!_A(1,0) = 1 app!_A(1,1) = 1 append_0!_A = 0 append_1!_A(0) = 0 append_1!_A(1) = 0 append_2!_A(0,0) = 0 append_2!_A(0,1) = 0 append_2!_A(1,0) = 0 append_2!_A(1,1) = 0 cons_0!_A = 0 cons_1!_A(0) = 0 cons_1!_A(1) = 0 flatwith_0!_A = 0 flatwith_1!_A(0) = 0 flatwith_1!_A(1) = 0 flatwith_2!_A(0,0) = 1 flatwith_2!_A(0,1) = 1 flatwith_2!_A(1,0) = 1 flatwith_2!_A(1,1) = 1 flatwithsub_0!_A = 0 flatwithsub_1!_A(0) = 0 flatwithsub_1!_A(1) = 0 flatwithsub_2!_A(0,0) = 1 flatwithsub_2!_A(0,1) = 1 flatwithsub_2!_A(1,0) = 1 flatwithsub_2!_A(1,1) = 1 leaf_0!_A = 0 leaf_1!_A(0) = 0 leaf_1!_A(1) = 0 node_0!_A = 0 nil_0!_A = 0 partial status: pi(flatwithsub_2#) = [2] pi(cons_2) = [1, 2] pi(flatwith_2#) = [2] pi(node_1) = [1] pi(app) = [1, 2] pi(append_0) = [] pi(append_1) = [1] pi(append_2) = [1, 2] pi(cons_0) = [] pi(cons_1) = [1] pi(flatwith_0) = [] pi(flatwith_1) = [1] pi(flatwith_2) = [1, 2] pi(flatwithsub_0) = [] pi(flatwithsub_1) = [1] pi(flatwithsub_2) = [1, 2] pi(leaf_0) = [] pi(leaf_1) = [1] pi(node_0) = [] pi(nil_0) = [] The following rules are removed: p2, p3 -- 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) 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, 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: model-based reduction triple (=A, >=A!, >A!): finite algebra: carrier: {0,1} interpretations: flatwithsub_2#_A(0,0) = 0 flatwithsub_2#_A(0,1) = 0 flatwithsub_2#_A(1,0) = 0 flatwithsub_2#_A(1,1) = 0 cons_2_A(0,0) = 0 cons_2_A(0,1) = 1 cons_2_A(1,0) = 0 cons_2_A(1,1) = 1 app_A(0,0) = 0 app_A(0,1) = 1 app_A(1,0) = 0 app_A(1,1) = 0 append_0_A = 1 append_1_A(0) = 0 append_1_A(1) = 0 append_2_A(0,0) = 0 append_2_A(0,1) = 1 append_2_A(1,0) = 0 append_2_A(1,1) = 1 cons_0_A = 1 cons_1_A(0) = 0 cons_1_A(1) = 0 flatwith_0_A = 0 flatwith_1_A(0) = 0 flatwith_1_A(1) = 1 flatwith_2_A(0,0) = 0 flatwith_2_A(0,1) = 1 flatwith_2_A(1,0) = 0 flatwith_2_A(1,1) = 0 flatwithsub_0_A = 0 flatwithsub_1_A(0) = 0 flatwithsub_1_A(1) = 1 flatwithsub_2_A(0,0) = 0 flatwithsub_2_A(0,1) = 1 flatwithsub_2_A(1,0) = 0 flatwithsub_2_A(1,1) = 0 leaf_0_A = 1 leaf_1_A(0) = 0 leaf_1_A(1) = 0 node_0_A = 0 node_1_A(0) = 0 node_1_A(1) = 1 nil_0_A = 0 flatwithsub_2#!_A(0,0) = 1 flatwithsub_2#!_A(0,1) = 1 flatwithsub_2#!_A(1,0) = 0 flatwithsub_2#!_A(1,1) = 0 cons_2!_A(0,0) = 0 cons_2!_A(0,1) = 0 cons_2!_A(1,0) = 0 cons_2!_A(1,1) = 0 app!_A(0,0) = 1 app!_A(0,1) = 1 app!_A(1,0) = 1 app!_A(1,1) = 1 append_0!_A = 0 append_1!_A(0) = 0 append_1!_A(1) = 0 append_2!_A(0,0) = 0 append_2!_A(0,1) = 0 append_2!_A(1,0) = 0 append_2!_A(1,1) = 0 cons_0!_A = 1 cons_1!_A(0) = 0 cons_1!_A(1) = 0 flatwith_0!_A = 1 flatwith_1!_A(0) = 0 flatwith_1!_A(1) = 0 flatwith_2!_A(0,0) = 1 flatwith_2!_A(0,1) = 1 flatwith_2!_A(1,0) = 1 flatwith_2!_A(1,1) = 1 flatwithsub_0!_A = 1 flatwithsub_1!_A(0) = 0 flatwithsub_1!_A(1) = 0 flatwithsub_2!_A(0,0) = 1 flatwithsub_2!_A(0,1) = 1 flatwithsub_2!_A(1,0) = 1 flatwithsub_2!_A(1,1) = 1 leaf_0!_A = 1 leaf_1!_A(0) = 0 leaf_1!_A(1) = 0 node_0!_A = 0 node_1!_A(0) = 0 node_1!_A(1) = 0 nil_0!_A = 0 partial status: pi(flatwithsub_2#) = [2] pi(cons_2) = [1, 2] pi(app) = [1, 2] pi(append_0) = [] pi(append_1) = [1] pi(append_2) = [1, 2] pi(cons_0) = [] pi(cons_1) = [1] pi(flatwith_0) = [] pi(flatwith_1) = [1] pi(flatwith_2) = [1, 2] pi(flatwithsub_0) = [] pi(flatwithsub_1) = [1] pi(flatwithsub_2) = [1, 2] pi(leaf_0) = [] pi(leaf_1) = [1] pi(node_0) = [] pi(node_1) = [1] pi(nil_0) = [] 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, 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: model-based reduction triple (=A, >=A!, >A!): finite algebra: carrier: {0,1} interpretations: append_2#_A(0,0) = 0 append_2#_A(0,1) = 0 append_2#_A(1,0) = 0 append_2#_A(1,1) = 0 cons_2_A(0,0) = 0 cons_2_A(0,1) = 1 cons_2_A(1,0) = 0 cons_2_A(1,1) = 1 app_A(0,0) = 1 app_A(0,1) = 1 app_A(1,0) = 0 app_A(1,1) = 1 append_0_A = 0 append_1_A(0) = 1 append_1_A(1) = 1 append_2_A(0,0) = 0 append_2_A(0,1) = 1 append_2_A(1,0) = 0 append_2_A(1,1) = 1 cons_0_A = 0 cons_1_A(0) = 1 cons_1_A(1) = 1 flatwith_0_A = 0 flatwith_1_A(0) = 1 flatwith_1_A(1) = 1 flatwith_2_A(0,0) = 0 flatwith_2_A(0,1) = 1 flatwith_2_A(1,0) = 0 flatwith_2_A(1,1) = 1 flatwithsub_0_A = 0 flatwithsub_1_A(0) = 1 flatwithsub_1_A(1) = 1 flatwithsub_2_A(0,0) = 0 flatwithsub_2_A(0,1) = 1 flatwithsub_2_A(1,0) = 0 flatwithsub_2_A(1,1) = 1 leaf_0_A = 0 leaf_1_A(0) = 1 leaf_1_A(1) = 1 node_0_A = 1 node_1_A(0) = 0 node_1_A(1) = 1 nil_0_A = 1 append_2#!_A(0,0) = 0 append_2#!_A(0,1) = 1 append_2#!_A(1,0) = 0 append_2#!_A(1,1) = 1 cons_2!_A(0,0) = 0 cons_2!_A(0,1) = 0 cons_2!_A(1,0) = 0 cons_2!_A(1,1) = 0 app!_A(0,0) = 1 app!_A(0,1) = 1 app!_A(1,0) = 1 app!_A(1,1) = 1 append_0!_A = 0 append_1!_A(0) = 0 append_1!_A(1) = 0 append_2!_A(0,0) = 0 append_2!_A(0,1) = 0 append_2!_A(1,0) = 0 append_2!_A(1,1) = 0 cons_0!_A = 1 cons_1!_A(0) = 0 cons_1!_A(1) = 0 flatwith_0!_A = 0 flatwith_1!_A(0) = 0 flatwith_1!_A(1) = 0 flatwith_2!_A(0,0) = 1 flatwith_2!_A(0,1) = 1 flatwith_2!_A(1,0) = 1 flatwith_2!_A(1,1) = 1 flatwithsub_0!_A = 0 flatwithsub_1!_A(0) = 0 flatwithsub_1!_A(1) = 0 flatwithsub_2!_A(0,0) = 1 flatwithsub_2!_A(0,1) = 1 flatwithsub_2!_A(1,0) = 1 flatwithsub_2!_A(1,1) = 1 leaf_0!_A = 1 leaf_1!_A(0) = 0 leaf_1!_A(1) = 0 node_0!_A = 1 node_1!_A(0) = 0 node_1!_A(1) = 0 nil_0!_A = 0 partial status: pi(append_2#) = [1, 2] pi(cons_2) = [1, 2] pi(app) = [1, 2] pi(append_0) = [] pi(append_1) = [1] pi(append_2) = [1, 2] pi(cons_0) = [] pi(cons_1) = [1] pi(flatwith_0) = [] pi(flatwith_1) = [1] pi(flatwith_2) = [1, 2] pi(flatwithsub_0) = [] pi(flatwithsub_1) = [1] pi(flatwithsub_2) = [1, 2] pi(leaf_0) = [] pi(leaf_1) = [1] pi(node_0) = [] pi(node_1) = [1] pi(nil_0) = [] The following rules are removed: p1 Then no dependency pair remains.