f(0, 1,

f(g(

f(

f(

R

↳Dependency Pair Analysis

F(0, 1,x) -> F(g(x), g(x),x)

F(g(x),y,z) -> F(x,y,z)

F(x, g(y),z) -> F(x,y,z)

F(x,y, g(z)) -> F(x,y,z)

Furthermore,

R

↳DPs

→DP Problem 1

↳Negative Polynomial Order

**F( x, y, g(z)) -> F(x, y, z)**

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

f(g(x),y,z) -> g(f(x,y,z))

f(x, g(y),z) -> g(f(x,y,z))

f(x,y, g(z)) -> g(f(x,y,z))

The following Dependency Pair can be strictly oriented using the given order.

F(x,y, g(z)) -> F(x,y,z)

There are no usable rules (regarding the implicit AFS).

Used ordering:

Polynomial Order with Interpretation:

**POL( **F(x_{1}, ..., x_{3})** )** = x_{3}

**POL( **g(x_{1})** )** = x_{1} + 1

This results in one new DP problem.

R

↳DPs

→DP Problem 1

↳Neg POLO

→DP Problem 2

↳Semantic Labelling

**F( x, g(y), z) -> F(x, y, z)**

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

f(g(x),y,z) -> g(f(x,y,z))

f(x, g(y),z) -> g(f(x,y,z))

f(x,y, g(z)) -> g(f(x,y,z))

Using Semantic Labelling, the DP problem could be transformed. The following model was found:

f(x_{0}, x_{1}, x_{2})= 1 g(x_{0})= x _{0}F(x_{0}, x_{1}, x_{2})= 1 + x _{2}0= 0 1= 1

From the dependency graph we obtain 8 (labeled) SCCs which each result in correspondingDP problem.

R

↳DPs

→DP Problem 1

↳Neg POLO

→DP Problem 2

↳SemLab

...

→DP Problem 3

↳Modular Removal of Rules

**F _{111}(g_{1}(x), y, z) -> F_{111}(x, y, z)**

f_{010}(0, 1,x) -> f_{000}(g_{0}(x), g_{0}(x),x)

f_{010}(g_{0}(x),y,z) -> g_{1}(f_{010}(x,y,z))

f_{010}(x, g_{1}(y),z) -> g_{1}(f_{010}(x,y,z))

f_{010}(x,y, g_{0}(z)) -> g_{1}(f_{010}(x,y,z))

f_{000}(g_{0}(x),y,z) -> g_{1}(f_{000}(x,y,z))

f_{000}(x, g_{0}(y),z) -> g_{1}(f_{000}(x,y,z))

f_{000}(x,y, g_{0}(z)) -> g_{1}(f_{000}(x,y,z))

f_{011}(0, 1,x) -> f_{111}(g_{1}(x), g_{1}(x),x)

f_{011}(g_{0}(x),y,z) -> g_{1}(f_{011}(x,y,z))

f_{011}(x, g_{1}(y),z) -> g_{1}(f_{011}(x,y,z))

f_{011}(x,y, g_{1}(z)) -> g_{1}(f_{011}(x,y,z))

f_{111}(g_{1}(x),y,z) -> g_{1}(f_{111}(x,y,z))

f_{111}(x, g_{1}(y),z) -> g_{1}(f_{111}(x,y,z))

f_{111}(x,y, g_{1}(z)) -> g_{1}(f_{111}(x,y,z))

f_{001}(g_{0}(x),y,z) -> g_{1}(f_{001}(x,y,z))

f_{001}(x, g_{0}(y),z) -> g_{1}(f_{001}(x,y,z))

f_{001}(x,y, g_{1}(z)) -> g_{1}(f_{001}(x,y,z))

f_{100}(g_{1}(x),y,z) -> g_{1}(f_{100}(x,y,z))

f_{100}(x, g_{0}(y),z) -> g_{1}(f_{100}(x,y,z))

f_{100}(x,y, g_{0}(z)) -> g_{1}(f_{100}(x,y,z))

f_{101}(g_{1}(x),y,z) -> g_{1}(f_{101}(x,y,z))

f_{101}(x, g_{0}(y),z) -> g_{1}(f_{101}(x,y,z))

f_{101}(x,y, g_{1}(z)) -> g_{1}(f_{101}(x,y,z))

f_{110}(g_{1}(x),y,z) -> g_{1}(f_{110}(x,y,z))

f_{110}(x, g_{1}(y),z) -> g_{1}(f_{110}(x,y,z))

f_{110}(x,y, g_{0}(z)) -> g_{1}(f_{110}(x,y,z))

We have the following set of usable rules: none

To remove rules and DPs from this DP problem we used the following monotonic and C

Polynomial interpretation:

_{ }^{ }POL(F_111(x)_{1}, x_{2}, x_{3})= x _{1}+ x_{2}+ x_{3}_{ }^{ }_{ }^{ }POL(g_1(x)_{1})= x _{1}_{ }^{ }

We have the following set D of usable symbols: {F

The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

F_{111}(g_{1}(x),y,z) -> F_{111}(x,y,z)

F_{111}(x, g_{1}(y),z) -> F_{111}(x,y,z)

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.

R

↳DPs

→DP Problem 1

↳Neg POLO

→DP Problem 2

↳SemLab

...

→DP Problem 4

↳Modular Removal of Rules

**F _{100}(g_{1}(x), y, z) -> F_{100}(x, y, z)**

f_{010}(0, 1,x) -> f_{000}(g_{0}(x), g_{0}(x),x)

f_{010}(g_{0}(x),y,z) -> g_{1}(f_{010}(x,y,z))

f_{010}(x, g_{1}(y),z) -> g_{1}(f_{010}(x,y,z))

f_{010}(x,y, g_{0}(z)) -> g_{1}(f_{010}(x,y,z))

f_{000}(g_{0}(x),y,z) -> g_{1}(f_{000}(x,y,z))

f_{000}(x, g_{0}(y),z) -> g_{1}(f_{000}(x,y,z))

f_{000}(x,y, g_{0}(z)) -> g_{1}(f_{000}(x,y,z))

f_{011}(0, 1,x) -> f_{111}(g_{1}(x), g_{1}(x),x)

f_{011}(g_{0}(x),y,z) -> g_{1}(f_{011}(x,y,z))

f_{011}(x, g_{1}(y),z) -> g_{1}(f_{011}(x,y,z))

f_{011}(x,y, g_{1}(z)) -> g_{1}(f_{011}(x,y,z))

f_{111}(g_{1}(x),y,z) -> g_{1}(f_{111}(x,y,z))

f_{111}(x, g_{1}(y),z) -> g_{1}(f_{111}(x,y,z))

f_{111}(x,y, g_{1}(z)) -> g_{1}(f_{111}(x,y,z))

f_{001}(g_{0}(x),y,z) -> g_{1}(f_{001}(x,y,z))

f_{001}(x, g_{0}(y),z) -> g_{1}(f_{001}(x,y,z))

f_{001}(x,y, g_{1}(z)) -> g_{1}(f_{001}(x,y,z))

f_{100}(g_{1}(x),y,z) -> g_{1}(f_{100}(x,y,z))

f_{100}(x, g_{0}(y),z) -> g_{1}(f_{100}(x,y,z))

f_{100}(x,y, g_{0}(z)) -> g_{1}(f_{100}(x,y,z))

f_{101}(g_{1}(x),y,z) -> g_{1}(f_{101}(x,y,z))

f_{101}(x, g_{0}(y),z) -> g_{1}(f_{101}(x,y,z))

f_{101}(x,y, g_{1}(z)) -> g_{1}(f_{101}(x,y,z))

f_{110}(g_{1}(x),y,z) -> g_{1}(f_{110}(x,y,z))

f_{110}(x, g_{1}(y),z) -> g_{1}(f_{110}(x,y,z))

f_{110}(x,y, g_{0}(z)) -> g_{1}(f_{110}(x,y,z))

We have the following set of usable rules: none

To remove rules and DPs from this DP problem we used the following monotonic and C

Polynomial interpretation:

_{ }^{ }POL(F_100(x)_{1}, x_{2}, x_{3})= x _{1}+ x_{2}+ x_{3}_{ }^{ }_{ }^{ }POL(g_1(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(g_0(x)_{1})= x _{1}_{ }^{ }

We have the following set D of usable symbols: {F

The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

F_{100}(g_{1}(x),y,z) -> F_{100}(x,y,z)

F_{100}(x, g_{0}(y),z) -> F_{100}(x,y,z)

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.

R

↳DPs

→DP Problem 1

↳Neg POLO

→DP Problem 2

↳SemLab

...

→DP Problem 5

↳Modular Removal of Rules

**F _{011}(g_{0}(x), y, z) -> F_{011}(x, y, z)**

f_{010}(0, 1,x) -> f_{000}(g_{0}(x), g_{0}(x),x)

f_{010}(g_{0}(x),y,z) -> g_{1}(f_{010}(x,y,z))

f_{010}(x, g_{1}(y),z) -> g_{1}(f_{010}(x,y,z))

f_{010}(x,y, g_{0}(z)) -> g_{1}(f_{010}(x,y,z))

f_{000}(g_{0}(x),y,z) -> g_{1}(f_{000}(x,y,z))

f_{000}(x, g_{0}(y),z) -> g_{1}(f_{000}(x,y,z))

f_{000}(x,y, g_{0}(z)) -> g_{1}(f_{000}(x,y,z))

f_{011}(0, 1,x) -> f_{111}(g_{1}(x), g_{1}(x),x)

f_{011}(g_{0}(x),y,z) -> g_{1}(f_{011}(x,y,z))

f_{011}(x, g_{1}(y),z) -> g_{1}(f_{011}(x,y,z))

f_{011}(x,y, g_{1}(z)) -> g_{1}(f_{011}(x,y,z))

f_{111}(g_{1}(x),y,z) -> g_{1}(f_{111}(x,y,z))

f_{111}(x, g_{1}(y),z) -> g_{1}(f_{111}(x,y,z))

f_{111}(x,y, g_{1}(z)) -> g_{1}(f_{111}(x,y,z))

f_{001}(g_{0}(x),y,z) -> g_{1}(f_{001}(x,y,z))

f_{001}(x, g_{0}(y),z) -> g_{1}(f_{001}(x,y,z))

f_{001}(x,y, g_{1}(z)) -> g_{1}(f_{001}(x,y,z))

f_{100}(g_{1}(x),y,z) -> g_{1}(f_{100}(x,y,z))

f_{100}(x, g_{0}(y),z) -> g_{1}(f_{100}(x,y,z))

f_{100}(x,y, g_{0}(z)) -> g_{1}(f_{100}(x,y,z))

f_{101}(g_{1}(x),y,z) -> g_{1}(f_{101}(x,y,z))

f_{101}(x, g_{0}(y),z) -> g_{1}(f_{101}(x,y,z))

f_{101}(x,y, g_{1}(z)) -> g_{1}(f_{101}(x,y,z))

f_{110}(g_{1}(x),y,z) -> g_{1}(f_{110}(x,y,z))

f_{110}(x, g_{1}(y),z) -> g_{1}(f_{110}(x,y,z))

f_{110}(x,y, g_{0}(z)) -> g_{1}(f_{110}(x,y,z))

We have the following set of usable rules: none

To remove rules and DPs from this DP problem we used the following monotonic and C

Polynomial interpretation:

_{ }^{ }POL(g_1(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(F_011(x)_{1}, x_{2}, x_{3})= x _{1}+ x_{2}+ x_{3}_{ }^{ }_{ }^{ }POL(g_0(x)_{1})= x _{1}_{ }^{ }

We have the following set D of usable symbols: {F

The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

F_{011}(g_{0}(x),y,z) -> F_{011}(x,y,z)

F_{011}(x, g_{1}(y),z) -> F_{011}(x,y,z)

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.

R

↳DPs

→DP Problem 1

↳Neg POLO

→DP Problem 2

↳SemLab

...

→DP Problem 6

↳Modular Removal of Rules

**F _{110}(g_{1}(x), y, z) -> F_{110}(x, y, z)**

f_{010}(0, 1,x) -> f_{000}(g_{0}(x), g_{0}(x),x)

f_{010}(g_{0}(x),y,z) -> g_{1}(f_{010}(x,y,z))

f_{010}(x, g_{1}(y),z) -> g_{1}(f_{010}(x,y,z))

f_{010}(x,y, g_{0}(z)) -> g_{1}(f_{010}(x,y,z))

f_{000}(g_{0}(x),y,z) -> g_{1}(f_{000}(x,y,z))

f_{000}(x, g_{0}(y),z) -> g_{1}(f_{000}(x,y,z))

f_{000}(x,y, g_{0}(z)) -> g_{1}(f_{000}(x,y,z))

f_{011}(0, 1,x) -> f_{111}(g_{1}(x), g_{1}(x),x)

f_{011}(g_{0}(x),y,z) -> g_{1}(f_{011}(x,y,z))

f_{011}(x, g_{1}(y),z) -> g_{1}(f_{011}(x,y,z))

f_{011}(x,y, g_{1}(z)) -> g_{1}(f_{011}(x,y,z))

f_{111}(g_{1}(x),y,z) -> g_{1}(f_{111}(x,y,z))

f_{111}(x, g_{1}(y),z) -> g_{1}(f_{111}(x,y,z))

f_{111}(x,y, g_{1}(z)) -> g_{1}(f_{111}(x,y,z))

f_{001}(g_{0}(x),y,z) -> g_{1}(f_{001}(x,y,z))

f_{001}(x, g_{0}(y),z) -> g_{1}(f_{001}(x,y,z))

f_{001}(x,y, g_{1}(z)) -> g_{1}(f_{001}(x,y,z))

f_{100}(g_{1}(x),y,z) -> g_{1}(f_{100}(x,y,z))

f_{100}(x, g_{0}(y),z) -> g_{1}(f_{100}(x,y,z))

f_{100}(x,y, g_{0}(z)) -> g_{1}(f_{100}(x,y,z))

f_{101}(g_{1}(x),y,z) -> g_{1}(f_{101}(x,y,z))

f_{101}(x, g_{0}(y),z) -> g_{1}(f_{101}(x,y,z))

f_{101}(x,y, g_{1}(z)) -> g_{1}(f_{101}(x,y,z))

f_{110}(g_{1}(x),y,z) -> g_{1}(f_{110}(x,y,z))

f_{110}(x, g_{1}(y),z) -> g_{1}(f_{110}(x,y,z))

f_{110}(x,y, g_{0}(z)) -> g_{1}(f_{110}(x,y,z))

We have the following set of usable rules: none

To remove rules and DPs from this DP problem we used the following monotonic and C

Polynomial interpretation:

_{ }^{ }POL(g_1(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(F_110(x)_{1}, x_{2}, x_{3})= x _{1}+ x_{2}+ x_{3}_{ }^{ }

We have the following set D of usable symbols: {F

The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

F_{110}(g_{1}(x),y,z) -> F_{110}(x,y,z)

F_{110}(x, g_{1}(y),z) -> F_{110}(x,y,z)

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.

R

↳DPs

→DP Problem 1

↳Neg POLO

→DP Problem 2

↳SemLab

...

→DP Problem 7

↳Modular Removal of Rules

**F _{001}(g_{0}(x), y, z) -> F_{001}(x, y, z)**

f_{010}(0, 1,x) -> f_{000}(g_{0}(x), g_{0}(x),x)

f_{010}(g_{0}(x),y,z) -> g_{1}(f_{010}(x,y,z))

f_{010}(x, g_{1}(y),z) -> g_{1}(f_{010}(x,y,z))

f_{010}(x,y, g_{0}(z)) -> g_{1}(f_{010}(x,y,z))

f_{000}(g_{0}(x),y,z) -> g_{1}(f_{000}(x,y,z))

f_{000}(x, g_{0}(y),z) -> g_{1}(f_{000}(x,y,z))

f_{000}(x,y, g_{0}(z)) -> g_{1}(f_{000}(x,y,z))

f_{011}(0, 1,x) -> f_{111}(g_{1}(x), g_{1}(x),x)

f_{011}(g_{0}(x),y,z) -> g_{1}(f_{011}(x,y,z))

f_{011}(x, g_{1}(y),z) -> g_{1}(f_{011}(x,y,z))

f_{011}(x,y, g_{1}(z)) -> g_{1}(f_{011}(x,y,z))

f_{111}(g_{1}(x),y,z) -> g_{1}(f_{111}(x,y,z))

f_{111}(x, g_{1}(y),z) -> g_{1}(f_{111}(x,y,z))

f_{111}(x,y, g_{1}(z)) -> g_{1}(f_{111}(x,y,z))

f_{001}(g_{0}(x),y,z) -> g_{1}(f_{001}(x,y,z))

f_{001}(x, g_{0}(y),z) -> g_{1}(f_{001}(x,y,z))

f_{001}(x,y, g_{1}(z)) -> g_{1}(f_{001}(x,y,z))

f_{100}(g_{1}(x),y,z) -> g_{1}(f_{100}(x,y,z))

f_{100}(x, g_{0}(y),z) -> g_{1}(f_{100}(x,y,z))

f_{100}(x,y, g_{0}(z)) -> g_{1}(f_{100}(x,y,z))

f_{101}(g_{1}(x),y,z) -> g_{1}(f_{101}(x,y,z))

f_{101}(x, g_{0}(y),z) -> g_{1}(f_{101}(x,y,z))

f_{101}(x,y, g_{1}(z)) -> g_{1}(f_{101}(x,y,z))

f_{110}(g_{1}(x),y,z) -> g_{1}(f_{110}(x,y,z))

f_{110}(x, g_{1}(y),z) -> g_{1}(f_{110}(x,y,z))

f_{110}(x,y, g_{0}(z)) -> g_{1}(f_{110}(x,y,z))

We have the following set of usable rules: none

To remove rules and DPs from this DP problem we used the following monotonic and C

Polynomial interpretation:

_{ }^{ }POL(F_001(x)_{1}, x_{2}, x_{3})= x _{1}+ x_{2}+ x_{3}_{ }^{ }_{ }^{ }POL(g_0(x)_{1})= x _{1}_{ }^{ }

We have the following set D of usable symbols: {F

The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

F_{001}(g_{0}(x),y,z) -> F_{001}(x,y,z)

F_{001}(x, g_{0}(y),z) -> F_{001}(x,y,z)

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.

R

↳DPs

→DP Problem 1

↳Neg POLO

→DP Problem 2

↳SemLab

...

→DP Problem 8

↳Modular Removal of Rules

**F _{000}(g_{0}(x), y, z) -> F_{000}(x, y, z)**

f_{010}(0, 1,x) -> f_{000}(g_{0}(x), g_{0}(x),x)

f_{010}(g_{0}(x),y,z) -> g_{1}(f_{010}(x,y,z))

f_{010}(x, g_{1}(y),z) -> g_{1}(f_{010}(x,y,z))

f_{010}(x,y, g_{0}(z)) -> g_{1}(f_{010}(x,y,z))

f_{000}(g_{0}(x),y,z) -> g_{1}(f_{000}(x,y,z))

f_{000}(x, g_{0}(y),z) -> g_{1}(f_{000}(x,y,z))

f_{000}(x,y, g_{0}(z)) -> g_{1}(f_{000}(x,y,z))

f_{011}(0, 1,x) -> f_{111}(g_{1}(x), g_{1}(x),x)

f_{011}(g_{0}(x),y,z) -> g_{1}(f_{011}(x,y,z))

f_{011}(x, g_{1}(y),z) -> g_{1}(f_{011}(x,y,z))

f_{011}(x,y, g_{1}(z)) -> g_{1}(f_{011}(x,y,z))

f_{111}(g_{1}(x),y,z) -> g_{1}(f_{111}(x,y,z))

f_{111}(x, g_{1}(y),z) -> g_{1}(f_{111}(x,y,z))

f_{111}(x,y, g_{1}(z)) -> g_{1}(f_{111}(x,y,z))

f_{001}(g_{0}(x),y,z) -> g_{1}(f_{001}(x,y,z))

f_{001}(x, g_{0}(y),z) -> g_{1}(f_{001}(x,y,z))

f_{001}(x,y, g_{1}(z)) -> g_{1}(f_{001}(x,y,z))

f_{100}(g_{1}(x),y,z) -> g_{1}(f_{100}(x,y,z))

f_{100}(x, g_{0}(y),z) -> g_{1}(f_{100}(x,y,z))

f_{100}(x,y, g_{0}(z)) -> g_{1}(f_{100}(x,y,z))

f_{101}(g_{1}(x),y,z) -> g_{1}(f_{101}(x,y,z))

f_{101}(x, g_{0}(y),z) -> g_{1}(f_{101}(x,y,z))

f_{101}(x,y, g_{1}(z)) -> g_{1}(f_{101}(x,y,z))

f_{110}(g_{1}(x),y,z) -> g_{1}(f_{110}(x,y,z))

f_{110}(x, g_{1}(y),z) -> g_{1}(f_{110}(x,y,z))

f_{110}(x,y, g_{0}(z)) -> g_{1}(f_{110}(x,y,z))

We have the following set of usable rules: none

To remove rules and DPs from this DP problem we used the following monotonic and C

Polynomial interpretation:

_{ }^{ }POL(F_000(x)_{1}, x_{2}, x_{3})= x _{1}+ x_{2}+ x_{3}_{ }^{ }_{ }^{ }POL(g_0(x)_{1})= x _{1}_{ }^{ }

We have the following set D of usable symbols: {F

The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

F_{000}(g_{0}(x),y,z) -> F_{000}(x,y,z)

F_{000}(x, g_{0}(y),z) -> F_{000}(x,y,z)

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.

R

↳DPs

→DP Problem 1

↳Neg POLO

→DP Problem 2

↳SemLab

...

→DP Problem 9

↳Modular Removal of Rules

**F _{101}(g_{1}(x), y, z) -> F_{101}(x, y, z)**

f_{010}(0, 1,x) -> f_{000}(g_{0}(x), g_{0}(x),x)

f_{010}(g_{0}(x),y,z) -> g_{1}(f_{010}(x,y,z))

f_{010}(x, g_{1}(y),z) -> g_{1}(f_{010}(x,y,z))

f_{010}(x,y, g_{0}(z)) -> g_{1}(f_{010}(x,y,z))

f_{000}(g_{0}(x),y,z) -> g_{1}(f_{000}(x,y,z))

f_{000}(x, g_{0}(y),z) -> g_{1}(f_{000}(x,y,z))

f_{000}(x,y, g_{0}(z)) -> g_{1}(f_{000}(x,y,z))

f_{011}(0, 1,x) -> f_{111}(g_{1}(x), g_{1}(x),x)

f_{011}(g_{0}(x),y,z) -> g_{1}(f_{011}(x,y,z))

f_{011}(x, g_{1}(y),z) -> g_{1}(f_{011}(x,y,z))

f_{011}(x,y, g_{1}(z)) -> g_{1}(f_{011}(x,y,z))

f_{111}(g_{1}(x),y,z) -> g_{1}(f_{111}(x,y,z))

f_{111}(x, g_{1}(y),z) -> g_{1}(f_{111}(x,y,z))

f_{111}(x,y, g_{1}(z)) -> g_{1}(f_{111}(x,y,z))

f_{001}(g_{0}(x),y,z) -> g_{1}(f_{001}(x,y,z))

f_{001}(x, g_{0}(y),z) -> g_{1}(f_{001}(x,y,z))

f_{001}(x,y, g_{1}(z)) -> g_{1}(f_{001}(x,y,z))

f_{100}(g_{1}(x),y,z) -> g_{1}(f_{100}(x,y,z))

f_{100}(x, g_{0}(y),z) -> g_{1}(f_{100}(x,y,z))

f_{100}(x,y, g_{0}(z)) -> g_{1}(f_{100}(x,y,z))

f_{101}(g_{1}(x),y,z) -> g_{1}(f_{101}(x,y,z))

f_{101}(x, g_{0}(y),z) -> g_{1}(f_{101}(x,y,z))

f_{101}(x,y, g_{1}(z)) -> g_{1}(f_{101}(x,y,z))

f_{110}(g_{1}(x),y,z) -> g_{1}(f_{110}(x,y,z))

f_{110}(x, g_{1}(y),z) -> g_{1}(f_{110}(x,y,z))

f_{110}(x,y, g_{0}(z)) -> g_{1}(f_{110}(x,y,z))

We have the following set of usable rules: none

To remove rules and DPs from this DP problem we used the following monotonic and C

Polynomial interpretation:

_{ }^{ }POL(g_1(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(F_101(x)_{1}, x_{2}, x_{3})= x _{1}+ x_{2}+ x_{3}_{ }^{ }_{ }^{ }POL(g_0(x)_{1})= x _{1}_{ }^{ }

We have the following set D of usable symbols: {F

The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

F_{101}(g_{1}(x),y,z) -> F_{101}(x,y,z)

F_{101}(x, g_{0}(y),z) -> F_{101}(x,y,z)

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.

R

↳DPs

→DP Problem 1

↳Neg POLO

→DP Problem 2

↳SemLab

...

→DP Problem 10

↳Modular Removal of Rules

**F _{010}(g_{0}(x), y, z) -> F_{010}(x, y, z)**

f_{010}(0, 1,x) -> f_{000}(g_{0}(x), g_{0}(x),x)

f_{010}(g_{0}(x),y,z) -> g_{1}(f_{010}(x,y,z))

f_{010}(x, g_{1}(y),z) -> g_{1}(f_{010}(x,y,z))

f_{010}(x,y, g_{0}(z)) -> g_{1}(f_{010}(x,y,z))

f_{000}(g_{0}(x),y,z) -> g_{1}(f_{000}(x,y,z))

f_{000}(x, g_{0}(y),z) -> g_{1}(f_{000}(x,y,z))

f_{000}(x,y, g_{0}(z)) -> g_{1}(f_{000}(x,y,z))

f_{011}(0, 1,x) -> f_{111}(g_{1}(x), g_{1}(x),x)

f_{011}(g_{0}(x),y,z) -> g_{1}(f_{011}(x,y,z))

f_{011}(x, g_{1}(y),z) -> g_{1}(f_{011}(x,y,z))

f_{011}(x,y, g_{1}(z)) -> g_{1}(f_{011}(x,y,z))

f_{111}(g_{1}(x),y,z) -> g_{1}(f_{111}(x,y,z))

f_{111}(x, g_{1}(y),z) -> g_{1}(f_{111}(x,y,z))

f_{111}(x,y, g_{1}(z)) -> g_{1}(f_{111}(x,y,z))

f_{001}(g_{0}(x),y,z) -> g_{1}(f_{001}(x,y,z))

f_{001}(x, g_{0}(y),z) -> g_{1}(f_{001}(x,y,z))

f_{001}(x,y, g_{1}(z)) -> g_{1}(f_{001}(x,y,z))

f_{100}(g_{1}(x),y,z) -> g_{1}(f_{100}(x,y,z))

f_{100}(x, g_{0}(y),z) -> g_{1}(f_{100}(x,y,z))

f_{100}(x,y, g_{0}(z)) -> g_{1}(f_{100}(x,y,z))

f_{101}(g_{1}(x),y,z) -> g_{1}(f_{101}(x,y,z))

f_{101}(x, g_{0}(y),z) -> g_{1}(f_{101}(x,y,z))

f_{101}(x,y, g_{1}(z)) -> g_{1}(f_{101}(x,y,z))

f_{110}(g_{1}(x),y,z) -> g_{1}(f_{110}(x,y,z))

f_{110}(x, g_{1}(y),z) -> g_{1}(f_{110}(x,y,z))

f_{110}(x,y, g_{0}(z)) -> g_{1}(f_{110}(x,y,z))

We have the following set of usable rules: none

To remove rules and DPs from this DP problem we used the following monotonic and C

Polynomial interpretation:

_{ }^{ }POL(F_010(x)_{1}, x_{2}, x_{3})= x _{1}+ x_{2}+ x_{3}_{ }^{ }_{ }^{ }POL(g_1(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(g_0(x)_{1})= x _{1}_{ }^{ }

We have the following set D of usable symbols: {F

The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

F_{010}(g_{0}(x),y,z) -> F_{010}(x,y,z)

F_{010}(x, g_{1}(y),z) -> F_{010}(x,y,z)

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.

**Termination** of *R* successfully shown.

Duration:

0:07 minutes