Term Rewriting System R:
[x, y, z]
f(f(a, b), x) -> f(b, f(a, f(c, f(b, f(a, x)))))
f(x, f(y, z)) -> f(f(x, y), z)

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

F(f(a, b), x) -> F(b, f(a, f(c, f(b, f(a, x)))))
F(f(a, b), x) -> F(a, f(c, f(b, f(a, x))))
F(f(a, b), x) -> F(c, f(b, f(a, x)))
F(f(a, b), x) -> F(b, f(a, x))
F(f(a, b), x) -> F(a, x)
F(x, f(y, z)) -> F(f(x, y), z)
F(x, f(y, z)) -> F(x, y)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Negative Polynomial Order


Dependency Pairs:

F(f(a, b), x) -> F(a, x)
F(f(a, b), x) -> F(b, f(a, x))
F(f(a, b), x) -> F(c, f(b, f(a, x)))
F(x, f(y, z)) -> F(x, y)
F(f(a, b), x) -> F(a, f(c, f(b, f(a, x))))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(a, b), x) -> F(b, f(a, f(c, f(b, f(a, x)))))


Rules:


f(f(a, b), x) -> f(b, f(a, f(c, f(b, f(a, x)))))
f(x, f(y, z)) -> f(f(x, y), z)


Strategy:

innermost




The following Dependency Pairs can be strictly oriented using the given order.

F(f(a, b), x) -> F(b, f(a, x))
F(f(a, b), x) -> F(c, f(b, f(a, x)))
F(f(a, b), x) -> F(b, f(a, f(c, f(b, f(a, x)))))


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

f(f(a, b), x) -> f(b, f(a, f(c, f(b, f(a, x)))))
f(x, f(y, z)) -> f(f(x, y), z)


Used ordering:
Polynomial Order with Interpretation:

POL( F(x1, x2) ) = x1

POL( f(x1, x2) ) = x1

POL( a ) = 1

POL( b ) = 0

POL( c ) = 0


This results in one new DP problem. 


   R
     ↳DPs
       →DP Problem 1
         ↳Neg POLO
           →DP Problem 2
             ↳Narrowing Transformation


Dependency Pairs:

F(f(a, b), x) -> F(a, x)
F(x, f(y, z)) -> F(x, y)
F(f(a, b), x) -> F(a, f(c, f(b, f(a, x))))
F(x, f(y, z)) -> F(f(x, y), z)


Rules:


f(f(a, b), x) -> f(b, f(a, f(c, f(b, f(a, x)))))
f(x, f(y, z)) -> f(f(x, y), z)


Strategy:

innermost




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

F(f(a, b), x) -> F(a, f(c, f(b, f(a, x))))
three new Dependency Pairs are created:

