YES (VAR Y X N M L K) (RULES 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))) ) The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting. Proving termination of innermost rewriting for selsort: -> Dependency pairs: nF_eq(s(X),s(Y)) -> nF_eq(X,Y) nF_le(s(X),s(Y)) -> nF_le(X,Y) nF_min(cons(N,cons(M,L))) -> nF_ifmin(le(N,M),cons(N,cons(M,L))) nF_min(cons(N,cons(M,L))) -> nF_le(N,M) nF_ifmin(true,cons(N,cons(M,L))) -> nF_min(cons(N,L)) nF_ifmin(false,cons(N,cons(M,L))) -> nF_min(cons(M,L)) nF_replace(N,M,cons(K,L)) -> nF_ifrepl(eq(N,K),N,M,cons(K,L)) nF_replace(N,M,cons(K,L)) -> nF_eq(N,K) nF_ifrepl(false,N,M,cons(K,L)) -> nF_replace(N,M,L) nF_selsort(cons(N,L)) -> nF_ifselsort(eq(N,min(cons(N,L))),cons(N,L)) nF_selsort(cons(N,L)) -> nF_eq(N,min(cons(N,L))) nF_selsort(cons(N,L)) -> nF_min(cons(N,L)) nF_ifselsort(true,cons(N,L)) -> nF_selsort(L) nF_ifselsort(false,cons(N,L)) -> nF_min(cons(N,L)) nF_ifselsort(false,cons(N,L)) -> nF_selsort(replace(min(cons(N,L)),N,L)) nF_ifselsort(false,cons(N,L)) -> nF_replace(min(cons(N,L)),N,L) -> Proof of termination for selsort_1_1: -> -> Dependency pairs in cycle: nF_selsort(cons(N,L)) -> nF_ifselsort(eq(N,min(cons(N,L))),cons(N,L)) nF_ifselsort(false,cons(N,L)) -> nF_selsort(replace(min(cons(N,L)),N,L)) nF_ifselsort(true,cons(N,L)) -> nF_selsort(L) UsableRules: 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)) Polynomial Interpretation: [eq](X1,X2) = 0 [0] = 0 [true] = 0 [s](X) = 0 [false] = 0 [le](X1,X2) = 0 [min](X) = 0 [cons](X1,X2) = X1 + X2 + 1 [nil] = 0 [ifmin](X1,X2) = 0 [replace](X1,X2,X3) = X2 + X3 [ifrepl](X1,X2,X3,X4) = X3 + X4 [selsort](X) = 0 [ifselsort](X1,X2) = 0 [nF_selsort](X) = X [nF_ifselsort](X1,X2) = X2 TIME: 6.5886e-2 -> -> Dependency pairs in cycle: nF_selsort(cons(N,L)) -> nF_ifselsort(eq(N,min(cons(N,L))),cons(N,L)) nF_ifselsort(false,cons(N,L)) -> nF_selsort(replace(min(cons(N,L)),N,L)) UsableRules: 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)) Polynomial Interpretation: [eq](X1,X2) = X1 [0] = 1 [true] = 0 [s](X) = X + 1 [false] = 0 [le](X1,X2) = X1 [min](X) = X [cons](X1,X2) = X1 + X2 + 1 [nil] = 1 [ifmin](X1,X2) = X2 [replace](X1,X2,X3) = X2 + X3 [ifrepl](X1,X2,X3,X4) = X3 + X4 [selsort](X) = 0 [ifselsort](X1,X2) = 0 [nF_selsort](X) = X [nF_ifselsort](X1,X2) = X2 TIME: 6.1378e-2 -> Proof of termination for selsort_1_2: -> -> Dependency pairs in cycle: nF_replace(N,M,cons(K,L)) -> nF_ifrepl(eq(N,K),N,M,cons(K,L)) nF_ifrepl(false,N,M,cons(K,L)) -> nF_replace(N,M,L) Termination proved: Cycles verify subterm criterion. -> Proof of termination for selsort_1_3: -> -> Dependency pairs in cycle: nF_min(cons(N,cons(M,L))) -> nF_ifmin(le(N,M),cons(N,cons(M,L))) nF_ifmin(false,cons(N,cons(M,L))) -> nF_min(cons(M,L)) nF_ifmin(true,cons(N,cons(M,L))) -> nF_min(cons(N,L)) UsableRules: le(0,Y) -> true le(s(X),0) -> false le(s(X),s(Y)) -> le(X,Y) Polynomial Interpretation: [eq](X1,X2) = 0 [0] = 1 [true] = 0 [s](X) = X + 1 [false] = 0 [le](X1,X2) = X1 [min](X) = 0 [cons](X1,X2) = X2 + 1 [nil] = 0 [ifmin](X1,X2) = 0 [replace](X1,X2,X3) = 0 [ifrepl](X1,X2,X3,X4) = 0 [selsort](X) = 0 [ifselsort](X1,X2) = 0 [nF_min](X) = X + 1 [nF_ifmin](X1,X2) = X2 + 1 TIME: 4.7657e-2 -> -> Dependency pairs in cycle: nF_min(cons(N,cons(M,L))) -> nF_ifmin(le(N,M),cons(N,cons(M,L))) nF_ifmin(false,cons(N,cons(M,L))) -> nF_min(cons(M,L)) Termination proved: Cycles verify subterm criterion. -> Proof of termination for selsort_1_4: -> -> Dependency pairs in cycle: nF_le(s(X),s(Y)) -> nF_le(X,Y) Termination proved: Cycles verify subterm criterion. -> Proof of termination for selsort_1_5: -> -> Dependency pairs in cycle: nF_eq(s(X),s(Y)) -> nF_eq(X,Y) Termination proved: Cycles verify subterm criterion. SETTINGS: Base ordering: Polynomial ordering Proof mode: SCCs in DG + base ordering Upper bound for coeffs: 1 Rationals below 1 for all non-replacing args: No Polynomial interpretation: Linear Coeffs in polynomials: No rationals Delta: automatic Termination was proved succesfully.