YES Problem: app(f(),app(f(),x)) -> app(g(),app(f(),x)) app(g(),app(g(),x)) -> app(f(),x) app(app(map(),fun),nil()) -> nil() app(app(map(),fun),app(app(cons(),x),xs)) -> app(app(cons(),app(fun,x)),app(app(map(),fun),xs)) app(app(filter(),fun),nil()) -> nil() app(app(filter(),fun),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(fun,x)),fun),x),xs) app(app(app(app(filter2(),true()),fun),x),xs) -> app(app(cons(),x),app(app(filter(),fun),xs)) app(app(app(app(filter2(),false()),fun),x),xs) -> app(app(filter(),fun),xs) Proof: Uncurry Processor: f1(f1(x)) -> g1(f1(x)) g1(g1(x)) -> f1(x) map2(fun,nil()) -> nil() map2(fun,cons2(x,xs)) -> cons2(app(fun,x),map2(fun,xs)) filter2(fun,nil()) -> nil() filter2(fun,cons2(x,xs)) -> filter24(app(fun,x),fun,x,xs) filter24(true(),fun,x,xs) -> cons2(x,filter2(fun,xs)) filter24(false(),fun,x,xs) -> filter2(fun,xs) app(f(),x6) -> f1(x6) app(g(),x6) -> g1(x6) app(map1(x5),x6) -> map2(x5,x6) app(map(),x6) -> map1(x6) app(cons1(x5),x6) -> cons2(x5,x6) app(cons(),x6) -> cons1(x6) app(filter1(x5),x6) -> filter2(x5,x6) app(filter(),x6) -> filter1(x6) app(filter23(x5,x4,x3),x6) -> filter24(x5,x4,x3,x6) app(filter22(x5,x4),x6) -> filter23(x5,x4,x6) app(filter21(x5),x6) -> filter22(x5,x6) app(filter2(),x6) -> filter21(x6) DP Processor: DPs: f{1,#}(f1(x)) -> g{1,#}(f1(x)) g{1,#}(g1(x)) -> f{1,#}(x) map{2,#}(fun,cons2(x,xs)) -> map{2,#}(fun,xs) map{2,#}(fun,cons2(x,xs)) -> app#(fun,x) filter{2,#}(fun,cons2(x,xs)) -> app#(fun,x) filter{2,#}(fun,cons2(x,xs)) -> filter2{4,#}(app(fun,x),fun,x,xs) filter2{4,#}(true(),fun,x,xs) -> filter{2,#}(fun,xs) filter2{4,#}(false(),fun,x,xs) -> filter{2,#}(fun,xs) app#(f(),x6) -> f{1,#}(x6) app#(g(),x6) -> g{1,#}(x6) app#(map1(x5),x6) -> map{2,#}(x5,x6) app#(filter1(x5),x6) -> filter{2,#}(x5,x6) app#(filter23(x5,x4,x3),x6) -> filter2{4,#}(x5,x4,x3,x6) TRS: f1(f1(x)) -> g1(f1(x)) g1(g1(x)) -> f1(x) map2(fun,nil()) -> nil() map2(fun,cons2(x,xs)) -> cons2(app(fun,x),map2(fun,xs)) filter2(fun,nil()) -> nil() filter2(fun,cons2(x,xs)) -> filter24(app(fun,x),fun,x,xs) filter24(true(),fun,x,xs) -> cons2(x,filter2(fun,xs)) filter24(false(),fun,x,xs) -> filter2(fun,xs) app(f(),x6) -> f1(x6) app(g(),x6) -> g1(x6) app(map1(x5),x6) -> map2(x5,x6) app(map(),x6) -> map1(x6) app(cons1(x5),x6) -> cons2(x5,x6) app(cons(),x6) -> cons1(x6) app(filter1(x5),x6) -> filter2(x5,x6) app(filter(),x6) -> filter1(x6) app(filter23(x5,x4,x3),x6) -> filter24(x5,x4,x3,x6) app(filter22(x5,x4),x6) -> filter23(x5,x4,x6) app(filter21(x5),x6) -> filter22(x5,x6) app(filter2(),x6) -> filter21(x6) TDG Processor: DPs: f{1,#}(f1(x)) -> g{1,#}(f1(x)) g{1,#}(g1(x)) -> f{1,#}(x) map{2,#}(fun,cons2(x,xs)) -> map{2,#}(fun,xs) map{2,#}(fun,cons2(x,xs)) -> app#(fun,x) filter{2,#}(fun,cons2(x,xs)) -> app#(fun,x) filter{2,#}(fun,cons2(x,xs)) -> filter2{4,#}(app(fun,x),fun,x,xs) filter2{4,#}(true(),fun,x,xs) -> filter{2,#}(fun,xs) filter2{4,#}(false(),fun,x,xs) -> filter{2,#}(fun,xs) app#(f(),x6) -> f{1,#}(x6) app#(g(),x6) -> g{1,#}(x6) app#(map1(x5),x6) -> map{2,#}(x5,x6) app#(filter1(x5),x6) -> filter{2,#}(x5,x6) app#(filter23(x5,x4,x3),x6) -> filter2{4,#}(x5,x4,x3,x6) TRS: f1(f1(x)) -> g1(f1(x)) g1(g1(x)) -> f1(x) map2(fun,nil()) -> nil() map2(fun,cons2(x,xs)) -> cons2(app(fun,x),map2(fun,xs)) filter2(fun,nil()) -> nil() filter2(fun,cons2(x,xs)) -> filter24(app(fun,x),fun,x,xs) filter24(true(),fun,x,xs) -> cons2(x,filter2(fun,xs)) filter24(false(),fun,x,xs) -> filter2(fun,xs) app(f(),x6) -> f1(x6) app(g(),x6) -> g1(x6) app(map1(x5),x6) -> map2(x5,x6) app(map(),x6) -> map1(x6) app(cons1(x5),x6) -> cons2(x5,x6) app(cons(),x6) -> cons1(x6) app(filter1(x5),x6) -> filter2(x5,x6) app(filter(),x6) -> filter1(x6) app(filter23(x5,x4,x3),x6) -> filter24(x5,x4,x3,x6) app(filter22(x5,x4),x6) -> filter23(x5,x4,x6) app(filter21(x5),x6) -> filter22(x5,x6) app(filter2(),x6) -> filter21(x6) graph: filter2{4,#}(false(),fun,x,xs) -> filter{2,#}(fun,xs) -> filter{2,#}(fun,cons2(x,xs)) -> filter2{4,#}(app(fun,x),fun,x,xs) filter2{4,#}(false(),fun,x,xs) -> filter{2,#}(fun,xs) -> filter{2,#}(fun,cons2(x,xs)) -> app#(fun,x) filter2{4,#}(true(),fun,x,xs) -> filter{2,#}(fun,xs) -> filter{2,#}(fun,cons2(x,xs)) -> filter2{4,#}(app(fun,x),fun,x,xs) filter2{4,#}(true(),fun,x,xs) -> filter{2,#}(fun,xs) -> filter{2,#}(fun,cons2(x,xs)) -> app#(fun,x) filter{2,#}(fun,cons2(x,xs)) -> filter2{4,#}(app(fun,x),fun,x,xs) -> filter2{4,#}(false(),fun,x,xs) -> filter{2,#}(fun,xs) filter{2,#}(fun,cons2(x,xs)) -> filter2{4,#}(app(fun,x),fun,x,xs) -> filter2{4,#}(true(),fun,x,xs) -> filter{2,#}(fun,xs) filter{2,#}(fun,cons2(x,xs)) -> app#(fun,x) -> app#(filter23(x5,x4,x3),x6) -> filter2{4,#}(x5,x4,x3,x6) filter{2,#}(fun,cons2(x,xs)) -> app#(fun,x) -> app#(filter1(x5),x6) -> filter{2,#}(x5,x6) filter{2,#}(fun,cons2(x,xs)) -> app#(fun,x) -> app#(map1(x5),x6) -> map{2,#}(x5,x6) filter{2,#}(fun,cons2(x,xs)) -> app#(fun,x) -> app#(g(),x6) -> g{1,#}(x6) filter{2,#}(fun,cons2(x,xs)) -> app#(fun,x) -> app#(f(),x6) -> f{1,#}(x6) app#(filter23(x5,x4,x3),x6) -> filter2{4,#}(x5,x4,x3,x6) -> filter2{4,#}(false(),fun,x,xs) -> filter{2,#}(fun,xs) app#(filter23(x5,x4,x3),x6) -> filter2{4,#}(x5,x4,x3,x6) -> filter2{4,#}(true(),fun,x,xs) -> filter{2,#}(fun,xs) app#(filter1(x5),x6) -> filter{2,#}(x5,x6) -> filter{2,#}(fun,cons2(x,xs)) -> filter2{4,#}(app(fun,x),fun,x,xs) app#(filter1(x5),x6) -> filter{2,#}(x5,x6) -> filter{2,#}(fun,cons2(x,xs)) -> app#(fun,x) app#(map1(x5),x6) -> map{2,#}(x5,x6) -> map{2,#}(fun,cons2(x,xs)) -> app#(fun,x) app#(map1(x5),x6) -> map{2,#}(x5,x6) -> map{2,#}(fun,cons2(x,xs)) -> map{2,#}(fun,xs) app#(g(),x6) -> g{1,#}(x6) -> g{1,#}(g1(x)) -> f{1,#}(x) app#(f(),x6) -> f{1,#}(x6) -> f{1,#}(f1(x)) -> g{1,#}(f1(x)) map{2,#}(fun,cons2(x,xs)) -> app#(fun,x) -> app#(filter23(x5,x4,x3),x6) -> filter2{4,#}(x5,x4,x3,x6) map{2,#}(fun,cons2(x,xs)) -> app#(fun,x) -> app#(filter1(x5),x6) -> filter{2,#}(x5,x6) map{2,#}(fun,cons2(x,xs)) -> app#(fun,x) -> app#(map1(x5),x6) -> map{2,#}(x5,x6) map{2,#}(fun,cons2(x,xs)) -> app#(fun,x) -> app#(g(),x6) -> g{1,#}(x6) map{2,#}(fun,cons2(x,xs)) -> app#(fun,x) -> app#(f(),x6) -> f{1,#}(x6) map{2,#}(fun,cons2(x,xs)) -> map{2,#}(fun,xs) -> map{2,#}(fun,cons2(x,xs)) -> app#(fun,x) map{2,#}(fun,cons2(x,xs)) -> map{2,#}(fun,xs) -> map{2,#}(fun,cons2(x,xs)) -> map{2,#}(fun,xs) g{1,#}(g1(x)) -> f{1,#}(x) -> f{1,#}(f1(x)) -> g{1,#}(f1(x)) f{1,#}(f1(x)) -> g{1,#}(f1(x)) -> g{1,#}(g1(x)) -> f{1,#}(x) SCC Processor: #sccs: 2 #rules: 11 #arcs: 28/169 DPs: filter2{4,#}(false(),fun,x,xs) -> filter{2,#}(fun,xs) filter{2,#}(fun,cons2(x,xs)) -> app#(fun,x) app#(map1(x5),x6) -> map{2,#}(x5,x6) map{2,#}(fun,cons2(x,xs)) -> map{2,#}(fun,xs) map{2,#}(fun,cons2(x,xs)) -> app#(fun,x) app#(filter1(x5),x6) -> filter{2,#}(x5,x6) filter{2,#}(fun,cons2(x,xs)) -> filter2{4,#}(app(fun,x),fun,x,xs) filter2{4,#}(true(),fun,x,xs) -> filter{2,#}(fun,xs) app#(filter23(x5,x4,x3),x6) -> filter2{4,#}(x5,x4,x3,x6) TRS: f1(f1(x)) -> g1(f1(x)) g1(g1(x)) -> f1(x) map2(fun,nil()) -> nil() map2(fun,cons2(x,xs)) -> cons2(app(fun,x),map2(fun,xs)) filter2(fun,nil()) -> nil() filter2(fun,cons2(x,xs)) -> filter24(app(fun,x),fun,x,xs) filter24(true(),fun,x,xs) -> cons2(x,filter2(fun,xs)) filter24(false(),fun,x,xs) -> filter2(fun,xs) app(f(),x6) -> f1(x6) app(g(),x6) -> g1(x6) app(map1(x5),x6) -> map2(x5,x6) app(map(),x6) -> map1(x6) app(cons1(x5),x6) -> cons2(x5,x6) app(cons(),x6) -> cons1(x6) app(filter1(x5),x6) -> filter2(x5,x6) app(filter(),x6) -> filter1(x6) app(filter23(x5,x4,x3),x6) -> filter24(x5,x4,x3,x6) app(filter22(x5,x4),x6) -> filter23(x5,x4,x6) app(filter21(x5),x6) -> filter22(x5,x6) app(filter2(),x6) -> filter21(x6) Subterm Criterion Processor: simple projection: pi(map{2,#}) = 1 pi(app#) = 1 pi(filter{2,#}) = 1 pi(filter2{4,#}) = 3 problem: DPs: filter2{4,#}(false(),fun,x,xs) -> filter{2,#}(fun,xs) app#(map1(x5),x6) -> map{2,#}(x5,x6) app#(filter1(x5),x6) -> filter{2,#}(x5,x6) filter2{4,#}(true(),fun,x,xs) -> filter{2,#}(fun,xs) app#(filter23(x5,x4,x3),x6) -> filter2{4,#}(x5,x4,x3,x6) TRS: f1(f1(x)) -> g1(f1(x)) g1(g1(x)) -> f1(x) map2(fun,nil()) -> nil() map2(fun,cons2(x,xs)) -> cons2(app(fun,x),map2(fun,xs)) filter2(fun,nil()) -> nil() filter2(fun,cons2(x,xs)) -> filter24(app(fun,x),fun,x,xs) filter24(true(),fun,x,xs) -> cons2(x,filter2(fun,xs)) filter24(false(),fun,x,xs) -> filter2(fun,xs) app(f(),x6) -> f1(x6) app(g(),x6) -> g1(x6) app(map1(x5),x6) -> map2(x5,x6) app(map(),x6) -> map1(x6) app(cons1(x5),x6) -> cons2(x5,x6) app(cons(),x6) -> cons1(x6) app(filter1(x5),x6) -> filter2(x5,x6) app(filter(),x6) -> filter1(x6) app(filter23(x5,x4,x3),x6) -> filter24(x5,x4,x3,x6) app(filter22(x5,x4),x6) -> filter23(x5,x4,x6) app(filter21(x5),x6) -> filter22(x5,x6) app(filter2(),x6) -> filter21(x6) SCC Processor: #sccs: 0 #rules: 0 #arcs: 20/25 DPs: f{1,#}(f1(x)) -> g{1,#}(f1(x)) g{1,#}(g1(x)) -> f{1,#}(x) TRS: f1(f1(x)) -> g1(f1(x)) g1(g1(x)) -> f1(x) map2(fun,nil()) -> nil() map2(fun,cons2(x,xs)) -> cons2(app(fun,x),map2(fun,xs)) filter2(fun,nil()) -> nil() filter2(fun,cons2(x,xs)) -> filter24(app(fun,x),fun,x,xs) filter24(true(),fun,x,xs) -> cons2(x,filter2(fun,xs)) filter24(false(),fun,x,xs) -> filter2(fun,xs) app(f(),x6) -> f1(x6) app(g(),x6) -> g1(x6) app(map1(x5),x6) -> map2(x5,x6) app(map(),x6) -> map1(x6) app(cons1(x5),x6) -> cons2(x5,x6) app(cons(),x6) -> cons1(x6) app(filter1(x5),x6) -> filter2(x5,x6) app(filter(),x6) -> filter1(x6) app(filter23(x5,x4,x3),x6) -> filter24(x5,x4,x3,x6) app(filter22(x5,x4),x6) -> filter23(x5,x4,x6) app(filter21(x5),x6) -> filter22(x5,x6) app(filter2(),x6) -> filter21(x6) Subterm Criterion Processor: simple projection: pi(f{1,#}) = 0 pi(g{1,#}) = 0 problem: DPs: f{1,#}(f1(x)) -> g{1,#}(f1(x)) TRS: f1(f1(x)) -> g1(f1(x)) g1(g1(x)) -> f1(x) map2(fun,nil()) -> nil() map2(fun,cons2(x,xs)) -> cons2(app(fun,x),map2(fun,xs)) filter2(fun,nil()) -> nil() filter2(fun,cons2(x,xs)) -> filter24(app(fun,x),fun,x,xs) filter24(true(),fun,x,xs) -> cons2(x,filter2(fun,xs)) filter24(false(),fun,x,xs) -> filter2(fun,xs) app(f(),x6) -> f1(x6) app(g(),x6) -> g1(x6) app(map1(x5),x6) -> map2(x5,x6) app(map(),x6) -> map1(x6) app(cons1(x5),x6) -> cons2(x5,x6) app(cons(),x6) -> cons1(x6) app(filter1(x5),x6) -> filter2(x5,x6) app(filter(),x6) -> filter1(x6) app(filter23(x5,x4,x3),x6) -> filter24(x5,x4,x3,x6) app(filter22(x5,x4),x6) -> filter23(x5,x4,x6) app(filter21(x5),x6) -> filter22(x5,x6) app(filter2(),x6) -> filter21(x6) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/1