Term Rewriting System R:
[x0, y, l12, l21, x, l, a4, l3, l', l1, l2, l5, a]
test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

APPEND(l12, l21) -> MATCH0(l12, l21, l12)
MATCH0(l12, l21, Cons(x, l)) -> APPEND(l, l21)
PART(a4, l3) -> MATCH1(a4, l3, l3)
MATCH1(a4, l3, Cons(x, l')) -> MATCH2(x, l', a4, l3, part(a4, l'))
MATCH1(a4, l3, Cons(x, l')) -> PART(a4, l')
MATCH2(x, l', a4, l3, Pair(l1, l2)) -> MATCH3(l1, l2, x, l', a4, l3, test(a4, x))
MATCH2(x, l', a4, l3, Pair(l1, l2)) -> TEST(a4, x)
QUICK(l5) -> MATCH4(l5, l5)
MATCH4(l5, Cons(a, l')) -> MATCH5(a, l', l5, part(a, l'))
MATCH4(l5, Cons(a, l')) -> PART(a, l')
MATCH5(a, l', l5, Pair(l1, l2)) -> APPEND(quick(l1), Cons(a, quick(l2)))
MATCH5(a, l', l5, Pair(l1, l2)) -> QUICK(l1)
MATCH5(a, l', l5, Pair(l1, l2)) -> QUICK(l2)

Furthermore, R contains three SCCs.


   R
DPs
       →DP Problem 1
Instantiation Transformation
       →DP Problem 2
Inst
       →DP Problem 3
Nar


Dependency Pairs:

MATCH0(l12, l21, Cons(x, l)) -> APPEND(l, l21)
APPEND(l12, l21) -> MATCH0(l12, l21, l12)


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




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

MATCH0(l12, l21, Cons(x, l)) -> APPEND(l, l21)
one new Dependency Pair is created:

MATCH0(Cons(x', l'), l21'', Cons(x', l')) -> APPEND(l', l21'')

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Inst
           →DP Problem 4
Forward Instantiation Transformation
       →DP Problem 2
Inst
       →DP Problem 3
Nar


Dependency Pairs:

MATCH0(Cons(x', l'), l21'', Cons(x', l')) -> APPEND(l', l21'')
APPEND(l12, l21) -> MATCH0(l12, l21, l12)


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




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

APPEND(l12, l21) -> MATCH0(l12, l21, l12)
one new Dependency Pair is created:

APPEND(Cons(x'''', l''''), l21') -> MATCH0(Cons(x'''', l''''), l21', Cons(x'''', l''''))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Inst
           →DP Problem 4
FwdInst
             ...
               →DP Problem 5
Forward Instantiation Transformation
       →DP Problem 2
Inst
       →DP Problem 3
Nar


Dependency Pairs:

APPEND(Cons(x'''', l''''), l21') -> MATCH0(Cons(x'''', l''''), l21', Cons(x'''', l''''))
MATCH0(Cons(x', l'), l21'', Cons(x', l')) -> APPEND(l', l21'')


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




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

MATCH0(Cons(x', l'), l21'', Cons(x', l')) -> APPEND(l', l21'')
one new Dependency Pair is created:

MATCH0(Cons(x', Cons(x'''''', l'''''')), l21'''', Cons(x', Cons(x'''''', l''''''))) -> APPEND(Cons(x'''''', l''''''), l21'''')

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Inst
           →DP Problem 4
FwdInst
             ...
               →DP Problem 6
Forward Instantiation Transformation
       →DP Problem 2
Inst
       →DP Problem 3
Nar


Dependency Pairs:

MATCH0(Cons(x', Cons(x'''''', l'''''')), l21'''', Cons(x', Cons(x'''''', l''''''))) -> APPEND(Cons(x'''''', l''''''), l21'''')
APPEND(Cons(x'''', l''''), l21') -> MATCH0(Cons(x'''', l''''), l21', Cons(x'''', l''''))


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




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

APPEND(Cons(x'''', l''''), l21') -> MATCH0(Cons(x'''', l''''), l21', Cons(x'''', l''''))
one new Dependency Pair is created:

APPEND(Cons(x''''', Cons(x''''''''', l''''''''')), l21'') -> MATCH0(Cons(x''''', Cons(x''''''''', l''''''''')), l21'', Cons(x''''', Cons(x''''''''', l''''''''')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Inst
           →DP Problem 4
FwdInst
             ...
               →DP Problem 7
Polynomial Ordering
       →DP Problem 2
Inst
       →DP Problem 3
Nar


Dependency Pairs:

APPEND(Cons(x''''', Cons(x''''''''', l''''''''')), l21'') -> MATCH0(Cons(x''''', Cons(x''''''''', l''''''''')), l21'', Cons(x''''', Cons(x''''''''', l''''''''')))
MATCH0(Cons(x', Cons(x'''''', l'''''')), l21'''', Cons(x', Cons(x'''''', l''''''))) -> APPEND(Cons(x'''''', l''''''), l21'''')


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




The following dependency pair can be strictly oriented:

MATCH0(Cons(x', Cons(x'''''', l'''''')), l21'''', Cons(x', Cons(x'''''', l''''''))) -> APPEND(Cons(x'''''', l''''''), l21'''')


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(MATCH_0(x1, x2, x3))=  x3  
  POL(Cons(x1, x2))=  1 + x2  
  POL(APPEND(x1, x2))=  x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Inst
           →DP Problem 4
FwdInst
             ...
               →DP Problem 8
Dependency Graph
       →DP Problem 2
Inst
       →DP Problem 3
Nar


Dependency Pair:

APPEND(Cons(x''''', Cons(x''''''''', l''''''''')), l21'') -> MATCH0(Cons(x''''', Cons(x''''''''', l''''''''')), l21'', Cons(x''''', Cons(x''''''''', l''''''''')))


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
Inst
       →DP Problem 2
Instantiation Transformation
       →DP Problem 3
Nar


Dependency Pairs:

MATCH1(a4, l3, Cons(x, l')) -> PART(a4, l')
PART(a4, l3) -> MATCH1(a4, l3, l3)


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




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

MATCH1(a4, l3, Cons(x, l')) -> PART(a4, l')
one new Dependency Pair is created:

MATCH1(a4'', Cons(x', l''), Cons(x', l'')) -> PART(a4'', l'')

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Inst
       →DP Problem 2
Inst
           →DP Problem 9
Forward Instantiation Transformation
       →DP Problem 3
Nar


Dependency Pairs:

MATCH1(a4'', Cons(x', l''), Cons(x', l'')) -> PART(a4'', l'')
PART(a4, l3) -> MATCH1(a4, l3, l3)


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




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

PART(a4, l3) -> MATCH1(a4, l3, l3)
one new Dependency Pair is created:

PART(a4', Cons(x'''', l''''')) -> MATCH1(a4', Cons(x'''', l'''''), Cons(x'''', l'''''))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Inst
       →DP Problem 2
Inst
           →DP Problem 9
FwdInst
             ...
               →DP Problem 10
Forward Instantiation Transformation
       →DP Problem 3
Nar


Dependency Pairs:

PART(a4', Cons(x'''', l''''')) -> MATCH1(a4', Cons(x'''', l'''''), Cons(x'''', l'''''))
MATCH1(a4'', Cons(x', l''), Cons(x', l'')) -> PART(a4'', l'')


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




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

MATCH1(a4'', Cons(x', l''), Cons(x', l'')) -> PART(a4'', l'')
one new Dependency Pair is created:

MATCH1(a4'''', Cons(x', Cons(x'''''', l''''''')), Cons(x', Cons(x'''''', l'''''''))) -> PART(a4'''', Cons(x'''''', l'''''''))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Inst
       →DP Problem 2
Inst
           →DP Problem 9
FwdInst
             ...
               →DP Problem 11
Forward Instantiation Transformation
       →DP Problem 3
Nar


Dependency Pairs:

MATCH1(a4'''', Cons(x', Cons(x'''''', l''''''')), Cons(x', Cons(x'''''', l'''''''))) -> PART(a4'''', Cons(x'''''', l'''''''))
PART(a4', Cons(x'''', l''''')) -> MATCH1(a4', Cons(x'''', l'''''), Cons(x'''', l'''''))


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




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

PART(a4', Cons(x'''', l''''')) -> MATCH1(a4', Cons(x'''', l'''''), Cons(x'''', l'''''))
one new Dependency Pair is created:

PART(a4'', Cons(x''''', Cons(x''''''''', l''''''''''))) -> MATCH1(a4'', Cons(x''''', Cons(x''''''''', l'''''''''')), Cons(x''''', Cons(x''''''''', l'''''''''')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Inst
       →DP Problem 2
Inst
           →DP Problem 9
FwdInst
             ...
               →DP Problem 12
Polynomial Ordering
       →DP Problem 3
Nar


Dependency Pairs:

PART(a4'', Cons(x''''', Cons(x''''''''', l''''''''''))) -> MATCH1(a4'', Cons(x''''', Cons(x''''''''', l'''''''''')), Cons(x''''', Cons(x''''''''', l'''''''''')))
MATCH1(a4'''', Cons(x', Cons(x'''''', l''''''')), Cons(x', Cons(x'''''', l'''''''))) -> PART(a4'''', Cons(x'''''', l'''''''))


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




The following dependency pair can be strictly oriented:

MATCH1(a4'''', Cons(x', Cons(x'''''', l''''''')), Cons(x', Cons(x'''''', l'''''''))) -> PART(a4'''', Cons(x'''''', l'''''''))


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(PART(x1, x2))=  x2  
  POL(Cons(x1, x2))=  1 + x2  
  POL(MATCH_1(x1, x2, x3))=  x3  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Inst
       →DP Problem 2
Inst
           →DP Problem 9
FwdInst
             ...
               →DP Problem 13
Dependency Graph
       →DP Problem 3
Nar


Dependency Pair:

PART(a4'', Cons(x''''', Cons(x''''''''', l''''''''''))) -> MATCH1(a4'', Cons(x''''', Cons(x''''''''', l'''''''''')), Cons(x''''', Cons(x''''''''', l'''''''''')))


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
Inst
       →DP Problem 2
Inst
       →DP Problem 3
Narrowing Transformation


Dependency Pairs:

MATCH5(a, l', l5, Pair(l1, l2)) -> QUICK(l2)
MATCH5(a, l', l5, Pair(l1, l2)) -> QUICK(l1)
MATCH4(l5, Cons(a, l')) -> MATCH5(a, l', l5, part(a, l'))
QUICK(l5) -> MATCH4(l5, l5)


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




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

MATCH4(l5, Cons(a, l')) -> MATCH5(a, l', l5, part(a, l'))
one new Dependency Pair is created:

MATCH4(l5, Cons(a', l'')) -> MATCH5(a', l'', l5, match1(a', l'', l''))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Inst
       →DP Problem 2
Inst
       →DP Problem 3
Nar
           →DP Problem 14
Narrowing Transformation


Dependency Pairs:

MATCH5(a, l', l5, Pair(l1, l2)) -> QUICK(l1)
MATCH4(l5, Cons(a', l'')) -> MATCH5(a', l'', l5, match1(a', l'', l''))
QUICK(l5) -> MATCH4(l5, l5)
MATCH5(a, l', l5, Pair(l1, l2)) -> QUICK(l2)


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




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

MATCH4(l5, Cons(a', l'')) -> MATCH5(a', l'', l5, match1(a', l'', l''))
two new Dependency Pairs are created:

MATCH4(l5, Cons(a'', Nil)) -> MATCH5(a'', Nil, l5, Pair(Nil, Nil))
MATCH4(l5, Cons(a'', Cons(x', l'''))) -> MATCH5(a'', Cons(x', l'''), l5, match2(x', l''', a'', Cons(x', l'''), part(a'', l''')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Inst
       →DP Problem 2
Inst
       →DP Problem 3
Nar
           →DP Problem 14
Nar
             ...
               →DP Problem 15
Instantiation Transformation


Dependency Pairs:

MATCH4(l5, Cons(a'', Cons(x', l'''))) -> MATCH5(a'', Cons(x', l'''), l5, match2(x', l''', a'', Cons(x', l'''), part(a'', l''')))
MATCH5(a, l', l5, Pair(l1, l2)) -> QUICK(l2)
MATCH4(l5, Cons(a'', Nil)) -> MATCH5(a'', Nil, l5, Pair(Nil, Nil))
QUICK(l5) -> MATCH4(l5, l5)
MATCH5(a, l', l5, Pair(l1, l2)) -> QUICK(l1)


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




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

MATCH5(a, l', l5, Pair(l1, l2)) -> QUICK(l1)
two new Dependency Pairs are created:

MATCH5(a', Nil, l5'', Pair(Nil, Nil)) -> QUICK(Nil)
MATCH5(a', Cons(x''', l'''''), l5'', Pair(l1', l2')) -> QUICK(l1')

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Inst
       →DP Problem 2
Inst
       →DP Problem 3
Nar
           →DP Problem 14
Nar
             ...
               →DP Problem 16
Instantiation Transformation


Dependency Pairs:

MATCH5(a', Cons(x''', l'''''), l5'', Pair(l1', l2')) -> QUICK(l1')
MATCH5(a', Nil, l5'', Pair(Nil, Nil)) -> QUICK(Nil)
MATCH4(l5, Cons(a'', Nil)) -> MATCH5(a'', Nil, l5, Pair(Nil, Nil))
QUICK(l5) -> MATCH4(l5, l5)
MATCH5(a, l', l5, Pair(l1, l2)) -> QUICK(l2)
MATCH4(l5, Cons(a'', Cons(x', l'''))) -> MATCH5(a'', Cons(x', l'''), l5, match2(x', l''', a'', Cons(x', l'''), part(a'', l''')))


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




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

MATCH5(a, l', l5, Pair(l1, l2)) -> QUICK(l2)
two new Dependency Pairs are created:

MATCH5(a', Nil, l5'', Pair(Nil, Nil)) -> QUICK(Nil)
MATCH5(a', Cons(x''', l'''''), l5'', Pair(l1', l2')) -> QUICK(l2')

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Inst
       →DP Problem 2
Inst
       →DP Problem 3
Nar
           →DP Problem 14
Nar
             ...
               →DP Problem 17
Forward Instantiation Transformation


Dependency Pairs:

MATCH5(a', Cons(x''', l'''''), l5'', Pair(l1', l2')) -> QUICK(l2')
MATCH4(l5, Cons(a'', Cons(x', l'''))) -> MATCH5(a'', Cons(x', l'''), l5, match2(x', l''', a'', Cons(x', l'''), part(a'', l''')))
MATCH5(a', Nil, l5'', Pair(Nil, Nil)) -> QUICK(Nil)
MATCH5(a', Nil, l5'', Pair(Nil, Nil)) -> QUICK(Nil)
MATCH4(l5, Cons(a'', Nil)) -> MATCH5(a'', Nil, l5, Pair(Nil, Nil))
QUICK(l5) -> MATCH4(l5, l5)
MATCH5(a', Cons(x''', l'''''), l5'', Pair(l1', l2')) -> QUICK(l1')


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




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

QUICK(l5) -> MATCH4(l5, l5)
two new Dependency Pairs are created:

QUICK(Cons(a'''', Nil)) -> MATCH4(Cons(a'''', Nil), Cons(a'''', Nil))
QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH4(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Inst
       →DP Problem 2
Inst
       →DP Problem 3
Nar
           →DP Problem 14
Nar
             ...
               →DP Problem 18
Forward Instantiation Transformation


Dependency Pairs:

MATCH5(a', Cons(x''', l'''''), l5'', Pair(l1', l2')) -> QUICK(l1')
MATCH4(l5, Cons(a'', Cons(x', l'''))) -> MATCH5(a'', Cons(x', l'''), l5, match2(x', l''', a'', Cons(x', l'''), part(a'', l''')))
QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH4(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))
MATCH5(a', Cons(x''', l'''''), l5'', Pair(l1', l2')) -> QUICK(l2')


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




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

MATCH5(a', Cons(x''', l'''''), l5'', Pair(l1', l2')) -> QUICK(l1')
one new Dependency Pair is created:

MATCH5(a', Cons(x''', l'''''), l5'', Pair(Cons(a'''''', Cons(x''''', l''''''')), l2')) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Inst
       →DP Problem 2
Inst
       →DP Problem 3
Nar
           →DP Problem 14
Nar
             ...
               →DP Problem 19
Forward Instantiation Transformation


Dependency Pairs:

MATCH5(a', Cons(x''', l'''''), l5'', Pair(Cons(a'''''', Cons(x''''', l''''''')), l2')) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))
QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH4(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))
MATCH5(a', Cons(x''', l'''''), l5'', Pair(l1', l2')) -> QUICK(l2')
MATCH4(l5, Cons(a'', Cons(x', l'''))) -> MATCH5(a'', Cons(x', l'''), l5, match2(x', l''', a'', Cons(x', l'''), part(a'', l''')))


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




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

MATCH5(a', Cons(x''', l'''''), l5'', Pair(l1', l2')) -> QUICK(l2')
one new Dependency Pair is created:

MATCH5(a', Cons(x''', l'''''), l5'', Pair(l1', Cons(a'''''', Cons(x''''', l''''''')))) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
Inst
       →DP Problem 2
Inst
       →DP Problem 3
Nar
           →DP Problem 14
Nar
             ...
               →DP Problem 20
Polynomial Ordering


Dependency Pairs:

MATCH5(a', Cons(x''', l'''''), l5'', Pair(l1', Cons(a'''''', Cons(x''''', l''''''')))) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))
MATCH4(l5, Cons(a'', Cons(x', l'''))) -> MATCH5(a'', Cons(x', l'''), l5, match2(x', l''', a'', Cons(x', l'''), part(a'', l''')))
QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH4(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))
MATCH5(a', Cons(x''', l'''''), l5'', Pair(Cons(a'''''', Cons(x''''', l''''''')), l2')) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




The following dependency pair can be strictly oriented:

MATCH4(l5, Cons(a'', Cons(x', l'''))) -> MATCH5(a'', Cons(x', l'''), l5, match2(x', l''', a'', Cons(x', l'''), part(a'', l''')))


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

match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(Nil)=  0  
  POL(MATCH_5(x1, x2, x3, x4))=  x4  
  POL(match_2(x1, x2, x3, x4, x5))=  1 + x5  
  POL(False)=  0  
  POL(MATCH_4(x1, x2))=  x2  
  POL(Cons(x1, x2))=  1 + x2  
  POL(match_3(x1, x2, x3, x4, x5, x6, x7))=  1 + x1 + x2  
  POL(QUICK(x1))=  x1  
  POL(test(x1, x2))=  0  
  POL(Pair(x1, x2))=  x1 + x2  
  POL(True)=  0  
  POL(part(x1, x2))=  x2  
  POL(match_1(x1, x2, x3))=  x3  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
Inst
       →DP Problem 2
Inst
       →DP Problem 3
Nar
           →DP Problem 14
Nar
             ...
               →DP Problem 21
Dependency Graph


Dependency Pairs:

MATCH5(a', Cons(x''', l'''''), l5'', Pair(l1', Cons(a'''''', Cons(x''''', l''''''')))) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))
QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH4(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))
MATCH5(a', Cons(x''', l'''''), l5'', Pair(Cons(a'''''', Cons(x''''', l''''''')), l2')) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

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