MAYBE Time: 0.012901 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()} UR: { 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)), a(y, z) -> y, a(y, z) -> z} 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))} 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()} Open 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()} Open 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()} Open 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()} Open 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()} Open