Termination Proof using AProVE

Term Rewriting System R:
[m, n, x, k]
eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

EQ(s(n), s(m)) -> EQ(n, m)
LE(s(n), s(m)) -> LE(n, m)
MIN(cons(n, cons(m, x))) -> IF_MIN(le(n, m), cons(n, cons(m, x)))
MIN(cons(n, cons(m, x))) -> LE(n, m)
IF_MIN(true, cons(n, cons(m, x))) -> MIN(cons(n, x))
IF_MIN(false, cons(n, cons(m, x))) -> MIN(cons(m, x))
REPLACE(n, m, cons(k, x)) -> IF_REPLACE(eq(n, k), n, m, cons(k, x))
REPLACE(n, m, cons(k, x)) -> EQ(n, k)
IF_REPLACE(false, n, m, cons(k, x)) -> REPLACE(n, m, x)
SORT(cons(n, x)) -> MIN(cons(n, x))
SORT(cons(n, x)) -> SORT(replace(min(cons(n, x)), n, x))
SORT(cons(n, x)) -> REPLACE(min(cons(n, x)), n, x)

Furthermore, R contains five SCCs.

     ↳DPs

       →DP Problem 1

         ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Remaining

Dependency Pair:

EQ(s(n), s(m)) -> EQ(n, m)

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:

innermost

The following dependency pair can be strictly oriented:

EQ(s(n), s(m)) -> EQ(n, m)

There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:

