MAYBE
Problem:
app(app(max(),0()),x) -> x
app(app(max(),x),0()) -> x
app(app(max(),app(s(),x)),app(s(),y)) -> app(app(max(),x),y)
app(app(min(),0()),x) -> 0()
app(app(min(),x),0()) -> 0()
app(app(min(),app(s(),x)),app(s(),y)) -> app(app(min(),x),y)
app(app(app(app(insert(),f),g),nil()),x) -> app(app(cons(),x),nil())
app(app(app(app(insert(),f),g),app(app(cons(),h),t)),x) ->
app(app(cons(),app(app(f,x),h)),app(app(app(app(insert(),f),g),t),app(app(g,x),h)))
app(app(app(sort(),f),g),nil()) -> nil()
app(app(app(sort(),f),g),app(app(cons(),h),t)) ->
app(app(app(app(insert(),f),g),app(app(app(sort(),f),g),t)),h)
app(ascending_sort(),l) -> app(app(app(sort(),min()),max()),l)
app(descending_sort(),l) -> app(app(app(sort(),max()),min()),l)
Proof:
Uncurry Processor:
max2(0(),x) -> x
max2(x,0()) -> x
max2(s1(x),s1(y)) -> max2(x,y)
min2(0(),x) -> 0()
min2(x,0()) -> 0()
min2(s1(x),s1(y)) -> min2(x,y)
insert4(f,g,nil(),x) -> cons2(x,nil())
insert4(f,g,cons2(h,t),x) -> cons2(app(app(f,x),h),insert4(f,g,t,app(app(g,x),h)))
sort3(f,g,nil()) -> nil()
sort3(f,g,cons2(h,t)) -> insert4(f,g,sort3(f,g,t),h)
ascending_sort1(l) -> sort3(min(),max(),l)
descending_sort1(l) -> sort3(max(),min(),l)
app(max1(x9),x10) -> max2(x9,x10)
app(max(),x10) -> max1(x10)
app(s(),x10) -> s1(x10)
app(min1(x9),x10) -> min2(x9,x10)
app(min(),x10) -> min1(x10)
app(insert3(x9,x8,x7),x10) -> insert4(x9,x8,x7,x10)
app(insert2(x9,x8),x10) -> insert3(x9,x8,x10)
app(insert1(x9),x10) -> insert2(x9,x10)
app(insert(),x10) -> insert1(x10)
app(cons1(x9),x10) -> cons2(x9,x10)
app(cons(),x10) -> cons1(x10)
app(sort2(x9,x8),x10) -> sort3(x9,x8,x10)
app(sort1(x9),x10) -> sort2(x9,x10)
app(sort(),x10) -> sort1(x10)
app(ascending_sort(),x10) -> ascending_sort1(x10)
app(descending_sort(),x10) -> descending_sort1(x10)
DP Processor:
DPs:
max{2,#}(s1(x),s1(y)) -> max{2,#}(x,y)
min{2,#}(s1(x),s1(y)) -> min{2,#}(x,y)
insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h)
insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h))
insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h)
sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t)
sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h)
ascending_sort{1,#}(l) -> sort{3,#}(min(),max(),l)
descending_sort{1,#}(l) -> sort{3,#}(max(),min(),l)
app#(max1(x9),x10) -> max{2,#}(x9,x10)
app#(min1(x9),x10) -> min{2,#}(x9,x10)
app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10)
app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10)
app#(ascending_sort(),x10) -> ascending_sort{1,#}(x10)
app#(descending_sort(),x10) -> descending_sort{1,#}(x10)
TRS:
max2(0(),x) -> x
max2(x,0()) -> x
max2(s1(x),s1(y)) -> max2(x,y)
min2(0(),x) -> 0()
min2(x,0()) -> 0()
min2(s1(x),s1(y)) -> min2(x,y)
insert4(f,g,nil(),x) -> cons2(x,nil())
insert4(f,g,cons2(h,t),x) -> cons2(app(app(f,x),h),insert4(f,g,t,app(app(g,x),h)))
sort3(f,g,nil()) -> nil()
sort3(f,g,cons2(h,t)) -> insert4(f,g,sort3(f,g,t),h)
ascending_sort1(l) -> sort3(min(),max(),l)
descending_sort1(l) -> sort3(max(),min(),l)
app(max1(x9),x10) -> max2(x9,x10)
app(max(),x10) -> max1(x10)
app(s(),x10) -> s1(x10)
app(min1(x9),x10) -> min2(x9,x10)
app(min(),x10) -> min1(x10)
app(insert3(x9,x8,x7),x10) -> insert4(x9,x8,x7,x10)
app(insert2(x9,x8),x10) -> insert3(x9,x8,x10)
app(insert1(x9),x10) -> insert2(x9,x10)
app(insert(),x10) -> insert1(x10)
app(cons1(x9),x10) -> cons2(x9,x10)
app(cons(),x10) -> cons1(x10)
app(sort2(x9,x8),x10) -> sort3(x9,x8,x10)
app(sort1(x9),x10) -> sort2(x9,x10)
app(sort(),x10) -> sort1(x10)
app(ascending_sort(),x10) -> ascending_sort1(x10)
app(descending_sort(),x10) -> descending_sort1(x10)
TDG Processor:
DPs:
max{2,#}(s1(x),s1(y)) -> max{2,#}(x,y)
min{2,#}(s1(x),s1(y)) -> min{2,#}(x,y)
insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h)
insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h))
insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h)
sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t)
sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h)
ascending_sort{1,#}(l) -> sort{3,#}(min(),max(),l)
descending_sort{1,#}(l) -> sort{3,#}(max(),min(),l)
app#(max1(x9),x10) -> max{2,#}(x9,x10)
app#(min1(x9),x10) -> min{2,#}(x9,x10)
app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10)
app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10)
app#(ascending_sort(),x10) -> ascending_sort{1,#}(x10)
app#(descending_sort(),x10) -> descending_sort{1,#}(x10)
TRS:
max2(0(),x) -> x
max2(x,0()) -> x
max2(s1(x),s1(y)) -> max2(x,y)
min2(0(),x) -> 0()
min2(x,0()) -> 0()
min2(s1(x),s1(y)) -> min2(x,y)
insert4(f,g,nil(),x) -> cons2(x,nil())
insert4(f,g,cons2(h,t),x) -> cons2(app(app(f,x),h),insert4(f,g,t,app(app(g,x),h)))
sort3(f,g,nil()) -> nil()
sort3(f,g,cons2(h,t)) -> insert4(f,g,sort3(f,g,t),h)
ascending_sort1(l) -> sort3(min(),max(),l)
descending_sort1(l) -> sort3(max(),min(),l)
app(max1(x9),x10) -> max2(x9,x10)
app(max(),x10) -> max1(x10)
app(s(),x10) -> s1(x10)
app(min1(x9),x10) -> min2(x9,x10)
app(min(),x10) -> min1(x10)
app(insert3(x9,x8,x7),x10) -> insert4(x9,x8,x7,x10)
app(insert2(x9,x8),x10) -> insert3(x9,x8,x10)
app(insert1(x9),x10) -> insert2(x9,x10)
app(insert(),x10) -> insert1(x10)
app(cons1(x9),x10) -> cons2(x9,x10)
app(cons(),x10) -> cons1(x10)
app(sort2(x9,x8),x10) -> sort3(x9,x8,x10)
app(sort1(x9),x10) -> sort2(x9,x10)
app(sort(),x10) -> sort1(x10)
app(ascending_sort(),x10) -> ascending_sort1(x10)
app(descending_sort(),x10) -> descending_sort1(x10)
graph:
descending_sort{1,#}(l) -> sort{3,#}(max(),min(),l) ->
sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h)
descending_sort{1,#}(l) -> sort{3,#}(max(),min(),l) ->
sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t)
ascending_sort{1,#}(l) -> sort{3,#}(min(),max(),l) ->
sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h)
ascending_sort{1,#}(l) -> sort{3,#}(min(),max(),l) ->
sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t)
sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t) ->
sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h)
sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t) ->
sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t)
sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h) ->
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h)
sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h) ->
insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x)
sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h) ->
insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h))
sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h) ->
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h)
sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h) ->
insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x)
app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10) ->
sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h)
app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10) ->
sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t)
app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10) ->
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h)
app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10) ->
insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x)
app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10) ->
insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h))
app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10) ->
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h)
app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10) ->
insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x)
app#(min1(x9),x10) -> min{2,#}(x9,x10) ->
min{2,#}(s1(x),s1(y)) -> min{2,#}(x,y)
app#(max1(x9),x10) -> max{2,#}(x9,x10) ->
max{2,#}(s1(x),s1(y)) -> max{2,#}(x,y)
app#(descending_sort(),x10) -> descending_sort{1,#}(x10) ->
descending_sort{1,#}(l) -> sort{3,#}(max(),min(),l)
app#(ascending_sort(),x10) -> ascending_sort{1,#}(x10) ->
ascending_sort{1,#}(l) -> sort{3,#}(min(),max(),l)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h) ->
app#(descending_sort(),x10) -> descending_sort{1,#}(x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h) ->
app#(ascending_sort(),x10) -> ascending_sort{1,#}(x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h) ->
app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h) ->
app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h) ->
app#(min1(x9),x10) -> min{2,#}(x9,x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h) ->
app#(max1(x9),x10) -> max{2,#}(x9,x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h) ->
app#(descending_sort(),x10) -> descending_sort{1,#}(x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h) ->
app#(ascending_sort(),x10) -> ascending_sort{1,#}(x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h) ->
app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h) ->
app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h) ->
app#(min1(x9),x10) -> min{2,#}(x9,x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h) ->
app#(max1(x9),x10) -> max{2,#}(x9,x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x) ->
app#(descending_sort(),x10) -> descending_sort{1,#}(x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x) ->
app#(ascending_sort(),x10) -> ascending_sort{1,#}(x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x) ->
app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x) ->
app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x) ->
app#(min1(x9),x10) -> min{2,#}(x9,x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x) ->
app#(max1(x9),x10) -> max{2,#}(x9,x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x) ->
app#(descending_sort(),x10) -> descending_sort{1,#}(x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x) ->
app#(ascending_sort(),x10) -> ascending_sort{1,#}(x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x) ->
app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x) ->
app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x) ->
app#(min1(x9),x10) -> min{2,#}(x9,x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x) ->
app#(max1(x9),x10) -> max{2,#}(x9,x10)
insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h)) ->
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h)
insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h)) ->
insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x)
insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h)) ->
insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h))
insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h)) ->
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h)
insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h)) ->
insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x)
min{2,#}(s1(x),s1(y)) -> min{2,#}(x,y) ->
min{2,#}(s1(x),s1(y)) -> min{2,#}(x,y)
max{2,#}(s1(x),s1(y)) -> max{2,#}(x,y) -> max{2,#}(s1(x),s1(y)) -> max{2,#}(x,y)
SCC Processor:
#sccs: 3
#rules: 15
#arcs: 53/289
DPs:
descending_sort{1,#}(l) -> sort{3,#}(max(),min(),l)
sort{3,#}(f,g,cons2(h,t)) -> sort{3,#}(f,g,t)
sort{3,#}(f,g,cons2(h,t)) -> insert{4,#}(f,g,sort3(f,g,t),h)
insert{4,#}(f,g,cons2(h,t),x) -> app#(g,x)
app#(insert3(x9,x8,x7),x10) -> insert{4,#}(x9,x8,x7,x10)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(g,x),h)
app#(sort2(x9,x8),x10) -> sort{3,#}(x9,x8,x10)
app#(ascending_sort(),x10) -> ascending_sort{1,#}(x10)
ascending_sort{1,#}(l) -> sort{3,#}(min(),max(),l)
app#(descending_sort(),x10) -> descending_sort{1,#}(x10)
insert{4,#}(f,g,cons2(h,t),x) -> insert{4,#}(f,g,t,app(app(g,x),h))
insert{4,#}(f,g,cons2(h,t),x) -> app#(f,x)
insert{4,#}(f,g,cons2(h,t),x) -> app#(app(f,x),h)
TRS:
max2(0(),x) -> x
max2(x,0()) -> x
max2(s1(x),s1(y)) -> max2(x,y)
min2(0(),x) -> 0()
min2(x,0()) -> 0()
min2(s1(x),s1(y)) -> min2(x,y)
insert4(f,g,nil(),x) -> cons2(x,nil())
insert4(f,g,cons2(h,t),x) -> cons2(app(app(f,x),h),insert4(f,g,t,app(app(g,x),h)))
sort3(f,g,nil()) -> nil()
sort3(f,g,cons2(h,t)) -> insert4(f,g,sort3(f,g,t),h)
ascending_sort1(l) -> sort3(min(),max(),l)
descending_sort1(l) -> sort3(max(),min(),l)
app(max1(x9),x10) -> max2(x9,x10)
app(max(),x10) -> max1(x10)
app(s(),x10) -> s1(x10)
app(min1(x9),x10) -> min2(x9,x10)
app(min(),x10) -> min1(x10)
app(insert3(x9,x8,x7),x10) -> insert4(x9,x8,x7,x10)
app(insert2(x9,x8),x10) -> insert3(x9,x8,x10)
app(insert1(x9),x10) -> insert2(x9,x10)
app(insert(),x10) -> insert1(x10)
app(cons1(x9),x10) -> cons2(x9,x10)
app(cons(),x10) -> cons1(x10)
app(sort2(x9,x8),x10) -> sort3(x9,x8,x10)
app(sort1(x9),x10) -> sort2(x9,x10)
app(sort(),x10) -> sort1(x10)
app(ascending_sort(),x10) -> ascending_sort1(x10)
app(descending_sort(),x10) -> descending_sort1(x10)
Open
DPs:
min{2,#}(s1(x),s1(y)) -> min{2,#}(x,y)
TRS:
max2(0(),x) -> x
max2(x,0()) -> x
max2(s1(x),s1(y)) -> max2(x,y)
min2(0(),x) -> 0()
min2(x,0()) -> 0()
min2(s1(x),s1(y)) -> min2(x,y)
insert4(f,g,nil(),x) -> cons2(x,nil())
insert4(f,g,cons2(h,t),x) -> cons2(app(app(f,x),h),insert4(f,g,t,app(app(g,x),h)))
sort3(f,g,nil()) -> nil()
sort3(f,g,cons2(h,t)) -> insert4(f,g,sort3(f,g,t),h)
ascending_sort1(l) -> sort3(min(),max(),l)
descending_sort1(l) -> sort3(max(),min(),l)
app(max1(x9),x10) -> max2(x9,x10)
app(max(),x10) -> max1(x10)
app(s(),x10) -> s1(x10)
app(min1(x9),x10) -> min2(x9,x10)
app(min(),x10) -> min1(x10)
app(insert3(x9,x8,x7),x10) -> insert4(x9,x8,x7,x10)
app(insert2(x9,x8),x10) -> insert3(x9,x8,x10)
app(insert1(x9),x10) -> insert2(x9,x10)
app(insert(),x10) -> insert1(x10)
app(cons1(x9),x10) -> cons2(x9,x10)
app(cons(),x10) -> cons1(x10)
app(sort2(x9,x8),x10) -> sort3(x9,x8,x10)
app(sort1(x9),x10) -> sort2(x9,x10)
app(sort(),x10) -> sort1(x10)
app(ascending_sort(),x10) -> ascending_sort1(x10)
app(descending_sort(),x10) -> descending_sort1(x10)
Subterm Criterion Processor:
simple projection:
pi(min{2,#}) = 1
problem:
DPs:
TRS:
max2(0(),x) -> x
max2(x,0()) -> x
max2(s1(x),s1(y)) -> max2(x,y)
min2(0(),x) -> 0()
min2(x,0()) -> 0()
min2(s1(x),s1(y)) -> min2(x,y)
insert4(f,g,nil(),x) -> cons2(x,nil())
insert4(f,g,cons2(h,t),x) -> cons2(app(app(f,x),h),insert4(f,g,t,app(app(g,x),h)))
sort3(f,g,nil()) -> nil()
sort3(f,g,cons2(h,t)) -> insert4(f,g,sort3(f,g,t),h)
ascending_sort1(l) -> sort3(min(),max(),l)
descending_sort1(l) -> sort3(max(),min(),l)
app(max1(x9),x10) -> max2(x9,x10)
app(max(),x10) -> max1(x10)
app(s(),x10) -> s1(x10)
app(min1(x9),x10) -> min2(x9,x10)
app(min(),x10) -> min1(x10)
app(insert3(x9,x8,x7),x10) -> insert4(x9,x8,x7,x10)
app(insert2(x9,x8),x10) -> insert3(x9,x8,x10)
app(insert1(x9),x10) -> insert2(x9,x10)
app(insert(),x10) -> insert1(x10)
app(cons1(x9),x10) -> cons2(x9,x10)
app(cons(),x10) -> cons1(x10)
app(sort2(x9,x8),x10) -> sort3(x9,x8,x10)
app(sort1(x9),x10) -> sort2(x9,x10)
app(sort(),x10) -> sort1(x10)
app(ascending_sort(),x10) -> ascending_sort1(x10)
app(descending_sort(),x10) -> descending_sort1(x10)
Qed
DPs:
max{2,#}(s1(x),s1(y)) -> max{2,#}(x,y)
TRS:
max2(0(),x) -> x
max2(x,0()) -> x
max2(s1(x),s1(y)) -> max2(x,y)
min2(0(),x) -> 0()
min2(x,0()) -> 0()
min2(s1(x),s1(y)) -> min2(x,y)
insert4(f,g,nil(),x) -> cons2(x,nil())
insert4(f,g,cons2(h,t),x) -> cons2(app(app(f,x),h),insert4(f,g,t,app(app(g,x),h)))
sort3(f,g,nil()) -> nil()
sort3(f,g,cons2(h,t)) -> insert4(f,g,sort3(f,g,t),h)
ascending_sort1(l) -> sort3(min(),max(),l)
descending_sort1(l) -> sort3(max(),min(),l)
app(max1(x9),x10) -> max2(x9,x10)
app(max(),x10) -> max1(x10)
app(s(),x10) -> s1(x10)
app(min1(x9),x10) -> min2(x9,x10)
app(min(),x10) -> min1(x10)
app(insert3(x9,x8,x7),x10) -> insert4(x9,x8,x7,x10)
app(insert2(x9,x8),x10) -> insert3(x9,x8,x10)
app(insert1(x9),x10) -> insert2(x9,x10)
app(insert(),x10) -> insert1(x10)
app(cons1(x9),x10) -> cons2(x9,x10)
app(cons(),x10) -> cons1(x10)
app(sort2(x9,x8),x10) -> sort3(x9,x8,x10)
app(sort1(x9),x10) -> sort2(x9,x10)
app(sort(),x10) -> sort1(x10)
app(ascending_sort(),x10) -> ascending_sort1(x10)
app(descending_sort(),x10) -> descending_sort1(x10)
Subterm Criterion Processor:
simple projection:
pi(max{2,#}) = 1
problem:
DPs:
TRS:
max2(0(),x) -> x
max2(x,0()) -> x
max2(s1(x),s1(y)) -> max2(x,y)
min2(0(),x) -> 0()
min2(x,0()) -> 0()
min2(s1(x),s1(y)) -> min2(x,y)
insert4(f,g,nil(),x) -> cons2(x,nil())
insert4(f,g,cons2(h,t),x) -> cons2(app(app(f,x),h),insert4(f,g,t,app(app(g,x),h)))
sort3(f,g,nil()) -> nil()
sort3(f,g,cons2(h,t)) -> insert4(f,g,sort3(f,g,t),h)
ascending_sort1(l) -> sort3(min(),max(),l)
descending_sort1(l) -> sort3(max(),min(),l)
app(max1(x9),x10) -> max2(x9,x10)
app(max(),x10) -> max1(x10)
app(s(),x10) -> s1(x10)
app(min1(x9),x10) -> min2(x9,x10)
app(min(),x10) -> min1(x10)
app(insert3(x9,x8,x7),x10) -> insert4(x9,x8,x7,x10)
app(insert2(x9,x8),x10) -> insert3(x9,x8,x10)
app(insert1(x9),x10) -> insert2(x9,x10)
app(insert(),x10) -> insert1(x10)
app(cons1(x9),x10) -> cons2(x9,x10)
app(cons(),x10) -> cons1(x10)
app(sort2(x9,x8),x10) -> sort3(x9,x8,x10)
app(sort1(x9),x10) -> sort2(x9,x10)
app(sort(),x10) -> sort1(x10)
app(ascending_sort(),x10) -> ascending_sort1(x10)
app(descending_sort(),x10) -> descending_sort1(x10)
Qed