f(

g(b) -> c

b -> c

R

↳Removing Redundant Rules for Innermost Termination

Removing the following rules from

g(b) -> c

R

↳RRRI

→TRS2

↳Dependency Pair Analysis

F(X, g(X),Y) -> F(Y,Y,Y)

Furthermore,

R

↳RRRI

→TRS2

↳DPs

→DP Problem 1

↳Non-Overlappingness Check

**F( X, g(X), Y) -> F(Y, Y, Y)**

f(X, g(X),Y) -> f(Y,Y,Y)

b -> c

R does not overlap into P. Moreover, R is locally confluent (all critical pairs are trivially joinable).Hence we can switch to innermost.

The transformation is resulting in one subcycle:

R

↳RRRI

→TRS2

↳DPs

→DP Problem 1

↳NOC

...

→DP Problem 2

↳Dependency Graph

**F( X, g(X), Y) -> F(Y, Y, Y)**

f(X, g(X),Y) -> f(Y,Y,Y)

b -> c

innermost

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:00 minutes