EQ(x₁, x₂) -> EQ(x₁, x₂)
s(x₁) -> s(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 6

             ↳Dependency Graph

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Remaining

Dependency Pair:

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Argument Filtering and Ordering

       →DP Problem 3

         ↳Nar

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Remaining

Dependency Pair:

LE(s(n), s(m)) -> LE(n, m)

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:

innermost

The following dependency pair can be strictly oriented:

LE(s(n), s(m)) -> LE(n, m)

There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:

LE(x₁, x₂) -> LE(x₁, x₂)
s(x₁) -> s(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

           →DP Problem 7

             ↳Dependency Graph

       →DP Problem 3

         ↳Nar

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Remaining

Dependency Pair:

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Narrowing Transformation

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Remaining

Dependency Pairs:

IF_REPLACE(false, n, m, cons(k, x)) -> REPLACE(n, m, x)
REPLACE(n, m, cons(k, x)) -> IF_REPLACE(eq(n, k), n, m, cons(k, x))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:

innermost

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

REPLACE(n, m, cons(k, x)) -> IF_REPLACE(eq(n, k), n, m, cons(k, x))

four new Dependency Pairs are created:

REPLACE(0, m, cons(0, x)) -> IF_REPLACE(true, 0, m, cons(0, x))
REPLACE(0, m, cons(s(m''), x)) -> IF_REPLACE(false, 0, m, cons(s(m''), x))
REPLACE(s(n''), m, cons(0, x)) -> IF_REPLACE(false, s(n''), m, cons(0, x))
REPLACE(s(n''), m, cons(s(m''), x)) -> IF_REPLACE(eq(n'', m''), s(n''), m, cons(s(m''), x))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 8

             ↳Instantiation Transformation

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Remaining

Dependency Pairs:

REPLACE(s(n''), m, cons(s(m''), x)) -> IF_REPLACE(eq(n'', m''), s(n''), m, cons(s(m''), x))
REPLACE(s(n''), m, cons(0, x)) -> IF_REPLACE(false, s(n''), m, cons(0, x))
REPLACE(0, m, cons(s(m''), x)) -> IF_REPLACE(false, 0, m, cons(s(m''), x))
IF_REPLACE(false, n, m, cons(k, x)) -> REPLACE(n, m, x)

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:

innermost

On this DP problem, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

IF_REPLACE(false, n, m, cons(k, x)) -> REPLACE(n, m, x)

three new Dependency Pairs are created:

IF_REPLACE(false, 0, m'', cons(s(m''''), x'')) -> REPLACE(0, m'', x'')
IF_REPLACE(false, s(n''''), m'', cons(0, x'')) -> REPLACE(s(n''''), m'', x'')
IF_REPLACE(false, s(n''''), m'', cons(s(m''''), x')) -> REPLACE(s(n''''), m'', x')

The transformation is resulting in two new DP problems:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 8

             ↳Inst

...

               →DP Problem 9

                 ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Remaining

Dependency Pairs:

IF_REPLACE(false, s(n''''), m'', cons(0, x'')) -> REPLACE(s(n''''), m'', x'')
REPLACE(s(n''), m, cons(0, x)) -> IF_REPLACE(false, s(n''), m, cons(0, x))
IF_REPLACE(false, s(n''''), m'', cons(s(m''''), x')) -> REPLACE(s(n''''), m'', x')
REPLACE(s(n''), m, cons(s(m''), x)) -> IF_REPLACE(eq(n'', m''), s(n''), m, cons(s(m''), x))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

IF_REPLACE(false, s(n''''), m'', cons(0, x'')) -> REPLACE(s(n''''), m'', x'')

two new Dependency Pairs are created:

IF_REPLACE(false, s(n'''''), m''', cons(0, cons(0, x'''))) -> REPLACE(s(n'''''), m''', cons(0, x'''))
IF_REPLACE(false, s(n'''''), m''0, cons(0, cons(s(m''''), x'''))) -> REPLACE(s(n'''''), m''0, cons(s(m''''), x'''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 8

             ↳Inst

...

               →DP Problem 11

                 ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Remaining

Dependency Pairs:

IF_REPLACE(false, s(n''''), m'', cons(s(m''''), x')) -> REPLACE(s(n''''), m'', x')
REPLACE(s(n''), m, cons(s(m''), x)) -> IF_REPLACE(eq(n'', m''), s(n''), m, cons(s(m''), x))
IF_REPLACE(false, s(n'''''), m''0, cons(0, cons(s(m''''), x'''))) -> REPLACE(s(n'''''), m''0, cons(s(m''''), x'''))
IF_REPLACE(false, s(n'''''), m''', cons(0, cons(0, x'''))) -> REPLACE(s(n'''''), m''', cons(0, x'''))
REPLACE(s(n''), m, cons(0, x)) -> IF_REPLACE(false, s(n''), m, cons(0, x))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

REPLACE(s(n''), m, cons(0, x)) -> IF_REPLACE(false, s(n''), m, cons(0, x))

two new Dependency Pairs are created:

REPLACE(s(n'''), m', cons(0, cons(0, x'''''))) -> IF_REPLACE(false, s(n'''), m', cons(0, cons(0, x''''')))
REPLACE(s(n'''), m', cons(0, cons(s(m''''''), x'''''))) -> IF_REPLACE(false, s(n'''), m', cons(0, cons(s(m''''''), x''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 8

             ↳Inst

...

               →DP Problem 13

                 ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Remaining

Dependency Pairs:

IF_REPLACE(false, s(n'''''), m''0, cons(0, cons(s(m''''), x'''))) -> REPLACE(s(n'''''), m''0, cons(s(m''''), x'''))
REPLACE(s(n'''), m', cons(0, cons(s(m''''''), x'''''))) -> IF_REPLACE(false, s(n'''), m', cons(0, cons(s(m''''''), x''''')))
IF_REPLACE(false, s(n'''''), m''', cons(0, cons(0, x'''))) -> REPLACE(s(n'''''), m''', cons(0, x'''))
REPLACE(s(n'''), m', cons(0, cons(0, x'''''))) -> IF_REPLACE(false, s(n'''), m', cons(0, cons(0, x''''')))
REPLACE(s(n''), m, cons(s(m''), x)) -> IF_REPLACE(eq(n'', m''), s(n''), m, cons(s(m''), x))
IF_REPLACE(false, s(n''''), m'', cons(s(m''''), x')) -> REPLACE(s(n''''), m'', x')

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

IF_REPLACE(false, s(n''''), m'', cons(s(m''''), x')) -> REPLACE(s(n''''), m'', x')

three new Dependency Pairs are created:

IF_REPLACE(false, s(n'''''), m''0, cons(s(m''''), cons(s(m''''), x'''))) -> REPLACE(s(n'''''), m''0, cons(s(m''''), x'''))
IF_REPLACE(false, s(n''''''), m'''', cons(s(m''''), cons(0, cons(0, x''''''')))) -> REPLACE(s(n''''''), m'''', cons(0, cons(0, x''''''')))
IF_REPLACE(false, s(n''''''), m'''', cons(s(m''''), cons(0, cons(s(m''''''''), x''''''')))) -> REPLACE(s(n''''''), m'''', cons(0, cons(s(m''''''''), x''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 8

             ↳Inst

...

               →DP Problem 15

                 ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Remaining

Dependency Pairs:

IF_REPLACE(false, s(n''''''), m'''', cons(s(m''''), cons(0, cons(s(m''''''''), x''''''')))) -> REPLACE(s(n''''''), m'''', cons(0, cons(s(m''''''''), x''''''')))
REPLACE(s(n'''), m', cons(0, cons(s(m''''''), x'''''))) -> IF_REPLACE(false, s(n'''), m', cons(0, cons(s(m''''''), x''''')))
IF_REPLACE(false, s(n'''''), m''', cons(0, cons(0, x'''))) -> REPLACE(s(n'''''), m''', cons(0, x'''))
REPLACE(s(n'''), m', cons(0, cons(0, x'''''))) -> IF_REPLACE(false, s(n'''), m', cons(0, cons(0, x''''')))
IF_REPLACE(false, s(n''''''), m'''', cons(s(m''''), cons(0, cons(0, x''''''')))) -> REPLACE(s(n''''''), m'''', cons(0, cons(0, x''''''')))
IF_REPLACE(false, s(n'''''), m''0, cons(s(m''''), cons(s(m''''), x'''))) -> REPLACE(s(n'''''), m''0, cons(s(m''''), x'''))
REPLACE(s(n''), m, cons(s(m''), x)) -> IF_REPLACE(eq(n'', m''), s(n''), m, cons(s(m''), x))
IF_REPLACE(false, s(n'''''), m''0, cons(0, cons(s(m''''), x'''))) -> REPLACE(s(n'''''), m''0, cons(s(m''''), x'''))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

