Termination w.r.t. Q of the given QTRS could not be shown:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

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(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
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))

Q is empty.

(1) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

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(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
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))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(4) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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, x)) → MINITER(add(n, x), add(n, x), 0)
MINITER(nil, add(n, y), m) → MINITER(add(n, y), add(n, y), s(m))
MINITER(add(n, x), y, m) → IF_MIN(le(n, m), x, y, m)
MINITER(add(n, x), y, m) → LE(n, m)
IF_MIN(false, x, y, m) → MINITER(x, y, m)
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
RM(n, add(m, x)) → EQ(n, m)
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) → IF_MINSORT(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))
IF_MINSORT(true, add(n, x), y) → MINSORT(app(rm(n, x), y), nil)
IF_MINSORT(true, add(n, x), y) → APP(rm(n, x), y)
IF_MINSORT(true, add(n, x), y) → RM(n, x)
IF_MINSORT(false, add(n, x), y) → MINSORT(x, add(n, y))

The TRS R consists of the following rules:

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(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
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))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 6 SCCs with 7 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP(add(n, x), y) → APP(x, y)

The TRS R consists of the following rules:

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(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
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))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LE(s(x), s(y)) → LE(x, y)

The TRS R consists of the following rules:

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(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
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))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MINITER(add(n, x), y, m) → IF_MIN(le(n, m), x, y, m)
IF_MIN(false, x, y, m) → MINITER(x, y, m)
MINITER(nil, add(n, y), m) → MINITER(add(n, y), add(n, y), s(m))

The TRS R consists of the following rules:

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(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
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))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

EQ(s(x), s(y)) → EQ(x, y)

The TRS R consists of the following rules:

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(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
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))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
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))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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(false, add(n, x), y) → MINSORT(x, add(n, y))

The TRS R consists of the following rules:

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(nil) → 0
min(add(n, x)) → minIter(add(n, x), add(n, x), 0)
minIter(nil, add(n, y), m) → minIter(add(n, y), add(n, y), s(m))
minIter(add(n, x), y, m) → if_min(le(n, m), x, y, m)
if_min(true, x, y, m) → m
if_min(false, x, y, m) → minIter(x, y, m)
head(add(n, x)) → n
tail(add(n, x)) → x
tail(nil) → nil
null(nil) → true
null(add(n, x)) → false
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))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
min(nil)
min(add(x0, x1))
minIter(nil, add(x0, x1), x2)
minIter(add(x0, x1), x2, x3)
if_min(true, x0, x1, x2)
if_min(false, x0, x1, x2)
head(add(x0, x1))
tail(add(x0, x1))
tail(nil)
null(nil)
null(add(x0, x1))
rm(x0, nil)
rm(x0, add(x1, x2))
if_rm(true, x0, add(x1, x2))
if_rm(false, x0, add(x1, x2))
minsort(nil, nil)
minsort(add(x0, x1), x2)
if_minsort(true, add(x0, x1), x2)
if_minsort(false, add(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.