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
Argument Filtering and 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 AFS that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
MATCH0(x1, x2, x3) -> x1
Cons(x1, x2) -> Cons(x1, x2)
APPEND(x1, x2) -> x1


   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
Argument Filtering and 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 AFS that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
MATCH1(x1, x2, x3) -> x2
Cons(x1, x2) -> Cons(x1, x2)
PART(x1, x2) -> x2


   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
Narrowing Transformation


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




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

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

MATCH4(l5, Cons(a''', Cons(x', l''''))) -> MATCH5(a''', Cons(x', l''''), l5, match2(x', l'''', a''', Cons(x', l''''), 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
Nar
             ...
               →DP Problem 21
Narrowing Transformation


Dependency Pairs:

MATCH5(a', Cons(x''', l'''''), l5'', Pair(Cons(a'''''', Cons(x''''', l''''''')), l2')) -> 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''''), match1(a''', l'''', 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', Cons(a'''''', Cons(x''''', l''''''')))) -> 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




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

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

MATCH4(l5, Cons(a'''', Cons(x', Nil))) -> MATCH5(a'''', Cons(x', Nil), l5, match2(x', Nil, a'''', Cons(x', Nil), Pair(Nil, Nil)))
MATCH4(l5, Cons(a'''', Cons(x', Cons(x'', l'')))) -> MATCH5(a'''', Cons(x', Cons(x'', l'')), l5, match2(x', Cons(x'', l''), a'''', Cons(x', Cons(x'', l'')), 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 22
Narrowing Transformation


Dependency Pairs:

MATCH4(l5, Cons(a'''', Cons(x', Cons(x'', l'')))) -> MATCH5(a'''', Cons(x', Cons(x'', l'')), l5, match2(x', Cons(x'', l''), a'''', Cons(x', Cons(x'', l'')), match2(x'', l'', a'''', Cons(x'', l''), part(a'''', l''))))
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', Nil))) -> MATCH5(a'''', Cons(x', Nil), l5, match2(x', Nil, a'''', Cons(x', Nil), Pair(Nil, Nil)))
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




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

MATCH4(l5, Cons(a'''', Cons(x', Nil))) -> MATCH5(a'''', Cons(x', Nil), l5, match2(x', Nil, a'''', Cons(x', Nil), Pair(Nil, Nil)))
one new Dependency Pair is created:

MATCH4(l5, Cons(a''''', Cons(x'', Nil))) -> MATCH5(a''''', Cons(x'', Nil), l5, match3(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))

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 23
Narrowing Transformation


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'', Nil))) -> MATCH5(a''''', Cons(x'', Nil), l5, match3(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
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''''''')))
MATCH4(l5, Cons(a'''', Cons(x', Cons(x'', l'')))) -> MATCH5(a'''', Cons(x', Cons(x'', l'')), l5, match2(x', Cons(x'', l''), a'''', Cons(x', Cons(x'', l'')), 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 Narrowing SCC transformation can be performed.
As a result of transforming the rule

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

