YES Time: 1.120459 TRS: { eq(0(), 0()) -> true(), eq(0(), s m) -> false(), eq(s n, 0()) -> false(), eq(s n, s m) -> eq(n, m), le(0(), m) -> true(), le(s n, 0()) -> false(), le(s n, s m) -> le(n, m), min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))), min cons(0(), nil()) -> 0(), min cons(s n, nil()) -> s n, if_min(true(), cons(n, cons(m, x))) -> min cons(n, x), if_min(false(), cons(n, cons(m, x))) -> min cons(m, x), replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)), replace(n, m, nil()) -> nil(), if_replace(true(), n, m, cons(k, x)) -> cons(m, x), if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)), sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)), sort nil() -> nil()} DP: DP: { eq#(s n, s m) -> eq#(n, m), le#(s n, s m) -> le#(n, m), min# cons(n, cons(m, x)) -> le#(n, m), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x), replace#(n, m, cons(k, x)) -> eq#(n, k), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)), if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), sort# cons(n, x) -> min# cons(n, x), sort# cons(n, x) -> replace#(min cons(n, x), n, x), sort# cons(n, x) -> sort# replace(min cons(n, x), n, x)} TRS: { eq(0(), 0()) -> true(), eq(0(), s m) -> false(), eq(s n, 0()) -> false(), eq(s n, s m) -> eq(n, m), le(0(), m) -> true(), le(s n, 0()) -> false(), le(s n, s m) -> le(n, m), min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))), min cons(0(), nil()) -> 0(), min cons(s n, nil()) -> s n, if_min(true(), cons(n, cons(m, x))) -> min cons(n, x), if_min(false(), cons(n, cons(m, x))) -> min cons(m, x), replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)), replace(n, m, nil()) -> nil(), if_replace(true(), n, m, cons(k, x)) -> cons(m, x), if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)), sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)), sort nil() -> nil()} EDG: {(if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x)))) (if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), min# cons(n, cons(m, x)) -> le#(n, m)) (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x))) (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> eq#(n, k)) (sort# cons(n, x) -> replace#(min cons(n, x), n, x), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x))) (sort# cons(n, x) -> replace#(min cons(n, x), n, x), replace#(n, m, cons(k, x)) -> eq#(n, k)) (replace#(n, m, cons(k, x)) -> eq#(n, k), eq#(s n, s m) -> eq#(n, m)) (le#(s n, s m) -> le#(n, m), le#(s n, s m) -> le#(n, m)) (min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x)) (min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x)) (min# cons(n, cons(m, x)) -> le#(n, m), le#(s n, s m) -> le#(n, m)) (eq#(s n, s m) -> eq#(n, m), eq#(s n, s m) -> eq#(n, m)) (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> min# cons(n, x)) (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> replace#(min cons(n, x), n, x)) (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> sort# replace(min cons(n, x), n, x)) (sort# cons(n, x) -> min# cons(n, x), min# cons(n, cons(m, x)) -> le#(n, m)) (sort# cons(n, x) -> min# cons(n, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x)))) (if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x), min# cons(n, cons(m, x)) -> le#(n, m)) (if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x)))) (replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)), if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x))} EDG: {(if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x)))) (if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), min# cons(n, cons(m, x)) -> le#(n, m)) (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x))) (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> eq#(n, k)) (sort# cons(n, x) -> replace#(min cons(n, x), n, x), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x))) (sort# cons(n, x) -> replace#(min cons(n, x), n, x), replace#(n, m, cons(k, x)) -> eq#(n, k)) (replace#(n, m, cons(k, x)) -> eq#(n, k), eq#(s n, s m) -> eq#(n, m)) (le#(s n, s m) -> le#(n, m), le#(s n, s m) -> le#(n, m)) (min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x)) (min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x)) (min# cons(n, cons(m, x)) -> le#(n, m), le#(s n, s m) -> le#(n, m)) (eq#(s n, s m) -> eq#(n, m), eq#(s n, s m) -> eq#(n, m)) (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> min# cons(n, x)) (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> replace#(min cons(n, x), n, x)) (sort# cons(n, x) -> sort# replace(min cons(n, x), n, x), sort# cons(n, x) -> sort# replace(min cons(n, x), n, x)) (sort# cons(n, x) -> min# cons(n, x), min# cons(n, cons(m, x)) -> le#(n, m)) (sort# cons(n, x) -> min# cons(n, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x)))) (if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x), min# cons(n, cons(m, x)) -> le#(n, m)) (if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x)))) (replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)), if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x))} STATUS: arrows: 0.861111 SCCS (5): Scc: {sort# cons(n, x) -> sort# replace(min cons(n, x), n, x)} Scc: { min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x)} Scc: {le#(s n, s m) -> le#(n, m)} Scc: { replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)), if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x)} Scc: {eq#(s n, s m) -> eq#(n, m)} SCC (1): Strict: {sort# cons(n, x) -> sort# replace(min cons(n, x), n, x)} Weak: { eq(0(), 0()) -> true(), eq(0(), s m) -> false(), eq(s n, 0()) -> false(), eq(s n, s m) -> eq(n, m), le(0(), m) -> true(), le(s n, 0()) -> false(), le(s n, s m) -> le(n, m), min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))), min cons(0(), nil()) -> 0(), min cons(s n, nil()) -> s n, if_min(true(), cons(n, cons(m, x))) -> min cons(n, x), if_min(false(), cons(n, cons(m, x))) -> min cons(m, x), replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)), replace(n, m, nil()) -> nil(), if_replace(true(), n, m, cons(k, x)) -> cons(m, x), if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)), sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)), sort nil() -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_replace](x0, x1, x2, x3) = x0, [replace](x0, x1, x2) = x0, [eq](x0, x1) = x0 + x1, [le](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + 1, [if_min](x0, x1) = 0, [s](x0) = 1, [min](x0) = x0 + 1, [sort](x0) = x0, [true] = 0, [0] = 1, [false] = 0, [nil] = 1, [sort#](x0) = x0 Strict: sort# cons(n, x) -> sort# replace(min cons(n, x), n, x) 1 + 0n + 1x >= 0 + 0n + 1x Weak: sort nil() -> nil() 1 >= 1 sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)) 1 + 0n + 1x >= 1 + 0n + 1x if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)) 1 + 0m + 0n + 1x + 0k >= 1 + 0m + 0n + 1x + 0k if_replace(true(), n, m, cons(k, x)) -> cons(m, x) 1 + 0m + 0n + 1x + 0k >= 1 + 0m + 1x replace(n, m, nil()) -> nil() 1 + 0m + 0n >= 1 replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)) 1 + 0m + 0n + 1x + 0k >= 1 + 0m + 0n + 1x + 0k if_min(false(), cons(n, cons(m, x))) -> min cons(m, x) 0 + 0m + 0n + 0x >= 2 + 0m + 1x if_min(true(), cons(n, cons(m, x))) -> min cons(n, x) 0 + 0m + 0n + 0x >= 2 + 0n + 1x min cons(s n, nil()) -> s n 3 + 0n >= 1 + 0n min cons(0(), nil()) -> 0() 3 >= 1 min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))) 3 + 0m + 0n + 1x >= 0 + 0m + 0n + 0x le(s n, s m) -> le(n, m) 2 + 0m + 0n >= 1 + 0m + 1n le(s n, 0()) -> false() 2 + 0n >= 0 le(0(), m) -> true() 2 + 0m >= 0 eq(s n, s m) -> eq(n, m) 2 + 0m + 0n >= 0 + 1m + 1n eq(s n, 0()) -> false() 2 + 0n >= 0 eq(0(), s m) -> false() 2 + 0m >= 0 eq(0(), 0()) -> true() 2 >= 0 Qed SCC (3): Strict: { min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x)} Weak: { eq(0(), 0()) -> true(), eq(0(), s m) -> false(), eq(s n, 0()) -> false(), eq(s n, s m) -> eq(n, m), le(0(), m) -> true(), le(s n, 0()) -> false(), le(s n, s m) -> le(n, m), min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))), min cons(0(), nil()) -> 0(), min cons(s n, nil()) -> s n, if_min(true(), cons(n, cons(m, x))) -> min cons(n, x), if_min(false(), cons(n, cons(m, x))) -> min cons(m, x), replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)), replace(n, m, nil()) -> nil(), if_replace(true(), n, m, cons(k, x)) -> cons(m, x), if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)), sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)), sort nil() -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_replace](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, [if_min](x0, x1) = x0 + 1, [s](x0) = 1, [min](x0) = 0, [sort](x0) = 0, [true] = 1, [0] = 1, [false] = 0, [nil] = 1, [if_min#](x0, x1) = x0, [min#](x0) = x0 Strict: if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x) 2 + 0m + 0n + 1x >= 1 + 0m + 1x if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x) 2 + 0m + 0n + 1x >= 1 + 0n + 1x min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))) 2 + 0m + 0n + 1x >= 2 + 0m + 0n + 1x Weak: sort nil() -> nil() 0 >= 1 sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)) 0 + 0n + 0x >= 1 + 0n + 0x if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)) 0 + 0m + 0n + 0x + 0k >= 2 + 0m + 0n + 1x + 0k if_replace(true(), n, m, cons(k, x)) -> cons(m, x) 0 + 0m + 0n + 0x + 0k >= 1 + 0m + 1x replace(n, m, nil()) -> nil() 2 + 0m + 0n >= 1 replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)) 2 + 0m + 0n + 1x + 0k >= 0 + 0m + 0n + 0x + 0k if_min(false(), cons(n, cons(m, x))) -> min cons(m, x) 1 + 0m + 0n + 0x >= 0 + 0m + 0x if_min(true(), cons(n, cons(m, x))) -> min cons(n, x) 2 + 0m + 0n + 0x >= 0 + 0n + 0x min cons(s n, nil()) -> s n 0 + 0n >= 1 + 0n min cons(0(), nil()) -> 0() 0 >= 1 min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))) 0 + 0m + 0n + 0x >= 1 + 0m + 0n + 0x le(s n, s m) -> le(n, m) 0 + 0m + 0n >= 0 + 0m + 0n le(s n, 0()) -> false() 0 + 0n >= 0 le(0(), m) -> true() 0 + 0m >= 1 eq(s n, s m) -> eq(n, m) 2 + 0m + 0n >= 1 + 0m + 1n eq(s n, 0()) -> false() 2 + 0n >= 0 eq(0(), s m) -> false() 2 + 0m >= 0 eq(0(), 0()) -> true() 2 >= 1 SCCS (0): SCC (1): Strict: {le#(s n, s m) -> le#(n, m)} Weak: { eq(0(), 0()) -> true(), eq(0(), s m) -> false(), eq(s n, 0()) -> false(), eq(s n, s m) -> eq(n, m), le(0(), m) -> true(), le(s n, 0()) -> false(), le(s n, s m) -> le(n, m), min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))), min cons(0(), nil()) -> 0(), min cons(s n, nil()) -> s n, if_min(true(), cons(n, cons(m, x))) -> min cons(n, x), if_min(false(), cons(n, cons(m, x))) -> min cons(m, x), replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)), replace(n, m, nil()) -> nil(), if_replace(true(), n, m, cons(k, x)) -> cons(m, x), if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)), sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)), sort nil() -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_replace](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 + 1, [if_min](x0, x1) = x0 + x1 + 1, [s](x0) = x0 + 1, [min](x0) = 0, [sort](x0) = 0, [true] = 1, [0] = 1, [false] = 1, [nil] = 1, [le#](x0, x1) = x0 + 1 Strict: le#(s n, s m) -> le#(n, m) 2 + 0m + 1n >= 1 + 0m + 1n Weak: sort nil() -> nil() 0 >= 1 sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)) 0 + 0n + 0x >= 1 + 0n + 0x if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)) 0 + 0m + 0n + 0x + 0k >= 2 + 0m + 0n + 1x + 0k if_replace(true(), n, m, cons(k, x)) -> cons(m, x) 0 + 0m + 0n + 0x + 0k >= 1 + 0m + 1x replace(n, m, nil()) -> nil() 2 + 0m + 0n >= 1 replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)) 2 + 0m + 0n + 1x + 0k >= 0 + 0m + 0n + 0x + 0k if_min(false(), cons(n, cons(m, x))) -> min cons(m, x) 4 + 0m + 0n + 1x >= 0 + 0m + 0x if_min(true(), cons(n, cons(m, x))) -> min cons(n, x) 4 + 0m + 0n + 1x >= 0 + 0n + 0x min cons(s n, nil()) -> s n 0 + 0n >= 1 + 1n min cons(0(), nil()) -> 0() 0 >= 1 min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))) 0 + 0m + 0n + 0x >= 4 + 0m + 1n + 1x le(s n, s m) -> le(n, m) 2 + 0m + 1n >= 1 + 0m + 1n le(s n, 0()) -> false() 2 + 1n >= 1 le(0(), m) -> true() 2 + 0m >= 1 eq(s n, s m) -> eq(n, m) 2 + 0m + 1n >= 1 + 0m + 1n eq(s n, 0()) -> false() 2 + 1n >= 1 eq(0(), s m) -> false() 2 + 0m >= 1 eq(0(), 0()) -> true() 2 >= 1 Qed SCC (2): Strict: { replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)), if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x)} Weak: { eq(0(), 0()) -> true(), eq(0(), s m) -> false(), eq(s n, 0()) -> false(), eq(s n, s m) -> eq(n, m), le(0(), m) -> true(), le(s n, 0()) -> false(), le(s n, s m) -> le(n, m), min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))), min cons(0(), nil()) -> 0(), min cons(s n, nil()) -> s n, if_min(true(), cons(n, cons(m, x))) -> min cons(n, x), if_min(false(), cons(n, cons(m, x))) -> min cons(m, x), replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)), replace(n, m, nil()) -> nil(), if_replace(true(), n, m, cons(k, x)) -> cons(m, x), if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)), sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)), sort nil() -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_replace](x0, x1, x2, x3) = x0 + x1 + x2 + 1, [replace](x0, x1, x2) = x0 + 1, [eq](x0, x1) = x0 + 1, [le](x0, x1) = x0 + 1, [cons](x0, x1) = x0 + x1 + 1, [if_min](x0, x1) = x0 + x1 + 1, [s](x0) = 1, [min](x0) = 0, [sort](x0) = 0, [true] = 1, [0] = 1, [false] = 1, [nil] = 0, [if_replace#](x0, x1, x2, x3) = x0, [replace#](x0, x1, x2) = x0 Strict: if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x) 1 + 0m + 0n + 1x + 1k >= 0 + 0m + 0n + 1x replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)) 1 + 0m + 0n + 1x + 1k >= 1 + 0m + 0n + 1x + 1k Weak: sort nil() -> nil() 0 >= 0 sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)) 0 + 0n + 0x >= 1 + 0n + 0x if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)) 3 + 0m + 1n + 1x + 1k >= 2 + 0m + 0n + 1x + 1k if_replace(true(), n, m, cons(k, x)) -> cons(m, x) 3 + 0m + 1n + 1x + 1k >= 1 + 1m + 1x replace(n, m, nil()) -> nil() 1 + 0m + 0n >= 0 replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)) 2 + 0m + 0n + 1x + 1k >= 3 + 0m + 2n + 1x + 1k if_min(false(), cons(n, cons(m, x))) -> min cons(m, x) 4 + 1m + 1n + 1x >= 0 + 0m + 0x if_min(true(), cons(n, cons(m, x))) -> min cons(n, x) 4 + 1m + 1n + 1x >= 0 + 0n + 0x min cons(s n, nil()) -> s n 0 + 0n >= 1 + 0n min cons(0(), nil()) -> 0() 0 >= 1 min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))) 0 + 0m + 0n + 0x >= 4 + 1m + 2n + 1x le(s n, s m) -> le(n, m) 2 + 0m + 0n >= 1 + 0m + 1n le(s n, 0()) -> false() 2 + 0n >= 1 le(0(), m) -> true() 2 + 0m >= 1 eq(s n, s m) -> eq(n, m) 2 + 0m + 0n >= 1 + 0m + 1n eq(s n, 0()) -> false() 2 + 0n >= 1 eq(0(), s m) -> false() 2 + 0m >= 1 eq(0(), 0()) -> true() 2 >= 1 SCCS (0): SCC (1): Strict: {eq#(s n, s m) -> eq#(n, m)} Weak: { eq(0(), 0()) -> true(), eq(0(), s m) -> false(), eq(s n, 0()) -> false(), eq(s n, s m) -> eq(n, m), le(0(), m) -> true(), le(s n, 0()) -> false(), le(s n, s m) -> le(n, m), min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))), min cons(0(), nil()) -> 0(), min cons(s n, nil()) -> s n, if_min(true(), cons(n, cons(m, x))) -> min cons(n, x), if_min(false(), cons(n, cons(m, x))) -> min cons(m, x), replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)), replace(n, m, nil()) -> nil(), if_replace(true(), n, m, cons(k, x)) -> cons(m, x), if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)), sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)), sort nil() -> nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_replace](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 + 1, [if_min](x0, x1) = x0 + x1 + 1, [s](x0) = x0 + 1, [min](x0) = 0, [sort](x0) = 0, [true] = 1, [0] = 1, [false] = 1, [nil] = 1, [eq#](x0, x1) = x0 + 1 Strict: eq#(s n, s m) -> eq#(n, m) 2 + 0m + 1n >= 1 + 0m + 1n Weak: sort nil() -> nil() 0 >= 1 sort cons(n, x) -> cons(min cons(n, x), sort replace(min cons(n, x), n, x)) 0 + 0n + 0x >= 1 + 0n + 0x if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)) 0 + 0m + 0n + 0x + 0k >= 2 + 0m + 0n + 1x + 0k if_replace(true(), n, m, cons(k, x)) -> cons(m, x) 0 + 0m + 0n + 0x + 0k >= 1 + 0m + 1x replace(n, m, nil()) -> nil() 2 + 0m + 0n >= 1 replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)) 2 + 0m + 0n + 1x + 0k >= 0 + 0m + 0n + 0x + 0k if_min(false(), cons(n, cons(m, x))) -> min cons(m, x) 4 + 0m + 0n + 1x >= 0 + 0m + 0x if_min(true(), cons(n, cons(m, x))) -> min cons(n, x) 4 + 0m + 0n + 1x >= 0 + 0n + 0x min cons(s n, nil()) -> s n 0 + 0n >= 1 + 1n min cons(0(), nil()) -> 0() 0 >= 1 min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))) 0 + 0m + 0n + 0x >= 4 + 0m + 1n + 1x le(s n, s m) -> le(n, m) 2 + 0m + 1n >= 1 + 0m + 1n le(s n, 0()) -> false() 2 + 1n >= 1 le(0(), m) -> true() 2 + 0m >= 1 eq(s n, s m) -> eq(n, m) 2 + 0m + 1n >= 1 + 0m + 1n eq(s n, 0()) -> false() 2 + 1n >= 1 eq(0(), s m) -> false() 2 + 0m >= 1 eq(0(), 0()) -> true() 2 >= 1 Qed