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!): max/plus interpretation on natural numbers: app#_A(x1,x2) = max{0, x1 - 27, x2 - 13} dropWhile_1_A(x1) = x1 + 26 dropWhile_2#_A(x1,x2) = max{0, x1 - 27, x2 - 18} cons_2_A(x1,x2) = max{x1 + 5, x2 + 17} takeWhile_1_A(x1) = x1 + 1 takeWhile_2#_A(x1,x2) = max{0, x1 - 27, x2 - 18} app#!_A(x1,x2) = max{8, x1 - 55, x2 - 20} dropWhile_1!_A(x1) = max{7, x1 - 7} dropWhile_2#!_A(x1,x2) = max{8, x1 - 29, x2 - 20} cons_2!_A(x1,x2) = max{2, x1 - 23, x2 - 21} takeWhile_1!_A(x1) = max{2, x1 - 53} takeWhile_2#!_A(x1,x2) = max{8, x1 - 54, x2 - 20} 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: app#_A(x1,x2) = max{0, x1 - 2, x2 - 7} dropWhile_1_A(x1) = max{1, x1} dropWhile_2#_A(x1,x2) = max{0, x1 - 2, x2 - 7} cons_2_A(x1,x2) = max{x1 + 6, x2 + 3} takeWhile_1_A(x1) = max{1, x1} takeWhile_2#_A(x1,x2) = max{0, x1 - 2, x2 - 7} app#!_A(x1,x2) = max{9, x1 - 2, x2 - 12} dropWhile_1!_A(x1) = max{8, x1 - 4} dropWhile_2#!_A(x1,x2) = max{9, x1 - 2, x2 - 15} cons_2!_A(x1,x2) = max{3, x1 - 13, x2 - 15} takeWhile_1!_A(x1) = max{2, x1 - 28} takeWhile_2#!_A(x1,x2) = max{9, x1 - 2, x2 - 16} partial status: pi(app#) = [1] pi(dropWhile_1) = [1] pi(dropWhile_2#) = [1] pi(cons_2) = [2] pi(takeWhile_1) = [1] pi(takeWhile_2#) = [1] 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 (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!): max/plus interpretation on natural numbers: dropWhile_2#_A(x1,x2) = 0 cons_2_A(x1,x2) = max{4, x1 - 3, x2 - 13} dropWhile_2#!_A(x1,x2) = max{0, x1 - 1} cons_2!_A(x1,x2) = max{0, x1 - 41, x2 - 43} 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: dropWhile_2#_A(x1,x2) = x2 cons_2_A(x1,x2) = max{x1 - 25, x2 + 3} dropWhile_2#!_A(x1,x2) = max{5, x1 - 1, x2 - 11} cons_2!_A(x1,x2) = max{4, x2 - 12} partial status: pi(dropWhile_2#) = [2] pi(cons_2) = [2] 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 (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!): max/plus interpretation on natural numbers: app#_A(x1,x2) = max{0, x1 - 8, x2 - 11} takeWhile_1_A(x1) = x1 + 7 takeWhile_2#_A(x1,x2) = max{0, x1 - 8, x2 - 13} cons_2_A(x1,x2) = max{x1 + 2, x2 + 12} app#!_A(x1,x2) = max{6, x1 - 53, x2 - 12} takeWhile_1!_A(x1) = max{5, x1 - 52} takeWhile_2#!_A(x1,x2) = max{6, x1 - 53, x2 - 13} cons_2!_A(x1,x2) = max{2, x1 - 16, x2 - 22} 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: app#_A(x1,x2) = max{0, x1 - 7, x2 - 9} takeWhile_1_A(x1) = x1 + 6 takeWhile_2#_A(x1,x2) = max{0, x1 - 7, x2 - 9} cons_2_A(x1,x2) = max{x1 + 8, x2} app#!_A(x1,x2) = max{1, x1 - 2, x2 - 18} takeWhile_1!_A(x1) = max{1, x1 - 40} takeWhile_2#!_A(x1,x2) = max{3, x1 - 1, x2 - 25} cons_2!_A(x1,x2) = max{2, x1 - 18, x2 - 29} partial status: pi(app#) = [] pi(takeWhile_1) = [1] pi(takeWhile_2#) = [] pi(cons_2) = [2] The following rules are removed: p1, p2 -- SCC decomposition. 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 estimated dependency graph contains the following SCCs: {p1} -- 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 (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!): max/plus interpretation on natural numbers: takeWhile_2#_A(x1,x2) = 0 cons_2_A(x1,x2) = max{3, x1 - 30, x2 - 101} takeWhile_2#!_A(x1,x2) = max{3, x1 - 1} cons_2!_A(x1,x2) = max{2, x1 - 79, x2 - 94} 2. marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: takeWhile_2#_A(x1,x2) = x2 cons_2_A(x1,x2) = max{3, x1 - 3, x2} takeWhile_2#!_A(x1,x2) = max{6, x1 - 1, x2 - 4} cons_2!_A(x1,x2) = max{5, x1 - 18, x2 - 58} partial status: pi(takeWhile_2#) = [2] pi(cons_2) = [2] The following rules are removed: p1 Then no dependency pair remains.