MATCH4(l5, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH5(a''''', Cons(x', Cons(x'', l''')), l5, match2(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match2(x'', l''', a''''', Cons(x'', l'''), 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
Nar
             ...
               →DP Problem 24
Instantiation Transformation


Dependency Pairs:

MATCH4(l5, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH5(a''''', Cons(x', Cons(x'', l''')), l5, match2(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match2(x'', l''', a''''', Cons(x'', l'''), match1(a''''', l''', l'''))))
MATCH5(a', Cons(x''', l'''''), l5'', Pair(Cons(a'''''', Cons(x''''', l''''''')), l2')) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))
MATCH4(l5, Cons(a''''', Cons(x'', Nil))) -> MATCH5(a''''', Cons(x'', Nil), l5, match3(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
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', Cons(a'''''', Cons(x''''', l''''''')))) -> 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




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

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

MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(Cons(a'''''''', Cons(x'''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))
MATCH5(a'', Cons(x'''0, 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 25
Instantiation Transformation


Dependency Pairs:

MATCH5(a'', Cons(x'''0, Cons(x'''''', l'''''')), l5''', Pair(Cons(a'''''''', Cons(x''''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(Cons(a'''''''', Cons(x'''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))
MATCH4(l5, Cons(a''''', Cons(x'', Nil))) -> MATCH5(a''''', Cons(x'', Nil), l5, match3(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
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', Cons(a'''''', Cons(x''''', l''''''')))) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))
MATCH4(l5, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH5(a''''', Cons(x', Cons(x'', l''')), l5, match2(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match2(x'', l''', a''''', Cons(x'', l'''), match1(a''''', l''', 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', Cons(x''', l'''''), l5'', Pair(l1', Cons(a'''''', Cons(x''''', l''''''')))) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))
two new Dependency Pairs are created:

MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(l1'', Cons(a'''''''', Cons(x'''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))
MATCH5(a'', Cons(x'''0, 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 26
Forward Instantiation Transformation


Dependency Pairs:

MATCH5(a'', Cons(x'''0, Cons(x'''''', l'''''')), l5''', Pair(l1'', Cons(a'''''''', Cons(x''''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))
MATCH4(l5, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH5(a''''', Cons(x', Cons(x'', l''')), l5, match2(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match2(x'', l''', a''''', Cons(x'', l'''), match1(a''''', l''', l'''))))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(l1'', Cons(a'''''''', Cons(x'''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(Cons(a'''''''', Cons(x'''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))
MATCH4(l5, Cons(a''''', Cons(x'', Nil))) -> MATCH5(a''''', Cons(x'', Nil), l5, match3(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH4(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))
MATCH5(a'', Cons(x'''0, 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




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

QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH4(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))
two new Dependency Pairs are created:

QUICK(Cons(a''''', Cons(x''''', Nil))) -> MATCH4(Cons(a''''', Cons(x''''', Nil)), Cons(a''''', Cons(x''''', Nil)))
QUICK(Cons(a''''', Cons(x'''0, Cons(x''''', l'''''')))) -> MATCH4(Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))), Cons(a''''', Cons(x'''0, 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 27
Forward Instantiation Transformation


Dependency Pairs:

MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(l1'', Cons(a'''''''', Cons(x'''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))
MATCH5(a'', Cons(x'''0, Cons(x'''''', l'''''')), l5''', Pair(Cons(a'''''''', Cons(x''''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))
MATCH4(l5, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH5(a''''', Cons(x', Cons(x'', l''')), l5, match2(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match2(x'', l''', a''''', Cons(x'', l'''), match1(a''''', l''', l'''))))
QUICK(Cons(a''''', Cons(x'''0, Cons(x''''', l'''''')))) -> MATCH4(Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))), Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(Cons(a'''''''', Cons(x'''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))
MATCH4(l5, Cons(a''''', Cons(x'', Nil))) -> MATCH5(a''''', Cons(x'', Nil), l5, match3(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
QUICK(Cons(a''''', Cons(x''''', Nil))) -> MATCH4(Cons(a''''', Cons(x''''', Nil)), Cons(a''''', Cons(x''''', Nil)))
MATCH5(a'', Cons(x'''0, Cons(x'''''', l'''''')), l5''', Pair(l1'', Cons(a'''''''', Cons(x''''''', l'''''''')))) -> 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




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

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

MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', 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 3
Nar
           →DP Problem 14
Nar
             ...
               →DP Problem 28
Forward Instantiation Transformation


Dependency Pairs:

MATCH5(a'', Cons(x'''0, Cons(x'''''', l'''''')), l5''', Pair(l1'', Cons(a'''''''', Cons(x''''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))
MATCH5(a'', Cons(x'''0, Cons(x'''''', l'''''')), l5''', Pair(Cons(a'''''''', Cons(x''''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))
MATCH4(l5, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH5(a''''', Cons(x', Cons(x'', l''')), l5, match2(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match2(x'', l''', a''''', Cons(x'', l'''), match1(a''''', l''', l'''))))
QUICK(Cons(a''''', Cons(x'''0, Cons(x''''', l'''''')))) -> MATCH4(Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))), Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH4(l5, Cons(a''''', Cons(x'', Nil))) -> MATCH5(a''''', Cons(x'', Nil), l5, match3(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
QUICK(Cons(a''''', Cons(x''''', Nil))) -> MATCH4(Cons(a''''', Cons(x''''', Nil)), Cons(a''''', Cons(x''''', Nil)))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(l1'', Cons(a'''''''', Cons(x'''''', l'''''''')))) -> 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




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

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

MATCH5(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH5(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l5''', Pair(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', 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 3
Nar
           →DP Problem 14
Nar
             ...
               →DP Problem 29
Forward Instantiation Transformation


Dependency Pairs:

MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH5(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l5''', Pair(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))))
MATCH5(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH4(l5, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH5(a''''', Cons(x', Cons(x'', l''')), l5, match2(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match2(x'', l''', a''''', Cons(x'', l'''), match1(a''''', l''', l'''))))
QUICK(Cons(a''''', Cons(x'''0, Cons(x''''', l'''''')))) -> MATCH4(Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))), Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(l1'', Cons(a'''''''', Cons(x'''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))
MATCH4(l5, Cons(a''''', Cons(x'', Nil))) -> MATCH5(a''''', Cons(x'', Nil), l5, match3(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
QUICK(Cons(a''''', Cons(x''''', Nil))) -> MATCH4(Cons(a''''', Cons(x''''', Nil)), Cons(a''''', Cons(x''''', Nil)))
MATCH5(a'', Cons(x'''0, Cons(x'''''', l'''''')), l5''', Pair(l1'', Cons(a'''''''', Cons(x''''''', l'''''''')))) -> 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




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

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

MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(l1'', Cons(a''''''''', Cons(x'''''''', Nil)))) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(l1'', Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))) -> QUICK(Cons(a''''''''', 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 3
Nar
           →DP Problem 14
Nar
             ...
               →DP Problem 30
Forward Instantiation Transformation


Dependency Pairs:

MATCH5(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l5''', Pair(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))))
MATCH5(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(l1'', Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))) -> QUICK(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(l1'', Cons(a''''''''', Cons(x'''''''', Nil)))) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH4(l5, Cons(a''''', Cons(x'', Nil))) -> MATCH5(a''''', Cons(x'', Nil), l5, match3(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
QUICK(Cons(a''''', Cons(x''''', Nil))) -> MATCH4(Cons(a''''', Cons(x''''', Nil)), Cons(a''''', Cons(x''''', Nil)))
MATCH5(a'', Cons(x'''0, Cons(x'''''', l'''''')), l5''', Pair(l1'', Cons(a'''''''', Cons(x''''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))
MATCH4(l5, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH5(a''''', Cons(x', Cons(x'', l''')), l5, match2(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match2(x'', l''', a''''', Cons(x'', l'''), match1(a''''', l''', l'''))))
QUICK(Cons(a''''', Cons(x'''0, Cons(x''''', l'''''')))) -> MATCH4(Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))), Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', 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




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

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

MATCH5(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l5''', Pair(l1'', Cons(a''''''''', Cons(x'''''''', Nil)))) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH5(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l5''', Pair(l1'', Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))))) -> QUICK(Cons(a''''''''', 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 3
Nar
           →DP Problem 14
Nar
             ...
               →DP Problem 31
Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

MATCH5(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l5''', Pair(l1'', Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))))) -> QUICK(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))))
MATCH5(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l5''', Pair(l1'', Cons(a''''''''', Cons(x'''''''', Nil)))) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(l1'', Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))) -> QUICK(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(l1'', Cons(a''''''''', Cons(x'''''''', Nil)))) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))
MATCH5(a'', Cons(x'''0, Nil), l5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH4(l5, Cons(a''''', Cons(x'', Nil))) -> MATCH5(a''''', Cons(x'', Nil), l5, match3(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
QUICK(Cons(a''''', Cons(x''''', Nil))) -> MATCH4(Cons(a''''', Cons(x''''', Nil)), Cons(a''''', Cons(x''''', Nil)))
MATCH5(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH4(l5, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH5(a''''', Cons(x', Cons(x'', l''')), l5, match2(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match2(x'', l''', a''''', Cons(x'', l'''), match1(a''''', l''', l'''))))
QUICK(Cons(a''''', Cons(x'''0, Cons(x''''', l'''''')))) -> MATCH4(Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))), Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))))
MATCH5(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l5''', Pair(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', 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



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