YES Problem: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) Proof: DP Processor: DPs: eq#(s(X),s(Y)) -> eq#(X,Y) le#(s(X),s(Y)) -> le#(X,Y) min#(cons(N,cons(M,L))) -> le#(N,M) min#(cons(N,cons(M,L))) -> ifmin#(le(N,M),cons(N,cons(M,L))) ifmin#(true(),cons(N,cons(M,L))) -> min#(cons(N,L)) ifmin#(false(),cons(N,cons(M,L))) -> min#(cons(M,L)) replace#(N,M,cons(K,L)) -> eq#(N,K) replace#(N,M,cons(K,L)) -> ifrepl#(eq(N,K),N,M,cons(K,L)) ifrepl#(false(),N,M,cons(K,L)) -> replace#(N,M,L) selsort#(cons(N,L)) -> min#(cons(N,L)) selsort#(cons(N,L)) -> eq#(N,min(cons(N,L))) selsort#(cons(N,L)) -> ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) ifselsort#(true(),cons(N,L)) -> selsort#(L) ifselsort#(false(),cons(N,L)) -> replace#(min(cons(N,L)),N,L) ifselsort#(false(),cons(N,L)) -> selsort#(replace(min(cons(N,L)),N,L)) ifselsort#(false(),cons(N,L)) -> min#(cons(N,L)) TRS: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) EDG Processor: DPs: eq#(s(X),s(Y)) -> eq#(X,Y) le#(s(X),s(Y)) -> le#(X,Y) min#(cons(N,cons(M,L))) -> le#(N,M) min#(cons(N,cons(M,L))) -> ifmin#(le(N,M),cons(N,cons(M,L))) ifmin#(true(),cons(N,cons(M,L))) -> min#(cons(N,L)) ifmin#(false(),cons(N,cons(M,L))) -> min#(cons(M,L)) replace#(N,M,cons(K,L)) -> eq#(N,K) replace#(N,M,cons(K,L)) -> ifrepl#(eq(N,K),N,M,cons(K,L)) ifrepl#(false(),N,M,cons(K,L)) -> replace#(N,M,L) selsort#(cons(N,L)) -> min#(cons(N,L)) selsort#(cons(N,L)) -> eq#(N,min(cons(N,L))) selsort#(cons(N,L)) -> ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) ifselsort#(true(),cons(N,L)) -> selsort#(L) ifselsort#(false(),cons(N,L)) -> replace#(min(cons(N,L)),N,L) ifselsort#(false(),cons(N,L)) -> selsort#(replace(min(cons(N,L)),N,L)) ifselsort#(false(),cons(N,L)) -> min#(cons(N,L)) TRS: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) graph: ifselsort#(false(),cons(N,L)) -> selsort#(replace(min(cons(N,L)),N,L)) -> selsort#(cons(N,L)) -> min#(cons(N,L)) ifselsort#(false(),cons(N,L)) -> selsort#(replace(min(cons(N,L)),N,L)) -> selsort#(cons(N,L)) -> eq#(N,min(cons(N,L))) ifselsort#(false(),cons(N,L)) -> selsort#(replace(min(cons(N,L)),N,L)) -> selsort#(cons(N,L)) -> ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) ifselsort#(false(),cons(N,L)) -> replace#(min(cons(N,L)),N,L) -> replace#(N,M,cons(K,L)) -> eq#(N,K) ifselsort#(false(),cons(N,L)) -> replace#(min(cons(N,L)),N,L) -> replace#(N,M,cons(K,L)) -> ifrepl#(eq(N,K),N,M,cons(K,L)) ifselsort#(false(),cons(N,L)) -> min#(cons(N,L)) -> min#(cons(N,cons(M,L))) -> le#(N,M) ifselsort#(false(),cons(N,L)) -> min#(cons(N,L)) -> min#(cons(N,cons(M,L))) -> ifmin#(le(N,M),cons(N,cons(M,L))) ifselsort#(true(),cons(N,L)) -> selsort#(L) -> selsort#(cons(N,L)) -> min#(cons(N,L)) ifselsort#(true(),cons(N,L)) -> selsort#(L) -> selsort#(cons(N,L)) -> eq#(N,min(cons(N,L))) ifselsort#(true(),cons(N,L)) -> selsort#(L) -> selsort#(cons(N,L)) -> ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) selsort#(cons(N,L)) -> ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) -> ifselsort#(true(),cons(N,L)) -> selsort#(L) selsort#(cons(N,L)) -> ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) -> ifselsort#(false(),cons(N,L)) -> replace#(min(cons(N,L)),N,L) selsort#(cons(N,L)) -> ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) -> ifselsort#(false(),cons(N,L)) -> selsort#(replace(min(cons(N,L)),N,L)) selsort#(cons(N,L)) -> ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) -> ifselsort#(false(),cons(N,L)) -> min#(cons(N,L)) selsort#(cons(N,L)) -> min#(cons(N,L)) -> min#(cons(N,cons(M,L))) -> le#(N,M) selsort#(cons(N,L)) -> min#(cons(N,L)) -> min#(cons(N,cons(M,L))) -> ifmin#(le(N,M),cons(N,cons(M,L))) selsort#(cons(N,L)) -> eq#(N,min(cons(N,L))) -> eq#(s(X),s(Y)) -> eq#(X,Y) ifrepl#(false(),N,M,cons(K,L)) -> replace#(N,M,L) -> replace#(N,M,cons(K,L)) -> eq#(N,K) ifrepl#(false(),N,M,cons(K,L)) -> replace#(N,M,L) -> replace#(N,M,cons(K,L)) -> ifrepl#(eq(N,K),N,M,cons(K,L)) replace#(N,M,cons(K,L)) -> ifrepl#(eq(N,K),N,M,cons(K,L)) -> ifrepl#(false(),N,M,cons(K,L)) -> replace#(N,M,L) replace#(N,M,cons(K,L)) -> eq#(N,K) -> eq#(s(X),s(Y)) -> eq#(X,Y) ifmin#(false(),cons(N,cons(M,L))) -> min#(cons(M,L)) -> min#(cons(N,cons(M,L))) -> le#(N,M) ifmin#(false(),cons(N,cons(M,L))) -> min#(cons(M,L)) -> min#(cons(N,cons(M,L))) -> ifmin#(le(N,M),cons(N,cons(M,L))) ifmin#(true(),cons(N,cons(M,L))) -> min#(cons(N,L)) -> min#(cons(N,cons(M,L))) -> le#(N,M) ifmin#(true(),cons(N,cons(M,L))) -> min#(cons(N,L)) -> min#(cons(N,cons(M,L))) -> ifmin#(le(N,M),cons(N,cons(M,L))) min#(cons(N,cons(M,L))) -> ifmin#(le(N,M),cons(N,cons(M,L))) -> ifmin#(true(),cons(N,cons(M,L))) -> min#(cons(N,L)) min#(cons(N,cons(M,L))) -> ifmin#(le(N,M),cons(N,cons(M,L))) -> ifmin#(false(),cons(N,cons(M,L))) -> min#(cons(M,L)) min#(cons(N,cons(M,L))) -> le#(N,M) -> le#(s(X),s(Y)) -> le#(X,Y) le#(s(X),s(Y)) -> le#(X,Y) -> le#(s(X),s(Y)) -> le#(X,Y) eq#(s(X),s(Y)) -> eq#(X,Y) -> eq#(s(X),s(Y)) -> eq#(X,Y) SCC Processor: #sccs: 5 #rules: 10 #arcs: 30/256 DPs: ifselsort#(false(),cons(N,L)) -> selsort#(replace(min(cons(N,L)),N,L)) selsort#(cons(N,L)) -> ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) ifselsort#(true(),cons(N,L)) -> selsort#(L) TRS: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) Matrix Interpretation Processor: dimension: 1 interpretation: [ifselsort#](x0, x1) = x0 + x1, [selsort#](x0) = x0 + 1, [ifselsort](x0, x1) = x1, [selsort](x0) = x0, [ifrepl](x0, x1, x2, x3) = x3, [replace](x0, x1, x2) = x2, [ifmin](x0, x1) = 0, [min](x0) = 0, [cons](x0, x1) = x1 + 1, [nil] = 0, [le](x0, x1) = 1, [false] = 0, [s](x0) = 0, [true] = 1, [eq](x0, x1) = 1, [0] = 0 orientation: ifselsort#(false(),cons(N,L)) = L + 1 >= L + 1 = selsort#(replace(min(cons(N,L)),N,L)) selsort#(cons(N,L)) = L + 2 >= L + 2 = ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) ifselsort#(true(),cons(N,L)) = L + 2 >= L + 1 = selsort#(L) eq(0(),0()) = 1 >= 1 = true() eq(0(),s(Y)) = 1 >= 0 = false() eq(s(X),0()) = 1 >= 0 = false() eq(s(X),s(Y)) = 1 >= 1 = eq(X,Y) le(0(),Y) = 1 >= 1 = true() le(s(X),0()) = 1 >= 0 = false() le(s(X),s(Y)) = 1 >= 1 = le(X,Y) min(cons(0(),nil())) = 0 >= 0 = 0() min(cons(s(N),nil())) = 0 >= 0 = s(N) min(cons(N,cons(M,L))) = 0 >= 0 = ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) = 0 >= 0 = min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) = 0 >= 0 = min(cons(M,L)) replace(N,M,nil()) = 0 >= 0 = nil() replace(N,M,cons(K,L)) = L + 1 >= L + 1 = ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) = L + 1 >= L + 1 = cons(M,L) ifrepl(false(),N,M,cons(K,L)) = L + 1 >= L + 1 = cons(K,replace(N,M,L)) selsort(nil()) = 0 >= 0 = nil() selsort(cons(N,L)) = L + 1 >= L + 1 = ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) = L + 1 >= L + 1 = cons(N,selsort(L)) ifselsort(false(),cons(N,L)) = L + 1 >= L + 1 = cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) problem: DPs: ifselsort#(false(),cons(N,L)) -> selsort#(replace(min(cons(N,L)),N,L)) selsort#(cons(N,L)) -> ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) TRS: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) Matrix Interpretation Processor: dimension: 1 interpretation: [ifselsort#](x0, x1) = x1, [selsort#](x0) = x0, [ifselsort](x0, x1) = x1, [selsort](x0) = x0, [ifrepl](x0, x1, x2, x3) = x3, [replace](x0, x1, x2) = x2, [ifmin](x0, x1) = 1, [min](x0) = 1, [cons](x0, x1) = x1 + 1, [nil] = 0, [le](x0, x1) = 1, [false] = 0, [s](x0) = 0, [true] = 0, [eq](x0, x1) = 0, [0] = 0 orientation: ifselsort#(false(),cons(N,L)) = L + 1 >= L = selsort#(replace(min(cons(N,L)),N,L)) selsort#(cons(N,L)) = L + 1 >= L + 1 = ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) eq(0(),0()) = 0 >= 0 = true() eq(0(),s(Y)) = 0 >= 0 = false() eq(s(X),0()) = 0 >= 0 = false() eq(s(X),s(Y)) = 0 >= 0 = eq(X,Y) le(0(),Y) = 1 >= 0 = true() le(s(X),0()) = 1 >= 0 = false() le(s(X),s(Y)) = 1 >= 1 = le(X,Y) min(cons(0(),nil())) = 1 >= 0 = 0() min(cons(s(N),nil())) = 1 >= 0 = s(N) min(cons(N,cons(M,L))) = 1 >= 1 = ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) = 1 >= 1 = min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) = 1 >= 1 = min(cons(M,L)) replace(N,M,nil()) = 0 >= 0 = nil() replace(N,M,cons(K,L)) = L + 1 >= L + 1 = ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) = L + 1 >= L + 1 = cons(M,L) ifrepl(false(),N,M,cons(K,L)) = L + 1 >= L + 1 = cons(K,replace(N,M,L)) selsort(nil()) = 0 >= 0 = nil() selsort(cons(N,L)) = L + 1 >= L + 1 = ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) = L + 1 >= L + 1 = cons(N,selsort(L)) ifselsort(false(),cons(N,L)) = L + 1 >= L + 1 = cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) problem: DPs: selsort#(cons(N,L)) -> ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) TRS: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) Matrix Interpretation Processor: dimension: 1 interpretation: [ifselsort#](x0, x1) = 0, [selsort#](x0) = 1, [ifselsort](x0, x1) = 0, [selsort](x0) = 0, [ifrepl](x0, x1, x2, x3) = x2, [replace](x0, x1, x2) = x1, [ifmin](x0, x1) = 0, [min](x0) = 0, [cons](x0, x1) = 0, [nil] = 0, [le](x0, x1) = 0, [false] = 0, [s](x0) = 0, [true] = 0, [eq](x0, x1) = 0, [0] = 0 orientation: selsort#(cons(N,L)) = 1 >= 0 = ifselsort#(eq(N,min(cons(N,L))),cons(N,L)) eq(0(),0()) = 0 >= 0 = true() eq(0(),s(Y)) = 0 >= 0 = false() eq(s(X),0()) = 0 >= 0 = false() eq(s(X),s(Y)) = 0 >= 0 = eq(X,Y) le(0(),Y) = 0 >= 0 = true() le(s(X),0()) = 0 >= 0 = false() le(s(X),s(Y)) = 0 >= 0 = le(X,Y) min(cons(0(),nil())) = 0 >= 0 = 0() min(cons(s(N),nil())) = 0 >= 0 = s(N) min(cons(N,cons(M,L))) = 0 >= 0 = ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) = 0 >= 0 = min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) = 0 >= 0 = min(cons(M,L)) replace(N,M,nil()) = M >= 0 = nil() replace(N,M,cons(K,L)) = M >= M = ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) = M >= 0 = cons(M,L) ifrepl(false(),N,M,cons(K,L)) = M >= 0 = cons(K,replace(N,M,L)) selsort(nil()) = 0 >= 0 = nil() selsort(cons(N,L)) = 0 >= 0 = ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) = 0 >= 0 = cons(N,selsort(L)) ifselsort(false(),cons(N,L)) = 0 >= 0 = cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) problem: DPs: TRS: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) Qed DPs: replace#(N,M,cons(K,L)) -> ifrepl#(eq(N,K),N,M,cons(K,L)) ifrepl#(false(),N,M,cons(K,L)) -> replace#(N,M,L) TRS: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) Subterm Criterion Processor: simple projection: pi(replace#) = 2 pi(ifrepl#) = 3 problem: DPs: replace#(N,M,cons(K,L)) -> ifrepl#(eq(N,K),N,M,cons(K,L)) TRS: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) Matrix Interpretation Processor: dimension: 1 interpretation: [ifrepl#](x0, x1, x2, x3) = 0, [replace#](x0, x1, x2) = 1, [ifselsort](x0, x1) = 0, [selsort](x0) = 0, [ifrepl](x0, x1, x2, x3) = 0, [replace](x0, x1, x2) = 0, [ifmin](x0, x1) = 0, [min](x0) = 0, [cons](x0, x1) = 0, [nil] = 0, [le](x0, x1) = 0, [false] = 0, [s](x0) = 0, [true] = 0, [eq](x0, x1) = 0, [0] = 0 orientation: replace#(N,M,cons(K,L)) = 1 >= 0 = ifrepl#(eq(N,K),N,M,cons(K,L)) eq(0(),0()) = 0 >= 0 = true() eq(0(),s(Y)) = 0 >= 0 = false() eq(s(X),0()) = 0 >= 0 = false() eq(s(X),s(Y)) = 0 >= 0 = eq(X,Y) le(0(),Y) = 0 >= 0 = true() le(s(X),0()) = 0 >= 0 = false() le(s(X),s(Y)) = 0 >= 0 = le(X,Y) min(cons(0(),nil())) = 0 >= 0 = 0() min(cons(s(N),nil())) = 0 >= 0 = s(N) min(cons(N,cons(M,L))) = 0 >= 0 = ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) = 0 >= 0 = min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) = 0 >= 0 = min(cons(M,L)) replace(N,M,nil()) = 0 >= 0 = nil() replace(N,M,cons(K,L)) = 0 >= 0 = ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) = 0 >= 0 = cons(M,L) ifrepl(false(),N,M,cons(K,L)) = 0 >= 0 = cons(K,replace(N,M,L)) selsort(nil()) = 0 >= 0 = nil() selsort(cons(N,L)) = 0 >= 0 = ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) = 0 >= 0 = cons(N,selsort(L)) ifselsort(false(),cons(N,L)) = 0 >= 0 = cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) problem: DPs: TRS: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) Qed DPs: eq#(s(X),s(Y)) -> eq#(X,Y) TRS: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) Subterm Criterion Processor: simple projection: pi(eq#) = 1 problem: DPs: TRS: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) Qed DPs: min#(cons(N,cons(M,L))) -> ifmin#(le(N,M),cons(N,cons(M,L))) ifmin#(false(),cons(N,cons(M,L))) -> min#(cons(M,L)) ifmin#(true(),cons(N,cons(M,L))) -> min#(cons(N,L)) TRS: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) Matrix Interpretation Processor: dimension: 1 interpretation: [ifmin#](x0, x1) = x0 + x1, [min#](x0) = x0 + 1, [ifselsort](x0, x1) = x1, [selsort](x0) = x0, [ifrepl](x0, x1, x2, x3) = x3, [replace](x0, x1, x2) = x2, [ifmin](x0, x1) = x1, [min](x0) = x0 + 1, [cons](x0, x1) = x1 + 1, [nil] = 1, [le](x0, x1) = 1, [false] = 1, [s](x0) = 0, [true] = 1, [eq](x0, x1) = 1, [0] = 0 orientation: min#(cons(N,cons(M,L))) = L + 3 >= L + 3 = ifmin#(le(N,M),cons(N,cons(M,L))) ifmin#(false(),cons(N,cons(M,L))) = L + 3 >= L + 2 = min#(cons(M,L)) ifmin#(true(),cons(N,cons(M,L))) = L + 3 >= L + 2 = min#(cons(N,L)) eq(0(),0()) = 1 >= 1 = true() eq(0(),s(Y)) = 1 >= 1 = false() eq(s(X),0()) = 1 >= 1 = false() eq(s(X),s(Y)) = 1 >= 1 = eq(X,Y) le(0(),Y) = 1 >= 1 = true() le(s(X),0()) = 1 >= 1 = false() le(s(X),s(Y)) = 1 >= 1 = le(X,Y) min(cons(0(),nil())) = 3 >= 0 = 0() min(cons(s(N),nil())) = 3 >= 0 = s(N) min(cons(N,cons(M,L))) = L + 3 >= L + 2 = ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) = L + 2 >= L + 2 = min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) = L + 2 >= L + 2 = min(cons(M,L)) replace(N,M,nil()) = 1 >= 1 = nil() replace(N,M,cons(K,L)) = L + 1 >= L + 1 = ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) = L + 1 >= L + 1 = cons(M,L) ifrepl(false(),N,M,cons(K,L)) = L + 1 >= L + 1 = cons(K,replace(N,M,L)) selsort(nil()) = 1 >= 1 = nil() selsort(cons(N,L)) = L + 1 >= L + 1 = ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) = L + 1 >= L + 1 = cons(N,selsort(L)) ifselsort(false(),cons(N,L)) = L + 1 >= L + 1 = cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) problem: DPs: min#(cons(N,cons(M,L))) -> ifmin#(le(N,M),cons(N,cons(M,L))) TRS: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) Matrix Interpretation Processor: dimension: 1 interpretation: [ifmin#](x0, x1) = 0, [min#](x0) = 1, [ifselsort](x0, x1) = 0, [selsort](x0) = 0, [ifrepl](x0, x1, x2, x3) = 0, [replace](x0, x1, x2) = 0, [ifmin](x0, x1) = 0, [min](x0) = 0, [cons](x0, x1) = 0, [nil] = 0, [le](x0, x1) = 0, [false] = 0, [s](x0) = 0, [true] = 0, [eq](x0, x1) = 0, [0] = 0 orientation: min#(cons(N,cons(M,L))) = 1 >= 0 = ifmin#(le(N,M),cons(N,cons(M,L))) eq(0(),0()) = 0 >= 0 = true() eq(0(),s(Y)) = 0 >= 0 = false() eq(s(X),0()) = 0 >= 0 = false() eq(s(X),s(Y)) = 0 >= 0 = eq(X,Y) le(0(),Y) = 0 >= 0 = true() le(s(X),0()) = 0 >= 0 = false() le(s(X),s(Y)) = 0 >= 0 = le(X,Y) min(cons(0(),nil())) = 0 >= 0 = 0() min(cons(s(N),nil())) = 0 >= 0 = s(N) min(cons(N,cons(M,L))) = 0 >= 0 = ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) = 0 >= 0 = min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) = 0 >= 0 = min(cons(M,L)) replace(N,M,nil()) = 0 >= 0 = nil() replace(N,M,cons(K,L)) = 0 >= 0 = ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) = 0 >= 0 = cons(M,L) ifrepl(false(),N,M,cons(K,L)) = 0 >= 0 = cons(K,replace(N,M,L)) selsort(nil()) = 0 >= 0 = nil() selsort(cons(N,L)) = 0 >= 0 = ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) = 0 >= 0 = cons(N,selsort(L)) ifselsort(false(),cons(N,L)) = 0 >= 0 = cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) problem: DPs: TRS: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) Qed DPs: le#(s(X),s(Y)) -> le#(X,Y) TRS: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) Subterm Criterion Processor: simple projection: pi(le#) = 1 problem: DPs: TRS: eq(0(),0()) -> true() eq(0(),s(Y)) -> false() eq(s(X),0()) -> false() eq(s(X),s(Y)) -> eq(X,Y) le(0(),Y) -> true() le(s(X),0()) -> false() le(s(X),s(Y)) -> le(X,Y) min(cons(0(),nil())) -> 0() min(cons(s(N),nil())) -> s(N) min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L))) ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L)) ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L)) replace(N,M,nil()) -> nil() replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L)) ifrepl(true(),N,M,cons(K,L)) -> cons(M,L) ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L)) selsort(nil()) -> nil() selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L)) ifselsort(true(),cons(N,L)) -> cons(N,selsort(L)) ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L))) Qed