Term Rewriting System R:
[]
f(g(i(a, b, b'), c), d) -> if(e, f(.(b, c), d'), f(.(b', c), d'))
f(g(h(a, b), c), d) -> if(e, f(.(b, g(h(a, b), c)), d), f(c, d'))

Termination of R to be shown. 



   R
     ↳Removing Redundant Rules



Removing the following rules from R which fullfill a polynomial ordering:

f(g(i(a, b, b'), c), d) -> if(e, f(.(b, c), d'), f(.(b', c), d'))

where the Polynomial interpretation:
  POL(d')=  0  
  POL(i(x1, x2, x3))=  x1 + x2 + x3  
  POL(e)=  0  
  POL(.(x1, x2))=  x1 + x2  
  POL(f(x1, x2))=  x1 + x2  
  POL(c)=  0  
  POL(if(x1, x2, x3))=  x1 + x2 + x3  
  POL(g(x1, x2))=  1 + x1 + x2  
  POL(b)=  0  
  POL(d)=  0  
  POL(h(x1, x2))=  x1 + x2  
  POL(a)=  0  
  POL(b')=  0  
was used.

Not all Rules of R can be deleted, so we still have to regard a part of R. 


   R
     ↳RRRPolo
       →TRS2
         ↳Overlay and local confluence Check



The TRS is overlay and locally confluent (all critical pairs are trivially joinable).Hence, we can switch to innermost. 


   R
     ↳RRRPolo
       →TRS2
         ↳OC
           →TRS3
             ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

F(g(h(a, b), c), d) -> F(.(b, g(h(a, b), c)), d)
F(g(h(a, b), c), d) -> F(c, d')

R contains no SCCs.

Termination of R successfully shown.
Duration:
0:05 minutes