YES Time: 0.278745 TRS: { eq(0(), 0()) -> true(), eq(0(), s x) -> 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), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} DP: DP: { eq#(s x, s y) -> eq#(x, y), le#(s x, s y) -> le#(x, y), app#(add(n, x), y) -> app#(x, y), min# add(n, add(m, x)) -> le#(n, m), min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(true(), add(n, add(m, x))) -> min# add(n, x), if_min#(false(), add(n, add(m, x))) -> min# add(m, x), rm#(n, add(m, x)) -> eq#(n, m), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x), if_rm#(false(), n, add(m, x)) -> rm#(n, x), minsort#(add(n, x), y) -> eq#(n, min add(n, x)), minsort#(add(n, x), y) -> min# add(n, x), minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(true(), add(n, x), y) -> app#(rm(n, x), y), if_minsort#(true(), add(n, x), y) -> rm#(n, x), if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))} TRS: { eq(0(), 0()) -> true(), eq(0(), s x) -> 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), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} UR: { eq(0(), 0()) -> true(), eq(0(), s x) -> 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), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), a(z, w) -> z, a(z, w) -> w} EDG: {(if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y)) (if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), minsort#(add(n, x), y) -> min# add(n, x)) (if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), minsort#(add(n, x), y) -> eq#(n, min add(n, x))) (if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)), minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y)) (if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)), minsort#(add(n, x), y) -> min# add(n, x)) (if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)), minsort#(add(n, x), y) -> eq#(n, min add(n, x))) (min# add(n, add(m, x)) -> le#(n, m), le#(s x, s y) -> le#(x, y)) (minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))) (minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil())) (minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(true(), add(n, x), y) -> rm#(n, x)) (minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(true(), add(n, x), y) -> app#(rm(n, x), y)) (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y)) (if_rm#(true(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x))) (if_rm#(true(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m)) (if_minsort#(true(), add(n, x), y) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x))) (if_minsort#(true(), add(n, x), y) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m)) (if_min#(true(), add(n, add(m, x))) -> min# add(n, x), min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x)))) (if_min#(true(), add(n, add(m, x))) -> min# add(n, x), min# add(n, add(m, x)) -> le#(n, m)) (minsort#(add(n, x), y) -> min# add(n, x), min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x)))) (minsort#(add(n, x), y) -> min# add(n, x), min# add(n, add(m, x)) -> le#(n, m)) (if_min#(false(), add(n, add(m, x))) -> min# add(m, x), min# add(n, add(m, x)) -> le#(n, m)) (if_min#(false(), add(n, add(m, x))) -> min# add(m, x), min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x)))) (min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(true(), add(n, add(m, x))) -> min# add(n, x)) (min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(false(), add(n, add(m, x))) -> min# add(m, x)) (if_rm#(false(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> eq#(n, m)) (if_rm#(false(), n, add(m, x)) -> rm#(n, x), rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x))) (app#(add(n, x), y) -> app#(x, y), app#(add(n, x), y) -> app#(x, y)) (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y)) (rm#(n, add(m, x)) -> eq#(n, m), eq#(s x, s y) -> eq#(x, y)) (rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x)) (rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(false(), n, add(m, x)) -> rm#(n, x)) (minsort#(add(n, x), y) -> eq#(n, min add(n, x)), eq#(s x, s y) -> eq#(x, y)) (if_minsort#(true(), add(n, x), y) -> app#(rm(n, x), y), app#(add(n, x), y) -> app#(x, y))} STATUS: arrows: 0.898148 SCCS (6): Scc: { minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))} Scc: { rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x), if_rm#(false(), n, add(m, x)) -> rm#(n, x)} Scc: { min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(true(), add(n, add(m, x))) -> min# add(n, x), if_min#(false(), add(n, add(m, x))) -> min# add(m, x)} Scc: {le#(s x, s y) -> le#(x, y)} Scc: {eq#(s x, s y) -> eq#(x, y)} Scc: {app#(add(n, x), y) -> app#(x, y)} SCC (3): Strict: { minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()), if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))} Weak: { eq(0(), 0()) -> true(), eq(0(), s x) -> 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), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_rm](x0, x1, x2) = x0, [if_minsort](x0, x1, x2) = 0, [eq](x0, x1) = 0, [le](x0, x1) = 0, [app](x0, x1) = x0 + x1, [add](x0, x1) = x0 + 1, [if_min](x0, x1) = 0, [rm](x0, x1) = x0, [minsort](x0, x1) = 0, [s](x0) = 0, [min](x0) = 0, [true] = 0, [0] = 0, [false] = 0, [nil] = 0, [if_minsort#](x0, x1, x2) = x0 + x1 + 1, [minsort#](x0, x1) = x0 + x1 + 1 Strict: if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)) 2 + 1x + 1y + 0n >= 2 + 1x + 1y + 0n if_minsort#(true(), add(n, x), y) -> minsort#(app(rm(n, x), y), nil()) 2 + 1x + 1y + 0n >= 1 + 1x + 1y + 0n minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y) 2 + 1x + 1y + 0n >= 2 + 1x + 1y + 0n Weak: if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y)) 0 + 0x + 0y + 0n >= 0 + 0x + 0y + 0n if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())) 0 + 0x + 0y + 0n >= 1 + 0x + 0y + 0n minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y) 0 + 0x + 0y + 0n >= 0 + 0x + 0y + 0n minsort(nil(), nil()) -> nil() 0 >= 0 if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)) 1 + 1x + 0n + 0m >= 1 + 1x + 0n + 0m if_rm(true(), n, add(m, x)) -> rm(n, x) 1 + 1x + 0n + 0m >= 0 + 1x + 0n rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)) 1 + 1x + 0n + 0m >= 1 + 1x + 0n + 0m rm(n, nil()) -> nil() 0 + 0n >= 0 if_min(false(), add(n, add(m, x))) -> min add(m, x) 0 + 0x + 0n + 0m >= 0 + 0x + 0m if_min(true(), add(n, add(m, x))) -> min add(n, x) 0 + 0x + 0n + 0m >= 0 + 0x + 0n min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))) 0 + 0x + 0n + 0m >= 0 + 0x + 0n + 0m min add(n, nil()) -> n 0 + 0n >= 1n app(add(n, x), y) -> add(n, app(x, y)) 1 + 1x + 1y + 0n >= 1 + 1x + 1y + 0n app(nil(), y) -> y 0 + 1y >= 1y le(s x, s y) -> le(x, y) 0 + 0x + 0y >= 0 + 0x + 0y le(s x, 0()) -> false() 0 + 0x >= 0 le(0(), y) -> true() 0 + 0y >= 0 eq(s x, s y) -> eq(x, y) 0 + 0x + 0y >= 0 + 0x + 0y eq(s x, 0()) -> false() 0 + 0x >= 0 eq(0(), s x) -> false() 0 + 0x >= 0 eq(0(), 0()) -> true() 0 >= 0 SCCS (1): Scc: { minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))} SCC (2): Strict: { minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y), if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y))} Weak: { eq(0(), 0()) -> true(), eq(0(), s x) -> 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), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_rm](x0, x1, x2) = 0, [if_minsort](x0, x1, x2) = x0 + x1, [eq](x0, x1) = x0 + x1 + 1, [le](x0, x1) = 0, [app](x0, x1) = x0 + 1, [add](x0, x1) = x0 + x1 + 1, [if_min](x0, x1) = 0, [rm](x0, x1) = x0 + 1, [minsort](x0, x1) = x0 + 1, [s](x0) = 0, [min](x0) = x0, [true] = 0, [0] = 0, [false] = 0, [nil] = 1, [if_minsort#](x0, x1, x2) = x0, [minsort#](x0, x1) = x0 + 1 Strict: if_minsort#(false(), add(n, x), y) -> minsort#(x, add(n, y)) 1 + 1x + 0y + 1n >= 1 + 1x + 0y + 0n minsort#(add(n, x), y) -> if_minsort#(eq(n, min add(n, x)), add(n, x), y) 2 + 1x + 0y + 1n >= 1 + 1x + 0y + 1n Weak: if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y)) 1 + 1x + 0y + 1n >= 2 + 0x + 1y + 1n if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())) 1 + 1x + 0y + 1n >= 3 + 0x + 0y + 1n minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y) 1 + 0x + 1y + 0n >= 3 + 2x + 0y + 3n minsort(nil(), nil()) -> nil() 2 >= 1 if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)) 0 + 0x + 0n + 0m >= 2 + 1x + 0n + 1m if_rm(true(), n, add(m, x)) -> rm(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 0n rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)) 2 + 1x + 0n + 1m >= 0 + 0x + 0n + 0m rm(n, nil()) -> nil() 2 + 0n >= 1 if_min(false(), add(n, add(m, x))) -> min add(m, x) 0 + 0x + 0n + 0m >= 1 + 1x + 1m if_min(true(), add(n, add(m, x))) -> min add(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 1n min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))) 2 + 1x + 1n + 1m >= 0 + 0x + 0n + 0m min add(n, nil()) -> n 2 + 1n >= 1n app(add(n, x), y) -> add(n, app(x, y)) 2 + 1x + 0y + 1n >= 2 + 1x + 0y + 1n app(nil(), y) -> y 2 + 0y >= 1y le(s x, s y) -> le(x, y) 0 + 0x + 0y >= 0 + 0x + 0y le(s x, 0()) -> false() 0 + 0x >= 0 le(0(), y) -> true() 0 + 0y >= 0 eq(s x, s y) -> eq(x, y) 1 + 0x + 0y >= 1 + 1x + 1y eq(s x, 0()) -> false() 1 + 0x >= 0 eq(0(), s x) -> false() 1 + 0x >= 0 eq(0(), 0()) -> true() 1 >= 0 SCCS (0): SCC (3): Strict: { rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)), if_rm#(true(), n, add(m, x)) -> rm#(n, x), if_rm#(false(), n, add(m, x)) -> rm#(n, x)} Weak: { eq(0(), 0()) -> true(), eq(0(), s x) -> 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), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_rm](x0, x1, x2) = 0, [if_minsort](x0, x1, x2) = 0, [eq](x0, x1) = 0, [le](x0, x1) = x0 + 1, [app](x0, x1) = 0, [add](x0, x1) = x0 + 1, [if_min](x0, x1) = x0 + x1 + 1, [rm](x0, x1) = 0, [minsort](x0, x1) = 0, [s](x0) = 1, [min](x0) = x0 + 1, [true] = 0, [0] = 1, [false] = 0, [nil] = 0, [if_rm#](x0, x1, x2) = x0, [rm#](x0, x1) = x0 + 1 Strict: if_rm#(false(), n, add(m, x)) -> rm#(n, x) 1 + 1x + 0n + 0m >= 1 + 1x + 0n if_rm#(true(), n, add(m, x)) -> rm#(n, x) 1 + 1x + 0n + 0m >= 1 + 1x + 0n rm#(n, add(m, x)) -> if_rm#(eq(n, m), n, add(m, x)) 2 + 1x + 0n + 0m >= 1 + 1x + 0n + 0m Weak: if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y)) 0 + 0x + 0y + 0n >= 0 + 0x + 0y + 0n if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())) 0 + 0x + 0y + 0n >= 1 + 0x + 0y + 0n minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y) 0 + 0x + 0y + 0n >= 0 + 0x + 0y + 0n minsort(nil(), nil()) -> nil() 0 >= 0 if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)) 0 + 0x + 0n + 0m >= 1 + 0x + 0n + 0m if_rm(true(), n, add(m, x)) -> rm(n, x) 0 + 0x + 0n + 0m >= 0 + 0x + 0n rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)) 0 + 0x + 0n + 0m >= 0 + 0x + 0n + 0m rm(n, nil()) -> nil() 0 + 0n >= 0 if_min(false(), add(n, add(m, x))) -> min add(m, x) 3 + 1x + 0n + 0m >= 2 + 1x + 0m if_min(true(), add(n, add(m, x))) -> min add(n, x) 3 + 1x + 0n + 0m >= 2 + 1x + 0n min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))) 3 + 1x + 0n + 0m >= 4 + 1x + 1n + 0m min add(n, nil()) -> n 2 + 0n >= 1n app(add(n, x), y) -> add(n, app(x, y)) 0 + 0x + 0y + 0n >= 1 + 0x + 0y + 0n app(nil(), y) -> y 0 + 0y >= 1y le(s x, s y) -> le(x, y) 2 + 0x + 0y >= 1 + 1x + 0y le(s x, 0()) -> false() 2 + 0x >= 0 le(0(), y) -> true() 2 + 0y >= 0 eq(s x, s y) -> eq(x, y) 0 + 0x + 0y >= 0 + 0x + 0y eq(s x, 0()) -> false() 0 + 0x >= 0 eq(0(), s x) -> false() 0 + 0x >= 0 eq(0(), 0()) -> true() 0 >= 0 SCCS (0): SCC (3): Strict: { min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))), if_min#(true(), add(n, add(m, x))) -> min# add(n, x), if_min#(false(), add(n, add(m, x))) -> min# add(m, x)} Weak: { eq(0(), 0()) -> true(), eq(0(), s x) -> 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), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_rm](x0, x1, x2) = x0 + x1, [if_minsort](x0, x1, x2) = x0 + x1, [eq](x0, x1) = x0 + x1, [le](x0, x1) = 0, [app](x0, x1) = 0, [add](x0, x1) = x0 + 1, [if_min](x0, x1) = 0, [rm](x0, x1) = 0, [minsort](x0, x1) = x0, [s](x0) = 0, [min](x0) = x0 + 1, [true] = 0, [0] = 0, [false] = 0, [nil] = 0, [if_min#](x0, x1) = x0, [min#](x0) = x0 Strict: if_min#(false(), add(n, add(m, x))) -> min# add(m, x) 2 + 1x + 0n + 0m >= 1 + 1x + 0m if_min#(true(), add(n, add(m, x))) -> min# add(n, x) 2 + 1x + 0n + 0m >= 1 + 1x + 0n min# add(n, add(m, x)) -> if_min#(le(n, m), add(n, add(m, x))) 2 + 1x + 0n + 0m >= 2 + 1x + 0n + 0m Weak: if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y)) 1 + 1x + 0y + 0n >= 1 + 0x + 1y + 0n if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())) 1 + 1x + 0y + 0n >= 1 + 0x + 0y + 0n minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y) 0 + 0x + 1y + 0n >= 3 + 2x + 0y + 1n minsort(nil(), nil()) -> nil() 0 >= 0 if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)) 0 + 0x + 1n + 0m >= 1 + 0x + 0n + 0m if_rm(true(), n, add(m, x)) -> rm(n, x) 0 + 0x + 1n + 0m >= 0 + 0x + 0n rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)) 0 + 0x + 0n + 0m >= 0 + 0x + 2n + 1m rm(n, nil()) -> nil() 0 + 0n >= 0 if_min(false(), add(n, add(m, x))) -> min add(m, x) 0 + 0x + 0n + 0m >= 2 + 1x + 0m if_min(true(), add(n, add(m, x))) -> min add(n, x) 0 + 0x + 0n + 0m >= 2 + 1x + 0n min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))) 3 + 1x + 0n + 0m >= 0 + 0x + 0n + 0m min add(n, nil()) -> n 2 + 0n >= 1n app(add(n, x), y) -> add(n, app(x, y)) 0 + 0x + 0y + 0n >= 1 + 0x + 0y + 0n app(nil(), y) -> y 0 + 0y >= 1y le(s x, s y) -> le(x, y) 0 + 0x + 0y >= 0 + 0x + 0y le(s x, 0()) -> false() 0 + 0x >= 0 le(0(), y) -> true() 0 + 0y >= 0 eq(s x, s y) -> eq(x, y) 0 + 0x + 0y >= 0 + 1x + 1y eq(s x, 0()) -> false() 0 + 0x >= 0 eq(0(), s x) -> false() 0 + 0x >= 0 eq(0(), 0()) -> true() 0 >= 0 SCCS (0): SCC (1): Strict: {le#(s x, s y) -> le#(x, y)} Weak: { eq(0(), 0()) -> true(), eq(0(), s x) -> 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), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_rm](x0, x1, x2) = 0, [if_minsort](x0, x1, x2) = x0 + 1, [eq](x0, x1) = x0 + 1, [le](x0, x1) = x0 + 1, [app](x0, x1) = x0 + 1, [add](x0, x1) = x0 + 1, [if_min](x0, x1) = x0 + x1 + 1, [rm](x0, x1) = x0 + x1 + 1, [minsort](x0, x1) = x0 + x1, [s](x0) = x0 + 1, [min](x0) = 0, [true] = 1, [0] = 1, [false] = 1, [nil] = 1, [le#](x0, x1) = x0 Strict: le#(s x, s y) -> le#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y)) 2 + 0x + 0y + 0n >= 1 + 1x + 1y + 0n if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())) 2 + 0x + 0y + 0n >= 4 + 1x + 0y + 1n minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y) 1 + 1x + 1y + 0n >= 2 + 0x + 0y + 1n minsort(nil(), nil()) -> nil() 2 >= 1 if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)) 0 + 0x + 0n + 0m >= 2 + 1x + 1n + 0m if_rm(true(), n, add(m, x)) -> rm(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 1n rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)) 2 + 1x + 1n + 0m >= 0 + 0x + 0n + 0m rm(n, nil()) -> nil() 2 + 1n >= 1 if_min(false(), add(n, add(m, x))) -> min add(m, x) 4 + 1x + 0n + 0m >= 0 + 0x + 0m if_min(true(), add(n, add(m, x))) -> min add(n, x) 4 + 1x + 0n + 0m >= 0 + 0x + 0n min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))) 0 + 0x + 0n + 0m >= 4 + 1x + 1n + 0m min add(n, nil()) -> n 0 + 0n >= 1n app(add(n, x), y) -> add(n, app(x, y)) 2 + 1x + 0y + 0n >= 2 + 1x + 0y + 0n app(nil(), y) -> y 2 + 0y >= 1y le(s x, s y) -> le(x, y) 2 + 1x + 0y >= 1 + 1x + 0y le(s x, 0()) -> false() 2 + 1x >= 1 le(0(), y) -> true() 2 + 0y >= 1 eq(s x, s y) -> eq(x, y) 2 + 1x + 0y >= 1 + 1x + 0y eq(s x, 0()) -> false() 2 + 1x >= 1 eq(0(), s x) -> false() 2 + 0x >= 1 eq(0(), 0()) -> true() 2 >= 1 Qed SCC (1): Strict: {eq#(s x, s y) -> eq#(x, y)} Weak: { eq(0(), 0()) -> true(), eq(0(), s x) -> 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), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_rm](x0, x1, x2) = 0, [if_minsort](x0, x1, x2) = x0 + 1, [eq](x0, x1) = x0 + 1, [le](x0, x1) = x0 + 1, [app](x0, x1) = x0 + 1, [add](x0, x1) = x0 + 1, [if_min](x0, x1) = x0 + x1 + 1, [rm](x0, x1) = x0 + x1 + 1, [minsort](x0, x1) = x0 + x1, [s](x0) = x0 + 1, [min](x0) = 0, [true] = 1, [0] = 1, [false] = 1, [nil] = 1, [eq#](x0, x1) = x0 Strict: eq#(s x, s y) -> eq#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y)) 2 + 0x + 0y + 0n >= 1 + 1x + 1y + 0n if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())) 2 + 0x + 0y + 0n >= 4 + 1x + 0y + 1n minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y) 1 + 1x + 1y + 0n >= 2 + 0x + 0y + 1n minsort(nil(), nil()) -> nil() 2 >= 1 if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)) 0 + 0x + 0n + 0m >= 2 + 1x + 1n + 0m if_rm(true(), n, add(m, x)) -> rm(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 1n rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)) 2 + 1x + 1n + 0m >= 0 + 0x + 0n + 0m rm(n, nil()) -> nil() 2 + 1n >= 1 if_min(false(), add(n, add(m, x))) -> min add(m, x) 4 + 1x + 0n + 0m >= 0 + 0x + 0m if_min(true(), add(n, add(m, x))) -> min add(n, x) 4 + 1x + 0n + 0m >= 0 + 0x + 0n min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))) 0 + 0x + 0n + 0m >= 4 + 1x + 1n + 0m min add(n, nil()) -> n 0 + 0n >= 1n app(add(n, x), y) -> add(n, app(x, y)) 2 + 1x + 0y + 0n >= 2 + 1x + 0y + 0n app(nil(), y) -> y 2 + 0y >= 1y le(s x, s y) -> le(x, y) 2 + 1x + 0y >= 1 + 1x + 0y le(s x, 0()) -> false() 2 + 1x >= 1 le(0(), y) -> true() 2 + 0y >= 1 eq(s x, s y) -> eq(x, y) 2 + 1x + 0y >= 1 + 1x + 0y eq(s x, 0()) -> false() 2 + 1x >= 1 eq(0(), s x) -> false() 2 + 0x >= 1 eq(0(), 0()) -> true() 2 >= 1 Qed SCC (1): Strict: {app#(add(n, x), y) -> app#(x, y)} Weak: { eq(0(), 0()) -> true(), eq(0(), s x) -> 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), app(nil(), y) -> y, app(add(n, x), y) -> add(n, app(x, y)), min add(n, nil()) -> n, min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))), if_min(true(), add(n, add(m, x))) -> min add(n, x), if_min(false(), add(n, add(m, x))) -> min add(m, x), rm(n, nil()) -> nil(), rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)), if_rm(true(), n, add(m, x)) -> rm(n, x), if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)), minsort(nil(), nil()) -> nil(), minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y), if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())), if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_rm](x0, x1, x2) = 0, [if_minsort](x0, x1, x2) = x0 + 1, [eq](x0, x1) = x0 + 1, [le](x0, x1) = x0 + 1, [app](x0, x1) = x0 + 1, [add](x0, x1) = x0 + 1, [if_min](x0, x1) = x0 + x1 + 1, [rm](x0, x1) = x0 + 1, [minsort](x0, x1) = x0 + 1, [s](x0) = 1, [min](x0) = 0, [true] = 1, [0] = 1, [false] = 1, [nil] = 1, [app#](x0, x1) = x0 Strict: app#(add(n, x), y) -> app#(x, y) 1 + 1x + 0y + 0n >= 0 + 1x + 0y Weak: if_minsort(false(), add(n, x), y) -> minsort(x, add(n, y)) 2 + 0x + 0y + 0n >= 2 + 0x + 1y + 0n if_minsort(true(), add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil())) 2 + 0x + 0y + 0n >= 3 + 0x + 0y + 0n minsort(add(n, x), y) -> if_minsort(eq(n, min add(n, x)), add(n, x), y) 1 + 0x + 1y + 0n >= 2 + 0x + 0y + 1n minsort(nil(), nil()) -> nil() 2 >= 1 if_rm(false(), n, add(m, x)) -> add(m, rm(n, x)) 0 + 0x + 0n + 0m >= 2 + 1x + 0n + 0m if_rm(true(), n, add(m, x)) -> rm(n, x) 0 + 0x + 0n + 0m >= 1 + 1x + 0n rm(n, add(m, x)) -> if_rm(eq(n, m), n, add(m, x)) 2 + 1x + 0n + 0m >= 0 + 0x + 0n + 0m rm(n, nil()) -> nil() 2 + 0n >= 1 if_min(false(), add(n, add(m, x))) -> min add(m, x) 4 + 1x + 0n + 0m >= 0 + 0x + 0m if_min(true(), add(n, add(m, x))) -> min add(n, x) 4 + 1x + 0n + 0m >= 0 + 0x + 0n min add(n, add(m, x)) -> if_min(le(n, m), add(n, add(m, x))) 0 + 0x + 0n + 0m >= 4 + 1x + 1n + 0m min add(n, nil()) -> n 0 + 0n >= 1n app(add(n, x), y) -> add(n, app(x, y)) 2 + 1x + 0y + 0n >= 2 + 1x + 0y + 0n app(nil(), y) -> y 2 + 0y >= 1y le(s x, s y) -> le(x, y) 2 + 0x + 0y >= 1 + 1x + 0y le(s x, 0()) -> false() 2 + 0x >= 1 le(0(), y) -> true() 2 + 0y >= 1 eq(s x, s y) -> eq(x, y) 2 + 0x + 0y >= 1 + 1x + 0y eq(s x, 0()) -> false() 2 + 0x >= 1 eq(0(), s x) -> false() 2 + 0x >= 1 eq(0(), 0()) -> true() 2 >= 1 Qed