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