YES Problem: app(app(.(),1()),x) -> x app(app(.(),x),1()) -> x app(app(.(),app(i(),x)),x) -> 1() app(app(.(),x),app(i(),x)) -> 1() app(app(.(),app(i(),y)),app(app(.(),y),z)) -> z app(app(.(),y),app(app(.(),app(i(),y)),z)) -> z app(i(),1()) -> 1() app(i(),app(i(),x)) -> x app(app(map(),f),nil()) -> nil() app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs)) app(app(filter(),f),nil()) -> nil() app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs) app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs)) app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs) Proof: Uncurry Processor: .2(1(),x) -> x .2(x,1()) -> x .2(i1(x),x) -> 1() .2(x,i1(x)) -> 1() .2(i1(y),.2(y,z)) -> z .2(y,.2(i1(y),z)) -> z i1(1()) -> 1() i1(i1(x)) -> x map2(f,nil()) -> nil() map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs) filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app(.1(x7),x8) -> .2(x7,x8) app(.(),x8) -> .1(x8) app(i(),x8) -> i1(x8) app(map1(x7),x8) -> map2(x7,x8) app(map(),x8) -> map1(x8) app(cons1(x7),x8) -> cons2(x7,x8) app(cons(),x8) -> cons1(x8) app(filter1(x7),x8) -> filter2(x7,x8) app(filter(),x8) -> filter1(x8) app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8) app(filter22(x7,x6),x8) -> filter23(x7,x6,x8) app(filter21(x7),x8) -> filter22(x7,x8) app(filter2(),x8) -> filter21(x8) DP Processor: DPs: map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) map{2,#}(f,cons2(x,xs)) -> app#(f,x) filter{2,#}(f,cons2(x,xs)) -> app#(f,x) filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs) filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) app#(.1(x7),x8) -> .{2,#}(x7,x8) app#(i(),x8) -> i{1,#}(x8) app#(map1(x7),x8) -> map{2,#}(x7,x8) app#(filter1(x7),x8) -> filter{2,#}(x7,x8) app#(filter23(x7,x6,x5),x8) -> filter2{4,#}(x7,x6,x5,x8) TRS: .2(1(),x) -> x .2(x,1()) -> x .2(i1(x),x) -> 1() .2(x,i1(x)) -> 1() .2(i1(y),.2(y,z)) -> z .2(y,.2(i1(y),z)) -> z i1(1()) -> 1() i1(i1(x)) -> x map2(f,nil()) -> nil() map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs) filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app(.1(x7),x8) -> .2(x7,x8) app(.(),x8) -> .1(x8) app(i(),x8) -> i1(x8) app(map1(x7),x8) -> map2(x7,x8) app(map(),x8) -> map1(x8) app(cons1(x7),x8) -> cons2(x7,x8) app(cons(),x8) -> cons1(x8) app(filter1(x7),x8) -> filter2(x7,x8) app(filter(),x8) -> filter1(x8) app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8) app(filter22(x7,x6),x8) -> filter23(x7,x6,x8) app(filter21(x7),x8) -> filter22(x7,x8) app(filter2(),x8) -> filter21(x8) TDG Processor: DPs: map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) map{2,#}(f,cons2(x,xs)) -> app#(f,x) filter{2,#}(f,cons2(x,xs)) -> app#(f,x) filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs) filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) app#(.1(x7),x8) -> .{2,#}(x7,x8) app#(i(),x8) -> i{1,#}(x8) app#(map1(x7),x8) -> map{2,#}(x7,x8) app#(filter1(x7),x8) -> filter{2,#}(x7,x8) app#(filter23(x7,x6,x5),x8) -> filter2{4,#}(x7,x6,x5,x8) TRS: .2(1(),x) -> x .2(x,1()) -> x .2(i1(x),x) -> 1() .2(x,i1(x)) -> 1() .2(i1(y),.2(y,z)) -> z .2(y,.2(i1(y),z)) -> z i1(1()) -> 1() i1(i1(x)) -> x map2(f,nil()) -> nil() map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs) filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app(.1(x7),x8) -> .2(x7,x8) app(.(),x8) -> .1(x8) app(i(),x8) -> i1(x8) app(map1(x7),x8) -> map2(x7,x8) app(map(),x8) -> map1(x8) app(cons1(x7),x8) -> cons2(x7,x8) app(cons(),x8) -> cons1(x8) app(filter1(x7),x8) -> filter2(x7,x8) app(filter(),x8) -> filter1(x8) app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8) app(filter22(x7,x6),x8) -> filter23(x7,x6,x8) app(filter21(x7),x8) -> filter22(x7,x8) app(filter2(),x8) -> filter21(x8) graph: filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) -> filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs) filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) -> filter{2,#}(f,cons2(x,xs)) -> app#(f,x) filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) -> filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs) filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) -> filter{2,#}(f,cons2(x,xs)) -> app#(f,x) filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs) -> filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs) -> filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) filter{2,#}(f,cons2(x,xs)) -> app#(f,x) -> app#(filter23(x7,x6,x5),x8) -> filter2{4,#}(x7,x6,x5,x8) filter{2,#}(f,cons2(x,xs)) -> app#(f,x) -> app#(filter1(x7),x8) -> filter{2,#}(x7,x8) filter{2,#}(f,cons2(x,xs)) -> app#(f,x) -> app#(map1(x7),x8) -> map{2,#}(x7,x8) filter{2,#}(f,cons2(x,xs)) -> app#(f,x) -> app#(i(),x8) -> i{1,#}(x8) filter{2,#}(f,cons2(x,xs)) -> app#(f,x) -> app#(.1(x7),x8) -> .{2,#}(x7,x8) app#(filter23(x7,x6,x5),x8) -> filter2{4,#}(x7,x6,x5,x8) -> filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) app#(filter23(x7,x6,x5),x8) -> filter2{4,#}(x7,x6,x5,x8) -> filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) app#(filter1(x7),x8) -> filter{2,#}(x7,x8) -> filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs) app#(filter1(x7),x8) -> filter{2,#}(x7,x8) -> filter{2,#}(f,cons2(x,xs)) -> app#(f,x) app#(map1(x7),x8) -> map{2,#}(x7,x8) -> map{2,#}(f,cons2(x,xs)) -> app#(f,x) app#(map1(x7),x8) -> map{2,#}(x7,x8) -> map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) map{2,#}(f,cons2(x,xs)) -> app#(f,x) -> app#(filter23(x7,x6,x5),x8) -> filter2{4,#}(x7,x6,x5,x8) map{2,#}(f,cons2(x,xs)) -> app#(f,x) -> app#(filter1(x7),x8) -> filter{2,#}(x7,x8) map{2,#}(f,cons2(x,xs)) -> app#(f,x) -> app#(map1(x7),x8) -> map{2,#}(x7,x8) map{2,#}(f,cons2(x,xs)) -> app#(f,x) -> app#(i(),x8) -> i{1,#}(x8) map{2,#}(f,cons2(x,xs)) -> app#(f,x) -> app#(.1(x7),x8) -> .{2,#}(x7,x8) map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) -> map{2,#}(f,cons2(x,xs)) -> app#(f,x) map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) -> map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) SCC Processor: #sccs: 1 #rules: 9 #arcs: 24/121 DPs: filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) filter{2,#}(f,cons2(x,xs)) -> app#(f,x) app#(map1(x7),x8) -> map{2,#}(x7,x8) map{2,#}(f,cons2(x,xs)) -> map{2,#}(f,xs) map{2,#}(f,cons2(x,xs)) -> app#(f,x) app#(filter1(x7),x8) -> filter{2,#}(x7,x8) filter{2,#}(f,cons2(x,xs)) -> filter2{4,#}(app(f,x),f,x,xs) filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) app#(filter23(x7,x6,x5),x8) -> filter2{4,#}(x7,x6,x5,x8) TRS: .2(1(),x) -> x .2(x,1()) -> x .2(i1(x),x) -> 1() .2(x,i1(x)) -> 1() .2(i1(y),.2(y,z)) -> z .2(y,.2(i1(y),z)) -> z i1(1()) -> 1() i1(i1(x)) -> x map2(f,nil()) -> nil() map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs) filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app(.1(x7),x8) -> .2(x7,x8) app(.(),x8) -> .1(x8) app(i(),x8) -> i1(x8) app(map1(x7),x8) -> map2(x7,x8) app(map(),x8) -> map1(x8) app(cons1(x7),x8) -> cons2(x7,x8) app(cons(),x8) -> cons1(x8) app(filter1(x7),x8) -> filter2(x7,x8) app(filter(),x8) -> filter1(x8) app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8) app(filter22(x7,x6),x8) -> filter23(x7,x6,x8) app(filter21(x7),x8) -> filter22(x7,x8) app(filter2(),x8) -> filter21(x8) 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(),f,x,xs) -> filter{2,#}(f,xs) app#(map1(x7),x8) -> map{2,#}(x7,x8) app#(filter1(x7),x8) -> filter{2,#}(x7,x8) filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) app#(filter23(x7,x6,x5),x8) -> filter2{4,#}(x7,x6,x5,x8) TRS: .2(1(),x) -> x .2(x,1()) -> x .2(i1(x),x) -> 1() .2(x,i1(x)) -> 1() .2(i1(y),.2(y,z)) -> z .2(y,.2(i1(y),z)) -> z i1(1()) -> 1() i1(i1(x)) -> x map2(f,nil()) -> nil() map2(f,cons2(x,xs)) -> cons2(app(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,cons2(x,xs)) -> filter24(app(f,x),f,x,xs) filter24(true(),f,x,xs) -> cons2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app(.1(x7),x8) -> .2(x7,x8) app(.(),x8) -> .1(x8) app(i(),x8) -> i1(x8) app(map1(x7),x8) -> map2(x7,x8) app(map(),x8) -> map1(x8) app(cons1(x7),x8) -> cons2(x7,x8) app(cons(),x8) -> cons1(x8) app(filter1(x7),x8) -> filter2(x7,x8) app(filter(),x8) -> filter1(x8) app(filter23(x7,x6,x5),x8) -> filter24(x7,x6,x5,x8) app(filter22(x7,x6),x8) -> filter23(x7,x6,x8) app(filter21(x7),x8) -> filter22(x7,x8) app(filter2(),x8) -> filter21(x8) SCC Processor: #sccs: 0 #rules: 0 #arcs: 20/25