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. 



   R
     ↳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. 


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



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



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 3
                 ↳Forward Instantiation 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 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: 



   R
     ↳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', z'), c'), A) -> F''(f(foldf(triple(cons(A, a'), nil, c'), z'), 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, 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

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: 



   R
     ↳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) -> 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', z'), c'), A) -> F''(f(foldf(triple(cons(A, a'), nil, c'), z'), y'))
F(t, B) -> 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, 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)) -> 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: 



   R
     ↳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'''')))
F'(triple(a', cons(y'', z''), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', z''))
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'), y'))
F(t, A) -> 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(t, A) -> F'(t, A)
four 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'''', 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: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 7
                 ↳Forward Instantiation Transformation


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''', cons(y''', z'''), c'''), A) -> F'(triple(a''', cons(y''', z'''), c'''), A)
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''))
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'), 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, 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), B) -> F(triple(a, b, c), A)
four 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'''''', 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: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 8
                 ↳Forward Instantiation Transformation


Dependency Pairs:

F(t, C) -> F'(t, B)
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'''''', z''''''), c'), B) -> F(triple(a', 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''', 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)
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''))
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(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', cons(y', z'), c'), A) -> F''(f(foldf(triple(cons(A, a'), nil, c'), z'), y'))
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), A) -> F'(triple(a''', cons(y'''', 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




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)
four 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'''', 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: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 9
                 ↳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''', 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, 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'''), 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) -> 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''))
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'), 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(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(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, B)
four 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'''''''', 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'''), B)

The transformation is resulting in one new DP problem: 



   R
     ↳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'''), B)
F(triple(a''', cons(y'''''''', z''''''''), c'''), B) -> F'(triple(a''', cons(y'''''''', z''''''''), 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'''', 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'''), 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'''''', 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'''', z''''), 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'''), 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, C) -> 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''))
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(t, C) -> 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', cons(y', z'), c'), A) -> F''(f(foldf(triple(cons(A, a'), nil, c'), z'), y'))
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), B) -> F'(triple(a''', cons(y'''', 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




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)
four 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'''', 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: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 11
                 ↳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''', 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'''''''', z''''''''), c'''), B) -> F'(triple(a''', cons(y'''''''', z''''''''), 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''', 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) -> 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'''', 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)
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'), 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)
four 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'''''''', 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'''), B)

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 12
                 ↳Narrowing 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'''''''', z''''''''), c'''), C) -> F'(triple(a''', cons(y'''''''', z''''''''), 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'''', z''''), c'''), C) -> F'(triple(a''', cons(y'''', z''''), 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'''''''', 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''''', 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''', 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'''), 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) -> 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''', z'''), c'''), A) -> F'(triple(a''', cons(y''', z'''), 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)
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'), y'))
F(triple(a''', cons(y'''', cons(y'''''', z'''''')), c'''), C) -> F'(triple(a''', cons(y'''', 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




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: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 13
                 ↳Forward Instantiation Transformation


Dependency Pairs:

F(triple(a''', cons(y'''''''', z''''''''), c'''), C) -> F'(triple(a''', cons(y'''''''', z''''''''), 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''', 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'''''''', 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''''''', 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''', 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'''), A) -> F'(triple(a''', cons(y'''', 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'', z''), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), 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'', z''))) -> F(f(foldf(x'', z''), 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, c'), A) -> F''(triple(cons(A, a'), nil, c'))
F(triple(a''', nil, c'''), A) -> F'(triple(a''', nil, c'''), A)
FOLDF(x'', cons(y, nil)) -> F(x'', y)
FOLDF(x'', cons(y, cons(y'', z''))) -> FOLDF(x'', cons(y'', z''))
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'), 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

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: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 14
                 ↳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''''''', 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''', 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'''''''', 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''''''', 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''', 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'''', 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'''', z''''), c'''), A) -> F'(triple(a''', cons(y'''', z''''), c'''), A)
FOLDF(x'', cons(y, cons(y'', z''))) -> F(f(foldf(x'', z''), 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)
FOLDF(x'', cons(y, cons(y'', z''))) -> FOLDF(x'', cons(y'', z''))
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'), 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'''''''', z''''''''), c'''), C) -> F'(triple(a''', 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)
18 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'''''', 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'''''', 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'''''''''', 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''''', 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'''''', 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'''''''''', 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)

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 15
                 ↳Remaining Obligation(s)




The following remains to be proven:
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'''''''''', z''''''''''), c'''''), cons(C, nil)) -> F(triple(a''''', 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''''', 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'''''''''', z''''''''''), c'''''), cons(B, nil)) -> F(triple(a''''', 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''''', 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''''', z'''''), c'''''), cons(A, nil)) -> F(triple(a''''', cons(y''''', z'''''), c'''''), A)
F(triple(a''', cons(y'''''''', z''''''''), c'''), C) -> F'(triple(a''', cons(y'''''''', z''''''''), 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''', 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'''''''', 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''''''', 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''', 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'', cons(y'''', z'''')), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', cons(y'''', z'''')))
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)
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', cons(y'', z''), c'), A) -> FOLDF(triple(cons(A, a'), nil, c'), cons(y'', z''))
F(triple(a''', cons(y'''', z''''), c'''), A) -> 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', 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, cons(y'', z''))) -> F(f(foldf(x'', z''), y''), y)
FOLDF(x'', cons(y, cons(y'', z''))) -> FOLDF(x'', cons(y'', z''))
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'), 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



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