REPLACE(s(n''), m, cons(s(m''), x)) -> IF_REPLACE(eq(n'', m''), s(n''), m, cons(s(m''), x))

three new Dependency Pairs are created:

REPLACE(s(n'''), m', cons(s(m'''), cons(s(m'''''''), x'''''))) -> IF_REPLACE(eq(n''', m'''), s(n'''), m', cons(s(m'''), cons(s(m'''''''), x''''')))
REPLACE(s(n'''), m', cons(s(m'''), cons(0, cons(0, x''''''''')))) -> IF_REPLACE(eq(n''', m'''), s(n'''), m', cons(s(m'''), cons(0, cons(0, x'''''''''))))
REPLACE(s(n'''), m', cons(s(m'''), cons(0, cons(s(m''''''''''), x''''''''')))) -> IF_REPLACE(eq(n''', m'''), s(n'''), m', cons(s(m'''), cons(0, cons(s(m''''''''''), x'''''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
REPLACE(s(n'''), m', cons(s(m'''), cons(0, cons(s(m''''''''''), x''''''''')))) -> IF_REPLACE(eq(n''', m'''), s(n'''), m', cons(s(m'''), cons(0, cons(s(m''''''''''), x'''''''''))))
IF_REPLACE(false, s(n'''''), m''', cons(0, cons(0, x'''))) -> REPLACE(s(n'''''), m''', cons(0, x'''))
REPLACE(s(n'''), m', cons(0, cons(0, x'''''))) -> IF_REPLACE(false, s(n'''), m', cons(0, cons(0, x''''')))
IF_REPLACE(false, s(n''''''), m'''', cons(s(m''''), cons(0, cons(0, x''''''')))) -> REPLACE(s(n''''''), m'''', cons(0, cons(0, x''''''')))
REPLACE(s(n'''), m', cons(s(m'''), cons(0, cons(0, x''''''''')))) -> IF_REPLACE(eq(n''', m'''), s(n'''), m', cons(s(m'''), cons(0, cons(0, x'''''''''))))
IF_REPLACE(false, s(n'''''), m''0, cons(s(m''''), cons(s(m''''), x'''))) -> REPLACE(s(n'''''), m''0, cons(s(m''''), x'''))
REPLACE(s(n'''), m', cons(s(m'''), cons(s(m'''''''), x'''''))) -> IF_REPLACE(eq(n''', m'''), s(n'''), m', cons(s(m'''), cons(s(m'''''''), x''''')))
IF_REPLACE(false, s(n'''''), m''0, cons(0, cons(s(m''''), x'''))) -> REPLACE(s(n'''''), m''0, cons(s(m''''), x'''))
REPLACE(s(n'''), m', cons(0, cons(s(m''''''), x'''''))) -> IF_REPLACE(false, s(n'''), m', cons(0, cons(s(m''''''), x''''')))
IF_REPLACE(false, s(n''''''), m'''', cons(s(m''''), cons(0, cons(s(m''''''''), x''''''')))) -> REPLACE(s(n''''''), m'''', cons(0, cons(s(m''''''''), x''''''')))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:
innermost
Dependency Pairs:
IF_MIN(false, cons(n, cons(m, x))) -> MIN(cons(m, x))
IF_MIN(true, cons(n, cons(m, x))) -> MIN(cons(n, x))
MIN(cons(n, cons(m, x))) -> IF_MIN(le(n, m), cons(n, cons(m, x)))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:
innermost
Dependency Pair:
SORT(cons(n, x)) -> SORT(replace(min(cons(n, x)), n, x))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:
innermost

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 8

             ↳Inst

...

               →DP Problem 10

                 ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Remaining

Dependency Pairs:

IF_REPLACE(false, 0, m'', cons(s(m''''), x'')) -> REPLACE(0, m'', x'')
REPLACE(0, m, cons(s(m''), x)) -> IF_REPLACE(false, 0, m, cons(s(m''), x))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

IF_REPLACE(false, 0, m'', cons(s(m''''), x'')) -> REPLACE(0, m'', x'')

one new Dependency Pair is created:

IF_REPLACE(false, 0, m''0, cons(s(m''''), cons(s(m''''), x'''))) -> REPLACE(0, m''0, cons(s(m''''), x'''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 8

             ↳Inst

...

               →DP Problem 12

                 ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Remaining

Dependency Pairs:

IF_REPLACE(false, 0, m''0, cons(s(m''''), cons(s(m''''), x'''))) -> REPLACE(0, m''0, cons(s(m''''), x'''))
REPLACE(0, m, cons(s(m''), x)) -> IF_REPLACE(false, 0, m, cons(s(m''), x))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

REPLACE(0, m, cons(s(m''), x)) -> IF_REPLACE(false, 0, m, cons(s(m''), x))

one new Dependency Pair is created:

REPLACE(0, m', cons(s(m'''), cons(s(m'''''''), x'''''))) -> IF_REPLACE(false, 0, m', cons(s(m'''), cons(s(m'''''''), x''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 8

             ↳Inst

...

               →DP Problem 14

                 ↳Argument Filtering and Ordering

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Remaining

Dependency Pairs:

REPLACE(0, m', cons(s(m'''), cons(s(m'''''''), x'''''))) -> IF_REPLACE(false, 0, m', cons(s(m'''), cons(s(m'''''''), x''''')))
IF_REPLACE(false, 0, m''0, cons(s(m''''), cons(s(m''''), x'''))) -> REPLACE(0, m''0, cons(s(m''''), x'''))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:

innermost

The following dependency pair can be strictly oriented:

IF_REPLACE(false, 0, m''0, cons(s(m''''), cons(s(m''''), x'''))) -> REPLACE(0, m''0, cons(s(m''''), x'''))

There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:

REPLACE(x₁, x₂, x₃) -> x₃
cons(x₁, x₂) -> cons(x₁, x₂)
IF_REPLACE(x₁, x₂, x₃, x₄) -> x₄
s(x₁) -> s(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

           →DP Problem 8

             ↳Inst

...

               →DP Problem 17

                 ↳Dependency Graph

       →DP Problem 4

         ↳Remaining

       →DP Problem 5

         ↳Remaining

Dependency Pair:

REPLACE(0, m', cons(s(m'''), cons(s(m'''''''), x'''''))) -> IF_REPLACE(false, 0, m', cons(s(m'''), cons(s(m'''''''), x''''')))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
REPLACE(s(n'''), m', cons(s(m'''), cons(0, cons(s(m''''''''''), x''''''''')))) -> IF_REPLACE(eq(n''', m'''), s(n'''), m', cons(s(m'''), cons(0, cons(s(m''''''''''), x'''''''''))))
IF_REPLACE(false, s(n'''''), m''', cons(0, cons(0, x'''))) -> REPLACE(s(n'''''), m''', cons(0, x'''))
REPLACE(s(n'''), m', cons(0, cons(0, x'''''))) -> IF_REPLACE(false, s(n'''), m', cons(0, cons(0, x''''')))
IF_REPLACE(false, s(n''''''), m'''', cons(s(m''''), cons(0, cons(0, x''''''')))) -> REPLACE(s(n''''''), m'''', cons(0, cons(0, x''''''')))
REPLACE(s(n'''), m', cons(s(m'''), cons(0, cons(0, x''''''''')))) -> IF_REPLACE(eq(n''', m'''), s(n'''), m', cons(s(m'''), cons(0, cons(0, x'''''''''))))
IF_REPLACE(false, s(n'''''), m''0, cons(s(m''''), cons(s(m''''), x'''))) -> REPLACE(s(n'''''), m''0, cons(s(m''''), x'''))
REPLACE(s(n'''), m', cons(s(m'''), cons(s(m'''''''), x'''''))) -> IF_REPLACE(eq(n''', m'''), s(n'''), m', cons(s(m'''), cons(s(m'''''''), x''''')))
IF_REPLACE(false, s(n'''''), m''0, cons(0, cons(s(m''''), x'''))) -> REPLACE(s(n'''''), m''0, cons(s(m''''), x'''))
REPLACE(s(n'''), m', cons(0, cons(s(m''''''), x'''''))) -> IF_REPLACE(false, s(n'''), m', cons(0, cons(s(m''''''), x''''')))
IF_REPLACE(false, s(n''''''), m'''', cons(s(m''''), cons(0, cons(s(m''''''''), x''''''')))) -> REPLACE(s(n''''''), m'''', cons(0, cons(s(m''''''''), x''''''')))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:
innermost
Dependency Pairs:
IF_MIN(false, cons(n, cons(m, x))) -> MIN(cons(m, x))
IF_MIN(true, cons(n, cons(m, x))) -> MIN(cons(n, x))
MIN(cons(n, cons(m, x))) -> IF_MIN(le(n, m), cons(n, cons(m, x)))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:
innermost
Dependency Pair:
SORT(cons(n, x)) -> SORT(replace(min(cons(n, x)), n, x))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:
innermost

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Nar

       →DP Problem 4

         ↳Remaining Obligation(s)

       →DP Problem 5

         ↳Remaining Obligation(s)

The following remains to be proven:

Dependency Pairs:
REPLACE(s(n'''), m', cons(s(m'''), cons(0, cons(s(m''''''''''), x''''''''')))) -> IF_REPLACE(eq(n''', m'''), s(n'''), m', cons(s(m'''), cons(0, cons(s(m''''''''''), x'''''''''))))
IF_REPLACE(false, s(n'''''), m''', cons(0, cons(0, x'''))) -> REPLACE(s(n'''''), m''', cons(0, x'''))
REPLACE(s(n'''), m', cons(0, cons(0, x'''''))) -> IF_REPLACE(false, s(n'''), m', cons(0, cons(0, x''''')))
IF_REPLACE(false, s(n''''''), m'''', cons(s(m''''), cons(0, cons(0, x''''''')))) -> REPLACE(s(n''''''), m'''', cons(0, cons(0, x''''''')))
REPLACE(s(n'''), m', cons(s(m'''), cons(0, cons(0, x''''''''')))) -> IF_REPLACE(eq(n''', m'''), s(n'''), m', cons(s(m'''), cons(0, cons(0, x'''''''''))))
IF_REPLACE(false, s(n'''''), m''0, cons(s(m''''), cons(s(m''''), x'''))) -> REPLACE(s(n'''''), m''0, cons(s(m''''), x'''))
REPLACE(s(n'''), m', cons(s(m'''), cons(s(m'''''''), x'''''))) -> IF_REPLACE(eq(n''', m'''), s(n'''), m', cons(s(m'''), cons(s(m'''''''), x''''')))
IF_REPLACE(false, s(n'''''), m''0, cons(0, cons(s(m''''), x'''))) -> REPLACE(s(n'''''), m''0, cons(s(m''''), x'''))
REPLACE(s(n'''), m', cons(0, cons(s(m''''''), x'''''))) -> IF_REPLACE(false, s(n'''), m', cons(0, cons(s(m''''''), x''''')))
IF_REPLACE(false, s(n''''''), m'''', cons(s(m''''), cons(0, cons(s(m''''''''), x''''''')))) -> REPLACE(s(n''''''), m'''', cons(0, cons(s(m''''''''), x''''''')))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:
innermost
Dependency Pairs:
IF_MIN(false, cons(n, cons(m, x))) -> MIN(cons(m, x))
IF_MIN(true, cons(n, cons(m, x))) -> MIN(cons(n, x))
MIN(cons(n, cons(m, x))) -> IF_MIN(le(n, m), cons(n, cons(m, x)))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:
innermost
Dependency Pair:
SORT(cons(n, x)) -> SORT(replace(min(cons(n, x)), n, x))

Rules:

eq(0, 0) -> true
eq(0, s(m)) -> false
eq(s(n), 0) -> false
eq(s(n), s(m)) -> eq(n, m)
le(0, m) -> true
le(s(n), 0) -> false
le(s(n), s(m)) -> le(n, m)
min(cons(0, nil)) -> 0
min(cons(s(n), nil)) -> s(n)
min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) -> min(cons(n, x))
if_min(false, cons(n, cons(m, x))) -> min(cons(m, x))
replace(n, m, nil) -> nil
replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) -> cons(m, x)
if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x))
sort(nil) -> nil
sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Strategy:
innermost

Innermost Termination of R could not be shown.
Duration:
0:04 minutes