f(0, 1,

f(

0 -> 2

1 -> 2

R

↳Removing Redundant Rules for Innermost Termination

Removing the following rules from

f(0, 1,x) -> f(x,x,x)

R

↳RRRI

→TRS2

↳Removing Redundant Rules

Removing the following rules from

f(x,y,z) -> 2

where the Polynomial interpretation:

was used.

_{ }^{ }POL(0)= 0 _{ }^{ }_{ }^{ }POL(1)= 0 _{ }^{ }_{ }^{ }POL(2)= 0 _{ }^{ }_{ }^{ }POL(f(x)_{1}, x_{2}, x_{3})= 1 + x _{1}+ x_{2}+ x_{3}_{ }^{ }

Not all Rules of

R

↳RRRI

→TRS2

↳RRRPolo

→TRS3

↳Removing Redundant Rules

Removing the following rules from

1 -> 2

where the Polynomial interpretation:

was used.

_{ }^{ }POL(0)= 0 _{ }^{ }_{ }^{ }POL(1)= 1 _{ }^{ }_{ }^{ }POL(2)= 0 _{ }^{ }

Not all Rules of

R

↳RRRI

→TRS2

↳RRRPolo

→TRS3

↳RRRPolo

...

→TRS4

↳Removing Redundant Rules

Removing the following rules from

0 -> 2

where the Polynomial interpretation:

was used.

_{ }^{ }POL(0)= 1 _{ }^{ }_{ }^{ }POL(2)= 0 _{ }^{ }

All Rules of

R

↳RRRI

→TRS2

↳RRRPolo

→TRS3

↳RRRPolo

...

→TRS5

↳Dependency Pair Analysis

Duration:

0:00 minutes