YES Problem: 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)) Proof: Uncurry Processor: if3(true(),x,y) -> x if3(true(),x,y) -> y takeWhile2(p,nil()) -> nil() takeWhile2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,takeWhile2(p,xs)),nil()) dropWhile2(p,nil()) -> nil() dropWhile2(p,cons2(x,xs)) -> if3(app(p,x),dropWhile2(p,xs),cons2(x,xs)) app(if2(x5,x4),x6) -> if3(x5,x4,x6) app(if1(x5),x6) -> if2(x5,x6) app(if(),x6) -> if1(x6) app(takeWhile1(x5),x6) -> takeWhile2(x5,x6) app(takeWhile(),x6) -> takeWhile1(x6) app(cons1(x5),x6) -> cons2(x5,x6) app(cons(),x6) -> cons1(x6) app(dropWhile1(x5),x6) -> dropWhile2(x5,x6) app(dropWhile(),x6) -> dropWhile1(x6) DP Processor: DPs: takeWhile{2,#}(p,cons2(x,xs)) -> takeWhile{2,#}(p,xs) takeWhile{2,#}(p,cons2(x,xs)) -> app#(p,x) takeWhile{2,#}(p,cons2(x,xs)) -> if{3,#}(app(p,x),cons2(x,takeWhile2(p,xs)),nil()) dropWhile{2,#}(p,cons2(x,xs)) -> dropWhile{2,#}(p,xs) dropWhile{2,#}(p,cons2(x,xs)) -> app#(p,x) dropWhile{2,#}(p,cons2(x,xs)) -> if{3,#}(app(p,x),dropWhile2(p,xs),cons2(x,xs)) app#(if2(x5,x4),x6) -> if{3,#}(x5,x4,x6) app#(takeWhile1(x5),x6) -> takeWhile{2,#}(x5,x6) app#(dropWhile1(x5),x6) -> dropWhile{2,#}(x5,x6) TRS: if3(true(),x,y) -> x if3(true(),x,y) -> y takeWhile2(p,nil()) -> nil() takeWhile2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,takeWhile2(p,xs)),nil()) dropWhile2(p,nil()) -> nil() dropWhile2(p,cons2(x,xs)) -> if3(app(p,x),dropWhile2(p,xs),cons2(x,xs)) app(if2(x5,x4),x6) -> if3(x5,x4,x6) app(if1(x5),x6) -> if2(x5,x6) app(if(),x6) -> if1(x6) app(takeWhile1(x5),x6) -> takeWhile2(x5,x6) app(takeWhile(),x6) -> takeWhile1(x6) app(cons1(x5),x6) -> cons2(x5,x6) app(cons(),x6) -> cons1(x6) app(dropWhile1(x5),x6) -> dropWhile2(x5,x6) app(dropWhile(),x6) -> dropWhile1(x6) TDG Processor: DPs: takeWhile{2,#}(p,cons2(x,xs)) -> takeWhile{2,#}(p,xs) takeWhile{2,#}(p,cons2(x,xs)) -> app#(p,x) takeWhile{2,#}(p,cons2(x,xs)) -> if{3,#}(app(p,x),cons2(x,takeWhile2(p,xs)),nil()) dropWhile{2,#}(p,cons2(x,xs)) -> dropWhile{2,#}(p,xs) dropWhile{2,#}(p,cons2(x,xs)) -> app#(p,x) dropWhile{2,#}(p,cons2(x,xs)) -> if{3,#}(app(p,x),dropWhile2(p,xs),cons2(x,xs)) app#(if2(x5,x4),x6) -> if{3,#}(x5,x4,x6) app#(takeWhile1(x5),x6) -> takeWhile{2,#}(x5,x6) app#(dropWhile1(x5),x6) -> dropWhile{2,#}(x5,x6) TRS: if3(true(),x,y) -> x if3(true(),x,y) -> y takeWhile2(p,nil()) -> nil() takeWhile2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,takeWhile2(p,xs)),nil()) dropWhile2(p,nil()) -> nil() dropWhile2(p,cons2(x,xs)) -> if3(app(p,x),dropWhile2(p,xs),cons2(x,xs)) app(if2(x5,x4),x6) -> if3(x5,x4,x6) app(if1(x5),x6) -> if2(x5,x6) app(if(),x6) -> if1(x6) app(takeWhile1(x5),x6) -> takeWhile2(x5,x6) app(takeWhile(),x6) -> takeWhile1(x6) app(cons1(x5),x6) -> cons2(x5,x6) app(cons(),x6) -> cons1(x6) app(dropWhile1(x5),x6) -> dropWhile2(x5,x6) app(dropWhile(),x6) -> dropWhile1(x6) graph: dropWhile{2,#}(p,cons2(x,xs)) -> dropWhile{2,#}(p,xs) -> dropWhile{2,#}(p,cons2(x,xs)) -> if{3,#}(app(p,x),dropWhile2(p,xs),cons2(x,xs)) dropWhile{2,#}(p,cons2(x,xs)) -> dropWhile{2,#}(p,xs) -> dropWhile{2,#}(p,cons2(x,xs)) -> app#(p,x) dropWhile{2,#}(p,cons2(x,xs)) -> dropWhile{2,#}(p,xs) -> dropWhile{2,#}(p,cons2(x,xs)) -> dropWhile{2,#}(p,xs) dropWhile{2,#}(p,cons2(x,xs)) -> app#(p,x) -> app#(dropWhile1(x5),x6) -> dropWhile{2,#}(x5,x6) dropWhile{2,#}(p,cons2(x,xs)) -> app#(p,x) -> app#(takeWhile1(x5),x6) -> takeWhile{2,#}(x5,x6) dropWhile{2,#}(p,cons2(x,xs)) -> app#(p,x) -> app#(if2(x5,x4),x6) -> if{3,#}(x5,x4,x6) app#(dropWhile1(x5),x6) -> dropWhile{2,#}(x5,x6) -> dropWhile{2,#}(p,cons2(x,xs)) -> if{3,#}(app(p,x),dropWhile2(p,xs),cons2(x,xs)) app#(dropWhile1(x5),x6) -> dropWhile{2,#}(x5,x6) -> dropWhile{2,#}(p,cons2(x,xs)) -> app#(p,x) app#(dropWhile1(x5),x6) -> dropWhile{2,#}(x5,x6) -> dropWhile{2,#}(p,cons2(x,xs)) -> dropWhile{2,#}(p,xs) app#(takeWhile1(x5),x6) -> takeWhile{2,#}(x5,x6) -> takeWhile{2,#}(p,cons2(x,xs)) -> if{3,#}(app(p,x),cons2(x,takeWhile2(p,xs)),nil()) app#(takeWhile1(x5),x6) -> takeWhile{2,#}(x5,x6) -> takeWhile{2,#}(p,cons2(x,xs)) -> app#(p,x) app#(takeWhile1(x5),x6) -> takeWhile{2,#}(x5,x6) -> takeWhile{2,#}(p,cons2(x,xs)) -> takeWhile{2,#}(p,xs) takeWhile{2,#}(p,cons2(x,xs)) -> app#(p,x) -> app#(dropWhile1(x5),x6) -> dropWhile{2,#}(x5,x6) takeWhile{2,#}(p,cons2(x,xs)) -> app#(p,x) -> app#(takeWhile1(x5),x6) -> takeWhile{2,#}(x5,x6) takeWhile{2,#}(p,cons2(x,xs)) -> app#(p,x) -> app#(if2(x5,x4),x6) -> if{3,#}(x5,x4,x6) takeWhile{2,#}(p,cons2(x,xs)) -> takeWhile{2,#}(p,xs) -> takeWhile{2,#}(p,cons2(x,xs)) -> if{3,#}(app(p,x),cons2(x,takeWhile2(p,xs)),nil()) takeWhile{2,#}(p,cons2(x,xs)) -> takeWhile{2,#}(p,xs) -> takeWhile{2,#}(p,cons2(x,xs)) -> app#(p,x) takeWhile{2,#}(p,cons2(x,xs)) -> takeWhile{2,#}(p,xs) -> takeWhile{2,#}(p,cons2(x,xs)) -> takeWhile{2,#}(p,xs) SCC Processor: #sccs: 1 #rules: 6 #arcs: 18/81 DPs: dropWhile{2,#}(p,cons2(x,xs)) -> dropWhile{2,#}(p,xs) dropWhile{2,#}(p,cons2(x,xs)) -> app#(p,x) app#(takeWhile1(x5),x6) -> takeWhile{2,#}(x5,x6) takeWhile{2,#}(p,cons2(x,xs)) -> takeWhile{2,#}(p,xs) takeWhile{2,#}(p,cons2(x,xs)) -> app#(p,x) app#(dropWhile1(x5),x6) -> dropWhile{2,#}(x5,x6) TRS: if3(true(),x,y) -> x if3(true(),x,y) -> y takeWhile2(p,nil()) -> nil() takeWhile2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,takeWhile2(p,xs)),nil()) dropWhile2(p,nil()) -> nil() dropWhile2(p,cons2(x,xs)) -> if3(app(p,x),dropWhile2(p,xs),cons2(x,xs)) app(if2(x5,x4),x6) -> if3(x5,x4,x6) app(if1(x5),x6) -> if2(x5,x6) app(if(),x6) -> if1(x6) app(takeWhile1(x5),x6) -> takeWhile2(x5,x6) app(takeWhile(),x6) -> takeWhile1(x6) app(cons1(x5),x6) -> cons2(x5,x6) app(cons(),x6) -> cons1(x6) app(dropWhile1(x5),x6) -> dropWhile2(x5,x6) app(dropWhile(),x6) -> dropWhile1(x6) Subterm Criterion Processor: simple projection: pi(takeWhile{2,#}) = 1 pi(app#) = 1 pi(dropWhile{2,#}) = 1 problem: DPs: app#(takeWhile1(x5),x6) -> takeWhile{2,#}(x5,x6) app#(dropWhile1(x5),x6) -> dropWhile{2,#}(x5,x6) TRS: if3(true(),x,y) -> x if3(true(),x,y) -> y takeWhile2(p,nil()) -> nil() takeWhile2(p,cons2(x,xs)) -> if3(app(p,x),cons2(x,takeWhile2(p,xs)),nil()) dropWhile2(p,nil()) -> nil() dropWhile2(p,cons2(x,xs)) -> if3(app(p,x),dropWhile2(p,xs),cons2(x,xs)) app(if2(x5,x4),x6) -> if3(x5,x4,x6) app(if1(x5),x6) -> if2(x5,x6) app(if(),x6) -> if1(x6) app(takeWhile1(x5),x6) -> takeWhile2(x5,x6) app(takeWhile(),x6) -> takeWhile1(x6) app(cons1(x5),x6) -> cons2(x5,x6) app(cons(),x6) -> cons1(x6) app(dropWhile1(x5),x6) -> dropWhile2(x5,x6) app(dropWhile(),x6) -> dropWhile1(x6) SCC Processor: #sccs: 0 #rules: 0 #arcs: 12/4