F(f(a, b), x'') -> F(a, f(f(c, b), f(a, x'')))
F(f(a, b), x'') -> F(a, f(c, f(f(b, a), x'')))
F(f(a, b), f(y', z')) -> F(a, f(c, f(b, f(f(a, y'), z'))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Neg POLO
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 3
                 ↳Semantic Labelling


Dependency Pairs:

F(f(a, b), f(y', z')) -> F(a, f(c, f(b, f(f(a, y'), z'))))
F(f(a, b), x'') -> F(a, f(c, f(f(b, a), x'')))
F(x, f(y, z)) -> F(x, y)
F(f(a, b), x'') -> F(a, f(f(c, b), f(a, x'')))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(a, b), x) -> F(a, x)


Rules:


f(f(a, b), x) -> f(b, f(a, f(c, f(b, f(a, x)))))
f(x, f(y, z)) -> f(f(x, y), z)


Strategy:

innermost




Using Semantic Labelling, the DP problem could be transformed. The following model was found:
F(x0, x1)=  1
f(x0, x1)=  x1
a=  1
b=  0
c=  0

From the dependency graph we obtain 2 (labeled) SCCs which each result in correspondingDP problem.


   R
     ↳DPs
       →DP Problem 1
         ↳Neg POLO
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 4
                 ↳Unlabel


Dependency Pairs:

F01(f10(a, b), x) -> F11(a, x)
F01(f10(a, b), x'') -> F11(a, f01(f00(c, b), f11(a, x'')))
F01(f10(a, b), x'') -> F11(a, f01(c, f11(f01(b, a), x'')))
F11(x, f01(y, z)) -> F01(f10(x, y), z)
F11(x, f11(y, z)) -> F11(x, y)
F00(f10(a, b), x) -> F10(a, x)
F00(f10(a, b), x'') -> F10(a, f00(f00(c, b), f10(a, x'')))
F00(f10(a, b), x'') -> F10(a, f00(c, f10(f01(b, a), x'')))
F10(x, f00(y, z)) -> F00(f10(x, y), z)
F11(x, f01(y, z)) -> F10(x, y)
F10(x, f10(y, z)) -> F11(x, y)
F10(x, f00(y, z)) -> F10(x, y)


Rules:


f00(f10(a, b), x) -> f00(b, f10(a, f00(c, f00(b, f10(a, x)))))
f00(x, f00(y, z)) -> f00(f00(x, y), z)
f00(x, f10(y, z)) -> f10(f01(x, y), z)
f10(x, f00(y, z)) -> f00(f10(x, y), z)
f10(x, f10(y, z)) -> f10(f11(x, y), z)
f01(f10(a, b), x) -> f01(b, f11(a, f01(c, f01(b, f11(a, x)))))
f01(x, f01(y, z)) -> f01(f00(x, y), z)
f01(x, f11(y, z)) -> f11(f01(x, y), z)
f11(x, f01(y, z)) -> f01(f10(x, y), z)
f11(x, f11(y, z)) -> f11(f11(x, y), z)


Strategy:

innermost




Removed all semantic labels.

   R
     ↳DPs
       →DP Problem 1
         ↳Neg POLO
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 6
                 ↳Narrowing Transformation


Dependency Pairs:

F(f(a, b), x'') -> F(a, f(c, f(f(b, a), x'')))
F(f(a, b), x'') -> F(a, f(f(c, b), f(a, x'')))
F(x, f(y, z)) -> F(f(x, y), z)
F(f(a, b), x) -> F(a, x)
F(x, f(y, z)) -> F(x, y)


Rules:


f(f(a, b), x) -> f(b, f(a, f(c, f(b, f(a, x)))))
f(x, f(y, z)) -> f(f(x, y), z)


Strategy:

innermost




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

F(f(a, b), x'') -> F(a, f(c, f(f(b, a), x'')))
two new Dependency Pairs are created:

F(f(a, b), x''') -> F(a, f(f(c, f(b, a)), x'''))
F(f(a, b), f(y', z')) -> F(a, f(c, f(f(f(b, a), y'), z')))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Neg POLO
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 7
                 ↳Narrowing Transformation


Dependency Pairs:

F(f(a, b), f(y', z')) -> F(a, f(c, f(f(f(b, a), y'), z')))
F(f(a, b), x''') -> F(a, f(f(c, f(b, a)), x'''))
F(x, f(y, z)) -> F(x, y)
F(f(a, b), x) -> F(a, x)
F(x, f(y, z)) -> F(f(x, y), z)
F(f(a, b), x'') -> F(a, f(f(c, b), f(a, x'')))


Rules:


f(f(a, b), x) -> f(b, f(a, f(c, f(b, f(a, x)))))
f(x, f(y, z)) -> f(f(x, y), z)


Strategy:

innermost




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

F(f(a, b), x'') -> F(a, f(f(c, b), f(a, x'')))
two new Dependency Pairs are created:

F(f(a, b), x''') -> F(a, f(f(f(c, b), a), x'''))
F(f(a, b), f(y', z')) -> F(a, f(f(c, b), f(f(a, y'), z')))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Neg POLO
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 8
                 ↳Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

F(f(a, b), f(y', z')) -> F(a, f(f(c, b), f(f(a, y'), z')))
F(f(a, b), x''') -> F(a, f(f(f(c, b), a), x'''))
F(f(a, b), x''') -> F(a, f(f(c, f(b, a)), x'''))
F(x, f(y, z)) -> F(x, y)
F(f(a, b), x) -> F(a, x)
F(x, f(y, z)) -> F(f(x, y), z)
F(f(a, b), f(y', z')) -> F(a, f(c, f(f(f(b, a), y'), z')))


Rules:


f(f(a, b), x) -> f(b, f(a, f(c, f(b, f(a, x)))))
f(x, f(y, z)) -> f(f(x, y), z)


Strategy:

innermost




   R
     ↳DPs
       →DP Problem 1
         ↳Neg POLO
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 5
                 ↳Modular Removal of Rules


Dependency Pairs:

F01(x, f11(y, z)) -> F01(x, y)
F01(x, f01(y, z)) -> F00(x, y)
F00(x, f10(y, z)) -> F01(x, y)
F00(x, f00(y, z)) -> F00(x, y)


Rules:


f00(f10(a, b), x) -> f00(b, f10(a, f00(c, f00(b, f10(a, x)))))
f00(x, f00(y, z)) -> f00(f00(x, y), z)
f00(x, f10(y, z)) -> f10(f01(x, y), z)
f10(x, f00(y, z)) -> f00(f10(x, y), z)
f10(x, f10(y, z)) -> f10(f11(x, y), z)
f01(f10(a, b), x) -> f01(b, f11(a, f01(c, f01(b, f11(a, x)))))
f01(x, f01(y, z)) -> f01(f00(x, y), z)
f01(x, f11(y, z)) -> f11(f01(x, y), z)
f11(x, f01(y, z)) -> f01(f10(x, y), z)
f11(x, f11(y, z)) -> f11(f11(x, y), z)


Strategy:

innermost




We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(f_11(x1, x2))=  x1 + x2  
  POL(F_00(x1, x2))=  x1 + x2  
  POL(f_00(x1, x2))=  x1 + x2  
  POL(f_10(x1, x2))=  x1 + x2  
  POL(F_01(x1, x2))=  x1 + x2  
  POL(f_01(x1, x2))=  x1 + x2  

We have the following set D of usable symbols: {F00, F01}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

F01(x, f11(y, z)) -> F01(x, y)
F01(x, f01(y, z)) -> F00(x, y)
F00(x, f10(y, z)) -> F01(x, y)
F00(x, f00(y, z)) -> F00(x, y)

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.


The Proof could not be continued due to a Timeout.
Innermost Termination of R could not be shown.
Duration:
1:00 minutes