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