R
↳Dependency Pair Analysis
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))) -> IFMIN(le(n, m), add(n, add(m, x)))
MIN(add(n, add(m, x))) -> LE(n, m)
IFMIN(true, add(n, add(m, x))) -> MIN(add(n, x))
IFMIN(false, add(n, add(m, x))) -> MIN(add(m, x))
RM(n, add(m, x)) -> IFRM(eq(n, m), n, add(m, x))
RM(n, add(m, x)) -> EQ(n, m)
IFRM(true, n, add(m, x)) -> RM(n, x)
IFRM(false, n, add(m, x)) -> RM(n, x)
MINSORT(add(n, x), y) -> IFMINSORT(eq(n, min(add(n, x))), add(n, x), y)
MINSORT(add(n, x), y) -> EQ(n, min(add(n, x)))
MINSORT(add(n, x), y) -> MIN(add(n, x))
IFMINSORT(true, add(n, x), y) -> MINSORT(app(rm(n, x), y), nil)
IFMINSORT(true, add(n, x), y) -> APP(rm(n, x), y)
IFMINSORT(true, add(n, x), y) -> RM(n, x)
IFMINSORT(false, add(n, x), y) -> MINSORT(x, add(n, y))
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
EQ(s(x), s(y)) -> EQ(x, y)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
EQ(s(x), s(y)) -> EQ(x, y)
EQ(x1, x2) -> EQ(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 7
↳Dependency Graph
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
LE(s(x), s(y)) -> LE(x, y)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
LE(s(x), s(y)) -> LE(x, y)
LE(x1, x2) -> LE(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 8
↳Dependency Graph
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Argument Filtering and Ordering
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
APP(add(n, x), y) -> APP(x, y)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
APP(add(n, x), y) -> APP(x, y)
APP(x1, x2) -> APP(x1, x2)
add(x1, x2) -> add(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 9
↳Dependency Graph
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳Argument Filtering and Ordering
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
IFRM(false, n, add(m, x)) -> RM(n, x)
IFRM(true, n, add(m, x)) -> RM(n, x)
RM(n, add(m, x)) -> IFRM(eq(n, m), n, add(m, x))
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
IFRM(false, n, add(m, x)) -> RM(n, x)
IFRM(true, n, add(m, x)) -> RM(n, x)
IFRM(x1, x2, x3) -> x3
add(x1, x2) -> add(x1, x2)
RM(x1, x2) -> x2
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 10
↳Dependency Graph
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
RM(n, add(m, x)) -> IFRM(eq(n, m), n, add(m, x))
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳Argument Filtering and Ordering
→DP Problem 6
↳Nar
IFMIN(false, add(n, add(m, x))) -> MIN(add(m, x))
IFMIN(true, add(n, add(m, x))) -> MIN(add(n, x))
MIN(add(n, add(m, x))) -> IFMIN(le(n, m), add(n, add(m, x)))
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
IFMIN(false, add(n, add(m, x))) -> MIN(add(m, x))
IFMIN(true, add(n, add(m, x))) -> MIN(add(n, x))
MIN(x1) -> x1
add(x1, x2) -> add(x1, x2)
IFMIN(x1, x2) -> x2
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 11
↳Dependency Graph
→DP Problem 6
↳Nar
MIN(add(n, add(m, x))) -> IFMIN(le(n, m), add(n, add(m, x)))
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Narrowing Transformation
IFMINSORT(false, add(n, x), y) -> MINSORT(x, add(n, y))
IFMINSORT(true, add(n, x), y) -> MINSORT(app(rm(n, x), y), nil)
MINSORT(add(n, x), y) -> IFMINSORT(eq(n, min(add(n, x))), add(n, x), y)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
IFMINSORT(true, add(n, x), y) -> MINSORT(app(rm(n, x), y), nil)
IFMINSORT(true, add(n'', nil), y) -> MINSORT(app(nil, y), nil)
IFMINSORT(true, add(n'', add(m', x'')), y) -> MINSORT(app(ifrm(eq(n'', m'), n'', add(m', x'')), y), nil)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Narrowing Transformation
IFMINSORT(true, add(n'', add(m', x'')), y) -> MINSORT(app(ifrm(eq(n'', m'), n'', add(m', x'')), y), nil)
IFMINSORT(true, add(n'', nil), y) -> MINSORT(app(nil, y), nil)
MINSORT(add(n, x), y) -> IFMINSORT(eq(n, min(add(n, x))), add(n, x), y)
IFMINSORT(false, add(n, x), y) -> MINSORT(x, add(n, y))
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
one new Dependency Pair is created:
IFMINSORT(true, add(n'', nil), y) -> MINSORT(app(nil, y), nil)
IFMINSORT(true, add(n'', nil), y'') -> MINSORT(y'', nil)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 13
↳Instantiation Transformation
IFMINSORT(true, add(n'', nil), y'') -> MINSORT(y'', nil)
IFMINSORT(false, add(n, x), y) -> MINSORT(x, add(n, y))
MINSORT(add(n, x), y) -> IFMINSORT(eq(n, min(add(n, x))), add(n, x), y)
IFMINSORT(true, add(n'', add(m', x'')), y) -> MINSORT(app(ifrm(eq(n'', m'), n'', add(m', x'')), y), nil)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
MINSORT(add(n, x), y) -> IFMINSORT(eq(n, min(add(n, x))), add(n, x), y)
MINSORT(add(n'', x''), add(n''', y'')) -> IFMINSORT(eq(n'', min(add(n'', x''))), add(n'', x''), add(n''', y''))
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 14
↳Instantiation Transformation
IFMINSORT(true, add(n'', add(m', x'')), y) -> MINSORT(app(ifrm(eq(n'', m'), n'', add(m', x'')), y), nil)
MINSORT(add(n'', x''), add(n''', y'')) -> IFMINSORT(eq(n'', min(add(n'', x''))), add(n'', x''), add(n''', y''))
IFMINSORT(false, add(n, x), y) -> MINSORT(x, add(n, y))
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n'', nil), y'') -> MINSORT(y'', nil)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
IFMINSORT(false, add(n, x), y) -> MINSORT(x, add(n, y))
IFMINSORT(false, add(n', x'), add(n'''''', y'''')) -> MINSORT(x', add(n', add(n'''''', y'''')))
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 15
↳Instantiation Transformation
IFMINSORT(false, add(n', x'), add(n'''''', y'''')) -> MINSORT(x', add(n', add(n'''''', y'''')))
MINSORT(add(n'', x''), add(n''', y'')) -> IFMINSORT(eq(n'', min(add(n'', x''))), add(n'', x''), add(n''', y''))
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
IFMINSORT(true, add(n'', nil), y'') -> MINSORT(y'', nil)
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n'', add(m', x'')), y) -> MINSORT(app(ifrm(eq(n'', m'), n'', add(m', x'')), y), nil)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
IFMINSORT(true, add(n'', add(m', x'')), y) -> MINSORT(app(ifrm(eq(n'', m'), n'', add(m', x'')), y), nil)
IFMINSORT(true, add(n''', add(m'', x'''')), add(n'''''', y'''')) -> MINSORT(app(ifrm(eq(n''', m''), n''', add(m'', x'''')), add(n'''''', y'''')), nil)
IFMINSORT(true, add(n'''', add(m'', x'''')), nil) -> MINSORT(app(ifrm(eq(n'''', m''), n'''', add(m'', x'''')), nil), nil)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 16
↳Instantiation Transformation
IFMINSORT(true, add(n''', add(m'', x'''')), add(n'''''', y'''')) -> MINSORT(app(ifrm(eq(n''', m''), n''', add(m'', x'''')), add(n'''''', y'''')), nil)
IFMINSORT(true, add(n'''', add(m'', x'''')), nil) -> MINSORT(app(ifrm(eq(n'''', m''), n'''', add(m'', x'''')), nil), nil)
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n'', nil), y'') -> MINSORT(y'', nil)
MINSORT(add(n'', x''), add(n''', y'')) -> IFMINSORT(eq(n'', min(add(n'', x''))), add(n'', x''), add(n''', y''))
IFMINSORT(false, add(n', x'), add(n'''''', y'''')) -> MINSORT(x', add(n', add(n'''''', y'''')))
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
MINSORT(add(n'', x''), add(n''', y'')) -> IFMINSORT(eq(n'', min(add(n'', x''))), add(n'', x''), add(n''', y''))
MINSORT(add(n'''', x''''), add(n''''', add(n'''''''', y''''''))) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', add(n'''''''', y'''''')))
MINSORT(add(n'''', x''''), add(n''''', nil)) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', nil))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 17
↳Instantiation Transformation
IFMINSORT(true, add(n'''', add(m'', x'''')), nil) -> MINSORT(app(ifrm(eq(n'''', m''), n'''', add(m'', x'''')), nil), nil)
MINSORT(add(n'''', x''''), add(n''''', add(n'''''''', y''''''))) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', add(n'''''''', y'''''')))
IFMINSORT(false, add(n', x'), add(n'''''', y'''')) -> MINSORT(x', add(n', add(n'''''', y'''')))
MINSORT(add(n'''', x''''), add(n''''', nil)) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', nil))
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
IFMINSORT(true, add(n'', nil), y'') -> MINSORT(y'', nil)
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n''', add(m'', x'''')), add(n'''''', y'''')) -> MINSORT(app(ifrm(eq(n''', m''), n''', add(m'', x'''')), add(n'''''', y'''')), nil)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
IFMINSORT(false, add(n', x'), add(n'''''', y'''')) -> MINSORT(x', add(n', add(n'''''', y'''')))
IFMINSORT(false, add(n'', x'''), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(x''', add(n'', add(n'''''''', add(n'''''''''', y''''''''))))
IFMINSORT(false, add(n'', x'''), add(n'''''''', nil)) -> MINSORT(x''', add(n'', add(n'''''''', nil)))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 18
↳Instantiation Transformation
IFMINSORT(false, add(n'', x'''), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(x''', add(n'', add(n'''''''', add(n'''''''''', y''''''''))))
MINSORT(add(n'''', x''''), add(n''''', add(n'''''''', y''''''))) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', add(n'''''''', y'''''')))
IFMINSORT(false, add(n'', x'''), add(n'''''''', nil)) -> MINSORT(x''', add(n'', add(n'''''''', nil)))
IFMINSORT(true, add(n''', add(m'', x'''')), add(n'''''', y'''')) -> MINSORT(app(ifrm(eq(n''', m''), n''', add(m'', x'''')), add(n'''''', y'''')), nil)
MINSORT(add(n'''', x''''), add(n''''', nil)) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', nil))
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
IFMINSORT(true, add(n'', nil), y'') -> MINSORT(y'', nil)
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n'''', add(m'', x'''')), nil) -> MINSORT(app(ifrm(eq(n'''', m''), n'''', add(m'', x'''')), nil), nil)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
three new Dependency Pairs are created:
IFMINSORT(true, add(n'', nil), y'') -> MINSORT(y'', nil)
IFMINSORT(true, add(n'''', nil), nil) -> MINSORT(nil, nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(add(n'''''''', add(n'''''''''', y'''''''')), nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', nil)) -> MINSORT(add(n'''''''', nil), nil)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 19
↳Instantiation Transformation
IFMINSORT(true, add(n''', nil), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(add(n'''''''', add(n'''''''''', y'''''''')), nil)
IFMINSORT(true, add(n'''', add(m'', x'''')), nil) -> MINSORT(app(ifrm(eq(n'''', m''), n'''', add(m'', x'''')), nil), nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', nil)) -> MINSORT(add(n'''''''', nil), nil)
IFMINSORT(false, add(n'', x'''), add(n'''''''', nil)) -> MINSORT(x''', add(n'', add(n'''''''', nil)))
MINSORT(add(n'''', x''''), add(n''''', nil)) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', nil))
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n''', add(m'', x'''')), add(n'''''', y'''')) -> MINSORT(app(ifrm(eq(n''', m''), n''', add(m'', x'''')), add(n'''''', y'''')), nil)
MINSORT(add(n'''', x''''), add(n''''', add(n'''''''', y''''''))) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', add(n'''''''', y'''''')))
IFMINSORT(false, add(n'', x'''), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(x''', add(n'', add(n'''''''', add(n'''''''''', y''''''''))))
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
IFMINSORT(true, add(n''', add(m'', x'''')), add(n'''''', y'''')) -> MINSORT(app(ifrm(eq(n''', m''), n''', add(m'', x'''')), add(n'''''', y'''')), nil)
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', add(n'''''''''', y''''''''))), nil)
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', nil)) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', nil)), nil)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 20
↳Instantiation Transformation
IFMINSORT(true, add(n'''', add(m'', x'''')), nil) -> MINSORT(app(ifrm(eq(n'''', m''), n'''', add(m'', x'''')), nil), nil)
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', nil)) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', nil)), nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', nil)) -> MINSORT(add(n'''''''', nil), nil)
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', add(n'''''''''', y''''''''))), nil)
IFMINSORT(false, add(n'', x'''), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(x''', add(n'', add(n'''''''', add(n'''''''''', y''''''''))))
MINSORT(add(n'''', x''''), add(n''''', add(n'''''''', y''''''))) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', add(n'''''''', y'''''')))
IFMINSORT(false, add(n'', x'''), add(n'''''''', nil)) -> MINSORT(x''', add(n'', add(n'''''''', nil)))
MINSORT(add(n'''', x''''), add(n''''', nil)) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', nil))
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(add(n'''''''', add(n'''''''''', y'''''''')), nil)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
MINSORT(add(n'''', x''''), add(n''''', add(n'''''''', y''''''))) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', add(n'''''''', y'''''')))
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', add(n'''''''''''', y'''''''''')))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', add(n'''''''''''', y''''''''''))))
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil)))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 21
↳Instantiation Transformation
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', nil)) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', nil)), nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', nil)) -> MINSORT(add(n'''''''', nil), nil)
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', add(n'''''''''', y''''''''))), nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(add(n'''''''', add(n'''''''''', y'''''''')), nil)
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', add(n'''''''''''', y'''''''''')))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', add(n'''''''''''', y''''''''''))))
IFMINSORT(false, add(n'', x'''), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(x''', add(n'', add(n'''''''', add(n'''''''''', y''''''''))))
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil)))
IFMINSORT(false, add(n'', x'''), add(n'''''''', nil)) -> MINSORT(x''', add(n'', add(n'''''''', nil)))
MINSORT(add(n'''', x''''), add(n''''', nil)) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', nil))
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n'''', add(m'', x'''')), nil) -> MINSORT(app(ifrm(eq(n'''', m''), n'''', add(m'', x'''')), nil), nil)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
IFMINSORT(false, add(n'', x'''), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(x''', add(n'', add(n'''''''', add(n'''''''''', y''''''''))))
IFMINSORT(false, add(n''', x''''), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(x'''', add(n''', add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))))
IFMINSORT(false, add(n''', x''''), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(x'''', add(n''', add(n''''''''0, add(n'''''''''''', nil))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 22
↳Instantiation Transformation
IFMINSORT(true, add(n'''', add(m'', x'''')), nil) -> MINSORT(app(ifrm(eq(n'''', m''), n'''', add(m'', x'''')), nil), nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', nil)) -> MINSORT(add(n'''''''', nil), nil)
IFMINSORT(false, add(n''', x''''), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(x'''', add(n''', add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))))
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', add(n'''''''''''', y'''''''''')))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', add(n'''''''''''', y''''''''''))))
IFMINSORT(false, add(n''', x''''), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(x'''', add(n''', add(n''''''''0, add(n'''''''''''', nil))))
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', add(n'''''''''', y''''''''))), nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(add(n'''''''', add(n'''''''''', y'''''''')), nil)
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil)))
IFMINSORT(false, add(n'', x'''), add(n'''''''', nil)) -> MINSORT(x''', add(n'', add(n'''''''', nil)))
MINSORT(add(n'''', x''''), add(n''''', nil)) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', nil))
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', nil)) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', nil)), nil)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
IFMINSORT(true, add(n''', nil), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(add(n'''''''', add(n'''''''''', y'''''''')), nil)
IFMINSORT(true, add(n'''', nil), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y''''''''''''))), nil)
IFMINSORT(true, add(n'''', nil), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(add(n''''''''0, add(n'''''''''''', nil)), nil)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 23
↳Instantiation Transformation
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', nil)) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', nil)), nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', nil)) -> MINSORT(add(n'''''''', nil), nil)
IFMINSORT(true, add(n'''', nil), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(add(n''''''''0, add(n'''''''''''', nil)), nil)
IFMINSORT(true, add(n'''', nil), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y''''''''''''))), nil)
IFMINSORT(false, add(n''', x''''), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(x'''', add(n''', add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))))
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', add(n'''''''''''', y'''''''''')))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', add(n'''''''''''', y''''''''''))))
IFMINSORT(false, add(n''', x''''), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(x'''', add(n''', add(n''''''''0, add(n'''''''''''', nil))))
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', add(n'''''''''', y''''''''))), nil)
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil)))
IFMINSORT(false, add(n'', x'''), add(n'''''''', nil)) -> MINSORT(x''', add(n'', add(n'''''''', nil)))
MINSORT(add(n'''', x''''), add(n''''', nil)) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', nil))
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n'''', add(m'', x'''')), nil) -> MINSORT(app(ifrm(eq(n'''', m''), n'''', add(m'', x'''')), nil), nil)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', add(n'''''''''', y''''''''))) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', add(n'''''''''', y''''''''))), nil)
IFMINSORT(true, add(n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(app(ifrm(eq(n''''', m''''), n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))), nil)
IFMINSORT(true, add(n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(app(ifrm(eq(n''''', m''''), n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', nil))), nil)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 24
↳Instantiation Transformation
IFMINSORT(true, add(n'''', add(m'', x'''')), nil) -> MINSORT(app(ifrm(eq(n'''', m''), n'''', add(m'', x'''')), nil), nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', nil)) -> MINSORT(add(n'''''''', nil), nil)
IFMINSORT(true, add(n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(app(ifrm(eq(n''''', m''''), n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', nil))), nil)
IFMINSORT(true, add(n'''', nil), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(add(n''''''''0, add(n'''''''''''', nil)), nil)
IFMINSORT(true, add(n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(app(ifrm(eq(n''''', m''''), n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))), nil)
IFMINSORT(true, add(n'''', nil), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y''''''''''''))), nil)
IFMINSORT(false, add(n''', x''''), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(x'''', add(n''', add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))))
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', add(n'''''''''''', y'''''''''')))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', add(n'''''''''''', y''''''''''))))
IFMINSORT(false, add(n''', x''''), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(x'''', add(n''', add(n''''''''0, add(n'''''''''''', nil))))
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil)))
IFMINSORT(false, add(n'', x'''), add(n'''''''', nil)) -> MINSORT(x''', add(n'', add(n'''''''', nil)))
MINSORT(add(n'''', x''''), add(n''''', nil)) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', nil))
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', nil)) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', nil)), nil)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', add(n'''''''''''', y'''''''''')))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', add(n'''''''''''', y''''''''''))))
MINSORT(add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', add(n'''''''''''''''', y''''''''''''''))))) -> IFMINSORT(eq(n''''''0, min(add(n''''''0, x'''''''))), add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', add(n'''''''''''''''', y'''''''''''''')))))
MINSORT(add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', nil)))) -> IFMINSORT(eq(n''''''0, min(add(n''''''0, x'''''''))), add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', nil))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 25
↳Instantiation Transformation
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', nil)) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', nil)), nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', nil)) -> MINSORT(add(n'''''''', nil), nil)
IFMINSORT(true, add(n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(app(ifrm(eq(n''''', m''''), n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', nil))), nil)
IFMINSORT(true, add(n'''', nil), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(add(n''''''''0, add(n'''''''''''', nil)), nil)
IFMINSORT(true, add(n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(app(ifrm(eq(n''''', m''''), n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))), nil)
IFMINSORT(true, add(n'''', nil), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y''''''''''''))), nil)
MINSORT(add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', add(n'''''''''''''''', y''''''''''''''))))) -> IFMINSORT(eq(n''''''0, min(add(n''''''0, x'''''''))), add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', add(n'''''''''''''''', y'''''''''''''')))))
IFMINSORT(false, add(n''', x''''), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(x'''', add(n''', add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))))
MINSORT(add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', nil)))) -> IFMINSORT(eq(n''''''0, min(add(n''''''0, x'''''''))), add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', nil))))
IFMINSORT(false, add(n''', x''''), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(x'''', add(n''', add(n''''''''0, add(n'''''''''''', nil))))
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil)))
IFMINSORT(false, add(n'', x'''), add(n'''''''', nil)) -> MINSORT(x''', add(n'', add(n'''''''', nil)))
MINSORT(add(n'''', x''''), add(n''''', nil)) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', nil))
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n'''', add(m'', x'''')), nil) -> MINSORT(app(ifrm(eq(n'''', m''), n'''', add(m'', x'''')), nil), nil)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
IFMINSORT(false, add(n''', x''''), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(x'''', add(n''', add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))))
IFMINSORT(false, add(n'''', x'''''), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))) -> MINSORT(x''''', add(n'''', add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))))
IFMINSORT(false, add(n'''', x'''''), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))) -> MINSORT(x''''', add(n'''', add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 26
↳Instantiation Transformation
IFMINSORT(true, add(n'''', add(m'', x'''')), nil) -> MINSORT(app(ifrm(eq(n'''', m''), n'''', add(m'', x'''')), nil), nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', nil)) -> MINSORT(add(n'''''''', nil), nil)
IFMINSORT(true, add(n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(app(ifrm(eq(n''''', m''''), n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', nil))), nil)
IFMINSORT(true, add(n'''', nil), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(add(n''''''''0, add(n'''''''''''', nil)), nil)
IFMINSORT(false, add(n'''', x'''''), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))) -> MINSORT(x''''', add(n'''', add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))))
MINSORT(add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', add(n'''''''''''''''', y''''''''''''''))))) -> IFMINSORT(eq(n''''''0, min(add(n''''''0, x'''''''))), add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', add(n'''''''''''''''', y'''''''''''''')))))
IFMINSORT(false, add(n'''', x'''''), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))) -> MINSORT(x''''', add(n'''', add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))))
IFMINSORT(true, add(n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(app(ifrm(eq(n''''', m''''), n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))), nil)
IFMINSORT(true, add(n'''', nil), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y''''''''''''))), nil)
MINSORT(add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', nil)))) -> IFMINSORT(eq(n''''''0, min(add(n''''''0, x'''''''))), add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', nil))))
IFMINSORT(false, add(n''', x''''), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(x'''', add(n''', add(n''''''''0, add(n'''''''''''', nil))))
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil)))
IFMINSORT(false, add(n'', x'''), add(n'''''''', nil)) -> MINSORT(x''', add(n'', add(n'''''''', nil)))
MINSORT(add(n'''', x''''), add(n''''', nil)) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', nil))
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', nil)) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', nil)), nil)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
IFMINSORT(true, add(n'''', nil), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y''''''''''''))), nil)
IFMINSORT(true, add(n''''', nil), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))) -> MINSORT(add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y'''''''''''''''')))), nil)
IFMINSORT(true, add(n''''', nil), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))) -> MINSORT(add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil))), nil)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 27
↳Instantiation Transformation
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', nil)) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', nil)), nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', nil)) -> MINSORT(add(n'''''''', nil), nil)
IFMINSORT(true, add(n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(app(ifrm(eq(n''''', m''''), n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', nil))), nil)
IFMINSORT(true, add(n'''', nil), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(add(n''''''''0, add(n'''''''''''', nil)), nil)
IFMINSORT(true, add(n''''', nil), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))) -> MINSORT(add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil))), nil)
IFMINSORT(true, add(n''''', nil), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))) -> MINSORT(add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y'''''''''''''''')))), nil)
IFMINSORT(false, add(n'''', x'''''), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))) -> MINSORT(x''''', add(n'''', add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))))
MINSORT(add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', add(n'''''''''''''''', y''''''''''''''))))) -> IFMINSORT(eq(n''''''0, min(add(n''''''0, x'''''''))), add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', add(n'''''''''''''''', y'''''''''''''')))))
IFMINSORT(false, add(n'''', x'''''), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))) -> MINSORT(x''''', add(n'''', add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))))
IFMINSORT(true, add(n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(app(ifrm(eq(n''''', m''''), n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))), nil)
MINSORT(add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', nil)))) -> IFMINSORT(eq(n''''''0, min(add(n''''''0, x'''''''))), add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', nil))))
IFMINSORT(false, add(n''', x''''), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(x'''', add(n''', add(n''''''''0, add(n'''''''''''', nil))))
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil)))
IFMINSORT(false, add(n'', x'''), add(n'''''''', nil)) -> MINSORT(x''', add(n'', add(n'''''''', nil)))
MINSORT(add(n'''', x''''), add(n''''', nil)) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', nil))
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n'''', add(m'', x'''')), nil) -> MINSORT(app(ifrm(eq(n'''', m''), n'''', add(m'', x'''')), nil), nil)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
IFMINSORT(true, add(n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))) -> MINSORT(app(ifrm(eq(n''''', m''''), n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', add(n'''''''''''''', y'''''''''''')))), nil)
IFMINSORT(true, add(n'''''', add(m''''', x'''''''''')), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))) -> MINSORT(app(ifrm(eq(n'''''', m'''''), n'''''', add(m''''', x'''''''''')), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))), nil)
IFMINSORT(true, add(n'''''', add(m''''', x'''''''''')), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))) -> MINSORT(app(ifrm(eq(n'''''', m'''''), n'''''', add(m''''', x'''''''''')), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))), nil)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 28
↳Instantiation Transformation
IFMINSORT(true, add(n'''', add(m'', x'''')), nil) -> MINSORT(app(ifrm(eq(n'''', m''), n'''', add(m'', x'''')), nil), nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', nil)) -> MINSORT(add(n'''''''', nil), nil)
IFMINSORT(true, add(n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(app(ifrm(eq(n''''', m''''), n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', nil))), nil)
IFMINSORT(true, add(n'''', nil), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(add(n''''''''0, add(n'''''''''''', nil)), nil)
IFMINSORT(true, add(n'''''', add(m''''', x'''''''''')), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))) -> MINSORT(app(ifrm(eq(n'''''', m'''''), n'''''', add(m''''', x'''''''''')), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))), nil)
IFMINSORT(true, add(n''''', nil), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))) -> MINSORT(add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil))), nil)
IFMINSORT(true, add(n'''''', add(m''''', x'''''''''')), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))) -> MINSORT(app(ifrm(eq(n'''''', m'''''), n'''''', add(m''''', x'''''''''')), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))), nil)
IFMINSORT(true, add(n''''', nil), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))) -> MINSORT(add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y'''''''''''''''')))), nil)
IFMINSORT(false, add(n'''', x'''''), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))) -> MINSORT(x''''', add(n'''', add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))))
MINSORT(add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', add(n'''''''''''''''', y''''''''''''''))))) -> IFMINSORT(eq(n''''''0, min(add(n''''''0, x'''''''))), add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', add(n'''''''''''''''', y'''''''''''''')))))
IFMINSORT(false, add(n'''', x'''''), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))) -> MINSORT(x''''', add(n'''', add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))))
MINSORT(add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', nil)))) -> IFMINSORT(eq(n''''''0, min(add(n''''''0, x'''''''))), add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', nil))))
IFMINSORT(false, add(n''', x''''), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(x'''', add(n''', add(n''''''''0, add(n'''''''''''', nil))))
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil)))
IFMINSORT(false, add(n'', x'''), add(n'''''''', nil)) -> MINSORT(x''', add(n'', add(n'''''''', nil)))
MINSORT(add(n'''', x''''), add(n''''', nil)) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', nil))
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', nil)) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', nil)), nil)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
MINSORT(add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', add(n'''''''''''''''', y''''''''''''''))))) -> IFMINSORT(eq(n''''''0, min(add(n''''''0, x'''''''))), add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', add(n'''''''''''''''', y'''''''''''''')))))
MINSORT(add(n''''''0', x''''''''), add(n''''''''', add(n'''''''''''', add(n''''''''''''''', add(n'''''''''''''''''', add(n'''''''''''''''''''', y'''''''''''''''''')))))) -> IFMINSORT(eq(n''''''0', min(add(n''''''0', x''''''''))), add(n''''''0', x''''''''), add(n''''''''', add(n'''''''''''', add(n''''''''''''''', add(n'''''''''''''''''', add(n'''''''''''''''''''', y''''''''''''''''''))))))
MINSORT(add(n''''''0', x''''''''), add(n''''''''', add(n'''''''''''', add(n''''''''''''''', add(n'''''''''''''''''', nil))))) -> IFMINSORT(eq(n''''''0', min(add(n''''''0', x''''''''))), add(n''''''0', x''''''''), add(n''''''''', add(n'''''''''''', add(n''''''''''''''', add(n'''''''''''''''''', nil)))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 29
↳Instantiation Transformation
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', nil)) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', nil)), nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', nil)) -> MINSORT(add(n'''''''', nil), nil)
IFMINSORT(true, add(n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(app(ifrm(eq(n''''', m''''), n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', nil))), nil)
IFMINSORT(true, add(n'''', nil), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(add(n''''''''0, add(n'''''''''''', nil)), nil)
IFMINSORT(true, add(n'''''', add(m''''', x'''''''''')), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))) -> MINSORT(app(ifrm(eq(n'''''', m'''''), n'''''', add(m''''', x'''''''''')), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))), nil)
IFMINSORT(true, add(n''''', nil), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))) -> MINSORT(add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil))), nil)
IFMINSORT(true, add(n'''''', add(m''''', x'''''''''')), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))) -> MINSORT(app(ifrm(eq(n'''''', m'''''), n'''''', add(m''''', x'''''''''')), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))), nil)
IFMINSORT(true, add(n''''', nil), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))) -> MINSORT(add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y'''''''''''''''')))), nil)
MINSORT(add(n''''''0', x''''''''), add(n''''''''', add(n'''''''''''', add(n''''''''''''''', add(n'''''''''''''''''', add(n'''''''''''''''''''', y'''''''''''''''''')))))) -> IFMINSORT(eq(n''''''0', min(add(n''''''0', x''''''''))), add(n''''''0', x''''''''), add(n''''''''', add(n'''''''''''', add(n''''''''''''''', add(n'''''''''''''''''', add(n'''''''''''''''''''', y''''''''''''''''''))))))
IFMINSORT(false, add(n'''', x'''''), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))) -> MINSORT(x''''', add(n'''', add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))))
MINSORT(add(n''''''0', x''''''''), add(n''''''''', add(n'''''''''''', add(n''''''''''''''', add(n'''''''''''''''''', nil))))) -> IFMINSORT(eq(n''''''0', min(add(n''''''0', x''''''''))), add(n''''''0', x''''''''), add(n''''''''', add(n'''''''''''', add(n''''''''''''''', add(n'''''''''''''''''', nil)))))
IFMINSORT(false, add(n'''', x'''''), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))) -> MINSORT(x''''', add(n'''', add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))))
MINSORT(add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', nil)))) -> IFMINSORT(eq(n''''''0, min(add(n''''''0, x'''''''))), add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', nil))))
IFMINSORT(false, add(n''', x''''), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(x'''', add(n''', add(n''''''''0, add(n'''''''''''', nil))))
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil)))
IFMINSORT(false, add(n'', x'''), add(n'''''''', nil)) -> MINSORT(x''', add(n'', add(n'''''''', nil)))
MINSORT(add(n'''', x''''), add(n''''', nil)) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', nil))
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n'''', add(m'', x'''')), nil) -> MINSORT(app(ifrm(eq(n'''', m''), n'''', add(m'', x'''')), nil), nil)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))
two new Dependency Pairs are created:
IFMINSORT(false, add(n'''', x'''''), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))) -> MINSORT(x''''', add(n'''', add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))))
IFMINSORT(false, add(n''''', x''''''), add(n''''''''0'', add(n''''''''''''0', add(n''''''''''''''''0, add(n'''''''''''''''''''', add(n'''''''''''''''''''''', y'''''''''''''''''''')))))) -> MINSORT(x'''''', add(n''''', add(n''''''''0'', add(n''''''''''''0', add(n''''''''''''''''0, add(n'''''''''''''''''''', add(n'''''''''''''''''''''', y'''''''''''''''''''')))))))
IFMINSORT(false, add(n''''', x''''''), add(n''''''''0'', add(n''''''''''''0', add(n''''''''''''''''0, add(n'''''''''''''''''''', nil))))) -> MINSORT(x'''''', add(n''''', add(n''''''''0'', add(n''''''''''''0', add(n''''''''''''''''0, add(n'''''''''''''''''''', nil))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳AFS
→DP Problem 4
↳AFS
→DP Problem 5
↳AFS
→DP Problem 6
↳Nar
→DP Problem 12
↳Nar
...
→DP Problem 30
↳Remaining Obligation(s)
IFMINSORT(true, add(n'''', add(m'', x'''')), nil) -> MINSORT(app(ifrm(eq(n'''', m''), n'''', add(m'', x'''')), nil), nil)
IFMINSORT(true, add(n''', nil), add(n'''''''', nil)) -> MINSORT(add(n'''''''', nil), nil)
IFMINSORT(true, add(n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(app(ifrm(eq(n''''', m''''), n''''', add(m'''', x'''''''')), add(n''''''''0, add(n'''''''''''', nil))), nil)
IFMINSORT(true, add(n'''', nil), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(add(n''''''''0, add(n'''''''''''', nil)), nil)
IFMINSORT(true, add(n'''''', add(m''''', x'''''''''')), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))) -> MINSORT(app(ifrm(eq(n'''''', m'''''), n'''''', add(m''''', x'''''''''')), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))), nil)
IFMINSORT(true, add(n''''', nil), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))) -> MINSORT(add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil))), nil)
IFMINSORT(false, add(n''''', x''''''), add(n''''''''0'', add(n''''''''''''0', add(n''''''''''''''''0, add(n'''''''''''''''''''', add(n'''''''''''''''''''''', y'''''''''''''''''''')))))) -> MINSORT(x'''''', add(n''''', add(n''''''''0'', add(n''''''''''''0', add(n''''''''''''''''0, add(n'''''''''''''''''''', add(n'''''''''''''''''''''', y'''''''''''''''''''')))))))
MINSORT(add(n''''''0', x''''''''), add(n''''''''', add(n'''''''''''', add(n''''''''''''''', add(n'''''''''''''''''', add(n'''''''''''''''''''', y'''''''''''''''''')))))) -> IFMINSORT(eq(n''''''0', min(add(n''''''0', x''''''''))), add(n''''''0', x''''''''), add(n''''''''', add(n'''''''''''', add(n''''''''''''''', add(n'''''''''''''''''', add(n'''''''''''''''''''', y''''''''''''''''''))))))
IFMINSORT(false, add(n''''', x''''''), add(n''''''''0'', add(n''''''''''''0', add(n''''''''''''''''0, add(n'''''''''''''''''''', nil))))) -> MINSORT(x'''''', add(n''''', add(n''''''''0'', add(n''''''''''''0', add(n''''''''''''''''0, add(n'''''''''''''''''''', nil))))))
IFMINSORT(true, add(n'''''', add(m''''', x'''''''''')), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))) -> MINSORT(app(ifrm(eq(n'''''', m'''''), n'''''', add(m''''', x'''''''''')), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))), nil)
IFMINSORT(true, add(n''''', nil), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y''''''''''''''''))))) -> MINSORT(add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', add(n'''''''''''''''''', y'''''''''''''''')))), nil)
MINSORT(add(n''''''0', x''''''''), add(n''''''''', add(n'''''''''''', add(n''''''''''''''', add(n'''''''''''''''''', nil))))) -> IFMINSORT(eq(n''''''0', min(add(n''''''0', x''''''''))), add(n''''''0', x''''''''), add(n''''''''', add(n'''''''''''', add(n''''''''''''''', add(n'''''''''''''''''', nil)))))
IFMINSORT(false, add(n'''', x'''''), add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))) -> MINSORT(x''''', add(n'''', add(n''''''''0', add(n''''''''''''0, add(n'''''''''''''''', nil)))))
MINSORT(add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', nil)))) -> IFMINSORT(eq(n''''''0, min(add(n''''''0, x'''''''))), add(n''''''0, x'''''''), add(n'''''''', add(n''''''''''', add(n'''''''''''''', nil))))
IFMINSORT(false, add(n''', x''''), add(n''''''''0, add(n'''''''''''', nil))) -> MINSORT(x'''', add(n''', add(n''''''''0, add(n'''''''''''', nil))))
MINSORT(add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil))) -> IFMINSORT(eq(n'''''', min(add(n'''''', x''''''))), add(n'''''', x''''''), add(n''''''', add(n'''''''''', nil)))
IFMINSORT(false, add(n'', x'''), add(n'''''''', nil)) -> MINSORT(x''', add(n'', add(n'''''''', nil)))
MINSORT(add(n'''', x''''), add(n''''', nil)) -> IFMINSORT(eq(n'''', min(add(n'''', x''''))), add(n'''', x''''), add(n''''', nil))
IFMINSORT(false, add(n', x'), nil) -> MINSORT(x', add(n', nil))
MINSORT(add(n', x'), nil) -> IFMINSORT(eq(n', min(add(n', x'))), add(n', x'), nil)
IFMINSORT(true, add(n'''', add(m''', x'''''')), add(n'''''''', nil)) -> MINSORT(app(ifrm(eq(n'''', m'''), n'''', add(m''', x'''''')), add(n'''''''', nil)), nil)
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))) -> ifmin(le(n, m), add(n, add(m, x)))
ifmin(true, add(n, add(m, x))) -> min(add(n, x))
ifmin(false, add(n, add(m, x))) -> min(add(m, x))
rm(n, nil) -> nil
rm(n, add(m, x)) -> ifrm(eq(n, m), n, add(m, x))
ifrm(true, n, add(m, x)) -> rm(n, x)
ifrm(false, n, add(m, x)) -> add(m, rm(n, x))
minsort(nil, nil) -> nil
minsort(add(n, x), y) -> ifminsort(eq(n, min(add(n, x))), add(n, x), y)
ifminsort(true, add(n, x), y) -> add(n, minsort(app(rm(n, x), y), nil))
ifminsort(false, add(n, x), y) -> minsort(x, add(n, y))