YES We show the termination of the TRS R: app(app(app(if(),true()),x),y) -> x app(app(app(if(),true()),x),y) -> y app(app(takeWhile(),p),nil()) -> nil() app(app(takeWhile(),p),app(app(cons(),x),xs)) -> app(app(app(if(),app(p,x)),app(app(cons(),x),app(app(takeWhile(),p),xs))),nil()) app(app(dropWhile(),p),nil()) -> nil() app(app(dropWhile(),p),app(app(cons(),x),xs)) -> app(app(app(if(),app(p,x)),app(app(dropWhile(),p),xs)),app(app(cons(),x),xs)) Instead we prove termination of the uncurried system: app(cons_0(),y) -> cons_1(y) app(cons_1(x1),y) -> cons_2(x1,y) app(dropWhile_0(),y) -> dropWhile_1(y) app(dropWhile_1(x1),y) -> dropWhile_2(x1,y) app(if_0(),y) -> if_1(y) app(if_1(x1),y) -> if_2(x1,y) app(if_2(x1,x2),y) -> if_3(x1,x2,y) app(takeWhile_0(),y) -> takeWhile_1(y) app(takeWhile_1(x1),y) -> takeWhile_2(x1,y) if_3(true_0(),x,y) -> x if_3(true_0(),x,y) -> y takeWhile_2(p,nil_0()) -> nil_0() takeWhile_2(p,cons_2(x,xs)) -> if_3(app(p,x),cons_2(x,takeWhile_2(p,xs)),nil_0()) dropWhile_2(p,nil_0()) -> nil_0() dropWhile_2(p,cons_2(x,xs)) -> if_3(app(p,x),dropWhile_2(p,xs),cons_2(x,xs)) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: app#(dropWhile_1(x1),y) -> dropWhile_2#(x1,y) p2: app#(if_2(x1,x2),y) -> if_3#(x1,x2,y) p3: app#(takeWhile_1(x1),y) -> takeWhile_2#(x1,y) p4: takeWhile_2#(p,cons_2(x,xs)) -> if_3#(app(p,x),cons_2(x,takeWhile_2(p,xs)),nil_0()) p5: takeWhile_2#(p,cons_2(x,xs)) -> app#(p,x) p6: takeWhile_2#(p,cons_2(x,xs)) -> takeWhile_2#(p,xs) p7: dropWhile_2#(p,cons_2(x,xs)) -> if_3#(app(p,x),dropWhile_2(p,xs),cons_2(x,xs)) p8: dropWhile_2#(p,cons_2(x,xs)) -> app#(p,x) p9: dropWhile_2#(p,cons_2(x,xs)) -> dropWhile_2#(p,xs) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(dropWhile_0(),y) -> dropWhile_1(y) r4: app(dropWhile_1(x1),y) -> dropWhile_2(x1,y) r5: app(if_0(),y) -> if_1(y) r6: app(if_1(x1),y) -> if_2(x1,y) r7: app(if_2(x1,x2),y) -> if_3(x1,x2,y) r8: app(takeWhile_0(),y) -> takeWhile_1(y) r9: app(takeWhile_1(x1),y) -> takeWhile_2(x1,y) r10: if_3(true_0(),x,y) -> x r11: if_3(true_0(),x,y) -> y r12: takeWhile_2(p,nil_0()) -> nil_0() r13: takeWhile_2(p,cons_2(x,xs)) -> if_3(app(p,x),cons_2(x,takeWhile_2(p,xs)),nil_0()) r14: dropWhile_2(p,nil_0()) -> nil_0() r15: dropWhile_2(p,cons_2(x,xs)) -> if_3(app(p,x),dropWhile_2(p,xs),cons_2(x,xs)) The estimated dependency graph contains the following SCCs: {p1, p3, p5, p6, p8, p9} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: app#(dropWhile_1(x1),y) -> dropWhile_2#(x1,y) p2: dropWhile_2#(p,cons_2(x,xs)) -> dropWhile_2#(p,xs) p3: dropWhile_2#(p,cons_2(x,xs)) -> app#(p,x) p4: app#(takeWhile_1(x1),y) -> takeWhile_2#(x1,y) p5: takeWhile_2#(p,cons_2(x,xs)) -> takeWhile_2#(p,xs) p6: takeWhile_2#(p,cons_2(x,xs)) -> app#(p,x) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(dropWhile_0(),y) -> dropWhile_1(y) r4: app(dropWhile_1(x1),y) -> dropWhile_2(x1,y) r5: app(if_0(),y) -> if_1(y) r6: app(if_1(x1),y) -> if_2(x1,y) r7: app(if_2(x1,x2),y) -> if_3(x1,x2,y) r8: app(takeWhile_0(),y) -> takeWhile_1(y) r9: app(takeWhile_1(x1),y) -> takeWhile_2(x1,y) r10: if_3(true_0(),x,y) -> x r11: if_3(true_0(),x,y) -> y r12: takeWhile_2(p,nil_0()) -> nil_0() r13: takeWhile_2(p,cons_2(x,xs)) -> if_3(app(p,x),cons_2(x,takeWhile_2(p,xs)),nil_0()) r14: dropWhile_2(p,nil_0()) -> nil_0() r15: dropWhile_2(p,cons_2(x,xs)) -> if_3(app(p,x),dropWhile_2(p,xs),cons_2(x,xs)) The set of usable rules consists of r1, r5, r6 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: app#_A(x1,x2) = x1 + 3 dropWhile_1_A(x1) = x1 + 5 dropWhile_2#_A(x1,x2) = x1 + 4 cons_2_A(x1,x2) = max{27, x1 + 25, x2 - 53} takeWhile_1_A(x1) = x1 + 9 takeWhile_2#_A(x1,x2) = x1 + 8 app_A(x1,x2) = max{51, x1 - 10, x2 - 30} cons_0_A = 9 cons_1_A(x1) = max{8, x1 - 31} if_0_A = 7 if_1_A(x1) = max{8, x1 - 31} if_2_A(x1,x2) = max{9, x1 - 42, x2 - 71} base order 2: precedence: app > dropWhile_1 > dropWhile_2# > cons_2 = takeWhile_1 = cons_0 = if_2 > takeWhile_2# = cons_1 = if_1 > app# = if_0 partial status: pi(app#) = [1] pi(dropWhile_1) = [1] pi(dropWhile_2#) = [1] pi(cons_2) = [1] pi(takeWhile_1) = [1] pi(takeWhile_2#) = [1] pi(app) = [] pi(cons_0) = [] pi(cons_1) = [] pi(if_0) = [] pi(if_1) = [] pi(if_2) = [] The following rules are removed: p3 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: app#(dropWhile_1(x1),y) -> dropWhile_2#(x1,y) p2: dropWhile_2#(p,cons_2(x,xs)) -> dropWhile_2#(p,xs) p3: app#(takeWhile_1(x1),y) -> takeWhile_2#(x1,y) p4: takeWhile_2#(p,cons_2(x,xs)) -> takeWhile_2#(p,xs) p5: takeWhile_2#(p,cons_2(x,xs)) -> app#(p,x) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(dropWhile_0(),y) -> dropWhile_1(y) r4: app(dropWhile_1(x1),y) -> dropWhile_2(x1,y) r5: app(if_0(),y) -> if_1(y) r6: app(if_1(x1),y) -> if_2(x1,y) r7: app(if_2(x1,x2),y) -> if_3(x1,x2,y) r8: app(takeWhile_0(),y) -> takeWhile_1(y) r9: app(takeWhile_1(x1),y) -> takeWhile_2(x1,y) r10: if_3(true_0(),x,y) -> x r11: if_3(true_0(),x,y) -> y r12: takeWhile_2(p,nil_0()) -> nil_0() r13: takeWhile_2(p,cons_2(x,xs)) -> if_3(app(p,x),cons_2(x,takeWhile_2(p,xs)),nil_0()) r14: dropWhile_2(p,nil_0()) -> nil_0() r15: dropWhile_2(p,cons_2(x,xs)) -> if_3(app(p,x),dropWhile_2(p,xs),cons_2(x,xs)) The estimated dependency graph contains the following SCCs: {p3, p4, p5} {p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: takeWhile_2#(p,cons_2(x,xs)) -> app#(p,x) p2: app#(takeWhile_1(x1),y) -> takeWhile_2#(x1,y) p3: takeWhile_2#(p,cons_2(x,xs)) -> takeWhile_2#(p,xs) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(dropWhile_0(),y) -> dropWhile_1(y) r4: app(dropWhile_1(x1),y) -> dropWhile_2(x1,y) r5: app(if_0(),y) -> if_1(y) r6: app(if_1(x1),y) -> if_2(x1,y) r7: app(if_2(x1,x2),y) -> if_3(x1,x2,y) r8: app(takeWhile_0(),y) -> takeWhile_1(y) r9: app(takeWhile_1(x1),y) -> takeWhile_2(x1,y) r10: if_3(true_0(),x,y) -> x r11: if_3(true_0(),x,y) -> y r12: takeWhile_2(p,nil_0()) -> nil_0() r13: takeWhile_2(p,cons_2(x,xs)) -> if_3(app(p,x),cons_2(x,takeWhile_2(p,xs)),nil_0()) r14: dropWhile_2(p,nil_0()) -> nil_0() r15: dropWhile_2(p,cons_2(x,xs)) -> if_3(app(p,x),dropWhile_2(p,xs),cons_2(x,xs)) The set of usable rules consists of r1, r3, r5 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: takeWhile_2#_A(x1,x2) = x1 + 6 cons_2_A(x1,x2) = max{4, x1 + 2, x2 - 19} app#_A(x1,x2) = max{5, x1 + 1} takeWhile_1_A(x1) = x1 + 6 app_A(x1,x2) = max{6, x1 - 8, x2 - 7} cons_0_A = 2 cons_1_A(x1) = max{3, x1 - 8} dropWhile_0_A = 1 dropWhile_1_A(x1) = max{2, x1 - 8} if_0_A = 4 if_1_A(x1) = max{5, x1 - 8} base order 2: precedence: app# = app > cons_2 = takeWhile_1 = dropWhile_1 > takeWhile_2# = cons_1 = dropWhile_0 = if_1 > cons_0 = if_0 partial status: pi(takeWhile_2#) = [1] pi(cons_2) = [1] pi(app#) = [1] pi(takeWhile_1) = [1] pi(app) = [] pi(cons_0) = [] pi(cons_1) = [] pi(dropWhile_0) = [] pi(dropWhile_1) = [] pi(if_0) = [] pi(if_1) = [] The following rules are removed: p2 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: takeWhile_2#(p,cons_2(x,xs)) -> app#(p,x) p2: takeWhile_2#(p,cons_2(x,xs)) -> takeWhile_2#(p,xs) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(dropWhile_0(),y) -> dropWhile_1(y) r4: app(dropWhile_1(x1),y) -> dropWhile_2(x1,y) r5: app(if_0(),y) -> if_1(y) r6: app(if_1(x1),y) -> if_2(x1,y) r7: app(if_2(x1,x2),y) -> if_3(x1,x2,y) r8: app(takeWhile_0(),y) -> takeWhile_1(y) r9: app(takeWhile_1(x1),y) -> takeWhile_2(x1,y) r10: if_3(true_0(),x,y) -> x r11: if_3(true_0(),x,y) -> y r12: takeWhile_2(p,nil_0()) -> nil_0() r13: takeWhile_2(p,cons_2(x,xs)) -> if_3(app(p,x),cons_2(x,takeWhile_2(p,xs)),nil_0()) r14: dropWhile_2(p,nil_0()) -> nil_0() r15: dropWhile_2(p,cons_2(x,xs)) -> if_3(app(p,x),dropWhile_2(p,xs),cons_2(x,xs)) The estimated dependency graph contains the following SCCs: {p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: takeWhile_2#(p,cons_2(x,xs)) -> takeWhile_2#(p,xs) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(dropWhile_0(),y) -> dropWhile_1(y) r4: app(dropWhile_1(x1),y) -> dropWhile_2(x1,y) r5: app(if_0(),y) -> if_1(y) r6: app(if_1(x1),y) -> if_2(x1,y) r7: app(if_2(x1,x2),y) -> if_3(x1,x2,y) r8: app(takeWhile_0(),y) -> takeWhile_1(y) r9: app(takeWhile_1(x1),y) -> takeWhile_2(x1,y) r10: if_3(true_0(),x,y) -> x r11: if_3(true_0(),x,y) -> y r12: takeWhile_2(p,nil_0()) -> nil_0() r13: takeWhile_2(p,cons_2(x,xs)) -> if_3(app(p,x),cons_2(x,takeWhile_2(p,xs)),nil_0()) r14: dropWhile_2(p,nil_0()) -> nil_0() r15: dropWhile_2(p,cons_2(x,xs)) -> if_3(app(p,x),dropWhile_2(p,xs),cons_2(x,xs)) The set of usable rules consists of r1, r3, r5, r6, r8, r11 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: takeWhile_2#_A(x1,x2) = max{25, x1 + 1, x2 + 6} cons_2_A(x1,x2) = max{19, x1 - 3, x2 + 5} app_A(x1,x2) = max{4, x1 - 27, x2 - 24} cons_0_A = 1 cons_1_A(x1) = max{2, x1 - 25} dropWhile_0_A = 28 dropWhile_1_A(x1) = max{3, x1 - 26} if_0_A = 1 if_1_A(x1) = max{2, x1 - 25} if_2_A(x1,x2) = max{3, x1 - 53, x2 - 29} takeWhile_0_A = 1 takeWhile_1_A(x1) = max{2, x1 - 27} if_3_A(x1,x2,x3) = max{21, x1 - 29, x2 - 28, x3 + 2} true_0_A = 0 base order 2: precedence: takeWhile_2# = if_3 > cons_2 > app = dropWhile_0 = true_0 > cons_1 = dropWhile_1 = if_2 = takeWhile_1 > cons_0 = if_1 = takeWhile_0 > if_0 partial status: pi(takeWhile_2#) = [2] pi(cons_2) = [2] pi(app) = [] pi(cons_0) = [] pi(cons_1) = [] pi(dropWhile_0) = [] pi(dropWhile_1) = [] pi(if_0) = [] pi(if_1) = [] pi(if_2) = [] pi(takeWhile_0) = [] pi(takeWhile_1) = [] pi(if_3) = [] pi(true_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: dropWhile_2#(p,cons_2(x,xs)) -> dropWhile_2#(p,xs) and R consists of: r1: app(cons_0(),y) -> cons_1(y) r2: app(cons_1(x1),y) -> cons_2(x1,y) r3: app(dropWhile_0(),y) -> dropWhile_1(y) r4: app(dropWhile_1(x1),y) -> dropWhile_2(x1,y) r5: app(if_0(),y) -> if_1(y) r6: app(if_1(x1),y) -> if_2(x1,y) r7: app(if_2(x1,x2),y) -> if_3(x1,x2,y) r8: app(takeWhile_0(),y) -> takeWhile_1(y) r9: app(takeWhile_1(x1),y) -> takeWhile_2(x1,y) r10: if_3(true_0(),x,y) -> x r11: if_3(true_0(),x,y) -> y r12: takeWhile_2(p,nil_0()) -> nil_0() r13: takeWhile_2(p,cons_2(x,xs)) -> if_3(app(p,x),cons_2(x,takeWhile_2(p,xs)),nil_0()) r14: dropWhile_2(p,nil_0()) -> nil_0() r15: dropWhile_2(p,cons_2(x,xs)) -> if_3(app(p,x),dropWhile_2(p,xs),cons_2(x,xs)) The set of usable rules consists of r1, r3, r5, r6, r8, r11 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: max/plus interpretation on natural numbers: dropWhile_2#_A(x1,x2) = max{16, x1 + 1, x2 + 9} cons_2_A(x1,x2) = max{7, x1 - 8, x2 + 1} app_A(x1,x2) = max{21, x1 - 4, x2 - 4} cons_0_A = 2 cons_1_A(x1) = max{3, x1 - 9} dropWhile_0_A = 3 dropWhile_1_A(x1) = max{0, x1 - 5} if_0_A = 1 if_1_A(x1) = max{2, x1 - 5} if_2_A(x1,x2) = max{3, x1 - 23, x2 - 19} takeWhile_0_A = 2 takeWhile_1_A(x1) = max{3, x1 - 5} if_3_A(x1,x2,x3) = max{9, x1 - 22, x2 - 18, x3 + 2} true_0_A = 0 base order 2: precedence: if_3 > dropWhile_2# = app > cons_2 = if_2 = true_0 > cons_1 = dropWhile_1 = if_1 = takeWhile_1 > cons_0 = dropWhile_0 = if_0 = takeWhile_0 partial status: pi(dropWhile_2#) = [2] pi(cons_2) = [] pi(app) = [] pi(cons_0) = [] pi(cons_1) = [] pi(dropWhile_0) = [] pi(dropWhile_1) = [] pi(if_0) = [] pi(if_1) = [] pi(if_2) = [] pi(takeWhile_0) = [] pi(takeWhile_1) = [] pi(if_3) = [3] pi(true_0) = [] The following rules are removed: p1 Then no dependency pair remains.