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 (no rules) 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: lexicographic combination of reduction triples: 1. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: app#_A(x1,x2) = x1 + x2 dropWhile_1_A(x1) = x1 + 2 dropWhile_2#_A(x1,x2) = x1 + x2 cons_2_A(x1,x2) = x1 + x2 + 2 takeWhile_1_A(x1) = x1 + 2 takeWhile_2#_A(x1,x2) = x1 + x2 app#!_A(x1,x2) = x2 + 3 dropWhile_1!_A(x1) = 4 dropWhile_2#!_A(x1,x2) = x2 + 3 cons_2!_A(x1,x2) = x1 + 7 takeWhile_1!_A(x1) = 1 takeWhile_2#!_A(x1,x2) = x2 + 2 2. marked-algebra reduction triple (>=A, >=A!, >A!): matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: app#_A(x1,x2) = x1 + x2 dropWhile_1_A(x1) = x1 + 3 dropWhile_2#_A(x1,x2) = x1 + x2 cons_2_A(x1,x2) = x1 + x2 + 6 takeWhile_1_A(x1) = x1 takeWhile_2#_A(x1,x2) = x1 + x2 app#!_A(x1,x2) = x2 + 5 dropWhile_1!_A(x1) = 4 dropWhile_2#!_A(x1,x2) = x2 + 5 cons_2!_A(x1,x2) = x1 + 6 takeWhile_1!_A(x1) = 1 takeWhile_2#!_A(x1,x2) = x2 partial status: pi(app#) = [2] pi(dropWhile_1) = [1] pi(dropWhile_2#) = [2] pi(cons_2) = [1, 2] pi(takeWhile_1) = [] pi(takeWhile_2#) = [2] The following rules are removed: p2, p3, p4, p5, p6 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: app#(dropWhile_1(x1),y) -> dropWhile_2#(x1,y) 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)