YES Problem: app'(app'(eq(),0()),0()) -> true() app'(app'(eq(),0()),app'(s(),x)) -> false() app'(app'(eq(),app'(s(),x)),0()) -> false() app'(app'(eq(),app'(s(),x)),app'(s(),y)) -> app'(app'(eq(),x),y) app'(app'(le(),0()),y) -> true() app'(app'(le(),app'(s(),x)),0()) -> false() app'(app'(le(),app'(s(),x)),app'(s(),y)) -> app'(app'(le(),x),y) app'(app'(app(),nil()),y) -> y app'(app'(app(),app'(app'(add(),n),x)),y) -> app'(app'(add(),n),app'(app'(app(),x),y)) app'(min(),app'(app'(add(),n),nil())) -> n app'(min(),app'(app'(add(),n),app'(app'(add(),m),x))) -> app'(app'(if_min(),app'(app'(le(),n),m)),app'(app'(add(),n),app'(app'(add(),m),x))) app'(app'(if_min(),true()),app'(app'(add(),n),app'(app'(add(),m),x))) -> app'(min(),app'(app'(add(),n),x)) app'(app'(if_min(),false()),app'(app'(add(),n),app'(app'(add(),m),x))) -> app'(min(),app'(app'(add(),m),x)) app'(app'(rm(),n),nil()) -> nil() app'(app'(rm(),n),app'(app'(add(),m),x)) -> app'(app'(app'(if_rm(),app'(app'(eq(),n),m)),n),app'(app'(add(),m),x)) app'(app'(app'(if_rm(),true()),n),app'(app'(add(),m),x)) -> app'(app'(rm(),n),x) app'(app'(app'(if_rm(),false()),n),app'(app'(add(),m),x)) -> app'(app'(add(),m),app'(app'(rm(),n),x)) app'(app'(minsort(),nil()),nil()) -> nil() app'(app'(minsort(),app'(app'(add(),n),x)),y) -> app'(app'(app'(if_minsort(),app'(app'(eq(),n),app'(min(),app'(app'(add(),n),x)))), app'(app'(add(),n),x)),y) app'(app'(app'(if_minsort(),true()),app'(app'(add(),n),x)),y) -> app'(app'(add(),n),app'(app'(minsort(),app'(app'(app(),app'(app'(rm(),n),x)),y)),nil())) app'(app'(app'(if_minsort(),false()),app'(app'(add(),n),x)),y) -> app'(app'(minsort(),x),app'(app'(add(),n),y)) app'(app'(map(),f),nil()) -> nil() app'(app'(map(),f),app'(app'(add(),x),xs)) -> app'(app'(add(),app'(f,x)),app'(app'(map(),f),xs)) app'(app'(filter(),f),nil()) -> nil() app'(app'(filter(),f),app'(app'(add(),x),xs)) -> app'(app'(app'(app'(filter2(),app'(f,x)),f),x),xs) app'(app'(app'(app'(filter2(),true()),f),x),xs) -> app'(app'(add(),x),app'(app'(filter(),f),xs)) app'(app'(app'(app'(filter2(),false()),f),x),xs) -> app'(app'(filter(),f),xs) Proof: Uncurry Processor: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) DP Processor: DPs: eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y) le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y) app{2,#}(add2(n,x),y) -> app{2,#}(x,y) min{1,#}(add2(n,add2(m,x))) -> le{2,#}(n,m) min{1,#}(add2(n,add2(m,x))) -> if_min{2,#}(le2(n,m),add2(n,add2(m,x))) if_min{2,#}(true(),add2(n,add2(m,x))) -> min{1,#}(add2(n,x)) if_min{2,#}(false(),add2(n,add2(m,x))) -> min{1,#}(add2(m,x)) rm{2,#}(n,add2(m,x)) -> eq{2,#}(n,m) rm{2,#}(n,add2(m,x)) -> if_rm{3,#}(eq2(n,m),n,add2(m,x)) if_rm{3,#}(true(),n,add2(m,x)) -> rm{2,#}(n,x) if_rm{3,#}(false(),n,add2(m,x)) -> rm{2,#}(n,x) minsort{2,#}(add2(n,x),y) -> min{1,#}(add2(n,x)) minsort{2,#}(add2(n,x),y) -> eq{2,#}(n,min1(add2(n,x))) minsort{2,#}(add2(n,x),y) -> if_minsort{3,#}(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort{3,#}(true(),add2(n,x),y) -> rm{2,#}(n,x) if_minsort{3,#}(true(),add2(n,x),y) -> app{2,#}(rm2(n,x),y) if_minsort{3,#}(true(),add2(n,x),y) -> minsort{2,#}(app2(rm2(n,x),y),nil()) if_minsort{3,#}(false(),add2(n,x),y) -> minsort{2,#}(x,add2(n,y)) map{2,#}(f,add2(x,xs)) -> map{2,#}(f,xs) map{2,#}(f,add2(x,xs)) -> app'#(f,x) filter{2,#}(f,add2(x,xs)) -> app'#(f,x) filter{2,#}(f,add2(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'#(eq1(x8),x9) -> eq{2,#}(x8,x9) app'#(le1(x8),x9) -> le{2,#}(x8,x9) app'#(app1(x8),x9) -> app{2,#}(x8,x9) app'#(min(),x9) -> min{1,#}(x9) app'#(if_min1(x8),x9) -> if_min{2,#}(x8,x9) app'#(rm1(x8),x9) -> rm{2,#}(x8,x9) app'#(if_rm2(x8,x7),x9) -> if_rm{3,#}(x8,x7,x9) app'#(minsort1(x8),x9) -> minsort{2,#}(x8,x9) app'#(if_minsort2(x8,x7),x9) -> if_minsort{3,#}(x8,x7,x9) app'#(map1(x8),x9) -> map{2,#}(x8,x9) app'#(filter1(x8),x9) -> filter{2,#}(x8,x9) app'#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9) TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) TDG Processor: DPs: eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y) le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y) app{2,#}(add2(n,x),y) -> app{2,#}(x,y) min{1,#}(add2(n,add2(m,x))) -> le{2,#}(n,m) min{1,#}(add2(n,add2(m,x))) -> if_min{2,#}(le2(n,m),add2(n,add2(m,x))) if_min{2,#}(true(),add2(n,add2(m,x))) -> min{1,#}(add2(n,x)) if_min{2,#}(false(),add2(n,add2(m,x))) -> min{1,#}(add2(m,x)) rm{2,#}(n,add2(m,x)) -> eq{2,#}(n,m) rm{2,#}(n,add2(m,x)) -> if_rm{3,#}(eq2(n,m),n,add2(m,x)) if_rm{3,#}(true(),n,add2(m,x)) -> rm{2,#}(n,x) if_rm{3,#}(false(),n,add2(m,x)) -> rm{2,#}(n,x) minsort{2,#}(add2(n,x),y) -> min{1,#}(add2(n,x)) minsort{2,#}(add2(n,x),y) -> eq{2,#}(n,min1(add2(n,x))) minsort{2,#}(add2(n,x),y) -> if_minsort{3,#}(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort{3,#}(true(),add2(n,x),y) -> rm{2,#}(n,x) if_minsort{3,#}(true(),add2(n,x),y) -> app{2,#}(rm2(n,x),y) if_minsort{3,#}(true(),add2(n,x),y) -> minsort{2,#}(app2(rm2(n,x),y),nil()) if_minsort{3,#}(false(),add2(n,x),y) -> minsort{2,#}(x,add2(n,y)) map{2,#}(f,add2(x,xs)) -> map{2,#}(f,xs) map{2,#}(f,add2(x,xs)) -> app'#(f,x) filter{2,#}(f,add2(x,xs)) -> app'#(f,x) filter{2,#}(f,add2(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'#(eq1(x8),x9) -> eq{2,#}(x8,x9) app'#(le1(x8),x9) -> le{2,#}(x8,x9) app'#(app1(x8),x9) -> app{2,#}(x8,x9) app'#(min(),x9) -> min{1,#}(x9) app'#(if_min1(x8),x9) -> if_min{2,#}(x8,x9) app'#(rm1(x8),x9) -> rm{2,#}(x8,x9) app'#(if_rm2(x8,x7),x9) -> if_rm{3,#}(x8,x7,x9) app'#(minsort1(x8),x9) -> minsort{2,#}(x8,x9) app'#(if_minsort2(x8,x7),x9) -> if_minsort{3,#}(x8,x7,x9) app'#(map1(x8),x9) -> map{2,#}(x8,x9) app'#(filter1(x8),x9) -> filter{2,#}(x8,x9) app'#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9) TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) graph: filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) -> filter{2,#}(f,add2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs) filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) -> filter{2,#}(f,add2(x,xs)) -> app'#(f,x) filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) -> filter{2,#}(f,add2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs) filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) -> filter{2,#}(f,add2(x,xs)) -> app'#(f,x) filter{2,#}(f,add2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs) -> filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) filter{2,#}(f,add2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs) -> filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) filter{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9) filter{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(filter1(x8),x9) -> filter{2,#}(x8,x9) filter{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(map1(x8),x9) -> map{2,#}(x8,x9) filter{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(if_minsort2(x8,x7),x9) -> if_minsort{3,#}(x8,x7,x9) filter{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(minsort1(x8),x9) -> minsort{2,#}(x8,x9) filter{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(if_rm2(x8,x7),x9) -> if_rm{3,#}(x8,x7,x9) filter{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(rm1(x8),x9) -> rm{2,#}(x8,x9) filter{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(if_min1(x8),x9) -> if_min{2,#}(x8,x9) filter{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(min(),x9) -> min{1,#}(x9) filter{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(app1(x8),x9) -> app{2,#}(x8,x9) filter{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(le1(x8),x9) -> le{2,#}(x8,x9) filter{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(eq1(x8),x9) -> eq{2,#}(x8,x9) app'#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9) -> filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) app'#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9) -> filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) app'#(filter1(x8),x9) -> filter{2,#}(x8,x9) -> filter{2,#}(f,add2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs) app'#(filter1(x8),x9) -> filter{2,#}(x8,x9) -> filter{2,#}(f,add2(x,xs)) -> app'#(f,x) app'#(map1(x8),x9) -> map{2,#}(x8,x9) -> map{2,#}(f,add2(x,xs)) -> app'#(f,x) app'#(map1(x8),x9) -> map{2,#}(x8,x9) -> map{2,#}(f,add2(x,xs)) -> map{2,#}(f,xs) app'#(if_minsort2(x8,x7),x9) -> if_minsort{3,#}(x8,x7,x9) -> if_minsort{3,#}(false(),add2(n,x),y) -> minsort{2,#}(x,add2(n,y)) app'#(if_minsort2(x8,x7),x9) -> if_minsort{3,#}(x8,x7,x9) -> if_minsort{3,#}(true(),add2(n,x),y) -> minsort{2,#}(app2(rm2(n,x),y),nil()) app'#(if_minsort2(x8,x7),x9) -> if_minsort{3,#}(x8,x7,x9) -> if_minsort{3,#}(true(),add2(n,x),y) -> app{2,#}(rm2(n,x),y) app'#(if_minsort2(x8,x7),x9) -> if_minsort{3,#}(x8,x7,x9) -> if_minsort{3,#}(true(),add2(n,x),y) -> rm{2,#}(n,x) app'#(minsort1(x8),x9) -> minsort{2,#}(x8,x9) -> minsort{2,#}(add2(n,x),y) -> if_minsort{3,#}(eq2(n,min1(add2(n,x))),add2(n,x),y) app'#(minsort1(x8),x9) -> minsort{2,#}(x8,x9) -> minsort{2,#}(add2(n,x),y) -> eq{2,#}(n,min1(add2(n,x))) app'#(minsort1(x8),x9) -> minsort{2,#}(x8,x9) -> minsort{2,#}(add2(n,x),y) -> min{1,#}(add2(n,x)) app'#(if_rm2(x8,x7),x9) -> if_rm{3,#}(x8,x7,x9) -> if_rm{3,#}(false(),n,add2(m,x)) -> rm{2,#}(n,x) app'#(if_rm2(x8,x7),x9) -> if_rm{3,#}(x8,x7,x9) -> if_rm{3,#}(true(),n,add2(m,x)) -> rm{2,#}(n,x) app'#(rm1(x8),x9) -> rm{2,#}(x8,x9) -> rm{2,#}(n,add2(m,x)) -> if_rm{3,#}(eq2(n,m),n,add2(m,x)) app'#(rm1(x8),x9) -> rm{2,#}(x8,x9) -> rm{2,#}(n,add2(m,x)) -> eq{2,#}(n,m) app'#(if_min1(x8),x9) -> if_min{2,#}(x8,x9) -> if_min{2,#}(false(),add2(n,add2(m,x))) -> min{1,#}(add2(m,x)) app'#(if_min1(x8),x9) -> if_min{2,#}(x8,x9) -> if_min{2,#}(true(),add2(n,add2(m,x))) -> min{1,#}(add2(n,x)) app'#(app1(x8),x9) -> app{2,#}(x8,x9) -> app{2,#}(add2(n,x),y) -> app{2,#}(x,y) app'#(le1(x8),x9) -> le{2,#}(x8,x9) -> le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y) app'#(eq1(x8),x9) -> eq{2,#}(x8,x9) -> eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y) app'#(min(),x9) -> min{1,#}(x9) -> min{1,#}(add2(n,add2(m,x))) -> if_min{2,#}(le2(n,m),add2(n,add2(m,x))) app'#(min(),x9) -> min{1,#}(x9) -> min{1,#}(add2(n,add2(m,x))) -> le{2,#}(n,m) map{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9) map{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(filter1(x8),x9) -> filter{2,#}(x8,x9) map{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(map1(x8),x9) -> map{2,#}(x8,x9) map{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(if_minsort2(x8,x7),x9) -> if_minsort{3,#}(x8,x7,x9) map{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(minsort1(x8),x9) -> minsort{2,#}(x8,x9) map{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(if_rm2(x8,x7),x9) -> if_rm{3,#}(x8,x7,x9) map{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(rm1(x8),x9) -> rm{2,#}(x8,x9) map{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(if_min1(x8),x9) -> if_min{2,#}(x8,x9) map{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(min(),x9) -> min{1,#}(x9) map{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(app1(x8),x9) -> app{2,#}(x8,x9) map{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(le1(x8),x9) -> le{2,#}(x8,x9) map{2,#}(f,add2(x,xs)) -> app'#(f,x) -> app'#(eq1(x8),x9) -> eq{2,#}(x8,x9) map{2,#}(f,add2(x,xs)) -> map{2,#}(f,xs) -> map{2,#}(f,add2(x,xs)) -> app'#(f,x) map{2,#}(f,add2(x,xs)) -> map{2,#}(f,xs) -> map{2,#}(f,add2(x,xs)) -> map{2,#}(f,xs) if_minsort{3,#}(false(),add2(n,x),y) -> minsort{2,#}(x,add2(n,y)) -> minsort{2,#}(add2(n,x),y) -> if_minsort{3,#}(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort{3,#}(false(),add2(n,x),y) -> minsort{2,#}(x,add2(n,y)) -> minsort{2,#}(add2(n,x),y) -> eq{2,#}(n,min1(add2(n,x))) if_minsort{3,#}(false(),add2(n,x),y) -> minsort{2,#}(x,add2(n,y)) -> minsort{2,#}(add2(n,x),y) -> min{1,#}(add2(n,x)) if_minsort{3,#}(true(),add2(n,x),y) -> minsort{2,#}(app2(rm2(n,x),y),nil()) -> minsort{2,#}(add2(n,x),y) -> if_minsort{3,#}(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort{3,#}(true(),add2(n,x),y) -> minsort{2,#}(app2(rm2(n,x),y),nil()) -> minsort{2,#}(add2(n,x),y) -> eq{2,#}(n,min1(add2(n,x))) if_minsort{3,#}(true(),add2(n,x),y) -> minsort{2,#}(app2(rm2(n,x),y),nil()) -> minsort{2,#}(add2(n,x),y) -> min{1,#}(add2(n,x)) if_minsort{3,#}(true(),add2(n,x),y) -> rm{2,#}(n,x) -> rm{2,#}(n,add2(m,x)) -> if_rm{3,#}(eq2(n,m),n,add2(m,x)) if_minsort{3,#}(true(),add2(n,x),y) -> rm{2,#}(n,x) -> rm{2,#}(n,add2(m,x)) -> eq{2,#}(n,m) if_minsort{3,#}(true(),add2(n,x),y) -> app{2,#}(rm2(n,x),y) -> app{2,#}(add2(n,x),y) -> app{2,#}(x,y) minsort{2,#}(add2(n,x),y) -> if_minsort{3,#}(eq2(n,min1(add2(n,x))),add2(n,x),y) -> if_minsort{3,#}(false(),add2(n,x),y) -> minsort{2,#}(x,add2(n,y)) minsort{2,#}(add2(n,x),y) -> if_minsort{3,#}(eq2(n,min1(add2(n,x))),add2(n,x),y) -> if_minsort{3,#}(true(),add2(n,x),y) -> minsort{2,#}(app2(rm2(n,x),y),nil()) minsort{2,#}(add2(n,x),y) -> if_minsort{3,#}(eq2(n,min1(add2(n,x))),add2(n,x),y) -> if_minsort{3,#}(true(),add2(n,x),y) -> app{2,#}(rm2(n,x),y) minsort{2,#}(add2(n,x),y) -> if_minsort{3,#}(eq2(n,min1(add2(n,x))),add2(n,x),y) -> if_minsort{3,#}(true(),add2(n,x),y) -> rm{2,#}(n,x) minsort{2,#}(add2(n,x),y) -> min{1,#}(add2(n,x)) -> min{1,#}(add2(n,add2(m,x))) -> if_min{2,#}(le2(n,m),add2(n,add2(m,x))) minsort{2,#}(add2(n,x),y) -> min{1,#}(add2(n,x)) -> min{1,#}(add2(n,add2(m,x))) -> le{2,#}(n,m) minsort{2,#}(add2(n,x),y) -> eq{2,#}(n,min1(add2(n,x))) -> eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y) if_rm{3,#}(false(),n,add2(m,x)) -> rm{2,#}(n,x) -> rm{2,#}(n,add2(m,x)) -> if_rm{3,#}(eq2(n,m),n,add2(m,x)) if_rm{3,#}(false(),n,add2(m,x)) -> rm{2,#}(n,x) -> rm{2,#}(n,add2(m,x)) -> eq{2,#}(n,m) if_rm{3,#}(true(),n,add2(m,x)) -> rm{2,#}(n,x) -> rm{2,#}(n,add2(m,x)) -> if_rm{3,#}(eq2(n,m),n,add2(m,x)) if_rm{3,#}(true(),n,add2(m,x)) -> rm{2,#}(n,x) -> rm{2,#}(n,add2(m,x)) -> eq{2,#}(n,m) rm{2,#}(n,add2(m,x)) -> if_rm{3,#}(eq2(n,m),n,add2(m,x)) -> if_rm{3,#}(false(),n,add2(m,x)) -> rm{2,#}(n,x) rm{2,#}(n,add2(m,x)) -> if_rm{3,#}(eq2(n,m),n,add2(m,x)) -> if_rm{3,#}(true(),n,add2(m,x)) -> rm{2,#}(n,x) rm{2,#}(n,add2(m,x)) -> eq{2,#}(n,m) -> eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y) if_min{2,#}(false(),add2(n,add2(m,x))) -> min{1,#}(add2(m,x)) -> min{1,#}(add2(n,add2(m,x))) -> if_min{2,#}(le2(n,m),add2(n,add2(m,x))) if_min{2,#}(false(),add2(n,add2(m,x))) -> min{1,#}(add2(m,x)) -> min{1,#}(add2(n,add2(m,x))) -> le{2,#}(n,m) if_min{2,#}(true(),add2(n,add2(m,x))) -> min{1,#}(add2(n,x)) -> min{1,#}(add2(n,add2(m,x))) -> if_min{2,#}(le2(n,m),add2(n,add2(m,x))) if_min{2,#}(true(),add2(n,add2(m,x))) -> min{1,#}(add2(n,x)) -> min{1,#}(add2(n,add2(m,x))) -> le{2,#}(n,m) min{1,#}(add2(n,add2(m,x))) -> if_min{2,#}(le2(n,m),add2(n,add2(m,x))) -> if_min{2,#}(false(),add2(n,add2(m,x))) -> min{1,#}(add2(m,x)) min{1,#}(add2(n,add2(m,x))) -> if_min{2,#}(le2(n,m),add2(n,add2(m,x))) -> if_min{2,#}(true(),add2(n,add2(m,x))) -> min{1,#}(add2(n,x)) min{1,#}(add2(n,add2(m,x))) -> le{2,#}(n,m) -> le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y) app{2,#}(add2(n,x),y) -> app{2,#}(x,y) -> app{2,#}(add2(n,x),y) -> app{2,#}(x,y) le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y) -> le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y) eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y) -> eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y) SCC Processor: #sccs: 7 #rules: 21 #arcs: 89/1296 DPs: filter2{4,#}(false(),f,x,xs) -> filter{2,#}(f,xs) filter{2,#}(f,add2(x,xs)) -> app'#(f,x) app'#(map1(x8),x9) -> map{2,#}(x8,x9) map{2,#}(f,add2(x,xs)) -> map{2,#}(f,xs) map{2,#}(f,add2(x,xs)) -> app'#(f,x) app'#(filter1(x8),x9) -> filter{2,#}(x8,x9) filter{2,#}(f,add2(x,xs)) -> filter2{4,#}(app'(f,x),f,x,xs) filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) app'#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9) TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) 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(x8),x9) -> map{2,#}(x8,x9) app'#(filter1(x8),x9) -> filter{2,#}(x8,x9) filter2{4,#}(true(),f,x,xs) -> filter{2,#}(f,xs) app'#(filter23(x8,x7,x6),x9) -> filter2{4,#}(x8,x7,x6,x9) TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) SCC Processor: #sccs: 0 #rules: 0 #arcs: 20/25 DPs: minsort{2,#}(add2(n,x),y) -> if_minsort{3,#}(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort{3,#}(true(),add2(n,x),y) -> minsort{2,#}(app2(rm2(n,x),y),nil()) if_minsort{3,#}(false(),add2(n,x),y) -> minsort{2,#}(x,add2(n,y)) TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) Usable Rule Processor: DPs: minsort{2,#}(add2(n,x),y) -> if_minsort{3,#}(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort{3,#}(true(),add2(n,x),y) -> minsort{2,#}(app2(rm2(n,x),y),nil()) if_minsort{3,#}(false(),add2(n,x),y) -> minsort{2,#}(x,add2(n,y)) TRS: min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) Matrix Interpretation Processor: dim=1 usable rules: rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) interpretation: [if_minsort{3,#}](x0, x1, x2) = x1 + x2, [minsort{2,#}](x0, x1) = x0 + x1, [if_rm3](x0, x1, x2) = 2x1 + x2, [rm2](x0, x1) = 2x0 + x1, [if_min2](x0, x1) = 3x0, [min1](x0) = 6x0 + 2, [add2](x0, x1) = 2x0 + x1 + 2, [app2](x0, x1) = x0 + x1, [le2](x0, x1) = 5x0 + 3x1 + 4, [s1](x0) = 6x0, [eq2](x0, x1) = 5x0 + 2x1, [nil] = 0, [false] = 0, [true] = 0, [0] = 0 orientation: minsort{2,#}(add2(n,x),y) = 2n + x + y + 2 >= 2n + x + y + 2 = if_minsort{3,#}(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort{3,#}(true(),add2(n,x),y) = 2n + x + y + 2 >= 2n + x + y = minsort{2,#}(app2(rm2(n,x),y),nil()) if_minsort{3,#}(false(),add2(n,x),y) = 2n + x + y + 2 >= 2n + x + y + 2 = minsort{2,#}(x,add2(n,y)) min1(add2(n,nil())) = 12n + 14 >= n = n min1(add2(n,add2(m,x))) = 12m + 12n + 6x + 26 >= 9m + 15n + 12 = if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) = 0 >= 12n + 6x + 14 = min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) = 0 >= 12m + 6x + 14 = min1(add2(m,x)) le2(0(),y) = 3y + 4 >= 0 = true() le2(s1(x),0()) = 30x + 4 >= 0 = false() le2(s1(x),s1(y)) = 30x + 18y + 4 >= 5x + 3y + 4 = le2(x,y) eq2(0(),0()) = 0 >= 0 = true() eq2(0(),s1(x)) = 12x >= 0 = false() eq2(s1(x),0()) = 30x >= 0 = false() eq2(s1(x),s1(y)) = 30x + 12y >= 5x + 2y = eq2(x,y) rm2(n,nil()) = 2n >= 0 = nil() rm2(n,add2(m,x)) = 2m + 2n + x + 2 >= 2m + 2n + x + 2 = if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) = 2m + 2n + x + 2 >= 2n + x = rm2(n,x) if_rm3(false(),n,add2(m,x)) = 2m + 2n + x + 2 >= 2m + 2n + x + 2 = add2(m,rm2(n,x)) app2(nil(),y) = y >= y = y app2(add2(n,x),y) = 2n + x + y + 2 >= 2n + x + y + 2 = add2(n,app2(x,y)) problem: DPs: minsort{2,#}(add2(n,x),y) -> if_minsort{3,#}(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort{3,#}(false(),add2(n,x),y) -> minsort{2,#}(x,add2(n,y)) TRS: min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) Restore Modifier: DPs: minsort{2,#}(add2(n,x),y) -> if_minsort{3,#}(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort{3,#}(false(),add2(n,x),y) -> minsort{2,#}(x,add2(n,y)) TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) Subterm Criterion Processor: simple projection: pi(minsort{2,#}) = 0 pi(if_minsort{3,#}) = 1 problem: DPs: minsort{2,#}(add2(n,x),y) -> if_minsort{3,#}(eq2(n,min1(add2(n,x))),add2(n,x),y) TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) SCC Processor: #sccs: 0 #rules: 0 #arcs: 4/1 DPs: rm{2,#}(n,add2(m,x)) -> if_rm{3,#}(eq2(n,m),n,add2(m,x)) if_rm{3,#}(true(),n,add2(m,x)) -> rm{2,#}(n,x) if_rm{3,#}(false(),n,add2(m,x)) -> rm{2,#}(n,x) TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) Subterm Criterion Processor: simple projection: pi(rm{2,#}) = 1 pi(if_rm{3,#}) = 2 problem: DPs: rm{2,#}(n,add2(m,x)) -> if_rm{3,#}(eq2(n,m),n,add2(m,x)) TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) SCC Processor: #sccs: 0 #rules: 0 #arcs: 4/1 DPs: min{1,#}(add2(n,add2(m,x))) -> if_min{2,#}(le2(n,m),add2(n,add2(m,x))) if_min{2,#}(true(),add2(n,add2(m,x))) -> min{1,#}(add2(n,x)) if_min{2,#}(false(),add2(n,add2(m,x))) -> min{1,#}(add2(m,x)) TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) Usable Rule Processor: DPs: min{1,#}(add2(n,add2(m,x))) -> if_min{2,#}(le2(n,m),add2(n,add2(m,x))) if_min{2,#}(true(),add2(n,add2(m,x))) -> min{1,#}(add2(n,x)) if_min{2,#}(false(),add2(n,add2(m,x))) -> min{1,#}(add2(m,x)) TRS: le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) Arctic Interpretation Processor: dimension: 1 usable rules: interpretation: [if_min{2,#}](x0, x1) = x1, [min{1,#}](x0) = x0 + -16, [add2](x0, x1) = 2x0 + 2x1 + -2, [le2](x0, x1) = 1x0 + 1x1 + -7, [s1](x0) = x0 + 0, [false] = 2, [true] = 0, [0] = 0 orientation: min{1,#}(add2(n,add2(m,x))) = 4m + 2n + 4x + 0 >= 4m + 2n + 4x + 0 = if_min{2,#}(le2(n,m),add2(n,add2(m,x))) if_min{2,#}(true(),add2(n,add2(m,x))) = 4m + 2n + 4x + 0 >= 2n + 2x + -2 = min{1,#}(add2(n,x)) if_min{2,#}(false(),add2(n,add2(m,x))) = 4m + 2n + 4x + 0 >= 2m + 2x + -2 = min{1,#}(add2(m,x)) le2(0(),y) = 1y + 1 >= 0 = true() le2(s1(x),0()) = 1x + 1 >= 2 = false() le2(s1(x),s1(y)) = 1x + 1y + 1 >= 1x + 1y + -7 = le2(x,y) problem: DPs: min{1,#}(add2(n,add2(m,x))) -> if_min{2,#}(le2(n,m),add2(n,add2(m,x))) if_min{2,#}(true(),add2(n,add2(m,x))) -> min{1,#}(add2(n,x)) TRS: le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) Restore Modifier: DPs: min{1,#}(add2(n,add2(m,x))) -> if_min{2,#}(le2(n,m),add2(n,add2(m,x))) if_min{2,#}(true(),add2(n,add2(m,x))) -> min{1,#}(add2(n,x)) TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) Usable Rule Processor: DPs: min{1,#}(add2(n,add2(m,x))) -> if_min{2,#}(le2(n,m),add2(n,add2(m,x))) if_min{2,#}(true(),add2(n,add2(m,x))) -> min{1,#}(add2(n,x)) TRS: le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) Arctic Interpretation Processor: dimension: 1 usable rules: le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) interpretation: [if_min{2,#}](x0, x1) = x0 + -2x1 + 0, [min{1,#}](x0) = x0 + 0, [add2](x0, x1) = 2x1 + 0, [le2](x0, x1) = 0, [s1](x0) = x0 + 0, [false] = 0, [true] = 0, [0] = 8 orientation: min{1,#}(add2(n,add2(m,x))) = 4x + 2 >= 2x + 0 = if_min{2,#}(le2(n,m),add2(n,add2(m,x))) if_min{2,#}(true(),add2(n,add2(m,x))) = 2x + 0 >= 2x + 0 = min{1,#}(add2(n,x)) le2(0(),y) = 0 >= 0 = true() le2(s1(x),0()) = 0 >= 0 = false() le2(s1(x),s1(y)) = 0 >= 0 = le2(x,y) problem: DPs: if_min{2,#}(true(),add2(n,add2(m,x))) -> min{1,#}(add2(n,x)) TRS: le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) Restore Modifier: DPs: if_min{2,#}(true(),add2(n,add2(m,x))) -> min{1,#}(add2(n,x)) TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) SCC Processor: #sccs: 0 #rules: 0 #arcs: 4/1 DPs: app{2,#}(add2(n,x),y) -> app{2,#}(x,y) TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) Subterm Criterion Processor: simple projection: pi(app{2,#}) = 0 problem: DPs: TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) Qed DPs: le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y) TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) Subterm Criterion Processor: simple projection: pi(le{2,#}) = 1 problem: DPs: TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) Qed DPs: eq{2,#}(s1(x),s1(y)) -> eq{2,#}(x,y) TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) Subterm Criterion Processor: simple projection: pi(eq{2,#}) = 1 problem: DPs: TRS: eq2(0(),0()) -> true() eq2(0(),s1(x)) -> false() eq2(s1(x),0()) -> false() eq2(s1(x),s1(y)) -> eq2(x,y) le2(0(),y) -> true() le2(s1(x),0()) -> false() le2(s1(x),s1(y)) -> le2(x,y) app2(nil(),y) -> y app2(add2(n,x),y) -> add2(n,app2(x,y)) min1(add2(n,nil())) -> n min1(add2(n,add2(m,x))) -> if_min2(le2(n,m),add2(n,add2(m,x))) if_min2(true(),add2(n,add2(m,x))) -> min1(add2(n,x)) if_min2(false(),add2(n,add2(m,x))) -> min1(add2(m,x)) rm2(n,nil()) -> nil() rm2(n,add2(m,x)) -> if_rm3(eq2(n,m),n,add2(m,x)) if_rm3(true(),n,add2(m,x)) -> rm2(n,x) if_rm3(false(),n,add2(m,x)) -> add2(m,rm2(n,x)) minsort2(nil(),nil()) -> nil() minsort2(add2(n,x),y) -> if_minsort3(eq2(n,min1(add2(n,x))),add2(n,x),y) if_minsort3(true(),add2(n,x),y) -> add2(n,minsort2(app2(rm2(n,x),y),nil())) if_minsort3(false(),add2(n,x),y) -> minsort2(x,add2(n,y)) map2(f,nil()) -> nil() map2(f,add2(x,xs)) -> add2(app'(f,x),map2(f,xs)) filter2(f,nil()) -> nil() filter2(f,add2(x,xs)) -> filter24(app'(f,x),f,x,xs) filter24(true(),f,x,xs) -> add2(x,filter2(f,xs)) filter24(false(),f,x,xs) -> filter2(f,xs) app'(eq1(x8),x9) -> eq2(x8,x9) app'(eq(),x9) -> eq1(x9) app'(s(),x9) -> s1(x9) app'(le1(x8),x9) -> le2(x8,x9) app'(le(),x9) -> le1(x9) app'(app1(x8),x9) -> app2(x8,x9) app'(app(),x9) -> app1(x9) app'(add1(x8),x9) -> add2(x8,x9) app'(add(),x9) -> add1(x9) app'(min(),x9) -> min1(x9) app'(if_min1(x8),x9) -> if_min2(x8,x9) app'(if_min(),x9) -> if_min1(x9) app'(rm1(x8),x9) -> rm2(x8,x9) app'(rm(),x9) -> rm1(x9) app'(if_rm2(x8,x7),x9) -> if_rm3(x8,x7,x9) app'(if_rm1(x8),x9) -> if_rm2(x8,x9) app'(if_rm(),x9) -> if_rm1(x9) app'(minsort1(x8),x9) -> minsort2(x8,x9) app'(minsort(),x9) -> minsort1(x9) app'(if_minsort2(x8,x7),x9) -> if_minsort3(x8,x7,x9) app'(if_minsort1(x8),x9) -> if_minsort2(x8,x9) app'(if_minsort(),x9) -> if_minsort1(x9) app'(map1(x8),x9) -> map2(x8,x9) app'(map(),x9) -> map1(x9) app'(filter1(x8),x9) -> filter2(x8,x9) app'(filter(),x9) -> filter1(x9) app'(filter23(x8,x7,x6),x9) -> filter24(x8,x7,x6,x9) app'(filter22(x8,x7),x9) -> filter23(x8,x7,x9) app'(filter21(x8),x9) -> filter22(x8,x9) app'(filter2(),x9) -> filter21(x9) Qed