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, r3, r5, r6, r8, r10, r11 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: app#_A(x1,x2) = x1 + x2 + 3 dropWhile_1_A(x1) = x1 + 2 dropWhile_2#_A(x1,x2) = x1 + x2 + 3 cons_2_A(x1,x2) = x1 + x2 + 2 takeWhile_1_A(x1) = x1 + 2 takeWhile_2#_A(x1,x2) = x1 + x2 + 3 app_A(x1,x2) = x2 + 6 cons_0_A() = 2 cons_1_A(x1) = 1 dropWhile_0_A() = 1 if_0_A() = 3 if_1_A(x1) = 2 if_2_A(x1,x2) = 1 takeWhile_0_A() = 1 if_3_A(x1,x2,x3) = x1 + x2 + x3 + 7 true_0_A() = 1 base order 2: precedence: dropWhile_2# = takeWhile_2# = if_3 > app# = app = cons_0 = if_0 = true_0 > dropWhile_1 = cons_2 = if_1 > takeWhile_1 = cons_1 = dropWhile_0 = if_2 > takeWhile_0 partial status: pi(app#) = [] pi(dropWhile_1) = [1] pi(dropWhile_2#) = [] pi(cons_2) = [1] pi(takeWhile_1) = [1] pi(takeWhile_2#) = [1] pi(app) = [] pi(cons_0) = [] pi(cons_1) = [] pi(dropWhile_0) = [] pi(if_0) = [] pi(if_1) = [] pi(if_2) = [] pi(takeWhile_0) = [] pi(if_3) = [] pi(true_0) = [] The following rules are removed: p1 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: dropWhile_2#(p,cons_2(x,xs)) -> dropWhile_2#(p,xs) p2: dropWhile_2#(p,cons_2(x,xs)) -> app#(p,x) 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: {p1} {p3, p4, p5} -- 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, r10, r11 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: dropWhile_2#_A(x1,x2) = x2 cons_2_A(x1,x2) = x1 + x2 + 4 app_A(x1,x2) = x2 + 3 cons_0_A() = 2 cons_1_A(x1) = 1 dropWhile_0_A() = 3 dropWhile_1_A(x1) = 2 if_0_A() = 3 if_1_A(x1) = 2 if_2_A(x1,x2) = 1 takeWhile_0_A() = 2 takeWhile_1_A(x1) = 1 if_3_A(x1,x2,x3) = x1 + x2 + x3 + 4 true_0_A() = 1 base order 2: precedence: if_3 > cons_2 > app = dropWhile_0 = if_0 = takeWhile_0 > dropWhile_2# = cons_1 = dropWhile_1 = if_1 = takeWhile_1 = true_0 > cons_0 = if_2 partial status: pi(dropWhile_2#) = [] pi(cons_2) = [1] pi(app) = [2] 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) = [1] 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: app#(takeWhile_1(x1),y) -> takeWhile_2#(x1,y) p2: takeWhile_2#(p,cons_2(x,xs)) -> app#(p,x) 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, r6, r8 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: app#_A(x1,x2) = x2 takeWhile_1_A(x1) = 5 takeWhile_2#_A(x1,x2) = x2 cons_2_A(x1,x2) = x1 + x2 app_A(x1,x2) = 6 cons_0_A() = 2 cons_1_A(x1) = 1 dropWhile_0_A() = 2 dropWhile_1_A(x1) = 1 if_0_A() = 3 if_1_A(x1) = 2 if_2_A(x1,x2) = 1 takeWhile_0_A() = 6 base order 2: precedence: app = dropWhile_1 > dropWhile_0 > if_0 > cons_2 = cons_0 = if_1 > app# = cons_1 = if_2 > takeWhile_2# = takeWhile_0 > takeWhile_1 partial status: pi(app#) = [2] pi(takeWhile_1) = [] pi(takeWhile_2#) = [2] pi(cons_2) = [1, 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) = [] The following rules are removed: p3 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: app#(takeWhile_1(x1),y) -> takeWhile_2#(x1,y) p2: 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: {p1, p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: app#(takeWhile_1(x1),y) -> takeWhile_2#(x1,y) p2: 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, r2, r3, r5, r6, r7, r8, r10, r11 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: app#_A(x1,x2) = x2 + 4 takeWhile_1_A(x1) = x1 + 2 takeWhile_2#_A(x1,x2) = x2 + 3 cons_2_A(x1,x2) = x1 + x2 + 5 app_A(x1,x2) = x1 + x2 + 6 cons_0_A() = 1 cons_1_A(x1) = x1 + 2 dropWhile_0_A() = 1 dropWhile_1_A(x1) = x1 + 2 if_0_A() = 1 if_1_A(x1) = x1 + 2 if_2_A(x1,x2) = x1 + x2 + 3 if_3_A(x1,x2,x3) = x1 + x2 + x3 + 4 takeWhile_0_A() = 1 true_0_A() = 1 base order 2: precedence: if_3 > app > takeWhile_2# > app# = takeWhile_1 = cons_2 = dropWhile_1 = if_2 = true_0 > cons_1 = dropWhile_0 = if_1 = takeWhile_0 > cons_0 = if_0 partial status: pi(app#) = [] pi(takeWhile_1) = [1] pi(takeWhile_2#) = [2] pi(cons_2) = [2] pi(app) = [1] pi(cons_0) = [] pi(cons_1) = [1] pi(dropWhile_0) = [] pi(dropWhile_1) = [1] pi(if_0) = [] pi(if_1) = [1] pi(if_2) = [2] pi(if_3) = [] pi(takeWhile_0) = [] pi(true_0) = [] The following rules are removed: p1 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: 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: (no SCCs)