Termination Proof using AProVE

Term Rewriting System R:
[x, y, z, t, a, b, c]
g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

FOLDF(x, cons(y, z)) -> F(foldf(x, z), y)
FOLDF(x, cons(y, z)) -> FOLDF(x, z)
F(t, x) -> F'(t, g(x))
F(t, x) -> G(x)
F'(triple(a, b, c), B) -> F(triple(a, b, c), A)
F'(triple(a, b, c), A) -> F''(foldf(triple(cons(A, a), nil, c), b))
F'(triple(a, b, c), A) -> FOLDF(triple(cons(A, a), nil, c), b)
F''(triple(a, b, c)) -> FOLDF(triple(a, b, nil), c)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Narrowing Transformation

Dependency Pairs:

F'(triple(a, b, c), A) -> FOLDF(triple(cons(A, a), nil, c), b)
FOLDF(x, cons(y, z)) -> FOLDF(x, z)
F''(triple(a, b, c)) -> FOLDF(triple(a, b, nil), c)
F'(triple(a, b, c), A) -> F''(foldf(triple(cons(A, a), nil, c), b))
F'(triple(a, b, c), B) -> F(triple(a, b, c), A)
F(t, x) -> F'(t, g(x))
FOLDF(x, cons(y, z)) -> F(foldf(x, z), y)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

F(t, x) -> F'(t, g(x))

six new Dependency Pairs are created:

F(t, A) -> F'(t, A)
F(t, B) -> F'(t, A)
F(t, B) -> F'(t, B)
F(t, C) -> F'(t, A)
F(t, C) -> F'(t, B)
F(t, C) -> F'(t, C)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Narrowing Transformation

Dependency Pairs:

F(t, C) -> F'(t, B)
F(t, C) -> F'(t, A)
F'(triple(a, b, c), B) -> F(triple(a, b, c), A)
F(t, B) -> F'(t, B)
F(t, B) -> F'(t, A)
FOLDF(x, cons(y, z)) -> FOLDF(x, z)
F''(triple(a, b, c)) -> FOLDF(triple(a, b, nil), c)
F'(triple(a, b, c), A) -> F''(foldf(triple(cons(A, a), nil, c), b))
F(t, A) -> F'(t, A)
FOLDF(x, cons(y, z)) -> F(foldf(x, z), y)
F'(triple(a, b, c), A) -> FOLDF(triple(cons(A, a), nil, c), b)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

F'(triple(a, b, c), A) -> F''(foldf(triple(cons(A, a), nil, c), b))

two new Dependency Pairs are created:

F'(triple(a', nil, c'), A) -> F''(triple(cons(A, a'), nil, c'))
F'(triple(a', cons(y', z'), c'), A) -> F''(f(foldf(triple(cons(A, a'), nil, c'), z'), y'))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 3

                 ↳Narrowing Transformation

Dependency Pairs:

F(t, C) -> F'(t, A)
F(t, B) -> F'(t, B)
F'(triple(a', cons(y', z'), c'), A) -> F''(f(foldf(triple(cons(A, a'), nil, c'), z'), y'))
FOLDF(x, cons(y, z)) -> FOLDF(x, z)
F''(triple(a, b, c)) -> FOLDF(triple(a, b, nil), c)
F'(triple(a', nil, c'), A) -> F''(triple(cons(A, a'), nil, c'))
F(t, B) -> F'(t, A)
FOLDF(x, cons(y, z)) -> F(foldf(x, z), y)
F'(triple(a, b, c), A) -> FOLDF(triple(cons(A, a), nil, c), b)
F(t, A) -> F'(t, A)
F'(triple(a, b, c), B) -> F(triple(a, b, c), A)
F(t, C) -> F'(t, B)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

F'(triple(a', cons(y', z'), c'), A) -> F''(f(foldf(triple(cons(A, a'), nil, c'), z'), y'))

three new Dependency Pairs are created:

F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 4

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F(t, C) -> F'(t, B)
F'(triple(a, b, c), B) -> F(triple(a, b, c), A)
F(t, B) -> F'(t, B)
F(t, B) -> F'(t, A)
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
FOLDF(x, cons(y, z)) -> FOLDF(x, z)
F''(triple(a, b, c)) -> FOLDF(triple(a, b, nil), c)
F'(triple(a', nil, c'), A) -> F''(triple(cons(A, a'), nil, c'))
F(t, A) -> F'(t, A)
FOLDF(x, cons(y, z)) -> F(foldf(x, z), y)
F'(triple(a, b, c), A) -> FOLDF(triple(cons(A, a), nil, c), b)
F(t, C) -> F'(t, A)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

FOLDF(x, cons(y, z)) -> FOLDF(x, z)

one new Dependency Pair is created:

FOLDF(x'', cons(y, cons(y'', z''))) -> FOLDF(x'', cons(y'', z''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 5

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F(t, C) -> F'(t, A)
F(t, B) -> F'(t, B)
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
FOLDF(x'', cons(y, cons(y'', z''))) -> FOLDF(x'', cons(y'', z''))
F''(triple(a, b, c)) -> FOLDF(triple(a, b, nil), c)
F'(triple(a', nil, c'), A) -> F''(triple(cons(A, a'), nil, c'))
F(t, B) -> F'(t, A)
FOLDF(x, cons(y, z)) -> F(foldf(x, z), y)
F'(triple(a, b, c), A) -> FOLDF(triple(cons(A, a), nil, c), b)
F(t, A) -> F'(t, A)
F'(triple(a, b, c), B) -> F(triple(a, b, c), A)
F(t, C) -> F'(t, B)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

F'(triple(a, b, c), A) -> FOLDF(triple(cons(A, a), nil, c), b)

two new Dependency Pairs are created:

F'(triple(a', cons(y'', z''), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', z''))
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 6

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F(t, C) -> F'(t, B)
F'(triple(a, b, c), B) -> F(triple(a, b, c), A)
F(t, B) -> F'(t, B)
F(t, B) -> F'(t, A)
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
FOLDF(x'', cons(y, cons(y'', z''))) -> FOLDF(x'', cons(y'', z''))
F'(triple(a', cons(y'', z''), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', z''))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
F(t, A) -> F'(t, A)
FOLDF(x, cons(y, z)) -> F(foldf(x, z), y)
F''(triple(a, b, c)) -> FOLDF(triple(a, b, nil), c)
F'(triple(a', nil, c'), A) -> F''(triple(cons(A, a'), nil, c'))
F(t, C) -> F'(t, A)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

F''(triple(a, b, c)) -> FOLDF(triple(a, b, nil), c)

two new Dependency Pairs are created:

F''(triple(a', b', cons(y'', z''))) -> FOLDF(triple(a', b', nil), cons(y'', z''))
F''(triple(a', b', cons(y'', cons(y'''', z'''')))) -> FOLDF(triple(a', b', nil), cons(y'', cons(y'''', z'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 7

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F(t, C) -> F'(t, A)
F(t, B) -> F'(t, B)
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
F'(triple(a', cons(y'', z''), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', z''))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
FOLDF(x'', cons(y, cons(y'', z''))) -> FOLDF(x'', cons(y'', z''))
F''(triple(a', b', cons(y'', cons(y'''', z'''')))) -> FOLDF(triple(a', b', nil), cons(y'', cons(y'''', z'''')))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
F(t, B) -> F'(t, A)
FOLDF(x, cons(y, z)) -> F(foldf(x, z), y)
F''(triple(a', b', cons(y'', z''))) -> FOLDF(triple(a', b', nil), cons(y'', z''))
F'(triple(a', nil, c'), A) -> F''(triple(cons(A, a'), nil, c'))
F(t, A) -> F'(t, A)
F'(triple(a, b, c), B) -> F(triple(a, b, c), A)
F(t, C) -> F'(t, B)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

F(t, A) -> F'(t, A)

six new Dependency Pairs are created:

F(triple(a''', nil, c'''), A) -> F'(triple(a''', nil, c'''), A)
F(triple(a'''', cons(y'''', z''''), c''''), A) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), A) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a''', cons(y'''', z''''), c'''), A) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 8

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F(t, C) -> F'(t, B)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), A) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), A) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y'''', z''''), c''''), A) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F(triple(a''', nil, c'''), A) -> F'(triple(a''', nil, c'''), A)
F'(triple(a, b, c), B) -> F(triple(a, b, c), A)
F(t, B) -> F'(t, B)
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
F'(triple(a', cons(y'', z''), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', z''))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
FOLDF(x'', cons(y, cons(y'', z''))) -> FOLDF(x'', cons(y'', z''))
F''(triple(a', b', cons(y'', cons(y'''', z'''')))) -> FOLDF(triple(a', b', nil), cons(y'', cons(y'''', z'''')))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
F(t, B) -> F'(t, A)
FOLDF(x, cons(y, z)) -> F(foldf(x, z), y)
F''(triple(a', b', cons(y'', z''))) -> FOLDF(triple(a', b', nil), cons(y'', z''))
F'(triple(a', nil, c'), A) -> F''(triple(cons(A, a'), nil, c'))
F(t, C) -> F'(t, A)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

F'(triple(a, b, c), B) -> F(triple(a, b, c), A)

five new Dependency Pairs are created:

F'(triple(a', nil, c'), B) -> F(triple(a', nil, c'), A)
F'(triple(a', cons(y'''''', z''''''), c'), B) -> F(triple(a', cons(y'''''', z''''''), c'), A)
F'(triple(a', cons(y''''', nil), c'), B) -> F(triple(a', cons(y''''', nil), c'), A)
F'(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), B) -> F(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), A)
F'(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), B) -> F(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), A)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 9

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F(t, C) -> F'(t, A)
F'(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), B) -> F(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), A)
F'(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), B) -> F(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), A)
F'(triple(a', cons(y''''', nil), c'), B) -> F(triple(a', cons(y''''', nil), c'), A)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), A) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), A) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y'''', z''''), c''''), A) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F'(triple(a', cons(y'''''', z''''''), c'), B) -> F(triple(a', cons(y'''''', z''''''), c'), A)
F(t, B) -> F'(t, B)
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
F'(triple(a', cons(y'', z''), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', z''))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
FOLDF(x'', cons(y, cons(y'', z''))) -> FOLDF(x'', cons(y'', z''))
F''(triple(a', b', cons(y'', cons(y'''', z'''')))) -> FOLDF(triple(a', b', nil), cons(y'', cons(y'''', z'''')))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
F(t, B) -> F'(t, A)
FOLDF(x, cons(y, z)) -> F(foldf(x, z), y)
F''(triple(a', b', cons(y'', z''))) -> FOLDF(triple(a', b', nil), cons(y'', z''))
F'(triple(a', nil, c'), A) -> F''(triple(cons(A, a'), nil, c'))
F(triple(a''', nil, c'''), A) -> F'(triple(a''', nil, c'''), A)
F'(triple(a', nil, c'), B) -> F(triple(a', nil, c'), A)
F(t, C) -> F'(t, B)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

F(t, B) -> F'(t, A)

six new Dependency Pairs are created:

F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), A)
F(triple(a'''', cons(y'''', z''''), c''''), B) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), B) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), B) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a''', cons(y'''', z''''), c'''), B) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), B) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 10

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), B) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), B) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), B) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), B) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y'''', z''''), c''''), B) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), A)
F(t, C) -> F'(t, B)
F'(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), B) -> F(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), A)
F'(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), B) -> F(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), A)
F'(triple(a', cons(y''''', nil), c'), B) -> F(triple(a', cons(y''''', nil), c'), A)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), A) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), A) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
F'(triple(a', cons(y'', z''), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', z''))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
FOLDF(x'', cons(y, cons(y'', z''))) -> FOLDF(x'', cons(y'', z''))
F''(triple(a', b', cons(y'', cons(y'''', z'''')))) -> FOLDF(triple(a', b', nil), cons(y'', cons(y'''', z'''')))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
F(triple(a'''', cons(y'''', z''''), c''''), A) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F'(triple(a', cons(y'''''', z''''''), c'), B) -> F(triple(a', cons(y'''''', z''''''), c'), A)
F(triple(a''', nil, c'''), A) -> F'(triple(a''', nil, c'''), A)
F'(triple(a', nil, c'), B) -> F(triple(a', nil, c'), A)
F(t, B) -> F'(t, B)
FOLDF(x, cons(y, z)) -> F(foldf(x, z), y)
F''(triple(a', b', cons(y'', z''))) -> FOLDF(triple(a', b', nil), cons(y'', z''))
F'(triple(a', nil, c'), A) -> F''(triple(cons(A, a'), nil, c'))
F(t, C) -> F'(t, A)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

F(t, B) -> F'(t, B)

five new Dependency Pairs are created:

F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), B)
F(triple(a''', cons(y'''''''', z''''''''), c'''), B) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), B) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)
F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 11

                 ↳Forward Instantiation Transformation

Dependency Pairs:

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

F(t, C) -> F'(t, A)

six new Dependency Pairs are created:

F(triple(a''', nil, c'''), C) -> F'(triple(a''', nil, c'''), A)
F(triple(a'''', cons(y'''', z''''), c''''), C) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), C) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), C) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a''', cons(y'''', z''''), c'''), C) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), C) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 12

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), C) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), C) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), C) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), C) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y'''', z''''), c''''), C) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F(triple(a''', nil, c'''), C) -> F'(triple(a''', nil, c'''), A)
F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), B) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F(triple(a''', cons(y'''''''', z''''''''), c'''), B) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), B)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), B) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), B) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), B) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), B) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y'''', z''''), c''''), B) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), A)
F'(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), B) -> F(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), A)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F'(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), B) -> F(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), A)
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F(triple(a''', cons(y'''', z''''), c'''), A) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F'(triple(a', cons(y'', z''), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', z''))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
F(triple(a'''', cons(y''', nil), c''''), A) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F'(triple(a', cons(y''''', nil), c'), B) -> F(triple(a', cons(y''''', nil), c'), A)
FOLDF(x'', cons(y, cons(y'', z''))) -> FOLDF(x'', cons(y'', z''))
F''(triple(a', b', cons(y'', cons(y'''', z'''')))) -> FOLDF(triple(a', b', nil), cons(y'', cons(y'''', z'''')))
F'(triple(a', nil, c'), A) -> F''(triple(cons(A, a'), nil, c'))
F(triple(a''', nil, c'''), A) -> F'(triple(a''', nil, c'''), A)
F'(triple(a', nil, c'), B) -> F(triple(a', nil, c'), A)
F(t, C) -> F'(t, B)
FOLDF(x, cons(y, z)) -> F(foldf(x, z), y)
F''(triple(a', b', cons(y'', z''))) -> FOLDF(triple(a', b', nil), cons(y'', z''))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
F(triple(a'''', cons(y'''', z''''), c''''), A) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F'(triple(a', cons(y'''''', z''''''), c'), B) -> F(triple(a', cons(y'''''', z''''''), c'), A)
F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

F(t, C) -> F'(t, B)

five new Dependency Pairs are created:

F(triple(a''', nil, c'''), C) -> F'(triple(a''', nil, c'''), B)
F(triple(a''', cons(y'''''''', z''''''''), c'''), C) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), C) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), C) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)
F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), C) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 13

                 ↳Narrowing Transformation

Dependency Pairs:

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

FOLDF(x, cons(y, z)) -> F(foldf(x, z), y)

two new Dependency Pairs are created:

FOLDF(x'', cons(y, nil)) -> F(x'', y)
FOLDF(x'', cons(y, cons(y'', z''))) -> F(f(foldf(x'', z''), y''), y)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 14

                 ↳Narrowing Transformation

Dependency Pairs:

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

FOLDF(x'', cons(y, cons(y'', z''))) -> F(f(foldf(x'', z''), y''), y)

three new Dependency Pairs are created:

FOLDF(x''', cons(y, cons(y''', z'''))) -> F(f'(foldf(x''', z'''), g(y''')), y)
FOLDF(x''', cons(y, cons(y'', nil))) -> F(f(x''', y''), y)
FOLDF(x''', cons(y, cons(y'', cons(y''', z')))) -> F(f(f(foldf(x''', z'), y'''), y''), y)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 15

                 ↳Forward Instantiation Transformation

Dependency Pairs:

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

F'(triple(a', nil, c'), A) -> F''(triple(cons(A, a'), nil, c'))

two new Dependency Pairs are created:

F'(triple(a''', nil, cons(y'''', z'''')), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', z'''')))
F'(triple(a''', nil, cons(y'''', cons(y'''''', z''''''))), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', cons(y'''''', z''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 16

                 ↳Forward Instantiation Transformation

Dependency Pairs:

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

FOLDF(x'', cons(y, cons(y'', z''))) -> FOLDF(x'', cons(y'', z''))

five new Dependency Pairs are created:

FOLDF(x'''', cons(y, cons(y''0, cons(y'''', z'''')))) -> FOLDF(x'''', cons(y''0, cons(y'''', z'''')))
FOLDF(x'''', cons(y, cons(y''', nil))) -> FOLDF(x'''', cons(y''', nil))
FOLDF(x''', cons(y, cons(y''', cons(y''''', z''''')))) -> FOLDF(x''', cons(y''', cons(y''''', z''''')))
FOLDF(x''', cons(y, cons(y''0, cons(y'''', nil)))) -> FOLDF(x''', cons(y''0, cons(y'''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(x''', cons(y''', cons(y''''0, cons(y'''''', z''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 17

                 ↳Forward Instantiation Transformation

Dependency Pairs:

FOLDF(x''', cons(y, cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(x''', cons(y''', cons(y''''0, cons(y'''''', z''''))))
FOLDF(x''', cons(y, cons(y''0, cons(y'''', nil)))) -> FOLDF(x''', cons(y''0, cons(y'''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''', z''''')))) -> FOLDF(x''', cons(y''', cons(y''''', z''''')))
FOLDF(x'''', cons(y, cons(y''', nil))) -> FOLDF(x'''', cons(y''', nil))
FOLDF(x'''', cons(y, cons(y''0, cons(y'''', z'''')))) -> FOLDF(x'''', cons(y''0, cons(y'''', z'''')))
F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), C) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), C) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F(triple(a''', cons(y'''''''', z''''''''), c'''), C) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F(triple(a''', nil, c'''), C) -> F'(triple(a''', nil, c'''), B)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), C) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), C) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), C) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), C) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y'''', z''''), c''''), C) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F(triple(a''', nil, c'''), C) -> F'(triple(a''', nil, c'''), A)
F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)
F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), B) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F'(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), B) -> F(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), A)
F'(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), B) -> F(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), A)
F'(triple(a', cons(y''''', nil), c'), B) -> F(triple(a', cons(y''''', nil), c'), A)
F(triple(a''', cons(y'''''''', z''''''''), c'''), B) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F'(triple(a', nil, c'), B) -> F(triple(a', nil, c'), A)
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), B)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), B) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), B) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), B) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), B) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y'''', z''''), c''''), B) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F'(triple(a''', nil, cons(y'''', cons(y'''''', z''''''))), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', cons(y'''''', z''''''))))
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), A)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), A) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
FOLDF(x''', cons(y, cons(y'', cons(y''', z')))) -> F(f(f(foldf(x''', z'), y'''), y''), y)
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
FOLDF(x''', cons(y, cons(y'', nil))) -> F(f(x''', y''), y)
F'(triple(a', cons(y'', z''), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', z''))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
F(triple(a'''', cons(y''', nil), c''''), A) -> F'(triple(a'''', cons(y''', nil), c''''), A)
FOLDF(x''', cons(y, cons(y''', z'''))) -> F(f'(foldf(x''', z'''), g(y''')), y)
F''(triple(a', b', cons(y'', cons(y'''', z'''')))) -> FOLDF(triple(a', b', nil), cons(y'', cons(y'''', z'''')))
F'(triple(a''', nil, cons(y'''', z'''')), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', z'''')))
F(triple(a''', nil, c'''), A) -> F'(triple(a''', nil, c'''), A)
FOLDF(x'', cons(y, nil)) -> F(x'', y)
F''(triple(a', b', cons(y'', z''))) -> FOLDF(triple(a', b', nil), cons(y'', z''))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
F(triple(a'''', cons(y'''', z''''), c''''), A) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F'(triple(a', cons(y'''''', z''''''), c'), B) -> F(triple(a', cons(y'''''', z''''''), c'), A)
F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), C) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

F'(triple(a', cons(y'', z''), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', z''))

nine new Dependency Pairs are created:

F'(triple(a'', cons(y''', nil), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', nil))
F'(triple(a'', cons(y''', cons(y''''', z''''')), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', z''''')))
F'(triple(a'', cons(y''0, cons(y'''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''0, cons(y'''', nil)))
F'(triple(a'', cons(y''', cons(y''''0, cons(y'''''', z''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''0, cons(y'''''', z''''))))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', z''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F'(triple(a'', cons(y''', cons(y''''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', nil)))
F'(triple(a'', cons(y''', cons(y''''', cons(y''''''', z'''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', nil))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', nil))))
F'(triple(a'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 18

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), C) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)
F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), C) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), C) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F(triple(a''', cons(y'''''''', z''''''''), c'''), C) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F(triple(a''', nil, c'''), C) -> F'(triple(a''', nil, c'''), B)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), C) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), C) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), C) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), C) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y'''', z''''), c''''), C) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F(triple(a''', nil, c'''), C) -> F'(triple(a''', nil, c'''), A)
F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)
F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), B) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F'(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), B) -> F(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), A)
F'(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), B) -> F(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), A)
F'(triple(a', cons(y''''', nil), c'), B) -> F(triple(a', cons(y''''', nil), c'), A)
F'(triple(a', cons(y'''''', z''''''), c'), B) -> F(triple(a', cons(y'''''', z''''''), c'), A)
F(triple(a''', cons(y'''''''', z''''''''), c'''), B) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F'(triple(a', nil, c'), B) -> F(triple(a', nil, c'), A)
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), B)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), B) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), B) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), B) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), B) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y'''', z''''), c''''), B) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F'(triple(a''', nil, cons(y'''', cons(y'''''', z''''''))), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', cons(y'''''', z''''''))))
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), A)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F'(triple(a'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', nil))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', nil))))
F'(triple(a'', cons(y''', cons(y''''', cons(y''''''', z'''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F'(triple(a'', cons(y''', cons(y''''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', nil)))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', z''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F'(triple(a'', cons(y''', cons(y''''0, cons(y'''''', z''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''0, cons(y'''''', z''''))))
F'(triple(a'', cons(y''0, cons(y'''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''0, cons(y'''', nil)))
FOLDF(x''', cons(y, cons(y''0, cons(y'''', nil)))) -> FOLDF(x''', cons(y''0, cons(y'''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''', z''''')))) -> FOLDF(x''', cons(y''', cons(y''''', z''''')))
FOLDF(x'''', cons(y, cons(y''', nil))) -> FOLDF(x'''', cons(y''', nil))
FOLDF(x'''', cons(y, cons(y''0, cons(y'''', z'''')))) -> FOLDF(x'''', cons(y''0, cons(y'''', z'''')))
F'(triple(a'', cons(y''', cons(y''''', z''''')), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', z''''')))
F(triple(a''', cons(y'''', z''''), c'''), A) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
FOLDF(x''', cons(y, cons(y'', cons(y''', z')))) -> F(f(f(foldf(x''', z'), y'''), y''), y)
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F'(triple(a'', cons(y''', nil), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', nil))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
F(triple(a'''', cons(y''', nil), c''''), A) -> F'(triple(a'''', cons(y''', nil), c''''), A)
FOLDF(x''', cons(y, cons(y'', nil))) -> F(f(x''', y''), y)
F''(triple(a', b', cons(y'', cons(y'''', z'''')))) -> FOLDF(triple(a', b', nil), cons(y'', cons(y'''', z'''')))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
F(triple(a'''', cons(y'''', z''''), c''''), A) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
FOLDF(x'', cons(y, nil)) -> F(x'', y)
F''(triple(a', b', cons(y'', z''))) -> FOLDF(triple(a', b', nil), cons(y'', z''))
F'(triple(a''', nil, cons(y'''', z'''')), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', z'''')))
F(triple(a''', nil, c'''), A) -> F'(triple(a''', nil, c'''), A)
FOLDF(x''', cons(y, cons(y''', z'''))) -> F(f'(foldf(x''', z'''), g(y''')), y)
FOLDF(x''', cons(y, cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(x''', cons(y''', cons(y''''0, cons(y'''''', z''''))))

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

F''(triple(a', b', cons(y'', z''))) -> FOLDF(triple(a', b', nil), cons(y'', z''))

nine new Dependency Pairs are created:

F''(triple(a'', b'', cons(y''', nil))) -> FOLDF(triple(a'', b'', nil), cons(y''', nil))
F''(triple(a'', b'', cons(y''', cons(y''''', z''''')))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', z''''')))
F''(triple(a'', b'', cons(y''0, cons(y'''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''0, cons(y'''', nil)))
F''(triple(a'', b'', cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''0, cons(y'''''', z''''))))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', z''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F''(triple(a'', b'', cons(y''', cons(y''''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', nil)))
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''''', z'''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', nil))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', nil))))
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 19

                 ↳Forward Instantiation Transformation

Dependency Pairs:

F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), C) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), C) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F(triple(a''', cons(y'''''''', z''''''''), c'''), C) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F(triple(a''', nil, c'''), C) -> F'(triple(a''', nil, c'''), B)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), C) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), C) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), C) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), C) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y'''', z''''), c''''), C) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F(triple(a''', nil, c'''), C) -> F'(triple(a''', nil, c'''), A)
F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)
F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), B) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F'(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), B) -> F(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), A)
F'(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), B) -> F(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), A)
F'(triple(a', cons(y''''', nil), c'), B) -> F(triple(a', cons(y''''', nil), c'), A)
F(triple(a''', cons(y'''''''', z''''''''), c'''), B) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F'(triple(a', nil, c'), B) -> F(triple(a', nil, c'), A)
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), B)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), B) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), B) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), B) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), B) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y'''', z''''), c''''), B) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', nil))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', nil))))
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''''', z'''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F''(triple(a'', b'', cons(y''', cons(y''''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', nil)))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', z''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F'(triple(a''', nil, cons(y'''', cons(y'''''', z''''''))), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', cons(y'''''', z''''''))))
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), A)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F'(triple(a'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', nil))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', nil))))
F'(triple(a'', cons(y''', cons(y''''', cons(y''''''', z'''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F'(triple(a'', cons(y''', cons(y''''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', nil)))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', z''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F'(triple(a'', cons(y''', cons(y''''0, cons(y'''''', z''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''0, cons(y'''''', z''''))))
F'(triple(a'', cons(y''0, cons(y'''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''0, cons(y'''', nil)))
F'(triple(a'', cons(y''', cons(y''''', z''''')), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', z''''')))
F'(triple(a'', cons(y''', nil), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', nil))
FOLDF(x''', cons(y, cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(x''', cons(y''', cons(y''''0, cons(y'''''', z''''))))
FOLDF(x''', cons(y, cons(y''0, cons(y'''', nil)))) -> FOLDF(x''', cons(y''0, cons(y'''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''', z''''')))) -> FOLDF(x''', cons(y''', cons(y''''', z''''')))
FOLDF(x'''', cons(y, cons(y''0, cons(y'''', z'''')))) -> FOLDF(x'''', cons(y''0, cons(y'''', z'''')))
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
F(triple(a''', cons(y'''', z''''), c'''), A) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
FOLDF(x''', cons(y, cons(y'', cons(y''', z')))) -> F(f(f(foldf(x''', z'), y'''), y''), y)
F''(triple(a'', b'', cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''0, cons(y'''''', z''''))))
FOLDF(x'''', cons(y, cons(y''', nil))) -> FOLDF(x'''', cons(y''', nil))
F''(triple(a'', b'', cons(y''0, cons(y'''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''0, cons(y'''', nil)))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
FOLDF(x''', cons(y, cons(y'', nil))) -> F(f(x''', y''), y)
F''(triple(a'', b'', cons(y''', cons(y''''', z''''')))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', z''''')))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
F(triple(a'''', cons(y''', nil), c''''), A) -> F'(triple(a'''', cons(y''', nil), c''''), A)
FOLDF(x'', cons(y, nil)) -> F(x'', y)
F''(triple(a'', b'', cons(y''', nil))) -> FOLDF(triple(a'', b'', nil), cons(y''', nil))
F'(triple(a''', nil, cons(y'''', z'''')), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', z'''')))
F(triple(a''', nil, c'''), A) -> F'(triple(a''', nil, c'''), A)
FOLDF(x''', cons(y, cons(y''', z'''))) -> F(f'(foldf(x''', z'''), g(y''')), y)
F''(triple(a', b', cons(y'', cons(y'''', z'''')))) -> FOLDF(triple(a', b', nil), cons(y'', cons(y'''', z'''')))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
F(triple(a'''', cons(y'''', z''''), c''''), A) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F'(triple(a', cons(y'''''', z''''''), c'), B) -> F(triple(a', cons(y'''''', z''''''), c'), A)
F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), C) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

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

FOLDF(x'', cons(y, nil)) -> F(x'', y)

26 new Dependency Pairs are created:

FOLDF(triple(a''''', nil, c'''''), cons(A, nil)) -> F(triple(a''''', nil, c'''''), A)
FOLDF(triple(a'''''', cons(y'''''', z''''''), c''''''), cons(A, nil)) -> F(triple(a'''''', cons(y'''''', z''''''), c''''''), A)
FOLDF(triple(a'''''', cons(y''''', nil), c''''''), cons(A, nil)) -> F(triple(a'''''', cons(y''''', nil), c''''''), A)
FOLDF(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), cons(A, nil)) -> F(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), A)
FOLDF(triple(a''''', cons(y'''''', z''''''), c'''''), cons(A, nil)) -> F(triple(a''''', cons(y'''''', z''''''), c'''''), A)
FOLDF(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), cons(A, nil)) -> F(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), A)
FOLDF(triple(a''''', nil, c'''''), cons(B, nil)) -> F(triple(a''''', nil, c'''''), B)
FOLDF(triple(a'''''', cons(y'''''', z''''''), c''''''), cons(B, nil)) -> F(triple(a'''''', cons(y'''''', z''''''), c''''''), B)
FOLDF(triple(a'''''', cons(y''''', nil), c''''''), cons(B, nil)) -> F(triple(a'''''', cons(y''''', nil), c''''''), B)
FOLDF(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), cons(B, nil)) -> F(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), B)
FOLDF(triple(a''''', cons(y'''''', z''''''), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y'''''', z''''''), c'''''), B)
FOLDF(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), B)
FOLDF(triple(a''''', cons(y'''''''''', z''''''''''), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y'''''''''', z''''''''''), c'''''), B)
FOLDF(triple(a''''', cons(y''''''''', nil), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y''''''''', nil), c'''''), B)
FOLDF(triple(a''''', cons(y'''''''0'''', cons(y''''''''''''', z'''''''''')), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y'''''''0'''', cons(y''''''''''''', z'''''''''')), c'''''), B)
FOLDF(triple(a''''', cons(y'''''''''', cons(y'''''''''''', z'''''''''''')), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y'''''''''', cons(y'''''''''''', z'''''''''''')), c'''''), B)
FOLDF(triple(a''''', nil, c'''''), cons(C, nil)) -> F(triple(a''''', nil, c'''''), C)
FOLDF(triple(a'''''', cons(y'''''', z''''''), c''''''), cons(C, nil)) -> F(triple(a'''''', cons(y'''''', z''''''), c''''''), C)
FOLDF(triple(a'''''', cons(y''''', nil), c''''''), cons(C, nil)) -> F(triple(a'''''', cons(y''''', nil), c''''''), C)
FOLDF(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), cons(C, nil)) -> F(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), C)
FOLDF(triple(a''''', cons(y'''''', z''''''), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y'''''', z''''''), c'''''), C)
FOLDF(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), C)
FOLDF(triple(a''''', cons(y'''''''''', z''''''''''), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y'''''''''', z''''''''''), c'''''), C)
FOLDF(triple(a''''', cons(y''''''''', nil), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y''''''''', nil), c'''''), C)
FOLDF(triple(a''''', cons(y'''''''0'''', cons(y''''''''''''', z'''''''''')), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y'''''''0'''', cons(y''''''''''''', z'''''''''')), c'''''), C)
FOLDF(triple(a''''', cons(y'''''''''', cons(y'''''''''''', z'''''''''''')), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y'''''''''', cons(y'''''''''''', z'''''''''''')), c'''''), C)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 20

                 ↳Polynomial Ordering

Dependency Pairs:

FOLDF(triple(a''''', cons(y'''''''''', cons(y'''''''''''', z'''''''''''')), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y'''''''''', cons(y'''''''''''', z'''''''''''')), c'''''), C)
FOLDF(triple(a''''', cons(y'''''''0'''', cons(y''''''''''''', z'''''''''')), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y'''''''0'''', cons(y''''''''''''', z'''''''''')), c'''''), C)
FOLDF(triple(a''''', cons(y''''''''', nil), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y''''''''', nil), c'''''), C)
FOLDF(triple(a''''', cons(y'''''''''', z''''''''''), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y'''''''''', z''''''''''), c'''''), C)
FOLDF(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), C)
FOLDF(triple(a''''', cons(y'''''', z''''''), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y'''''', z''''''), c'''''), C)
FOLDF(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), cons(C, nil)) -> F(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), C)
FOLDF(triple(a'''''', cons(y''''', nil), c''''''), cons(C, nil)) -> F(triple(a'''''', cons(y''''', nil), c''''''), C)
FOLDF(triple(a'''''', cons(y'''''', z''''''), c''''''), cons(C, nil)) -> F(triple(a'''''', cons(y'''''', z''''''), c''''''), C)
FOLDF(triple(a''''', cons(y'''''''''', cons(y'''''''''''', z'''''''''''')), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y'''''''''', cons(y'''''''''''', z'''''''''''')), c'''''), B)
FOLDF(triple(a''''', cons(y'''''''0'''', cons(y''''''''''''', z'''''''''')), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y'''''''0'''', cons(y''''''''''''', z'''''''''')), c'''''), B)
FOLDF(triple(a''''', cons(y''''''''', nil), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y''''''''', nil), c'''''), B)
FOLDF(triple(a''''', cons(y'''''''''', z''''''''''), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y'''''''''', z''''''''''), c'''''), B)
FOLDF(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), B)
FOLDF(triple(a''''', cons(y'''''', z''''''), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y'''''', z''''''), c'''''), B)
FOLDF(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), cons(B, nil)) -> F(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), B)
FOLDF(triple(a'''''', cons(y''''', nil), c''''''), cons(B, nil)) -> F(triple(a'''''', cons(y''''', nil), c''''''), B)
FOLDF(triple(a'''''', cons(y'''''', z''''''), c''''''), cons(B, nil)) -> F(triple(a'''''', cons(y'''''', z''''''), c''''''), B)
FOLDF(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), cons(A, nil)) -> F(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), A)
FOLDF(triple(a''''', cons(y'''''', z''''''), c'''''), cons(A, nil)) -> F(triple(a''''', cons(y'''''', z''''''), c'''''), A)
FOLDF(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), cons(A, nil)) -> F(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), A)
F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), C) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), C) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F(triple(a''', cons(y'''''''', z''''''''), c'''), C) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), C) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), C) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), C) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), C) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y'''', z''''), c''''), C) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)
F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), B) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F'(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), B) -> F(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), A)
F'(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), B) -> F(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), A)
F'(triple(a', cons(y''''', nil), c'), B) -> F(triple(a', cons(y''''', nil), c'), A)
F(triple(a''', cons(y'''''''', z''''''''), c'''), B) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), B) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), B) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), B) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), B) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a''', nil, c'''), C) -> F'(triple(a''', nil, c'''), B)
F(triple(a''', nil, c'''), C) -> F'(triple(a''', nil, c'''), A)
FOLDF(triple(a''''', nil, c'''''), cons(C, nil)) -> F(triple(a''''', nil, c'''''), C)
F'(triple(a', nil, c'), B) -> F(triple(a', nil, c'), A)
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), B)
FOLDF(triple(a''''', nil, c'''''), cons(B, nil)) -> F(triple(a''''', nil, c'''''), B)
F'(triple(a'', cons(y''', nil), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', nil))
F(triple(a'''', cons(y'''', z''''), c''''), B) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', nil))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', nil))))
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''''', z'''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F''(triple(a'', b'', cons(y''', cons(y''''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', nil)))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', z''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F''(triple(a'', b'', cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''0, cons(y'''''', z''''))))
F'(triple(a''', nil, cons(y'''', cons(y'''''', z''''''))), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', cons(y'''''', z''''''))))
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), A)
F'(triple(a'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', nil))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', nil))))
F'(triple(a'', cons(y''', cons(y''''', cons(y''''''', z'''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F'(triple(a'', cons(y''', cons(y''''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', nil)))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', z''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F'(triple(a'', cons(y''', cons(y''''0, cons(y'''''', z''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''0, cons(y'''''', z''''))))
F'(triple(a'', cons(y''0, cons(y'''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''0, cons(y'''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(x''', cons(y''', cons(y''''0, cons(y'''''', z''''))))
FOLDF(x''', cons(y, cons(y''0, cons(y'''', nil)))) -> FOLDF(x''', cons(y''0, cons(y'''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''', z''''')))) -> FOLDF(x''', cons(y''', cons(y''''', z''''')))
FOLDF(x'''', cons(y, cons(y''0, cons(y'''', z'''')))) -> FOLDF(x'''', cons(y''0, cons(y'''', z'''')))
F'(triple(a'', cons(y''', cons(y''''', z''''')), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', z''''')))
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
FOLDF(x''', cons(y, cons(y'', cons(y''', z')))) -> F(f(f(foldf(x''', z'), y'''), y''), y)
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
F(triple(a''', cons(y'''', z''''), c'''), A) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
FOLDF(triple(a'''''', cons(y''''', nil), c''''''), cons(A, nil)) -> F(triple(a'''''', cons(y''''', nil), c''''''), A)
FOLDF(x'''', cons(y, cons(y''', nil))) -> FOLDF(x'''', cons(y''', nil))
F''(triple(a'', b'', cons(y''0, cons(y'''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''0, cons(y'''', nil)))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
FOLDF(x''', cons(y, cons(y'', nil))) -> F(f(x''', y''), y)
F''(triple(a'', b'', cons(y''', cons(y''''', z''''')))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', z''''')))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
F(triple(a'''', cons(y''', nil), c''''), A) -> F'(triple(a'''', cons(y''', nil), c''''), A)
FOLDF(triple(a'''''', cons(y'''''', z''''''), c''''''), cons(A, nil)) -> F(triple(a'''''', cons(y'''''', z''''''), c''''''), A)
FOLDF(triple(a''''', nil, c'''''), cons(A, nil)) -> F(triple(a''''', nil, c'''''), A)
F''(triple(a'', b'', cons(y''', nil))) -> FOLDF(triple(a'', b'', nil), cons(y''', nil))
F'(triple(a''', nil, cons(y'''', z'''')), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', z'''')))
F(triple(a''', nil, c'''), A) -> F'(triple(a''', nil, c'''), A)
FOLDF(x''', cons(y, cons(y''', z'''))) -> F(f'(foldf(x''', z'''), g(y''')), y)
F''(triple(a', b', cons(y'', cons(y'''', z'''')))) -> FOLDF(triple(a', b', nil), cons(y'', cons(y'''', z'''')))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
F(triple(a'''', cons(y'''', z''''), c''''), A) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F'(triple(a', cons(y'''''', z''''''), c'), B) -> F(triple(a', cons(y'''''', z''''''), c'), A)
F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), C) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

The following dependency pairs can be strictly oriented:

FOLDF(triple(a''''', cons(y'''''''''', cons(y'''''''''''', z'''''''''''')), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y'''''''''', cons(y'''''''''''', z'''''''''''')), c'''''), C)
FOLDF(triple(a''''', cons(y'''''''0'''', cons(y''''''''''''', z'''''''''')), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y'''''''0'''', cons(y''''''''''''', z'''''''''')), c'''''), C)
FOLDF(triple(a''''', cons(y''''''''', nil), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y''''''''', nil), c'''''), C)
FOLDF(triple(a''''', cons(y'''''''''', z''''''''''), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y'''''''''', z''''''''''), c'''''), C)
FOLDF(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), C)
FOLDF(triple(a''''', cons(y'''''', z''''''), c'''''), cons(C, nil)) -> F(triple(a''''', cons(y'''''', z''''''), c'''''), C)
FOLDF(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), cons(C, nil)) -> F(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), C)
FOLDF(triple(a'''''', cons(y''''', nil), c''''''), cons(C, nil)) -> F(triple(a'''''', cons(y''''', nil), c''''''), C)
FOLDF(triple(a'''''', cons(y'''''', z''''''), c''''''), cons(C, nil)) -> F(triple(a'''''', cons(y'''''', z''''''), c''''''), C)
FOLDF(triple(a''''', cons(y'''''''''', cons(y'''''''''''', z'''''''''''')), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y'''''''''', cons(y'''''''''''', z'''''''''''')), c'''''), B)
FOLDF(triple(a''''', cons(y'''''''0'''', cons(y''''''''''''', z'''''''''')), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y'''''''0'''', cons(y''''''''''''', z'''''''''')), c'''''), B)
FOLDF(triple(a''''', cons(y''''''''', nil), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y''''''''', nil), c'''''), B)
FOLDF(triple(a''''', cons(y'''''''''', z''''''''''), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y'''''''''', z''''''''''), c'''''), B)
FOLDF(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), B)
FOLDF(triple(a''''', cons(y'''''', z''''''), c'''''), cons(B, nil)) -> F(triple(a''''', cons(y'''''', z''''''), c'''''), B)
FOLDF(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), cons(B, nil)) -> F(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), B)
FOLDF(triple(a'''''', cons(y''''', nil), c''''''), cons(B, nil)) -> F(triple(a'''''', cons(y''''', nil), c''''''), B)
FOLDF(triple(a'''''', cons(y'''''', z''''''), c''''''), cons(B, nil)) -> F(triple(a'''''', cons(y'''''', z''''''), c''''''), B)
FOLDF(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), cons(A, nil)) -> F(triple(a''''', cons(y'''''', cons(y'''''''', z'''''''')), c'''''), A)
FOLDF(triple(a''''', cons(y'''''', z''''''), c'''''), cons(A, nil)) -> F(triple(a''''', cons(y'''''', z''''''), c'''''), A)
FOLDF(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), cons(A, nil)) -> F(triple(a'''''', cons(y'''''''0, cons(y''''''''', z'''''')), c''''''), A)
FOLDF(triple(a'''''', cons(y''''', nil), c''''''), cons(A, nil)) -> F(triple(a'''''', cons(y''''', nil), c''''''), A)
FOLDF(triple(a'''''', cons(y'''''', z''''''), c''''''), cons(A, nil)) -> F(triple(a'''''', cons(y'''''', z''''''), c''''''), A)

Additionally, the following usable rules for innermost can be oriented:

f(t, x) -> f'(t, g(x))
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C

Used ordering: Polynomial ordering with Polynomial interpretation:

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

POL(f'(x₁, x₂)) = x₁

POL(f(x₁, x₂)) = x₁

POL(F(x₁, x₂)) = 0

POL(FOLDF(x₁, x₂)) = x₁

POL(F''(x₁)) = x₁

POL(C) = 0

POL(g(x₁)) = 0

POL(B) = 0

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

POL(F'(x₁, x₂)) = 0

POL(nil) = 0

POL(foldf(x₁, x₂)) = x₁

POL(f''(x₁)) = x₁

POL(A) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 21

                 ↳Polynomial Ordering

Dependency Pairs:

F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), C) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), C) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F(triple(a''', cons(y'''''''', z''''''''), c'''), C) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), C) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), C) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), C) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), C) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y'''', z''''), c''''), C) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)
F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), B) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F'(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), B) -> F(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), A)
F'(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), B) -> F(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), A)
F'(triple(a', cons(y''''', nil), c'), B) -> F(triple(a', cons(y''''', nil), c'), A)
F(triple(a''', cons(y'''''''', z''''''''), c'''), B) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), B) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), B) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), B) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), B) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a''', nil, c'''), C) -> F'(triple(a''', nil, c'''), B)
F(triple(a''', nil, c'''), C) -> F'(triple(a''', nil, c'''), A)
FOLDF(triple(a''''', nil, c'''''), cons(C, nil)) -> F(triple(a''''', nil, c'''''), C)
F'(triple(a', nil, c'), B) -> F(triple(a', nil, c'), A)
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), B)
FOLDF(triple(a''''', nil, c'''''), cons(B, nil)) -> F(triple(a''''', nil, c'''''), B)
F'(triple(a'', cons(y''', nil), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', nil))
F(triple(a'''', cons(y'''', z''''), c''''), B) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', nil))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', nil))))
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''''', z'''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F''(triple(a'', b'', cons(y''', cons(y''''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', nil)))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', z''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F''(triple(a'', b'', cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''0, cons(y'''''', z''''))))
F'(triple(a''', nil, cons(y'''', cons(y'''''', z''''''))), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', cons(y'''''', z''''''))))
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), A)
F'(triple(a'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', nil))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', nil))))
F'(triple(a'', cons(y''', cons(y''''', cons(y''''''', z'''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F'(triple(a'', cons(y''', cons(y''''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', nil)))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', z''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F'(triple(a'', cons(y''', cons(y''''0, cons(y'''''', z''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''0, cons(y'''''', z''''))))
F'(triple(a'', cons(y''0, cons(y'''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''0, cons(y'''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(x''', cons(y''', cons(y''''0, cons(y'''''', z''''))))
FOLDF(x''', cons(y, cons(y''0, cons(y'''', nil)))) -> FOLDF(x''', cons(y''0, cons(y'''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''', z''''')))) -> FOLDF(x''', cons(y''', cons(y''''', z''''')))
FOLDF(x'''', cons(y, cons(y''0, cons(y'''', z'''')))) -> FOLDF(x'''', cons(y''0, cons(y'''', z'''')))
F'(triple(a'', cons(y''', cons(y''''', z''''')), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', z''''')))
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
FOLDF(x''', cons(y, cons(y'', cons(y''', z')))) -> F(f(f(foldf(x''', z'), y'''), y''), y)
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
F(triple(a''', cons(y'''', z''''), c'''), A) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
FOLDF(x'''', cons(y, cons(y''', nil))) -> FOLDF(x'''', cons(y''', nil))
F''(triple(a'', b'', cons(y''0, cons(y'''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''0, cons(y'''', nil)))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
FOLDF(x''', cons(y, cons(y'', nil))) -> F(f(x''', y''), y)
F''(triple(a'', b'', cons(y''', cons(y''''', z''''')))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', z''''')))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
F(triple(a'''', cons(y''', nil), c''''), A) -> F'(triple(a'''', cons(y''', nil), c''''), A)
FOLDF(triple(a''''', nil, c'''''), cons(A, nil)) -> F(triple(a''''', nil, c'''''), A)
F''(triple(a'', b'', cons(y''', nil))) -> FOLDF(triple(a'', b'', nil), cons(y''', nil))
F'(triple(a''', nil, cons(y'''', z'''')), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', z'''')))
F(triple(a''', nil, c'''), A) -> F'(triple(a''', nil, c'''), A)
FOLDF(x''', cons(y, cons(y''', z'''))) -> F(f'(foldf(x''', z'''), g(y''')), y)
F''(triple(a', b', cons(y'', cons(y'''', z'''')))) -> FOLDF(triple(a', b', nil), cons(y'', cons(y'''', z'''')))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
F(triple(a'''', cons(y'''', z''''), c''''), A) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F'(triple(a', cons(y'''''', z''''''), c'), B) -> F(triple(a', cons(y'''''', z''''''), c'), A)
F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), C) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

The following dependency pairs can be strictly oriented:

F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), C) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), C) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F(triple(a''', cons(y'''''''', z''''''''), c'''), C) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), C) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), C) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), C) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), C) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y'''', z''''), c''''), C) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F(triple(a''', nil, c'''), C) -> F'(triple(a''', nil, c'''), B)
F(triple(a''', nil, c'''), C) -> F'(triple(a''', nil, c'''), A)
F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), C) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)

Additionally, the following usable rules for innermost can be oriented:

f(t, x) -> f'(t, g(x))
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(triple(x₁, x₂, x₃)) = x₂ + x₃

POL(f'(x₁, x₂)) = x₁ + x₂

POL(f(x₁, x₂)) = x₁ + x₂

POL(F(x₁, x₂)) = x₁ + x₂

POL(FOLDF(x₁, x₂)) = x₁ + x₂

POL(F''(x₁)) = x₁

POL(C) = 1

POL(g(x₁)) = x₁

POL(B) = 0

POL(cons(x₁, x₂)) = x₁ + x₂

POL(nil) = 0

POL(F'(x₁, x₂)) = x₁

POL(foldf(x₁, x₂)) = x₁ + x₂

POL(f''(x₁)) = x₁

POL(A) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 22

                 ↳Dependency Graph

Dependency Pairs:

F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)
F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), B) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F'(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), B) -> F(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), A)
F'(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), B) -> F(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), A)
F'(triple(a', cons(y''''', nil), c'), B) -> F(triple(a', cons(y''''', nil), c'), A)
F(triple(a''', cons(y'''''''', z''''''''), c'''), B) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), B) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), B) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), B) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), B) -> F'(triple(a'''', cons(y''', nil), c''''), A)
FOLDF(triple(a''''', nil, c'''''), cons(C, nil)) -> F(triple(a''''', nil, c'''''), C)
F'(triple(a', nil, c'), B) -> F(triple(a', nil, c'), A)
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), B)
FOLDF(triple(a''''', nil, c'''''), cons(B, nil)) -> F(triple(a''''', nil, c'''''), B)
F'(triple(a'', cons(y''', nil), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', nil))
F(triple(a'''', cons(y'''', z''''), c''''), B) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', nil))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', nil))))
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''''', z'''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F''(triple(a'', b'', cons(y''', cons(y''''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', nil)))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', z''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F''(triple(a'', b'', cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''0, cons(y'''''', z''''))))
F'(triple(a''', nil, cons(y'''', cons(y'''''', z''''''))), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', cons(y'''''', z''''''))))
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), A)
F'(triple(a'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', nil))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', nil))))
F'(triple(a'', cons(y''', cons(y''''', cons(y''''''', z'''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F'(triple(a'', cons(y''', cons(y''''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', nil)))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', z''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F'(triple(a'', cons(y''', cons(y''''0, cons(y'''''', z''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''0, cons(y'''''', z''''))))
F'(triple(a'', cons(y''0, cons(y'''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''0, cons(y'''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(x''', cons(y''', cons(y''''0, cons(y'''''', z''''))))
FOLDF(x''', cons(y, cons(y''0, cons(y'''', nil)))) -> FOLDF(x''', cons(y''0, cons(y'''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''', z''''')))) -> FOLDF(x''', cons(y''', cons(y''''', z''''')))
FOLDF(x'''', cons(y, cons(y''0, cons(y'''', z'''')))) -> FOLDF(x'''', cons(y''0, cons(y'''', z'''')))
F'(triple(a'', cons(y''', cons(y''''', z''''')), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', z''''')))
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
FOLDF(x''', cons(y, cons(y'', cons(y''', z')))) -> F(f(f(foldf(x''', z'), y'''), y''), y)
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
F(triple(a''', cons(y'''', z''''), c'''), A) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
FOLDF(x'''', cons(y, cons(y''', nil))) -> FOLDF(x'''', cons(y''', nil))
F''(triple(a'', b'', cons(y''0, cons(y'''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''0, cons(y'''', nil)))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
FOLDF(x''', cons(y, cons(y'', nil))) -> F(f(x''', y''), y)
F''(triple(a'', b'', cons(y''', cons(y''''', z''''')))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', z''''')))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
F(triple(a'''', cons(y''', nil), c''''), A) -> F'(triple(a'''', cons(y''', nil), c''''), A)
FOLDF(triple(a''''', nil, c'''''), cons(A, nil)) -> F(triple(a''''', nil, c'''''), A)
F''(triple(a'', b'', cons(y''', nil))) -> FOLDF(triple(a'', b'', nil), cons(y''', nil))
F'(triple(a''', nil, cons(y'''', z'''')), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', z'''')))
F(triple(a''', nil, c'''), A) -> F'(triple(a''', nil, c'''), A)
FOLDF(x''', cons(y, cons(y''', z'''))) -> F(f'(foldf(x''', z'''), g(y''')), y)
F''(triple(a', b', cons(y'', cons(y'''', z'''')))) -> FOLDF(triple(a', b', nil), cons(y'', cons(y'''', z'''')))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
F(triple(a'''', cons(y'''', z''''), c''''), A) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F'(triple(a', cons(y'''''', z''''''), c'), B) -> F(triple(a', cons(y'''''', z''''''), c'), A)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

Using the Dependency Graph the DP problem was split into 1 DP problems.

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 23

                 ↳Polynomial Ordering

Dependency Pairs:

F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), B) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F'(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), B) -> F(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), A)
F'(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), B) -> F(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), A)
F'(triple(a', cons(y''''', nil), c'), B) -> F(triple(a', cons(y''''', nil), c'), A)
F(triple(a''', cons(y'''''''', z''''''''), c'''), B) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F'(triple(a', nil, c'), B) -> F(triple(a', nil, c'), A)
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), B)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), B) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), B) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), B) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), B) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y'''', z''''), c''''), B) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F'(triple(a'', cons(y''', nil), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', nil))
F(triple(a''', cons(y'''', z''''), c'''), A) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F'(triple(a'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', nil))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', nil))))
F'(triple(a'', cons(y''', cons(y''''', cons(y''''''', z'''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F'(triple(a'', cons(y''', cons(y''''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', nil)))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', z''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F'(triple(a'', cons(y''', cons(y''''0, cons(y'''''', z''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''0, cons(y'''''', z''''))))
F'(triple(a'', cons(y''0, cons(y'''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''0, cons(y'''', nil)))
F'(triple(a'', cons(y''', cons(y''''', z''''')), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', z''''')))
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', nil))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', nil))))
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''''', z'''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F''(triple(a'', b'', cons(y''', cons(y''''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(x''', cons(y''', cons(y''''0, cons(y'''''', z''''))))
FOLDF(x''', cons(y, cons(y''0, cons(y'''', nil)))) -> FOLDF(x''', cons(y''0, cons(y'''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''', z''''')))) -> FOLDF(x''', cons(y''', cons(y''''', z''''')))
FOLDF(x'''', cons(y, cons(y''0, cons(y'''', z'''')))) -> FOLDF(x'''', cons(y''0, cons(y'''', z'''')))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', z''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
FOLDF(x''', cons(y, cons(y'', cons(y''', z')))) -> F(f(f(foldf(x''', z'), y'''), y''), y)
F''(triple(a'', b'', cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''0, cons(y'''''', z''''))))
FOLDF(x'''', cons(y, cons(y''', nil))) -> FOLDF(x'''', cons(y''', nil))
F''(triple(a'', b'', cons(y''0, cons(y'''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''0, cons(y'''', nil)))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
F(triple(a'''', cons(y''', nil), c''''), A) -> F'(triple(a'''', cons(y''', nil), c''''), A)
FOLDF(x''', cons(y, cons(y'', nil))) -> F(f(x''', y''), y)
F''(triple(a'', b'', cons(y''', cons(y''''', z''''')))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', z''''')))
F'(triple(a''', nil, cons(y'''', cons(y'''''', z''''''))), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', cons(y'''''', z''''''))))
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), A)
FOLDF(triple(a''''', nil, c'''''), cons(B, nil)) -> F(triple(a''''', nil, c'''''), B)
FOLDF(triple(a''''', nil, c'''''), cons(A, nil)) -> F(triple(a''''', nil, c'''''), A)
F''(triple(a'', b'', cons(y''', nil))) -> FOLDF(triple(a'', b'', nil), cons(y''', nil))
F'(triple(a''', nil, cons(y'''', z'''')), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', z'''')))
F(triple(a''', nil, c'''), A) -> F'(triple(a''', nil, c'''), A)
FOLDF(x''', cons(y, cons(y''', z'''))) -> F(f'(foldf(x''', z'''), g(y''')), y)
F''(triple(a', b', cons(y'', cons(y'''', z'''')))) -> FOLDF(triple(a', b', nil), cons(y'', cons(y'''', z'''')))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
F(triple(a'''', cons(y'''', z''''), c''''), A) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F'(triple(a', cons(y'''''', z''''''), c'), B) -> F(triple(a', cons(y'''''', z''''''), c'), A)
F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

The following dependency pairs can be strictly oriented:

F(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''0'', cons(y''''''''''', z'''''''')), c'''), B)
F(triple(a''', cons(y''''''', nil), c'''), B) -> F'(triple(a''', cons(y''''''', nil), c'''), B)
F(triple(a''', cons(y'''''''', z''''''''), c'''), B) -> F'(triple(a''', cons(y'''''''', z''''''''), c'''), B)
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), B)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), B) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), B) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), B) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
F(triple(a'''', cons(y''', nil), c''''), B) -> F'(triple(a'''', cons(y''', nil), c''''), A)
F(triple(a'''', cons(y'''', z''''), c''''), B) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F(triple(a''', nil, c'''), B) -> F'(triple(a''', nil, c'''), A)
F(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B) -> F'(triple(a''', cons(y'''''''', cons(y'''''''''', z'''''''''')), c'''), B)

Additionally, the following usable rules for innermost can be oriented:

f(t, x) -> f'(t, g(x))
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(triple(x₁, x₂, x₃)) = x₂ + x₃

POL(f'(x₁, x₂)) = x₁

POL(f(x₁, x₂)) = x₁

POL(F(x₁, x₂)) = x₁ + x₂

POL(FOLDF(x₁, x₂)) = x₁ + x₂

POL(F''(x₁)) = x₁

POL(C) = 0

POL(g(x₁)) = 1

POL(B) = 1

POL(cons(x₁, x₂)) = x₁ + x₂

POL(nil) = 0

POL(F'(x₁, x₂)) = x₁

POL(foldf(x₁, x₂)) = x₁

POL(f''(x₁)) = x₁

POL(A) = 0

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 24

                 ↳Dependency Graph

Dependency Pairs:

F'(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), B) -> F(triple(a', cons(y'''''', cons(y'''''''', z'''''''')), c'), A)
F'(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), B) -> F(triple(a', cons(y'''''''0, cons(y''''''''', z'''''')), c'), A)
F'(triple(a', cons(y''''', nil), c'), B) -> F(triple(a', cons(y''''', nil), c'), A)
F'(triple(a', nil, c'), B) -> F(triple(a', nil, c'), A)
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F'(triple(a'', cons(y''', nil), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', nil))
F(triple(a''', cons(y'''', z''''), c'''), A) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F'(triple(a'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', nil))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', nil))))
F'(triple(a'', cons(y''', cons(y''''', cons(y''''''', z'''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F'(triple(a'', cons(y''', cons(y''''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', nil)))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', z''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F'(triple(a'', cons(y''', cons(y''''0, cons(y'''''', z''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''0, cons(y'''''', z''''))))
F'(triple(a'', cons(y''0, cons(y'''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''0, cons(y'''', nil)))
F'(triple(a'', cons(y''', cons(y''''', z''''')), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', z''''')))
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', nil))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', nil))))
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''''', z'''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F''(triple(a'', b'', cons(y''', cons(y''''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(x''', cons(y''', cons(y''''0, cons(y'''''', z''''))))
FOLDF(x''', cons(y, cons(y''0, cons(y'''', nil)))) -> FOLDF(x''', cons(y''0, cons(y'''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''', z''''')))) -> FOLDF(x''', cons(y''', cons(y''''', z''''')))
FOLDF(x'''', cons(y, cons(y''0, cons(y'''', z'''')))) -> FOLDF(x'''', cons(y''0, cons(y'''', z'''')))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', z''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
FOLDF(x''', cons(y, cons(y'', cons(y''', z')))) -> F(f(f(foldf(x''', z'), y'''), y''), y)
F''(triple(a'', b'', cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''0, cons(y'''''', z''''))))
FOLDF(x'''', cons(y, cons(y''', nil))) -> FOLDF(x'''', cons(y''', nil))
F''(triple(a'', b'', cons(y''0, cons(y'''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''0, cons(y'''', nil)))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
F(triple(a'''', cons(y''', nil), c''''), A) -> F'(triple(a'''', cons(y''', nil), c''''), A)
FOLDF(x''', cons(y, cons(y'', nil))) -> F(f(x''', y''), y)
F''(triple(a'', b'', cons(y''', cons(y''''', z''''')))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', z''''')))
F'(triple(a''', nil, cons(y'''', cons(y'''''', z''''''))), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', cons(y'''''', z''''''))))
FOLDF(triple(a''''', nil, c'''''), cons(B, nil)) -> F(triple(a''''', nil, c'''''), B)
FOLDF(triple(a''''', nil, c'''''), cons(A, nil)) -> F(triple(a''''', nil, c'''''), A)
F''(triple(a'', b'', cons(y''', nil))) -> FOLDF(triple(a'', b'', nil), cons(y''', nil))
F'(triple(a''', nil, cons(y'''', z'''')), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', z'''')))
F(triple(a''', nil, c'''), A) -> F'(triple(a''', nil, c'''), A)
FOLDF(x''', cons(y, cons(y''', z'''))) -> F(f'(foldf(x''', z'''), g(y''')), y)
F''(triple(a', b', cons(y'', cons(y'''', z'''')))) -> FOLDF(triple(a', b', nil), cons(y'', cons(y'''', z'''')))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
F(triple(a'''', cons(y'''', z''''), c''''), A) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)
F'(triple(a', cons(y'''''', z''''''), c'), B) -> F(triple(a', cons(y'''''', z''''''), c'), A)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

Using the Dependency Graph the DP problem was split into 1 DP problems.

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 25

                 ↳Polynomial Ordering

Dependency Pairs:

F'(triple(a''', nil, cons(y'''', cons(y'''''', z''''''))), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', cons(y'''''', z''''''))))
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F'(triple(a'', cons(y''', nil), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', nil))
F(triple(a''', cons(y'''', z''''), c'''), A) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F'(triple(a'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', nil))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', nil))))
F'(triple(a'', cons(y''', cons(y''''', cons(y''''''', z'''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F'(triple(a'', cons(y''', cons(y''''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', nil)))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', z''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F'(triple(a'', cons(y''', cons(y''''0, cons(y'''''', z''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''0, cons(y'''''', z''''))))
F'(triple(a'', cons(y''0, cons(y'''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''0, cons(y'''', nil)))
F'(triple(a'', cons(y''', cons(y''''', z''''')), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', z''''')))
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', nil))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', nil))))
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''''', z'''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F''(triple(a'', b'', cons(y''', cons(y''''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(x''', cons(y''', cons(y''''0, cons(y'''''', z''''))))
FOLDF(x''', cons(y, cons(y''0, cons(y'''', nil)))) -> FOLDF(x''', cons(y''0, cons(y'''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''', z''''')))) -> FOLDF(x''', cons(y''', cons(y''''', z''''')))
FOLDF(x'''', cons(y, cons(y''0, cons(y'''', z'''')))) -> FOLDF(x'''', cons(y''0, cons(y'''', z'''')))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', z''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
FOLDF(x''', cons(y, cons(y'', cons(y''', z')))) -> F(f(f(foldf(x''', z'), y'''), y''), y)
F''(triple(a'', b'', cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''0, cons(y'''''', z''''))))
FOLDF(x'''', cons(y, cons(y''', nil))) -> FOLDF(x'''', cons(y''', nil))
F''(triple(a'', b'', cons(y''0, cons(y'''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''0, cons(y'''', nil)))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
F(triple(a'''', cons(y''', nil), c''''), A) -> F'(triple(a'''', cons(y''', nil), c''''), A)
FOLDF(x''', cons(y, cons(y'', nil))) -> F(f(x''', y''), y)
F''(triple(a'', b'', cons(y''', cons(y''''', z''''')))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', z''''')))
FOLDF(triple(a''''', nil, c'''''), cons(A, nil)) -> F(triple(a''''', nil, c'''''), A)
F''(triple(a'', b'', cons(y''', nil))) -> FOLDF(triple(a'', b'', nil), cons(y''', nil))
F'(triple(a''', nil, cons(y'''', z'''')), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', z'''')))
F(triple(a''', nil, c'''), A) -> F'(triple(a''', nil, c'''), A)
FOLDF(x''', cons(y, cons(y''', z'''))) -> F(f'(foldf(x''', z'''), g(y''')), y)
F''(triple(a', b', cons(y'', cons(y'''', z'''')))) -> FOLDF(triple(a', b', nil), cons(y'', cons(y'''', z'''')))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))
F(triple(a'''', cons(y'''', z''''), c''''), A) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

The following dependency pairs can be strictly oriented:

F'(triple(a''', nil, cons(y'''', cons(y'''''', z''''''))), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', cons(y'''''', z''''''))))
F'(triple(a'', cons(y''', nil), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', nil))
F'(triple(a'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', nil))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', nil))))
F'(triple(a'', cons(y''', cons(y''''', cons(y''''''', z'''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F'(triple(a'', cons(y''', cons(y''''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', nil)))
F'(triple(a'', cons(y''', cons(y''0'', cons(y'''''', z''''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F'(triple(a'', cons(y''', cons(y''''0, cons(y'''''', z''''))), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''0, cons(y'''''', z''''))))
F'(triple(a'', cons(y''0, cons(y'''', nil)), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''0, cons(y'''', nil)))
F'(triple(a'', cons(y''', cons(y''''', z''''')), c''), A) -> FOLDF(triple(cons(A, a''), nil, c''), cons(y''', cons(y''''', z''''')))
F'(triple(a', cons(y'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
F'(triple(a'', cons(y', cons(y'', z'')), c''), A) -> F''(f(f(foldf(triple(cons(A, a''), nil, c''), z''), y''), y'))
F'(triple(a'', cons(y', nil), c''), A) -> F''(f(triple(cons(A, a''), nil, c''), y'))
F'(triple(a''', nil, cons(y'''', z'''')), A) -> F''(triple(cons(A, a'''), nil, cons(y'''', z'''')))
F'(triple(a'', cons(y'', z''), c''), A) -> F''(f'(foldf(triple(cons(A, a''), nil, c''), z''), g(y'')))

Additionally, the following usable rules for innermost can be oriented:

f(t, x) -> f'(t, g(x))
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(triple(x₁, x₂, x₃)) = x₂ + x₃

POL(f'(x₁, x₂)) = x₁

POL(F(x₁, x₂)) = x₁ + x₂

POL(f(x₁, x₂)) = x₁

POL(FOLDF(x₁, x₂)) = x₁ + x₂

POL(F''(x₁)) = x₁

POL(C) = 0

POL(g(x₁)) = 1

POL(B) = 0

POL(cons(x₁, x₂)) = x₁ + x₂

POL(nil) = 0

POL(F'(x₁, x₂)) = 1 + x₁

POL(foldf(x₁, x₂)) = x₁

POL(f''(x₁)) = x₁

POL(A) = 1

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 26

                 ↳Dependency Graph

Dependency Pairs:

F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A) -> F'(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A)
F(triple(a''', cons(y'''', z''''), c'''), A) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''0'', cons(y'''''''', z'''''')))))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', nil))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', nil))))
F''(triple(a'', b'', cons(y''', cons(y''''', cons(y''''''', z'''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', cons(y''''''', z'''''''))))
F''(triple(a'', b'', cons(y''', cons(y''''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(x''', cons(y''', cons(y''''0, cons(y'''''', z''''))))
FOLDF(x''', cons(y, cons(y''0, cons(y'''', nil)))) -> FOLDF(x''', cons(y''0, cons(y'''', nil)))
FOLDF(x''', cons(y, cons(y''', cons(y''''', z''''')))) -> FOLDF(x''', cons(y''', cons(y''''', z''''')))
FOLDF(x'''', cons(y, cons(y''0, cons(y'''', z'''')))) -> FOLDF(x'''', cons(y''0, cons(y'''', z'''')))
F''(triple(a'', b'', cons(y''', cons(y''0'', cons(y'''''', z''''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''0'', cons(y'''''', z''''''))))
F(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A) -> F'(triple(a'''', cons(y''''', cons(y'''''', z'''')), c''''), A)
FOLDF(x''', cons(y, cons(y'', cons(y''', z')))) -> F(f(f(foldf(x''', z'), y'''), y''), y)
F''(triple(a'', b'', cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''0, cons(y'''''', z''''))))
FOLDF(x'''', cons(y, cons(y''', nil))) -> FOLDF(x'''', cons(y''', nil))
F''(triple(a'', b'', cons(y''0, cons(y'''', nil)))) -> FOLDF(triple(a'', b'', nil), cons(y''0, cons(y'''', nil)))
F(triple(a'''', cons(y''', nil), c''''), A) -> F'(triple(a'''', cons(y''', nil), c''''), A)
FOLDF(x''', cons(y, cons(y'', nil))) -> F(f(x''', y''), y)
F''(triple(a'', b'', cons(y''', cons(y''''', z''''')))) -> FOLDF(triple(a'', b'', nil), cons(y''', cons(y''''', z''''')))
FOLDF(triple(a''''', nil, c'''''), cons(A, nil)) -> F(triple(a''''', nil, c'''''), A)
F''(triple(a'', b'', cons(y''', nil))) -> FOLDF(triple(a'', b'', nil), cons(y''', nil))
F(triple(a''', nil, c'''), A) -> F'(triple(a''', nil, c'''), A)
FOLDF(x''', cons(y, cons(y''', z'''))) -> F(f'(foldf(x''', z'''), g(y''')), y)
F''(triple(a', b', cons(y'', cons(y'''', z'''')))) -> FOLDF(triple(a', b', nil), cons(y'', cons(y'''', z'''')))
F(triple(a'''', cons(y'''', z''''), c''''), A) -> F'(triple(a'''', cons(y'''', z''''), c''''), A)

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

Using the Dependency Graph the DP problem was split into 1 DP problems.

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 27

                 ↳Polynomial Ordering

Dependency Pairs:

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

The following dependency pairs can be strictly oriented:

FOLDF(x''', cons(y, cons(y''', cons(y''''0, cons(y'''''', z''''))))) -> FOLDF(x''', cons(y''', cons(y''''0, cons(y'''''', z''''))))
FOLDF(x''', cons(y, cons(y''', cons(y''''', z''''')))) -> FOLDF(x''', cons(y''', cons(y''''', z''''')))
FOLDF(x'''', cons(y, cons(y''0, cons(y'''', z'''')))) -> FOLDF(x'''', cons(y''0, cons(y'''', z'''')))

There are no usable rules for innermost that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Nar

           →DP Problem 2

             ↳Nar

...

               →DP Problem 28

                 ↳Dependency Graph

Dependency Pair:

Rules:

g(A) -> A
g(B) -> A
g(B) -> B
g(C) -> A
g(C) -> B
g(C) -> C
foldf(x, nil) -> x
foldf(x, cons(y, z)) -> f(foldf(x, z), y)
f(t, x) -> f'(t, g(x))
f'(triple(a, b, c), C) -> triple(a, b, cons(C, c))
f'(triple(a, b, c), B) -> f(triple(a, b, c), A)
f'(triple(a, b, c), A) -> f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) -> foldf(triple(a, b, nil), c)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

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

POL(triple(x₁, x₂, x₃))	= x₂
POL(f'(x₁, x₂))	= x₁
POL(f(x₁, x₂))	= x₁
POL(F(x₁, x₂))	= 0
POL(FOLDF(x₁, x₂))	= x₁
POL(F''(x₁))	= x₁
POL(C)	= 0
POL(g(x₁))	= 0
POL(B)	= 0
POL(cons(x₁, x₂))	= 1
POL(F'(x₁, x₂))	= 0
POL(nil)	= 0
POL(foldf(x₁, x₂))	= x₁
POL(f''(x₁))	= x₁
POL(A)	= 0

POL(triple(x₁, x₂, x₃))	= x₂ + x₃
POL(f'(x₁, x₂))	= x₁ + x₂
POL(f(x₁, x₂))	= x₁ + x₂
POL(F(x₁, x₂))	= x₁ + x₂
POL(FOLDF(x₁, x₂))	= x₁ + x₂
POL(F''(x₁))	= x₁
POL(C)	= 1
POL(g(x₁))	= x₁
POL(B)	= 0
POL(cons(x₁, x₂))	= x₁ + x₂
POL(nil)	= 0
POL(F'(x₁, x₂))	= x₁
POL(foldf(x₁, x₂))	= x₁ + x₂
POL(f''(x₁))	= x₁
POL(A)	= 0

POL(cons(x₁, x₂))	= 1 + x₂
POL(FOLDF(x₁, x₂))	= 1 + x₂