MAYBE
Problem:
app'(app'(minus(),x),0()) -> x
app'(app'(minus(),app'(s(),x)),app'(s(),y)) -> app'(app'(minus(),x),y)
app'(app'(quot(),0()),app'(s(),y)) -> 0()
app'(app'(quot(),app'(s(),x)),app'(s(),y)) ->
app'(s(),app'(app'(quot(),app'(app'(minus(),x),y)),app'(s(),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'(app'(low(),n),nil()) -> nil()
app'(app'(low(),n),app'(app'(add(),m),x)) ->
app'(app'(app'(if_low(),app'(app'(le(),m),n)),n),app'(app'(add(),m),x))
app'(app'(app'(if_low(),true()),n),app'(app'(add(),m),x)) ->
app'(app'(add(),m),app'(app'(low(),n),x))
app'(app'(app'(if_low(),false()),n),app'(app'(add(),m),x)) -> app'(app'(low(),n),x)
app'(app'(high(),n),nil()) -> nil()
app'(app'(high(),n),app'(app'(add(),m),x)) ->
app'(app'(app'(if_high(),app'(app'(le(),m),n)),n),app'(app'(add(),m),x))
app'(app'(app'(if_high(),true()),n),app'(app'(add(),m),x)) -> app'(app'(high(),n),x)
app'(app'(app'(if_high(),false()),n),app'(app'(add(),m),x)) ->
app'(app'(add(),m),app'(app'(high(),n),x))
app'(quicksort(),nil()) -> nil()
app'(quicksort(),app'(app'(add(),n),x)) ->
app'(app'(app(),app'(quicksort(),app'(app'(low(),n),x))),app'(app'(add(),n),
app'(quicksort(),
app'
(app'(high(),n),x))))
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:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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:
minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
quot{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y))
le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
app{2,#}(add2(n,x),y) -> app{2,#}(x,y)
low{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x))
if_low{3,#}(true(),n,add2(m,x)) -> low{2,#}(n,x)
if_low{3,#}(false(),n,add2(m,x)) -> low{2,#}(n,x)
high{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x))
if_high{3,#}(true(),n,add2(m,x)) -> high{2,#}(n,x)
if_high{3,#}(false(),n,add2(m,x)) -> high{2,#}(n,x)
quicksort{1,#}(add2(n,x)) -> high{2,#}(n,x)
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x))
quicksort{1,#}(add2(n,x)) -> low{2,#}(n,x)
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x))
quicksort{1,#}(add2(n,x)) -> app{2,#}(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'#(minus1(x8),x9) -> minus{2,#}(x8,x9)
app'#(quot1(x8),x9) -> quot{2,#}(x8,x9)
app'#(le1(x8),x9) -> le{2,#}(x8,x9)
app'#(app1(x8),x9) -> app{2,#}(x8,x9)
app'#(low1(x8),x9) -> low{2,#}(x8,x9)
app'#(if_low2(x8,x7),x9) -> if_low{3,#}(x8,x7,x9)
app'#(high1(x8),x9) -> high{2,#}(x8,x9)
app'#(if_high2(x8,x7),x9) -> if_high{3,#}(x8,x7,x9)
app'#(quicksort(),x9) -> quicksort{1,#}(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:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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:
minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
quot{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y))
le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
app{2,#}(add2(n,x),y) -> app{2,#}(x,y)
low{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x))
if_low{3,#}(true(),n,add2(m,x)) -> low{2,#}(n,x)
if_low{3,#}(false(),n,add2(m,x)) -> low{2,#}(n,x)
high{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x))
if_high{3,#}(true(),n,add2(m,x)) -> high{2,#}(n,x)
if_high{3,#}(false(),n,add2(m,x)) -> high{2,#}(n,x)
quicksort{1,#}(add2(n,x)) -> high{2,#}(n,x)
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x))
quicksort{1,#}(add2(n,x)) -> low{2,#}(n,x)
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x))
quicksort{1,#}(add2(n,x)) -> app{2,#}(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'#(minus1(x8),x9) -> minus{2,#}(x8,x9)
app'#(quot1(x8),x9) -> quot{2,#}(x8,x9)
app'#(le1(x8),x9) -> le{2,#}(x8,x9)
app'#(app1(x8),x9) -> app{2,#}(x8,x9)
app'#(low1(x8),x9) -> low{2,#}(x8,x9)
app'#(if_low2(x8,x7),x9) -> if_low{3,#}(x8,x7,x9)
app'#(high1(x8),x9) -> high{2,#}(x8,x9)
app'#(if_high2(x8,x7),x9) -> if_high{3,#}(x8,x7,x9)
app'#(quicksort(),x9) -> quicksort{1,#}(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:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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'#(quicksort(),x9) -> quicksort{1,#}(x9)
filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
app'#(if_high2(x8,x7),x9) -> if_high{3,#}(x8,x7,x9)
filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
app'#(high1(x8),x9) -> high{2,#}(x8,x9)
filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
app'#(if_low2(x8,x7),x9) -> if_low{3,#}(x8,x7,x9)
filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
app'#(low1(x8),x9) -> low{2,#}(x8,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'#(quot1(x8),x9) -> quot{2,#}(x8,x9)
filter{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
app'#(minus1(x8),x9) -> minus{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_high2(x8,x7),x9) -> if_high{3,#}(x8,x7,x9) ->
if_high{3,#}(false(),n,add2(m,x)) -> high{2,#}(n,x)
app'#(if_high2(x8,x7),x9) -> if_high{3,#}(x8,x7,x9) ->
if_high{3,#}(true(),n,add2(m,x)) -> high{2,#}(n,x)
app'#(high1(x8),x9) -> high{2,#}(x8,x9) ->
high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x))
app'#(high1(x8),x9) -> high{2,#}(x8,x9) ->
high{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
app'#(if_low2(x8,x7),x9) -> if_low{3,#}(x8,x7,x9) ->
if_low{3,#}(false(),n,add2(m,x)) -> low{2,#}(n,x)
app'#(if_low2(x8,x7),x9) -> if_low{3,#}(x8,x7,x9) ->
if_low{3,#}(true(),n,add2(m,x)) -> low{2,#}(n,x)
app'#(low1(x8),x9) -> low{2,#}(x8,x9) ->
low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x))
app'#(low1(x8),x9) -> low{2,#}(x8,x9) ->
low{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
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'#(quot1(x8),x9) -> quot{2,#}(x8,x9) ->
quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y))
app'#(quot1(x8),x9) -> quot{2,#}(x8,x9) ->
quot{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
app'#(minus1(x8),x9) -> minus{2,#}(x8,x9) ->
minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
app'#(quicksort(),x9) -> quicksort{1,#}(x9) ->
quicksort{1,#}(add2(n,x)) -> app{2,#}(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
app'#(quicksort(),x9) -> quicksort{1,#}(x9) ->
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x))
app'#(quicksort(),x9) -> quicksort{1,#}(x9) ->
quicksort{1,#}(add2(n,x)) -> low{2,#}(n,x)
app'#(quicksort(),x9) -> quicksort{1,#}(x9) ->
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x))
app'#(quicksort(),x9) -> quicksort{1,#}(x9) ->
quicksort{1,#}(add2(n,x)) -> high{2,#}(n,x)
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'#(quicksort(),x9) -> quicksort{1,#}(x9)
map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
app'#(if_high2(x8,x7),x9) -> if_high{3,#}(x8,x7,x9)
map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
app'#(high1(x8),x9) -> high{2,#}(x8,x9)
map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
app'#(if_low2(x8,x7),x9) -> if_low{3,#}(x8,x7,x9)
map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
app'#(low1(x8),x9) -> low{2,#}(x8,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'#(quot1(x8),x9) -> quot{2,#}(x8,x9)
map{2,#}(f,add2(x,xs)) -> app'#(f,x) ->
app'#(minus1(x8),x9) -> minus{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)
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x)) ->
quicksort{1,#}(add2(n,x)) -> app{2,#}(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x)) ->
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x))
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x)) ->
quicksort{1,#}(add2(n,x)) -> low{2,#}(n,x)
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x)) ->
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x))
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x)) ->
quicksort{1,#}(add2(n,x)) -> high{2,#}(n,x)
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x)) ->
quicksort{1,#}(add2(n,x)) -> app{2,#}(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x)) ->
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x))
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x)) ->
quicksort{1,#}(add2(n,x)) -> low{2,#}(n,x)
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x)) ->
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x))
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x)) ->
quicksort{1,#}(add2(n,x)) -> high{2,#}(n,x)
quicksort{1,#}(add2(n,x)) -> high{2,#}(n,x) ->
high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x))
quicksort{1,#}(add2(n,x)) -> high{2,#}(n,x) ->
high{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
quicksort{1,#}(add2(n,x)) -> low{2,#}(n,x) ->
low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x))
quicksort{1,#}(add2(n,x)) -> low{2,#}(n,x) ->
low{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
quicksort{1,#}(add2(n,x)) -> app{2,#}(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x)))) ->
app{2,#}(add2(n,x),y) -> app{2,#}(x,y)
if_high{3,#}(false(),n,add2(m,x)) -> high{2,#}(n,x) ->
high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x))
if_high{3,#}(false(),n,add2(m,x)) -> high{2,#}(n,x) ->
high{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
if_high{3,#}(true(),n,add2(m,x)) -> high{2,#}(n,x) ->
high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x))
if_high{3,#}(true(),n,add2(m,x)) -> high{2,#}(n,x) ->
high{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x)) ->
if_high{3,#}(false(),n,add2(m,x)) -> high{2,#}(n,x)
high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x)) ->
if_high{3,#}(true(),n,add2(m,x)) -> high{2,#}(n,x)
high{2,#}(n,add2(m,x)) -> le{2,#}(m,n) ->
le{2,#}(s1(x),s1(y)) -> le{2,#}(x,y)
if_low{3,#}(false(),n,add2(m,x)) -> low{2,#}(n,x) ->
low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x))
if_low{3,#}(false(),n,add2(m,x)) -> low{2,#}(n,x) ->
low{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
if_low{3,#}(true(),n,add2(m,x)) -> low{2,#}(n,x) ->
low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x))
if_low{3,#}(true(),n,add2(m,x)) -> low{2,#}(n,x) ->
low{2,#}(n,add2(m,x)) -> le{2,#}(m,n)
low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x)) ->
if_low{3,#}(false(),n,add2(m,x)) -> low{2,#}(n,x)
low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x)) ->
if_low{3,#}(true(),n,add2(m,x)) -> low{2,#}(n,x)
low{2,#}(n,add2(m,x)) -> le{2,#}(m,n) ->
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)
quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y)) ->
quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y))
quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y)) ->
quot{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
quot{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y) ->
minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y) -> minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
SCC Processor:
#sccs: 8
#rules: 21
#arcs: 91/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:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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:
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(high2(n,x))
quicksort{1,#}(add2(n,x)) -> quicksort{1,#}(low2(n,x))
TRS:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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)
Open
DPs:
high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x))
if_high{3,#}(true(),n,add2(m,x)) -> high{2,#}(n,x)
if_high{3,#}(false(),n,add2(m,x)) -> high{2,#}(n,x)
TRS:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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(high{2,#}) = 1
pi(if_high{3,#}) = 2
problem:
DPs:
high{2,#}(n,add2(m,x)) -> if_high{3,#}(le2(m,n),n,add2(m,x))
TRS:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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:
low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x))
if_low{3,#}(true(),n,add2(m,x)) -> low{2,#}(n,x)
if_low{3,#}(false(),n,add2(m,x)) -> low{2,#}(n,x)
TRS:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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(low{2,#}) = 1
pi(if_low{3,#}) = 2
problem:
DPs:
low{2,#}(n,add2(m,x)) -> if_low{3,#}(le2(m,n),n,add2(m,x))
TRS:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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:
quot{2,#}(s1(x),s1(y)) -> quot{2,#}(minus2(x,y),s1(y))
TRS:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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)
Matrix Interpretation Processor: dim=1
interpretation:
[quot{2,#}](x0, x1) = x0,
[filter21](x0) = 4x0 + 2,
[filter22](x0, x1) = 3,
[filter24](x0, x1, x2, x3) = 0,
[filter23](x0, x1, x2) = x2,
[filter2](x0, x1) = 0,
[filter1](x0) = 2,
[map2](x0, x1) = x0 + 4x1 + 6,
[map1](x0) = 4x0 + 3,
[quicksort1](x0) = 0,
[if_high1](x0) = 4,
[if_high3](x0, x1, x2) = 4x2,
[if_high2](x0, x1) = 2x1 + 1,
[high2](x0, x1) = 0,
[high1](x0) = 2x0 + 1,
[if_low1](x0) = 1,
[if_low3](x0, x1, x2) = 0,
[if_low2](x0, x1) = 2x1 + 1,
[low2](x0, x1) = 0,
[low1](x0) = 0,
[add2](x0, x1) = 0,
[add1](x0) = 4x0 + 6,
[app2](x0, x1) = 2x1,
[app1](x0) = 2x0 + 1,
[le2](x0, x1) = 2x1,
[le1](x0) = 2x0 + 2,
[quot2](x0, x1) = 4x0 + 1,
[quot1](x0) = 2x0 + 4,
[s1](x0) = 4x0 + 1,
[minus2](x0, x1) = x0,
[minus1](x0) = 4x0 + 5,
[filter2] = 0,
[filter] = 0,
[map] = 0,
[quicksort] = 1,
[if_high] = 0,
[high] = 4,
[if_low] = 0,
[low] = 2,
[add] = 1,
[nil] = 0,
[app] = 0,
[false] = 0,
[true] = 0,
[le] = 6,
[quot] = 3,
[s] = 0,
[0] = 0,
[app'](x0, x1) = 4x0 + 4x1 + 4,
[minus] = 2
orientation:
quot{2,#}(s1(x),s1(y)) = 4x + 1 >= x = quot{2,#}(minus2(x,y),s1(y))
minus2(x,0()) = x >= x = x
minus2(s1(x),s1(y)) = 4x + 1 >= x = minus2(x,y)
quot2(0(),s1(y)) = 1 >= 0 = 0()
quot2(s1(x),s1(y)) = 16x + 5 >= 16x + 5 = s1(quot2(minus2(x,y),s1(y)))
le2(0(),y) = 2y >= 0 = true()
le2(s1(x),0()) = 0 >= 0 = false()
le2(s1(x),s1(y)) = 8y + 2 >= 2y = le2(x,y)
app2(nil(),y) = 2y >= y = y
app2(add2(n,x),y) = 2y >= 0 = add2(n,app2(x,y))
low2(n,nil()) = 0 >= 0 = nil()
low2(n,add2(m,x)) = 0 >= 0 = if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) = 0 >= 0 = add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) = 0 >= 0 = low2(n,x)
high2(n,nil()) = 0 >= 0 = nil()
high2(n,add2(m,x)) = 0 >= 0 = if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) = 0 >= 0 = high2(n,x)
if_high3(false(),n,add2(m,x)) = 0 >= 0 = add2(m,high2(n,x))
quicksort1(nil()) = 0 >= 0 = nil()
quicksort1(add2(n,x)) = 0 >= 0 = app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
map2(f,nil()) = f + 6 >= 0 = nil()
map2(f,add2(x,xs)) = f + 6 >= 0 = add2(app'(f,x),map2(f,xs))
filter2(f,nil()) = 0 >= 0 = nil()
filter2(f,add2(x,xs)) = 0 >= 0 = filter24(app'(f,x),f,x,xs)
filter24(true(),f,x,xs) = 0 >= 0 = add2(x,filter2(f,xs))
filter24(false(),f,x,xs) = 0 >= 0 = filter2(f,xs)
app'(minus1(x8),x9) = 16x8 + 4x9 + 24 >= x8 = minus2(x8,x9)
app'(minus(),x9) = 4x9 + 12 >= 4x9 + 5 = minus1(x9)
app'(s(),x9) = 4x9 + 4 >= 4x9 + 1 = s1(x9)
app'(quot1(x8),x9) = 8x8 + 4x9 + 20 >= 4x8 + 1 = quot2(x8,x9)
app'(quot(),x9) = 4x9 + 16 >= 2x9 + 4 = quot1(x9)
app'(le1(x8),x9) = 8x8 + 4x9 + 12 >= 2x9 = le2(x8,x9)
app'(le(),x9) = 4x9 + 28 >= 2x9 + 2 = le1(x9)
app'(app1(x8),x9) = 8x8 + 4x9 + 8 >= 2x9 = app2(x8,x9)
app'(app(),x9) = 4x9 + 4 >= 2x9 + 1 = app1(x9)
app'(add1(x8),x9) = 16x8 + 4x9 + 28 >= 0 = add2(x8,x9)
app'(add(),x9) = 4x9 + 8 >= 4x9 + 6 = add1(x9)
app'(low1(x8),x9) = 4x9 + 4 >= 0 = low2(x8,x9)
app'(low(),x9) = 4x9 + 12 >= 0 = low1(x9)
app'(if_low2(x8,x7),x9) = 8x7 + 4x9 + 8 >= 0 = if_low3(x8,x7,x9)
app'(if_low1(x8),x9) = 4x9 + 8 >= 2x9 + 1 = if_low2(x8,x9)
app'(if_low(),x9) = 4x9 + 4 >= 1 = if_low1(x9)
app'(high1(x8),x9) = 8x8 + 4x9 + 8 >= 0 = high2(x8,x9)
app'(high(),x9) = 4x9 + 20 >= 2x9 + 1 = high1(x9)
app'(if_high2(x8,x7),x9) = 8x7 + 4x9 + 8 >= 4x9 = if_high3(x8,x7,x9)
app'(if_high1(x8),x9) = 4x9 + 20 >= 2x9 + 1 = if_high2(x8,x9)
app'(if_high(),x9) = 4x9 + 4 >= 4 = if_high1(x9)
app'(quicksort(),x9) = 4x9 + 8 >= 0 = quicksort1(x9)
app'(map1(x8),x9) = 16x8 + 4x9 + 16 >= x8 + 4x9 + 6 = map2(x8,x9)
app'(map(),x9) = 4x9 + 4 >= 4x9 + 3 = map1(x9)
app'(filter1(x8),x9) = 4x9 + 12 >= 0 = filter2(x8,x9)
app'(filter(),x9) = 4x9 + 4 >= 2 = filter1(x9)
app'(filter23(x8,x7,x6),x9) = 4x6 + 4x9 + 4 >= 0 = filter24(x8,x7,x6,x9)
app'(filter22(x8,x7),x9) = 4x9 + 16 >= x9 = filter23(x8,x7,x9)
app'(filter21(x8),x9) = 16x8 + 4x9 + 12 >= 3 = filter22(x8,x9)
app'(filter2(),x9) = 4x9 + 4 >= 4x9 + 2 = filter21(x9)
problem:
DPs:
TRS:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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:
minus{2,#}(s1(x),s1(y)) -> minus{2,#}(x,y)
TRS:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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(minus{2,#}) = 1
problem:
DPs:
TRS:
minus2(x,0()) -> x
minus2(s1(x),s1(y)) -> minus2(x,y)
quot2(0(),s1(y)) -> 0()
quot2(s1(x),s1(y)) -> s1(quot2(minus2(x,y),s1(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))
low2(n,nil()) -> nil()
low2(n,add2(m,x)) -> if_low3(le2(m,n),n,add2(m,x))
if_low3(true(),n,add2(m,x)) -> add2(m,low2(n,x))
if_low3(false(),n,add2(m,x)) -> low2(n,x)
high2(n,nil()) -> nil()
high2(n,add2(m,x)) -> if_high3(le2(m,n),n,add2(m,x))
if_high3(true(),n,add2(m,x)) -> high2(n,x)
if_high3(false(),n,add2(m,x)) -> add2(m,high2(n,x))
quicksort1(nil()) -> nil()
quicksort1(add2(n,x)) -> app2(quicksort1(low2(n,x)),add2(n,quicksort1(high2(n,x))))
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'(minus1(x8),x9) -> minus2(x8,x9)
app'(minus(),x9) -> minus1(x9)
app'(s(),x9) -> s1(x9)
app'(quot1(x8),x9) -> quot2(x8,x9)
app'(quot(),x9) -> quot1(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'(low1(x8),x9) -> low2(x8,x9)
app'(low(),x9) -> low1(x9)
app'(if_low2(x8,x7),x9) -> if_low3(x8,x7,x9)
app'(if_low1(x8),x9) -> if_low2(x8,x9)
app'(if_low(),x9) -> if_low1(x9)
app'(high1(x8),x9) -> high2(x8,x9)
app'(high(),x9) -> high1(x9)
app'(if_high2(x8,x7),x9) -> if_high3(x8,x7,x9)
app'(if_high1(x8),x9) -> if_high2(x8,x9)
app'(if_high(),x9) -> if_high1(x9)
app'(quicksort(),x9) -> quicksort1(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