YES Time: 0.238416 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(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))), min cons(0(), nil()) -> 0(), min cons(s N, nil()) -> s N, 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)) -> ifrepl(eq(N, K), N, M, cons(K, L)), replace(N, M, nil()) -> nil(), ifrepl(true(), N, M, cons(K, L)) -> cons(M, L), ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)), selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)), selsort nil() -> nil(), 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))} DP: DP: { 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) -> eq#(N, min cons(N, L)), selsort# cons(N, L) -> 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)) -> min# cons(N, 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)} 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(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))), min cons(0(), nil()) -> 0(), min cons(s N, nil()) -> s N, 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)) -> ifrepl(eq(N, K), N, M, cons(K, L)), replace(N, M, nil()) -> nil(), ifrepl(true(), N, M, cons(K, L)) -> cons(M, L), ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)), selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)), selsort nil() -> nil(), 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))} UR: { 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(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))), min cons(0(), nil()) -> 0(), min cons(s N, nil()) -> s N, 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)) -> ifrepl(eq(N, K), N, M, cons(K, L)), replace(N, M, nil()) -> nil(), ifrepl(true(), N, M, cons(K, L)) -> cons(M, L), ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)), a(x, y) -> x, a(x, y) -> y} EDG: {(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)) -> 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)) (ifselsort#(true(), cons(N, L)) -> selsort# 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) -> min# cons(N, L)) (ifselsort#(true(), cons(N, L)) -> selsort# 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)) -> 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))) (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)) (le#(s X, s Y) -> le#(X, Y), le#(s X, s Y) -> le#(X, Y)) (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)) -> 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) -> 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), replace#(N, M, cons(K, L)) -> ifrepl#(eq(N, K), N, M, cons(K, L))) (ifselsort#(false(), cons(N, L)) -> replace#(min cons(N, L), N, 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)) -> 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))) (min# cons(N, cons(M, L)) -> le#(N, M), le#(s X, s Y) -> le#(X, Y)) (eq#(s X, s Y) -> eq#(X, Y), eq#(s X, s Y) -> eq#(X, Y)) (selsort# cons(N, L) -> eq#(N, min cons(N, L)), eq#(s X, s Y) -> eq#(X, Y)) (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)))) (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)))) (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))} STATUS: arrows: 0.882812 SCCS (5): Scc: { 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)) -> selsort# replace(min cons(N, L), N, L)} Scc: { 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)} Scc: {eq#(s X, s Y) -> eq#(X, Y)} Scc: { 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)} Scc: {le#(s X, s Y) -> le#(X, Y)} SCC (3): Strict: { 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)) -> selsort# replace(min cons(N, L), N, L)} Weak: { 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(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))), min cons(0(), nil()) -> 0(), min cons(s N, nil()) -> s N, 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)) -> ifrepl(eq(N, K), N, M, cons(K, L)), replace(N, M, nil()) -> nil(), ifrepl(true(), N, M, cons(K, L)) -> cons(M, L), ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)), selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)), selsort nil() -> nil(), 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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifrepl](x0, x1, x2, x3) = x0, [replace](x0, x1, x2) = x0, [eq](x0, x1) = 0, [le](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + 1, [ifmin](x0, x1) = x0 + x1 + 1, [ifselsort](x0, x1) = 0, [s](x0) = 1, [min](x0) = 0, [selsort](x0) = 0, [true] = 0, [0] = 0, [false] = 0, [nil] = 1, [ifselsort#](x0, x1) = x0, [selsort#](x0) = x0 + 1 Strict: ifselsort#(false(), cons(N, L)) -> selsort# replace(min cons(N, L), N, L) 1 + 0N + 1L >= 1 + 0N + 1L ifselsort#(true(), cons(N, L)) -> selsort# L 1 + 0N + 1L >= 1 + 1L selsort# cons(N, L) -> ifselsort#(eq(N, min cons(N, L)), cons(N, L)) 2 + 0N + 1L >= 1 + 0N + 1L Weak: ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L)) 0 + 0N + 0L >= 1 + 0N + 0L ifselsort(true(), cons(N, L)) -> cons(N, selsort L) 0 + 0N + 0L >= 1 + 0N + 0L selsort nil() -> nil() 0 >= 1 selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)) 0 + 0N + 0L >= 0 + 0N + 0L ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) 1 + 0N + 0M + 1L + 0K >= 1 + 0N + 0M + 1L + 0K ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 1 + 0N + 0M + 1L + 0K >= 1 + 0M + 1L replace(N, M, nil()) -> nil() 1 + 0N + 0M >= 1 replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 1 + 0N + 0M + 1L + 0K >= 1 + 0N + 0M + 1L + 0K ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L) 3 + 0N + 0M + 1L >= 0 + 0M + 0L ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L) 3 + 0N + 0M + 1L >= 0 + 0N + 0L min cons(s N, nil()) -> s N 0 + 0N >= 1 + 0N min cons(0(), nil()) -> 0() 0 >= 0 min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))) 0 + 0N + 0M + 0L >= 4 + 0N + 1M + 1L le(s X, s Y) -> le(X, Y) 2 + 0Y + 0X >= 1 + 1Y + 0X le(s X, 0()) -> false() 1 + 0X >= 0 le(0(), Y) -> true() 1 + 1Y >= 0 eq(s X, s Y) -> eq(X, Y) 0 + 0Y + 0X >= 0 + 0Y + 0X eq(s X, 0()) -> false() 0 + 0X >= 0 eq(0(), s Y) -> false() 0 + 0Y >= 0 eq(0(), 0()) -> true() 0 >= 0 SCCS (0): SCC (2): Strict: { 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)} Weak: { 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(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))), min cons(0(), nil()) -> 0(), min cons(s N, nil()) -> s N, 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)) -> ifrepl(eq(N, K), N, M, cons(K, L)), replace(N, M, nil()) -> nil(), ifrepl(true(), N, M, cons(K, L)) -> cons(M, L), ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)), selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)), selsort nil() -> nil(), 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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifrepl](x0, x1, x2, x3) = x0 + x1, [replace](x0, x1, x2) = x0 + 1, [eq](x0, x1) = x0 + x1, [le](x0, x1) = 0, [cons](x0, x1) = x0 + 1, [ifmin](x0, x1) = 0, [ifselsort](x0, x1) = x0 + 1, [s](x0) = 0, [min](x0) = x0, [selsort](x0) = x0 + 1, [true] = 0, [0] = 0, [false] = 0, [nil] = 1, [ifrepl#](x0, x1, x2, x3) = x0 + 1, [replace#](x0, x1, x2) = x0 + 1 Strict: ifrepl#(false(), N, M, cons(K, L)) -> replace#(N, M, L) 2 + 0N + 0M + 1L + 0K >= 1 + 0N + 0M + 1L replace#(N, M, cons(K, L)) -> ifrepl#(eq(N, K), N, M, cons(K, L)) 2 + 0N + 0M + 1L + 0K >= 2 + 0N + 0M + 1L + 0K Weak: ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L)) 1 + 0N + 0L >= 3 + 0N + 1L ifselsort(true(), cons(N, L)) -> cons(N, selsort L) 1 + 0N + 0L >= 2 + 0N + 1L selsort nil() -> nil() 2 >= 1 selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)) 2 + 0N + 1L >= 2 + 1N + 1L ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) 0 + 1N + 0M + 0L + 0K >= 2 + 0N + 0M + 1L + 0K ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 0 + 1N + 0M + 0L + 0K >= 1 + 0M + 1L replace(N, M, nil()) -> nil() 2 + 0N + 0M >= 1 replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 2 + 0N + 0M + 1L + 0K >= 0 + 2N + 0M + 0L + 1K ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L) 0 + 0N + 0M + 0L >= 1 + 0M + 1L ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L) 0 + 0N + 0M + 0L >= 1 + 0N + 1L min cons(s N, nil()) -> s N 2 + 0N >= 0 + 0N min cons(0(), nil()) -> 0() 2 >= 0 min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))) 2 + 0N + 0M + 1L >= 0 + 0N + 0M + 0L le(s X, s Y) -> le(X, Y) 0 + 0Y + 0X >= 0 + 0Y + 0X le(s X, 0()) -> false() 0 + 0X >= 0 le(0(), Y) -> true() 0 + 0Y >= 0 eq(s X, s Y) -> eq(X, Y) 0 + 0Y + 0X >= 0 + 1Y + 1X eq(s X, 0()) -> false() 0 + 0X >= 0 eq(0(), s Y) -> false() 0 + 0Y >= 0 eq(0(), 0()) -> true() 0 >= 0 SCCS (0): SCC (1): Strict: {eq#(s X, s Y) -> eq#(X, Y)} Weak: { 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(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))), min cons(0(), nil()) -> 0(), min cons(s N, nil()) -> s N, 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)) -> ifrepl(eq(N, K), N, M, cons(K, L)), replace(N, M, nil()) -> nil(), ifrepl(true(), N, M, cons(K, L)) -> cons(M, L), ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)), selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)), selsort nil() -> nil(), 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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifrepl](x0, x1, x2, x3) = 0, [replace](x0, x1, x2) = x0 + 1, [eq](x0, x1) = x0 + 1, [le](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + x1 + 1, [ifmin](x0, x1) = x0 + x1 + 1, [ifselsort](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [min](x0) = 0, [selsort](x0) = 0, [true] = 1, [0] = 1, [false] = 1, [nil] = 0, [eq#](x0, x1) = x0 + 1 Strict: eq#(s X, s Y) -> eq#(X, Y) 2 + 0Y + 1X >= 1 + 0Y + 1X Weak: ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L)) 2 + 0N + 0L >= 1 + 0N + 0L ifselsort(true(), cons(N, L)) -> cons(N, selsort L) 2 + 0N + 0L >= 1 + 1N + 0L selsort nil() -> nil() 0 >= 0 selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)) 0 + 0N + 0L >= 2 + 1N + 0L ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) 0 + 0N + 0M + 0L + 0K >= 2 + 0N + 0M + 1L + 1K ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 0 + 0N + 0M + 0L + 0K >= 1 + 1M + 1L replace(N, M, nil()) -> nil() 1 + 0N + 0M >= 0 replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 2 + 0N + 0M + 1L + 1K >= 0 + 0N + 0M + 0L + 0K ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L) 4 + 1N + 1M + 1L >= 0 + 0M + 0L ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L) 4 + 1N + 1M + 1L >= 0 + 0N + 0L min cons(s N, nil()) -> s N 0 + 0N >= 1 + 1N min cons(0(), nil()) -> 0() 0 >= 1 min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))) 0 + 0N + 0M + 0L >= 4 + 2N + 1M + 1L le(s X, s Y) -> le(X, Y) 2 + 0Y + 1X >= 1 + 0Y + 1X le(s X, 0()) -> false() 2 + 1X >= 1 le(0(), Y) -> true() 2 + 0Y >= 1 eq(s X, s Y) -> eq(X, Y) 2 + 0Y + 1X >= 1 + 0Y + 1X eq(s X, 0()) -> false() 2 + 1X >= 1 eq(0(), s Y) -> false() 2 + 0Y >= 1 eq(0(), 0()) -> true() 2 >= 1 Qed SCC (3): Strict: { 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)} Weak: { 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(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))), min cons(0(), nil()) -> 0(), min cons(s N, nil()) -> s N, 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)) -> ifrepl(eq(N, K), N, M, cons(K, L)), replace(N, M, nil()) -> nil(), ifrepl(true(), N, M, cons(K, L)) -> cons(M, L), ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)), selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)), selsort nil() -> nil(), 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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifrepl](x0, x1, x2, x3) = 0, [replace](x0, x1, x2) = x0 + 1, [eq](x0, x1) = x0 + 1, [le](x0, x1) = 0, [cons](x0, x1) = x0 + 1, [ifmin](x0, x1) = 0, [ifselsort](x0, x1) = x0 + 1, [s](x0) = 1, [min](x0) = x0 + 1, [selsort](x0) = x0 + 1, [true] = 0, [0] = 1, [false] = 0, [nil] = 0, [ifmin#](x0, x1) = x0, [min#](x0) = x0 Strict: ifmin#(false(), cons(N, cons(M, L))) -> min# cons(M, L) 2 + 0N + 0M + 1L >= 1 + 0M + 1L ifmin#(true(), cons(N, cons(M, L))) -> min# cons(N, L) 2 + 0N + 0M + 1L >= 1 + 0N + 1L min# cons(N, cons(M, L)) -> ifmin#(le(N, M), cons(N, cons(M, L))) 2 + 0N + 0M + 1L >= 2 + 0N + 0M + 1L Weak: ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L)) 2 + 0N + 1L >= 3 + 0N + 1L ifselsort(true(), cons(N, L)) -> cons(N, selsort L) 2 + 0N + 1L >= 2 + 0N + 1L selsort nil() -> nil() 1 >= 0 selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)) 2 + 0N + 1L >= 2 + 0N + 1L ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) 0 + 0N + 0M + 0L + 0K >= 2 + 0N + 0M + 1L + 0K ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 0 + 0N + 0M + 0L + 0K >= 1 + 0M + 1L replace(N, M, nil()) -> nil() 1 + 0N + 0M >= 0 replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 2 + 0N + 0M + 1L + 0K >= 0 + 0N + 0M + 0L + 0K ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L) 0 + 0N + 0M + 0L >= 2 + 0M + 1L ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L) 0 + 0N + 0M + 0L >= 2 + 0N + 1L min cons(s N, nil()) -> s N 2 + 0N >= 1 + 0N min cons(0(), nil()) -> 0() 2 >= 1 min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))) 3 + 0N + 0M + 1L >= 0 + 0N + 0M + 0L le(s X, s Y) -> le(X, Y) 0 + 0Y + 0X >= 0 + 0Y + 0X le(s X, 0()) -> false() 0 + 0X >= 0 le(0(), Y) -> true() 0 + 0Y >= 0 eq(s X, s Y) -> eq(X, Y) 2 + 0Y + 0X >= 1 + 0Y + 1X eq(s X, 0()) -> false() 2 + 0X >= 0 eq(0(), s Y) -> false() 2 + 0Y >= 0 eq(0(), 0()) -> true() 2 >= 0 SCCS (0): SCC (1): Strict: {le#(s X, s Y) -> le#(X, Y)} Weak: { 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(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))), min cons(0(), nil()) -> 0(), min cons(s N, nil()) -> s N, 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)) -> ifrepl(eq(N, K), N, M, cons(K, L)), replace(N, M, nil()) -> nil(), ifrepl(true(), N, M, cons(K, L)) -> cons(M, L), ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)), selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)), selsort nil() -> nil(), 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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifrepl](x0, x1, x2, x3) = 0, [replace](x0, x1, x2) = x0 + 1, [eq](x0, x1) = x0 + 1, [le](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + x1 + 1, [ifmin](x0, x1) = x0 + x1 + 1, [ifselsort](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [min](x0) = 0, [selsort](x0) = 0, [true] = 1, [0] = 1, [false] = 1, [nil] = 0, [le#](x0, x1) = x0 + 1 Strict: le#(s X, s Y) -> le#(X, Y) 2 + 0Y + 1X >= 1 + 0Y + 1X Weak: ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L)) 2 + 0N + 0L >= 1 + 0N + 0L ifselsort(true(), cons(N, L)) -> cons(N, selsort L) 2 + 0N + 0L >= 1 + 1N + 0L selsort nil() -> nil() 0 >= 0 selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)) 0 + 0N + 0L >= 2 + 1N + 0L ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) 0 + 0N + 0M + 0L + 0K >= 2 + 0N + 0M + 1L + 1K ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) 0 + 0N + 0M + 0L + 0K >= 1 + 1M + 1L replace(N, M, nil()) -> nil() 1 + 0N + 0M >= 0 replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) 2 + 0N + 0M + 1L + 1K >= 0 + 0N + 0M + 0L + 0K ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L) 4 + 1N + 1M + 1L >= 0 + 0M + 0L ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L) 4 + 1N + 1M + 1L >= 0 + 0N + 0L min cons(s N, nil()) -> s N 0 + 0N >= 1 + 1N min cons(0(), nil()) -> 0() 0 >= 1 min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))) 0 + 0N + 0M + 0L >= 4 + 2N + 1M + 1L le(s X, s Y) -> le(X, Y) 2 + 0Y + 1X >= 1 + 0Y + 1X le(s X, 0()) -> false() 2 + 1X >= 1 le(0(), Y) -> true() 2 + 0Y >= 1 eq(s X, s Y) -> eq(X, Y) 2 + 0Y + 1X >= 1 + 0Y + 1X eq(s X, 0()) -> false() 2 + 1X >= 1 eq(0(), s Y) -> false() 2 + 0Y >= 1 eq(0(), 0()) -> true() 2 >= 1 Qed