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
Argument Filtering and Ordering
       →DP Problem 2
AFS
       →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




The following dependency pair can be strictly oriented:

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


There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
MATCH0(x1, x2, x3) -> x3
Cons(x1, x2) -> Cons(x1, x2)
APPEND(x1, x2) -> x1


   R
DPs
       →DP Problem 1
AFS
           →DP Problem 4
Dependency Graph
       →DP Problem 2
AFS
       →DP Problem 3
Nar


Dependency Pair:

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




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
Argument Filtering and Ordering
       →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




The following dependency pair can be strictly oriented:

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


There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
MATCH1(x1, x2, x3) -> x3
Cons(x1, x2) -> Cons(x1, x2)
PART(x1, x2) -> x2


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
           →DP Problem 5
Dependency Graph
       →DP Problem 3
Nar


Dependency Pair:

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




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →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
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Nar
           →DP Problem 6
Instantiation 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, an Instantiation 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''))
one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Nar
           →DP Problem 6
Inst
             ...
               →DP Problem 7
Instantiation Transformation


Dependency Pairs:

MATCH5(a, l', l5, Pair(l1, l2)) -> QUICK(l2)
MATCH4(Cons(a'', l'''), Cons(a'', l''')) -> MATCH5(a'', l''', Cons(a'', l'''), match1(a'', l''', l'''))
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)
one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Nar
           →DP Problem 6
Inst
             ...
               →DP Problem 8
Instantiation Transformation


Dependency Pairs:

MATCH5(a', l'', Cons(a', l''), Pair(l1', l2')) -> QUICK(l1')
MATCH4(Cons(a'', l'''), Cons(a'', l''')) -> MATCH5(a'', l''', Cons(a'', l'''), 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, an Instantiation SCC transformation can be performed.
As a result of transforming the rule

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

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

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Nar
           →DP Problem 6
Inst
             ...
               →DP Problem 9
Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

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



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