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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))

Innermost Termination of R to be shown.



   R
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)) -> F1(split(N, Y), N, M, Y)
SPLIT(N, add(M, Y)) -> SPLIT(N, Y)
F1(pair(X, Z), N, M, Y) -> F2(lt(N, M), N, M, Y, X, Z)
F1(pair(X, Z), N, M, Y) -> LT(N, M)
QSORT(add(N, X)) -> F3(split(N, X), N, X)
QSORT(add(N, X)) -> SPLIT(N, X)
F3(pair(Y, Z), N, X) -> APPEND(qsort(Y), add(X, qsort(Z)))
F3(pair(Y, Z), N, X) -> QSORT(Y)
F3(pair(Y, Z), N, X) -> QSORT(Z)

Furthermore, R contains four SCCs.


   R
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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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:



   R
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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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:



   R
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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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(x1, x2))=  1 + x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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:



   R
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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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:



   R
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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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(x1, x2))=  1 + x1  
  POL(add(x1, x2))=  1 + x2  

resulting in one new DP problem.



   R
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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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:



   R
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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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:



   R
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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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(x1, x2))=  1 + x2  
  POL(add(x1, x2))=  1 + x2  

resulting in one new DP problem.



   R
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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
FwdInst
       →DP Problem 3
FwdInst
       →DP Problem 4
Narrowing Transformation


Dependency Pairs:

F3(pair(Y, Z), N, X) -> QSORT(Z)
F3(pair(Y, Z), N, X) -> QSORT(Y)
QSORT(add(N, X)) -> F3(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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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)) -> F3(split(N, X), N, X)
two new Dependency Pairs are created:

QSORT(add(N'', nil)) -> F3(pair(nil, nil), N'', nil)
QSORT(add(N'', add(M', Y'))) -> F3(f1(split(N'', Y'), N'', M', Y'), N'', add(M', Y'))

The transformation is resulting in one new DP problem:



   R
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'))) -> F3(f1(split(N'', Y'), N'', M', Y'), N'', add(M', Y'))
F3(pair(Y, Z), N, X) -> QSORT(Y)
QSORT(add(N'', nil)) -> F3(pair(nil, nil), N'', nil)
F3(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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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'))) -> F3(f1(split(N'', Y'), N'', M', Y'), N'', add(M', Y'))
two new Dependency Pairs are created:

QSORT(add(N''', add(M', nil))) -> F3(f1(pair(nil, nil), N''', M', nil), N''', add(M', nil))
QSORT(add(N''', add(M', add(M'', Y'')))) -> F3(f1(f1(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:



   R
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'')))) -> F3(f1(f1(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))
QSORT(add(N''', add(M', nil))) -> F3(f1(pair(nil, nil), N''', M', nil), N''', add(M', nil))
F3(pair(Y, Z), N, X) -> QSORT(Z)
QSORT(add(N'', nil)) -> F3(pair(nil, nil), N'', nil)
F3(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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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))) -> F3(f1(pair(nil, nil), N''', M', nil), N''', add(M', nil))
one new Dependency Pair is created:

QSORT(add(N''', add(M', nil))) -> F3(f2(lt(N''', M'), N''', M', nil, nil, nil), N''', add(M', nil))

The transformation is resulting in one new DP problem:



   R
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))) -> F3(f2(lt(N''', M'), N''', M', nil, nil, nil), N''', add(M', nil))
F3(pair(Y, Z), N, X) -> QSORT(Z)
QSORT(add(N'', nil)) -> F3(pair(nil, nil), N'', nil)
F3(pair(Y, Z), N, X) -> QSORT(Y)
QSORT(add(N''', add(M', add(M'', Y'')))) -> F3(f1(f1(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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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

F3(pair(Y, Z), N, X) -> QSORT(Y)
three new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem:



   R
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:

F3(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Y')
F3(pair(Y', Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(Y')
QSORT(add(N''', add(M', add(M'', Y'')))) -> F3(f1(f1(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))
QSORT(add(N'', nil)) -> F3(pair(nil, nil), N'', nil)
F3(pair(Y, Z), N, X) -> QSORT(Z)
QSORT(add(N''', add(M', nil))) -> F3(f2(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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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

F3(pair(Y, Z), N, X) -> QSORT(Z)
three new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem:



   R
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:

F3(pair(Y', Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(Z')
F3(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Z')
QSORT(add(N''', add(M', nil))) -> F3(f2(lt(N''', M'), N''', M', nil, nil, nil), N''', add(M', nil))
F3(pair(Y', Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(Y')
QSORT(add(N''', add(M', add(M'', Y'')))) -> F3(f1(f1(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))
F3(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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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

F3(pair(Y', Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(Y')
two new Dependency Pairs are created:

F3(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''''))))
F3(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:



   R
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:

F3(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Z')
F3(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Y')
QSORT(add(N''', add(M', nil))) -> F3(f2(lt(N''', M'), N''', M', nil, nil, nil), N''', add(M', nil))
F3(pair(add(N''''', add(M''', nil)), Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))
F3(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'')))) -> F3(f1(f1(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))
F3(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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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

F3(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Y')
two new Dependency Pairs are created:

F3(pair(add(N''''', add(M'''0, add(M''''', Y''''))), Z'), N', add(M'''0, nil)) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F3(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:



   R
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:

F3(pair(add(N''''', add(M''', nil)), Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))
F3(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''''))))
F3(pair(add(N''''', add(M''', nil)), Z'), N', add(M''', nil)) -> QSORT(add(N''''', add(M''', nil)))
F3(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))) -> F3(f2(lt(N''', M'), N''', M', nil, nil, nil), N''', add(M', nil))
F3(pair(Y', Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(Z')
QSORT(add(N''', add(M', add(M'', Y'')))) -> F3(f1(f1(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))
F3(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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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

F3(pair(Y', Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(Z')
two new Dependency Pairs are created:

F3(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''''))))
F3(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:



   R
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:

F3(pair(add(N''''', add(M''', nil)), Z'), N', add(M''', nil)) -> QSORT(add(N''''', add(M''', nil)))
F3(pair(add(N''''', add(M'''0, add(M''''', Y''''))), Z'), N', add(M'''0, nil)) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F3(pair(Y', add(N''''', add(M''', nil))), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))
F3(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''''))))
F3(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'')))) -> F3(f1(f1(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))
F3(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Z')
QSORT(add(N''', add(M', nil))) -> F3(f2(lt(N''', M'), N''', M', nil, nil, nil), N''', add(M', nil))
F3(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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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

F3(pair(Y', Z'), N', add(M''', nil)) -> QSORT(Z')
two new Dependency Pairs are created:

F3(pair(Y', add(N''''', add(M'''0, add(M''''', Y'''')))), N', add(M'''0, nil)) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F3(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:



   R
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:

F3(pair(Y', add(N''''', add(M''', nil))), N', add(M''', nil)) -> QSORT(add(N''''', add(M''', nil)))
F3(pair(Y', add(N''''', add(M'''0, add(M''''', Y'''')))), N', add(M'''0, nil)) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F3(pair(Y', add(N''''', add(M''', nil))), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))
F3(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''''))))
F3(pair(add(N''''', add(M''', nil)), Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))
F3(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'')))) -> F3(f1(f1(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))
F3(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))) -> F3(f2(lt(N''', M'), N''', M', nil, nil, nil), N''', add(M', nil))
F3(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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))


Strategy:

innermost




The following dependency pairs can be strictly oriented:

F3(pair(Y', add(N''''', add(M''', nil))), N', add(M''', nil)) -> QSORT(add(N''''', add(M''', nil)))
F3(pair(Y', add(N''''', add(M'''0, add(M''''', Y'''')))), N', add(M'''0, nil)) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F3(pair(Y', add(N''''', add(M''', nil))), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))
F3(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''''))))
F3(pair(add(N''''', add(M''', nil)), Z'), N', add(M'''0, add(M''''', Y''''))) -> QSORT(add(N''''', add(M''', nil)))
F3(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''''))))
F3(pair(add(N''''', add(M'''0, add(M''''', Y''''))), Z'), N', add(M'''0, nil)) -> QSORT(add(N''''', add(M'''0, add(M''''', Y''''))))
F3(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:

f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
split(N, nil) -> pair(nil, nil)
split(N, add(M, Y)) -> f1(split(N, Y), N, M, Y)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(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(x1, x2, x3, x4))=  1 + x1  
  POL(false)=  1  
  POL(F_3(x1, x2, x3))=  x1  
  POL(lt(x1, x2))=  1  
  POL(true)=  1  
  POL(add(x1, x2))=  1 + x2  
  POL(0)=  0  
  POL(pair(x1, x2))=  1 + x1 + x2  
  POL(f_2(x1, x2, x3, x4, x5, x6))=  1 + x1 + x5 + x6  
  POL(split(x1, x2))=  1 + x2  
  POL(nil)=  0  
  POL(s(x1))=  0  
  POL(QSORT(x1))=  x1  

resulting in one new DP problem.



   R
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:

QSORT(add(N''', add(M', add(M'', Y'')))) -> F3(f1(f1(split(N''', Y''), N''', M'', Y''), N''', M', add(M'', Y'')), N''', add(M', add(M'', Y'')))
QSORT(add(N''', add(M', nil))) -> F3(f2(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)) -> f1(split(N, Y), N, M, Y)
f1(pair(X, Z), N, M, Y) -> f2(lt(N, M), N, M, Y, X, Z)
f2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
f2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
qsort(nil) -> nil
qsort(add(N, X)) -> f3(split(N, X), N, X)
f3(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