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'))

R

↳Removing Redundant Rules

Removing the following rules from

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

where the Polynomial interpretation:

was used.

_{ }^{ }POL(d')= 0 _{ }^{ }_{ }^{ }POL(i(x)_{1}, x_{2}, x_{3})= x _{1}+ x_{2}+ x_{3}_{ }^{ }_{ }^{ }POL(e)= 0 _{ }^{ }_{ }^{ }POL(.(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(f(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(c)= 0 _{ }^{ }_{ }^{ }POL(if(x)_{1}, x_{2}, x_{3})= x _{1}+ x_{2}+ x_{3}_{ }^{ }_{ }^{ }POL(g(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(b)= 0 _{ }^{ }_{ }^{ }POL(d)= 0 _{ }^{ }_{ }^{ }POL(h(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(a)= 0 _{ }^{ }_{ }^{ }POL(b')= 0 _{ }^{ }

Not all Rules of

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

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')

Duration:

0:05 minutes