Termination Proof using AProVE

Term Rewriting System R:
[X, Y, N, M, Z]
lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

LT(s(X), s(Y)) -> LT(X, Y)
APPEND(add(N, X), Y) -> APPEND(X, Y)
SPLIT(N, add(M, Y)) -> F₁(split(N, Y), N, M, Y)
SPLIT(N, add(M, Y)) -> SPLIT(N, Y)
F₁(pair(X, Z), N, M, Y) -> F₂(lt(N, M), N, M, Y, X, Z)
F₁(pair(X, Z), N, M, Y) -> LT(N, M)
QSORT(add(N, X)) -> F₃(split(N, X), N, X)
QSORT(add(N, X)) -> SPLIT(N, X)
F₃(pair(Y, Z), N, X) -> APPEND(qsort(Y), add(X, qsort(Z)))
F₃(pair(Y, Z), N, X) -> QSORT(Y)
F₃(pair(Y, Z), N, X) -> QSORT(Z)

Furthermore, R contains four SCCs.

     ↳DPs

       →DP Problem 1

         ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

Dependency Pair:

LT(s(X), s(Y)) -> LT(X, Y)

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

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

LT(s(X), s(Y)) -> LT(X, Y)

one new Dependency Pair is created:

LT(s(s(X'')), s(s(Y''))) -> LT(s(X''), s(Y''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 5

             ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

Dependency Pair:

LT(s(s(X'')), s(s(Y''))) -> LT(s(X''), s(Y''))

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

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

LT(s(s(X'')), s(s(Y''))) -> LT(s(X''), s(Y''))

one new Dependency Pair is created:

LT(s(s(s(X''''))), s(s(s(Y'''')))) -> LT(s(s(X'''')), s(s(Y'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 5

             ↳FwdInst

...

               →DP Problem 6

                 ↳Polynomial Ordering

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

Dependency Pair:

LT(s(s(s(X''''))), s(s(s(Y'''')))) -> LT(s(s(X'''')), s(s(Y'''')))

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

The following dependency pair can be strictly oriented:

LT(s(s(s(X''''))), s(s(s(Y'''')))) -> LT(s(s(X'''')), s(s(Y'''')))

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(LT(x₁, x₂)) = 1 + x₁

POL(s(x₁)) = 1 + x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 5

             ↳FwdInst

...

               →DP Problem 7

                 ↳Dependency Graph

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

Dependency Pair:

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

Dependency Pair:

APPEND(add(N, X), Y) -> APPEND(X, Y)

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

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

APPEND(add(N, X), Y) -> APPEND(X, Y)

one new Dependency Pair is created:

APPEND(add(N, add(N'', X'')), Y'') -> APPEND(add(N'', X''), Y'')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 8

             ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

Dependency Pair:

APPEND(add(N, add(N'', X'')), Y'') -> APPEND(add(N'', X''), Y'')

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

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

APPEND(add(N, add(N'', X'')), Y'') -> APPEND(add(N'', X''), Y'')

one new Dependency Pair is created:

APPEND(add(N, add(N'''', add(N''''', X''''))), Y'''') -> APPEND(add(N'''', add(N''''', X'''')), Y'''')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 8

             ↳FwdInst

...

               →DP Problem 9

                 ↳Polynomial Ordering

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

Dependency Pair:

APPEND(add(N, add(N'''', add(N''''', X''''))), Y'''') -> APPEND(add(N'''', add(N''''', X'''')), Y'''')

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

The following dependency pair can be strictly oriented:

APPEND(add(N, add(N'''', add(N''''', X''''))), Y'''') -> APPEND(add(N'''', add(N''''', X'''')), Y'''')

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(APPEND(x₁, x₂)) = 1 + x₁

POL(add(x₁, x₂)) = 1 + x₂

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 8

             ↳FwdInst

...

               →DP Problem 10

                 ↳Dependency Graph

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

Dependency Pair:

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳Nar

Dependency Pair:

SPLIT(N, add(M, Y)) -> SPLIT(N, Y)

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

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

SPLIT(N, add(M, Y)) -> SPLIT(N, Y)

one new Dependency Pair is created:

SPLIT(N'', add(M, add(M'', Y''))) -> SPLIT(N'', add(M'', Y''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

           →DP Problem 11

             ↳Forward Instantiation Transformation

       →DP Problem 4

         ↳Nar

Dependency Pair:

SPLIT(N'', add(M, add(M'', Y''))) -> SPLIT(N'', add(M'', Y''))

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

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

SPLIT(N'', add(M, add(M'', Y''))) -> SPLIT(N'', add(M'', Y''))

one new Dependency Pair is created:

SPLIT(N'''', add(M, add(M'''', add(M''''', Y'''')))) -> SPLIT(N'''', add(M'''', add(M''''', Y'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

           →DP Problem 11

             ↳FwdInst

...

               →DP Problem 12

                 ↳Polynomial Ordering

       →DP Problem 4

         ↳Nar

Dependency Pair:

SPLIT(N'''', add(M, add(M'''', add(M''''', Y'''')))) -> SPLIT(N'''', add(M'''', add(M''''', Y'''')))

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

The following dependency pair can be strictly oriented:

SPLIT(N'''', add(M, add(M'''', add(M''''', Y'''')))) -> SPLIT(N'''', add(M'''', add(M''''', Y'''')))

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(SPLIT(x₁, x₂)) = 1 + x₂

POL(add(x₁, x₂)) = 1 + x₂

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

           →DP Problem 11

             ↳FwdInst

...

               →DP Problem 13

                 ↳Dependency Graph

       →DP Problem 4

         ↳Nar

Dependency Pair:

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Narrowing Transformation

Dependency Pairs:

F₃(pair(Y, Z), N, X) -> QSORT(Z)
F₃(pair(Y, Z), N, X) -> QSORT(Y)
QSORT(add(N, X)) -> F₃(split(N, X), N, X)

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

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

QSORT(add(N, X)) -> F₃(split(N, X), N, X)

two new Dependency Pairs are created:

QSORT(add(N'', nil)) -> F₃(pair(nil, nil), N'', nil)
QSORT(add(N'', add(M', Y'))) -> F₃(f₁(split(N'', Y'), N'', M', Y'), N'', add(M', Y'))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

           →DP Problem 14

             ↳Narrowing Transformation

Dependency Pairs:

QSORT(add(N'', add(M', Y'))) -> F₃(f₁(split(N'', Y'), N'', M', Y'), N'', add(M', Y'))
F₃(pair(Y, Z), N, X) -> QSORT(Y)
QSORT(add(N'', nil)) -> F₃(pair(nil, nil), N'', nil)
F₃(pair(Y, Z), N, X) -> QSORT(Z)

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

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

QSORT(add(N'', add(M', Y'))) -> F₃(f₁(split(N'', Y'), N'', M', Y'), N'', add(M', Y'))

two new Dependency Pairs are created:

QSORT(add(N''', add(M', nil))) -> F₃(f₁(pair(nil, nil), N''', M', nil), N''', add(M', nil))
QSORT(add(N''', add(M', add(M'', Y'')))) -> F₃(f₁(f₁(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 15

                 ↳Rewriting Transformation

Dependency Pairs:

QSORT(add(N''', add(M', add(M'', Y'')))) -> F₃(f₁(f₁(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))
QSORT(add(N''', add(M', nil))) -> F₃(f₁(pair(nil, nil), N''', M', nil), N''', add(M', nil))
F₃(pair(Y, Z), N, X) -> QSORT(Z)
QSORT(add(N'', nil)) -> F₃(pair(nil, nil), N'', nil)
F₃(pair(Y, Z), N, X) -> QSORT(Y)

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

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

QSORT(add(N''', add(M', nil))) -> F₃(f₁(pair(nil, nil), N''', M', nil), N''', add(M', nil))

one new Dependency Pair is created:

QSORT(add(N''', add(M', nil))) -> F₃(f₂(lt(N''', M'), N''', M', nil, nil, nil), N''', add(M', nil))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 16

                 ↳Instantiation Transformation

Dependency Pairs:

QSORT(add(N''', add(M', nil))) -> F₃(f₂(lt(N''', M'), N''', M', nil, nil, nil), N''', add(M', nil))
F₃(pair(Y, Z), N, X) -> QSORT(Z)
QSORT(add(N'', nil)) -> F₃(pair(nil, nil), N'', nil)
F₃(pair(Y, Z), N, X) -> QSORT(Y)
QSORT(add(N''', add(M', add(M'', Y'')))) -> F₃(f₁(f₁(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

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

F₃(pair(Y, Z), N, X) -> QSORT(Y)

three new Dependency Pairs are created:

F₃(pair(nil, nil), N', nil) -> QSORT(nil)
F₃(pair(Y', Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(Y')
F₃(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Y')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 17

                 ↳Instantiation Transformation

Dependency Pairs:

F₃(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Y')
F₃(pair(Y', Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(Y')
QSORT(add(N''', add(M', add(M'', Y'')))) -> F₃(f₁(f₁(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))
QSORT(add(N'', nil)) -> F₃(pair(nil, nil), N'', nil)
F₃(pair(Y, Z), N, X) -> QSORT(Z)
QSORT(add(N''', add(M', nil))) -> F₃(f₂(lt(N''', M'), N''', M', nil, nil, nil), N''', add(M', nil))

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

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

F₃(pair(Y, Z), N, X) -> QSORT(Z)

three new Dependency Pairs are created:

F₃(pair(nil, nil), N', nil) -> QSORT(nil)
F₃(pair(Y', Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(Z')
F₃(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Z')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 18

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F₃(pair(Y', Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(Z')
F₃(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Z')
QSORT(add(N''', add(M', nil))) -> F₃(f₂(lt(N''', M'), N''', M', nil, nil, nil), N''', add(M', nil))
F₃(pair(Y', Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(Y')
QSORT(add(N''', add(M', add(M'', Y'')))) -> F₃(f₁(f₁(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))
F₃(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Y')

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

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

F₃(pair(Y', Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(Y')

two new Dependency Pairs are created:

F₃(pair(add(N''''', add(M'''0, add(M''''', Y''''))), Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F₃(pair(add(N''''', add(M''', nil)), Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 19

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F₃(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Z')
F₃(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Y')
QSORT(add(N''', add(M', nil))) -> F₃(f₂(lt(N''', M'), N''', M', nil, nil, nil), N''', add(M', nil))
F₃(pair(add(N''''', add(M''', nil)), Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))
F₃(pair(add(N''''', add(M'''0, add(M''''', Y''''))), Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
QSORT(add(N''', add(M', add(M'', Y'')))) -> F₃(f₁(f₁(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))
F₃(pair(Y', Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(Z')

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

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

F₃(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Y')

two new Dependency Pairs are created:

F₃(pair(add(N''''', add(M'''0, add(M''''', Y''''))), Z'), N', add(M'''0, nil)) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F₃(pair(add(N''''', add(M''', nil)), Z'), N', add(M''', nil)) -> QSORT(add(N''''', add(M''', nil)))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 20

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F₃(pair(add(N''''', add(M''', nil)), Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))
F₃(pair(add(N''''', add(M'''0, add(M''''', Y''''))), Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F₃(pair(add(N''''', add(M''', nil)), Z'), N', add(M''', nil)) -> QSORT(add(N''''', add(M''', nil)))
F₃(pair(add(N''''', add(M'''0, add(M''''', Y''''))), Z'), N', add(M'''0, nil)) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
QSORT(add(N''', add(M', nil))) -> F₃(f₂(lt(N''', M'), N''', M', nil, nil, nil), N''', add(M', nil))
F₃(pair(Y', Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(Z')
QSORT(add(N''', add(M', add(M'', Y'')))) -> F₃(f₁(f₁(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))
F₃(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Z')

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

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

F₃(pair(Y', Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(Z')

two new Dependency Pairs are created:

F₃(pair(Y', add(N''''', add(M'''0, add(M''''', Y'''')))), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F₃(pair(Y', add(N''''', add(M''', nil))), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 21

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F₃(pair(add(N''''', add(M''', nil)), Z'), N', add(M''', nil)) -> QSORT(add(N''''', add(M''', nil)))
F₃(pair(add(N''''', add(M'''0, add(M''''', Y''''))), Z'), N', add(M'''0, nil)) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F₃(pair(Y', add(N''''', add(M''', nil))), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))
F₃(pair(Y', add(N''''', add(M'''0, add(M''''', Y'''')))), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F₃(pair(add(N''''', add(M'''0, add(M''''', Y''''))), Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
QSORT(add(N''', add(M', add(M'', Y'')))) -> F₃(f₁(f₁(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))
F₃(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Z')
QSORT(add(N''', add(M', nil))) -> F₃(f₂(lt(N''', M'), N''', M', nil, nil, nil), N''', add(M', nil))
F₃(pair(add(N''''', add(M''', nil)), Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

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

F₃(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Z')

two new Dependency Pairs are created:

F₃(pair(Y', add(N''''', add(M'''0, add(M''''', Y'''')))), N', add(M'''0, nil)) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F₃(pair(Y', add(N''''', add(M''', nil))), N', add(M''', nil)) -> QSORT(add(N''''', add(M''', nil)))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 22

                 ↳Polynomial Ordering

Dependency Pairs:

F₃(pair(Y', add(N''''', add(M''', nil))), N', add(M''', nil)) -> QSORT(add(N''''', add(M''', nil)))
F₃(pair(Y', add(N''''', add(M'''0, add(M''''', Y'''')))), N', add(M'''0, nil)) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F₃(pair(Y', add(N''''', add(M''', nil))), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))
F₃(pair(Y', add(N''''', add(M'''0, add(M''''', Y'''')))), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F₃(pair(add(N''''', add(M''', nil)), Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))
F₃(pair(add(N''''', add(M'''0, add(M''''', Y''''))), Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
QSORT(add(N''', add(M', add(M'', Y'')))) -> F₃(f₁(f₁(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))
F₃(pair(add(N''''', add(M'''0, add(M''''', Y''''))), Z'), N', add(M'''0, nil)) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
QSORT(add(N''', add(M', nil))) -> F₃(f₂(lt(N''', M'), N''', M', nil, nil, nil), N''', add(M', nil))
F₃(pair(add(N''''', add(M''', nil)), Z'), N', add(M''', nil)) -> QSORT(add(N''''', add(M''', nil)))

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

The following dependency pairs can be strictly oriented:

F₃(pair(Y', add(N''''', add(M''', nil))), N', add(M''', nil)) -> QSORT(add(N''''', add(M''', nil)))
F₃(pair(Y', add(N''''', add(M'''0, add(M''''', Y'''')))), N', add(M'''0, nil)) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F₃(pair(Y', add(N''''', add(M''', nil))), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))
F₃(pair(Y', add(N''''', add(M'''0, add(M''''', Y'''')))), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F₃(pair(add(N''''', add(M''', nil)), Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))
F₃(pair(add(N''''', add(M'''0, add(M''''', Y''''))), Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F₃(pair(add(N''''', add(M'''0, add(M''''', Y''''))), Z'), N', add(M'''0, nil)) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F₃(pair(add(N''''', add(M''', nil)), Z'), N', add(M''', nil)) -> QSORT(add(N''''', add(M''', nil)))

Additionally, the following usable rules for innermost w.r.t. to the implicit AFS can be oriented:

f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(f_1(x₁, x₂, x₃, x₄)) = 1 + x₁

POL(false) = 1

POL(F_3(x₁, x₂, x₃)) = x₁

POL(lt(x₁, x₂)) = 1

POL(true) = 1

POL(add(x₁, x₂)) = 1 + x₂

POL(0) = 0

POL(pair(x₁, x₂)) = 1 + x₁ + x₂

POL(f_2(x₁, x₂, x₃, x₄, x₅, x₆)) = 1 + x₁ + x₅ + x₆

POL(split(x₁, x₂)) = 1 + x₂

POL(nil) = 0

POL(s(x₁)) = 0

POL(QSORT(x₁)) = x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

       →DP Problem 4

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 23

                 ↳Dependency Graph

Dependency Pairs:

Rules:

lt(0, s(X)) -> true
lt(s(X), 0) -> false
lt(s(X), s(Y)) -> lt(X, Y)
append(nil, Y) -> Y
append(add(N, X), Y) -> add(N, append(X, Y))
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f₁(split(N, Y), N, M, Y)
f₁(pair(X, Z), N, M, Y) -> f₂(lt(N, M), N, M, Y, X, Z)
f₂(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f₂(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f₃(split(N, X), N, X)
f₃(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:02 minutes

POL(APPEND(x₁, x₂))	= 1 + x₁
POL(add(x₁, x₂))	= 1 + x₂

POL(SPLIT(x₁, x₂))	= 1 + x₂
POL(add(x₁, x₂))	= 1 + x₂

POL(f_1(x₁, x₂, x₃, x₄))	= 1 + x₁
POL(false)	= 1
POL(F_3(x₁, x₂, x₃))	= x₁
POL(lt(x₁, x₂))	= 1
POL(true)	= 1
POL(add(x₁, x₂))	= 1 + x₂
POL(0)	= 0
POL(pair(x₁, x₂))	= 1 + x₁ + x₂
POL(f_2(x₁, x₂, x₃, x₄, x₅, x₆))	= 1 + x₁ + x₅ + x₆
POL(split(x₁, x₂))	= 1 + x₂
POL(nil)	= 0
POL(s(x₁))	= 0
POL(QSORT(x₁))	= x₁