MAYBE
Problem:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(get(n,cons(x,xs)),
qs(half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
Proof:
DP Processor:
DPs:
qsort#(xs) -> length#(xs)
qsort#(xs) -> half#(length(xs))
qsort#(xs) -> qs#(half(length(xs)),xs)
qs#(n,cons(x,xs)) -> filterhigh#(get(n,cons(x,xs)),cons(x,xs))
qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs)))
qs#(n,cons(x,xs)) -> get#(n,cons(x,xs))
qs#(n,cons(x,xs)) -> filterlow#(get(n,cons(x,xs)),cons(x,xs))
qs#(n,cons(x,xs)) -> half#(n)
qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs)))
qs#(n,cons(x,xs)) ->
append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(get(n,cons(x,xs)),
qs
(
half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow#(n,cons(x,xs)) -> ge#(n,x)
filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
if1#(true(),n,x,xs) -> filterlow#(n,xs)
if1#(false(),n,x,xs) -> filterlow#(n,xs)
filterhigh#(n,cons(x,xs)) -> ge#(x,n)
filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
if2#(true(),n,x,xs) -> filterhigh#(n,xs)
if2#(false(),n,x,xs) -> filterhigh#(n,xs)
ge#(s(x),s(y)) -> ge#(x,y)
append#(cons(x,xs),ys()) -> append#(xs,ys())
length#(cons(x,xs)) -> length#(xs)
half#(s(s(x))) -> half#(x)
get#(s(n),cons(x,cons(y,xs))) -> get#(n,cons(y,xs))
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(get(n,cons(x,xs)),
qs
(half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
TDG Processor:
DPs:
qsort#(xs) -> length#(xs)
qsort#(xs) -> half#(length(xs))
qsort#(xs) -> qs#(half(length(xs)),xs)
qs#(n,cons(x,xs)) -> filterhigh#(get(n,cons(x,xs)),cons(x,xs))
qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs)))
qs#(n,cons(x,xs)) -> get#(n,cons(x,xs))
qs#(n,cons(x,xs)) -> filterlow#(get(n,cons(x,xs)),cons(x,xs))
qs#(n,cons(x,xs)) -> half#(n)
qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs)))
qs#(n,cons(x,xs)) ->
append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(
get(n,cons(x,xs)),
qs
(
half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow#(n,cons(x,xs)) -> ge#(n,x)
filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
if1#(true(),n,x,xs) -> filterlow#(n,xs)
if1#(false(),n,x,xs) -> filterlow#(n,xs)
filterhigh#(n,cons(x,xs)) -> ge#(x,n)
filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
if2#(true(),n,x,xs) -> filterhigh#(n,xs)
if2#(false(),n,x,xs) -> filterhigh#(n,xs)
ge#(s(x),s(y)) -> ge#(x,y)
append#(cons(x,xs),ys()) -> append#(xs,ys())
length#(cons(x,xs)) -> length#(xs)
half#(s(s(x))) -> half#(x)
get#(s(n),cons(x,cons(y,xs))) -> get#(n,cons(y,xs))
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(get(n,cons(x,xs)),
qs
(
half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
graph:
if2#(false(),n,x,xs) -> filterhigh#(n,xs) ->
filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
if2#(false(),n,x,xs) -> filterhigh#(n,xs) ->
filterhigh#(n,cons(x,xs)) -> ge#(x,n)
if2#(true(),n,x,xs) -> filterhigh#(n,xs) ->
filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
if2#(true(),n,x,xs) -> filterhigh#(n,xs) ->
filterhigh#(n,cons(x,xs)) -> ge#(x,n)
if1#(false(),n,x,xs) -> filterlow#(n,xs) ->
filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
if1#(false(),n,x,xs) -> filterlow#(n,xs) ->
filterlow#(n,cons(x,xs)) -> ge#(n,x)
if1#(true(),n,x,xs) -> filterlow#(n,xs) ->
filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
if1#(true(),n,x,xs) -> filterlow#(n,xs) ->
filterlow#(n,cons(x,xs)) -> ge#(n,x)
ge#(s(x),s(y)) -> ge#(x,y) ->
ge#(s(x),s(y)) -> ge#(x,y)
append#(cons(x,xs),ys()) -> append#(xs,ys()) ->
append#(cons(x,xs),ys()) -> append#(xs,ys())
filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs) ->
if1#(false(),n,x,xs) -> filterlow#(n,xs)
filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs) ->
if1#(true(),n,x,xs) -> filterlow#(n,xs)
filterlow#(n,cons(x,xs)) -> ge#(n,x) ->
ge#(s(x),s(y)) -> ge#(x,y)
get#(s(n),cons(x,cons(y,xs))) -> get#(n,cons(y,xs)) ->
get#(s(n),cons(x,cons(y,xs))) -> get#(n,cons(y,xs))
filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs) ->
if2#(false(),n,x,xs) -> filterhigh#(n,xs)
filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs) ->
if2#(true(),n,x,xs) -> filterhigh#(n,xs)
filterhigh#(n,cons(x,xs)) -> ge#(x,n) ->
ge#(s(x),s(y)) -> ge#(x,y)
qs#(n,cons(x,xs)) ->
append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(
get(n,cons(x,xs)),
qs
(
half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
->
append#(cons(x,xs),ys()) -> append#(xs,ys())
qs#(n,cons(x,xs)) -> filterlow#(get(n,cons(x,xs)),cons(x,xs)) ->
filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
qs#(n,cons(x,xs)) -> filterlow#(get(n,cons(x,xs)),cons(x,xs)) ->
filterlow#(n,cons(x,xs)) -> ge#(n,x)
qs#(n,cons(x,xs)) -> get#(n,cons(x,xs)) ->
get#(s(n),cons(x,cons(y,xs))) -> get#(n,cons(y,xs))
qs#(n,cons(x,xs)) -> filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ->
filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
qs#(n,cons(x,xs)) -> filterhigh#(get(n,cons(x,xs)),cons(x,xs)) ->
filterhigh#(n,cons(x,xs)) -> ge#(x,n)
qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ->
qs#(n,cons(x,xs)) ->
append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(
get(n,cons(x,xs)),
qs
(
half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ->
qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs)))
qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ->
qs#(n,cons(x,xs)) -> half#(n)
qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ->
qs#(n,cons(x,xs)) -> filterlow#(get(n,cons(x,xs)),cons(x,xs))
qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ->
qs#(n,cons(x,xs)) -> get#(n,cons(x,xs))
qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ->
qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs)))
qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs))) ->
qs#(n,cons(x,xs)) -> filterhigh#(get(n,cons(x,xs)),cons(x,xs))
qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ->
qs#(n,cons(x,xs)) ->
append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(
get(n,cons(x,xs)),
qs
(
half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ->
qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs)))
qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ->
qs#(n,cons(x,xs)) -> half#(n)
qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ->
qs#(n,cons(x,xs)) -> filterlow#(get(n,cons(x,xs)),cons(x,xs))
qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ->
qs#(n,cons(x,xs)) -> get#(n,cons(x,xs))
qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ->
qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs)))
qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))) ->
qs#(n,cons(x,xs)) -> filterhigh#(get(n,cons(x,xs)),cons(x,xs))
qs#(n,cons(x,xs)) -> half#(n) -> half#(s(s(x))) -> half#(x)
half#(s(s(x))) -> half#(x) -> half#(s(s(x))) -> half#(x)
length#(cons(x,xs)) -> length#(xs) ->
length#(cons(x,xs)) -> length#(xs)
qsort#(xs) -> qs#(half(length(xs)),xs) ->
qs#(n,cons(x,xs)) ->
append#(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(
get(n,cons(x,xs)),
qs
(
half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
qsort#(xs) -> qs#(half(length(xs)),xs) ->
qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs)))
qsort#(xs) -> qs#(half(length(xs)),xs) ->
qs#(n,cons(x,xs)) -> half#(n)
qsort#(xs) -> qs#(half(length(xs)),xs) ->
qs#(n,cons(x,xs)) -> filterlow#(get(n,cons(x,xs)),cons(x,xs))
qsort#(xs) -> qs#(half(length(xs)),xs) ->
qs#(n,cons(x,xs)) -> get#(n,cons(x,xs))
qsort#(xs) -> qs#(half(length(xs)),xs) ->
qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs)))
qsort#(xs) -> qs#(half(length(xs)),xs) ->
qs#(n,cons(x,xs)) -> filterhigh#(get(n,cons(x,xs)),cons(x,xs))
qsort#(xs) -> half#(length(xs)) -> half#(s(s(x))) -> half#(x)
qsort#(xs) -> length#(xs) -> length#(cons(x,xs)) -> length#(xs)
SCC Processor:
#sccs: 8
#rules: 13
#arcs: 49/529
DPs:
length#(cons(x,xs)) -> length#(xs)
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(
get(n,cons(x,xs)),
qs
(
half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
Subterm Criterion Processor:
simple projection:
pi(length#) = 0
problem:
DPs:
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons
(get(n,cons(x,xs)),
qs
(half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
Qed
DPs:
qs#(n,cons(x,xs)) -> qs#(half(n),filterhigh(get(n,cons(x,xs)),cons(x,xs)))
qs#(n,cons(x,xs)) -> qs#(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs)))
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(
get(n,cons(x,xs)),
qs
(
half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
Open
DPs:
half#(s(s(x))) -> half#(x)
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(
get(n,cons(x,xs)),
qs
(
half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
Subterm Criterion Processor:
simple projection:
pi(half#) = 0
problem:
DPs:
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons
(get(n,cons(x,xs)),
qs
(half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
Qed
DPs:
get#(s(n),cons(x,cons(y,xs))) -> get#(n,cons(y,xs))
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(
get(n,cons(x,xs)),
qs
(
half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
Subterm Criterion Processor:
simple projection:
pi(get#) = 1
problem:
DPs:
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons
(get(n,cons(x,xs)),
qs
(half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
Qed
DPs:
append#(cons(x,xs),ys()) -> append#(xs,ys())
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(
get(n,cons(x,xs)),
qs
(
half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
Subterm Criterion Processor:
simple projection:
pi(append#) = 0
problem:
DPs:
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons
(get(n,cons(x,xs)),
qs
(half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
Qed
DPs:
if1#(false(),n,x,xs) -> filterlow#(n,xs)
filterlow#(n,cons(x,xs)) -> if1#(ge(n,x),n,x,xs)
if1#(true(),n,x,xs) -> filterlow#(n,xs)
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(
get(n,cons(x,xs)),
qs
(
half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
Subterm Criterion Processor:
simple projection:
pi(filterlow#) = 1
pi(if1#) = 3
problem:
DPs:
if1#(false(),n,x,xs) -> filterlow#(n,xs)
if1#(true(),n,x,xs) -> filterlow#(n,xs)
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons
(get(n,cons(x,xs)),
qs
(half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
SCC Processor:
#sccs: 0
#rules: 0
#arcs: 4/4
DPs:
if2#(false(),n,x,xs) -> filterhigh#(n,xs)
filterhigh#(n,cons(x,xs)) -> if2#(ge(x,n),n,x,xs)
if2#(true(),n,x,xs) -> filterhigh#(n,xs)
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(
get(n,cons(x,xs)),
qs
(
half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
Subterm Criterion Processor:
simple projection:
pi(filterhigh#) = 1
pi(if2#) = 3
problem:
DPs:
if2#(false(),n,x,xs) -> filterhigh#(n,xs)
if2#(true(),n,x,xs) -> filterhigh#(n,xs)
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons
(get(n,cons(x,xs)),
qs
(half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
SCC Processor:
#sccs: 0
#rules: 0
#arcs: 4/4
DPs:
ge#(s(x),s(y)) -> ge#(x,y)
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons(
get(n,cons(x,xs)),
qs
(
half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
Subterm Criterion Processor:
simple projection:
pi(ge#) = 1
problem:
DPs:
TRS:
qsort(xs) -> qs(half(length(xs)),xs)
qs(n,nil()) -> nil()
qs(n,cons(x,xs)) ->
append(qs(half(n),filterlow(get(n,cons(x,xs)),cons(x,xs))),cons
(get(n,cons(x,xs)),
qs
(half(n),
filterhigh
(
get(n,cons(x,xs)),cons(x,xs)))))
filterlow(n,nil()) -> nil()
filterlow(n,cons(x,xs)) -> if1(ge(n,x),n,x,xs)
if1(true(),n,x,xs) -> filterlow(n,xs)
if1(false(),n,x,xs) -> cons(x,filterlow(n,xs))
filterhigh(n,nil()) -> nil()
filterhigh(n,cons(x,xs)) -> if2(ge(x,n),n,x,xs)
if2(true(),n,x,xs) -> filterhigh(n,xs)
if2(false(),n,x,xs) -> cons(x,filterhigh(n,xs))
ge(x,0()) -> true()
ge(0(),s(x)) -> false()
ge(s(x),s(y)) -> ge(x,y)
append(nil(),ys()) -> ys()
append(cons(x,xs),ys()) -> cons(x,append(xs,ys()))
length(nil()) -> 0()
length(cons(x,xs)) -> s(length(xs))
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
get(n,nil()) -> 0()
get(n,cons(x,nil())) -> x
get(0(),cons(x,cons(y,xs))) -> x
get(s(n),cons(x,cons(y,xs))) -> get(n,cons(y,xs))
Qed