a(a(f(

f(a(

f(b(

R

↳Dependency Pair Analysis

A(a(f(x,y))) -> F(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

A(a(f(x,y))) -> A(b(a(b(a(x)))))

A(a(f(x,y))) -> A(b(a(x)))

A(a(f(x,y))) -> A(x)

A(a(f(x,y))) -> A(b(a(b(a(y)))))

A(a(f(x,y))) -> A(b(a(y)))

A(a(f(x,y))) -> A(y)

F(a(x), a(y)) -> A(f(x,y))

F(a(x), a(y)) -> F(x,y)

F(b(x), b(y)) -> F(x,y)

Furthermore,

R

↳DPs

→DP Problem 1

↳Modular Removal of Rules

**F(b( x), b(y)) -> F(x, y)**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

We have the following set of usable rules:

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

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

Polynomial interpretation:

_{ }^{ }POL(b(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(a(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(F(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(A(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(f(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }

We have the following set D of usable symbols: {b, a, F, A, f}

The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

A(a(f(x,y))) -> A(y)

A(a(f(x,y))) -> A(x)

No Rules can be deleted.

The result of this processor delivers one new DP problem.

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳Narrowing Transformation

**F(b( x), b(y)) -> F(x, y)**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

On this DP problem, a Narrowing SCC transformation can be performed.

As a result of transforming the rule

two new Dependency Pairs are created:

F(a(x), a(y)) -> A(f(x,y))

F(a(a(x'')), a(a(y''))) -> A(a(f(x'',y'')))

F(a(b(x'')), a(b(y''))) -> A(b(f(x'',y'')))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳Nar

...

→DP Problem 3

↳Semantic Labelling

**A(a(f( x, y))) -> F(a(b(a(b(a(x))))), a(b(a(b(a(y))))))**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

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

a(x_{0})= 0 f(x_{0}, x_{1})= x _{1}b(x_{0})= 1 + x _{0}F(x_{0}, x_{1})= 0 A(x_{0})= x _{0}

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

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳Nar

...

→DP Problem 4

↳Modular Removal of Rules

**F _{00}(b_{1}(x), b_{1}(y)) -> F_{11}(x, y)**

a_{0}(a_{0}(f_{00}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(y))))))

a_{0}(a_{1}(f_{01}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(y))))))

a_{0}(a_{0}(f_{10}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(y))))))

a_{0}(a_{1}(f_{11}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(y))))))

f_{00}(a_{0}(x), a_{0}(y)) -> a_{0}(f_{00}(x,y))

f_{00}(a_{0}(x), a_{1}(y)) -> a_{1}(f_{01}(x,y))

f_{00}(a_{1}(x), a_{0}(y)) -> a_{0}(f_{10}(x,y))

f_{00}(a_{1}(x), a_{1}(y)) -> a_{1}(f_{11}(x,y))

f_{00}(b_{1}(x), b_{1}(y)) -> b_{1}(f_{11}(x,y))

f_{01}(b_{1}(x), b_{0}(y)) -> b_{0}(f_{10}(x,y))

f_{10}(b_{0}(x), b_{1}(y)) -> b_{1}(f_{01}(x,y))

f_{11}(b_{0}(x), b_{0}(y)) -> b_{0}(f_{00}(x,y))

We have the following set of usable rules:

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

a_{0}(a_{0}(f_{00}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(y))))))

a_{0}(a_{1}(f_{01}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(y))))))

a_{0}(a_{0}(f_{10}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(y))))))

a_{0}(a_{1}(f_{11}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(y))))))

f_{11}(b_{0}(x), b_{0}(y)) -> b_{0}(f_{00}(x,y))

f_{10}(b_{0}(x), b_{1}(y)) -> b_{1}(f_{01}(x,y))

f_{00}(a_{1}(x), a_{1}(y)) -> a_{1}(f_{11}(x,y))

f_{01}(b_{1}(x), b_{0}(y)) -> b_{0}(f_{10}(x,y))

f_{00}(a_{0}(x), a_{0}(y)) -> a_{0}(f_{00}(x,y))

f_{00}(a_{0}(x), a_{1}(y)) -> a_{1}(f_{01}(x,y))

f_{00}(a_{1}(x), a_{0}(y)) -> a_{0}(f_{10}(x,y))

f_{00}(b_{1}(x), b_{1}(y)) -> b_{1}(f_{11}(x,y))

Polynomial interpretation:

_{ }^{ }POL(A_0(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(f_11(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(F_00(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(a_1(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(f_00(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(b_0(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(a_0(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(F_11(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(f_10(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(f_01(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(b_1(x)_{1})= 1 + x _{1}_{ }^{ }

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

The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

F_{00}(b_{1}(x), b_{1}(y)) -> F_{11}(x,y)

The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

f_{01}(b_{1}(x), b_{0}(y)) -> b_{0}(f_{10}(x,y))

f_{00}(b_{1}(x), b_{1}(y)) -> b_{1}(f_{11}(x,y))

The result of this processor delivers one new DP problem.

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳Nar

...

→DP Problem 6

↳Modular Removal of Rules

**F _{00}(a_{0}(a_{1}(x'')), a_{0}(a_{1}(y''))) -> A_{0}(a_{1}(f_{11}(x'', y'')))**

a_{0}(a_{0}(f_{00}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(y))))))

a_{0}(a_{1}(f_{01}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(y))))))

a_{0}(a_{0}(f_{10}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(y))))))

a_{0}(a_{1}(f_{11}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(y))))))

f_{00}(a_{1}(x), a_{1}(y)) -> a_{1}(f_{11}(x,y))

f_{00}(a_{0}(x), a_{0}(y)) -> a_{0}(f_{00}(x,y))

f_{00}(a_{0}(x), a_{1}(y)) -> a_{1}(f_{01}(x,y))

f_{00}(a_{1}(x), a_{0}(y)) -> a_{0}(f_{10}(x,y))

f_{10}(b_{0}(x), b_{1}(y)) -> b_{1}(f_{01}(x,y))

f_{11}(b_{0}(x), b_{0}(y)) -> b_{0}(f_{00}(x,y))

We have the following set of usable rules:

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

a_{0}(a_{0}(f_{00}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(y))))))

a_{0}(a_{1}(f_{01}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(y))))))

a_{0}(a_{0}(f_{10}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(y))))))

a_{0}(a_{1}(f_{11}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(y))))))

f_{11}(b_{0}(x), b_{0}(y)) -> b_{0}(f_{00}(x,y))

f_{10}(b_{0}(x), b_{1}(y)) -> b_{1}(f_{01}(x,y))

f_{00}(a_{1}(x), a_{1}(y)) -> a_{1}(f_{11}(x,y))

f_{00}(a_{0}(x), a_{0}(y)) -> a_{0}(f_{00}(x,y))

f_{00}(a_{0}(x), a_{1}(y)) -> a_{1}(f_{01}(x,y))

f_{00}(a_{1}(x), a_{0}(y)) -> a_{0}(f_{10}(x,y))

Polynomial interpretation:

_{ }^{ }POL(A_0(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(f_11(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(F_00(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(a_1(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(f_00(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(b_0(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(a_0(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(f_10(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(F_11(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(f_01(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(b_1(x)_{1})= x _{1}_{ }^{ }

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

The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

F_{00}(a_{0}(a_{1}(x'')), a_{0}(a_{1}(y''))) -> A_{0}(a_{1}(f_{11}(x'',y'')))

A_{0}(a_{1}(f_{11}(x,y))) -> F_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(y))))))

A_{0}(a_{0}(f_{10}(x,y))) -> F_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(y))))))

F_{00}(a_{0}(a_{1}(x'')), a_{0}(a_{0}(y''))) -> A_{0}(a_{0}(f_{10}(x'',y'')))

F_{00}(a_{0}(a_{0}(x'')), a_{0}(a_{1}(y''))) -> A_{0}(a_{1}(f_{01}(x'',y'')))

F_{00}(a_{0}(a_{0}(x'')), a_{0}(a_{0}(y''))) -> A_{0}(a_{0}(f_{00}(x'',y'')))

F_{00}(a_{0}(x), a_{0}(y)) -> F_{00}(x,y)

The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

a_{0}(a_{0}(f_{10}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(y))))))

a_{0}(a_{1}(f_{11}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(y))))))

f_{00}(a_{0}(x), a_{0}(y)) -> a_{0}(f_{00}(x,y))

f_{00}(a_{0}(x), a_{1}(y)) -> a_{1}(f_{01}(x,y))

The result of this processor delivers one new DP problem.

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳Nar

...

→DP Problem 7

↳Modular Removal of Rules

**F _{11}(b_{0}(x), b_{0}(y)) -> F_{00}(x, y)**

a_{0}(a_{0}(f_{00}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(y))))))

a_{0}(a_{1}(f_{01}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(y))))))

f_{00}(a_{1}(x), a_{1}(y)) -> a_{1}(f_{11}(x,y))

f_{00}(a_{1}(x), a_{0}(y)) -> a_{0}(f_{10}(x,y))

f_{11}(b_{0}(x), b_{0}(y)) -> b_{0}(f_{00}(x,y))

f_{10}(b_{0}(x), b_{1}(y)) -> b_{1}(f_{01}(x,y))

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_00(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(a_1(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(b_0(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(F_11(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }

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_{11}(b_{0}(x), b_{0}(y)) -> F_{00}(x,y)

F_{00}(a_{1}(x), a_{1}(y)) -> F_{11}(x,y)

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

↳MRR

→DP Problem 2

↳Nar

...

→DP Problem 5

↳Modular Removal of Rules

**F _{10}(b_{0}(x), b_{1}(y)) -> F_{01}(x, y)**

a_{0}(a_{0}(f_{00}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(y))))))

a_{0}(a_{1}(f_{01}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(y))))))

a_{0}(a_{0}(f_{10}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{0}(y))))))

a_{0}(a_{1}(f_{11}(x,y))) -> f_{00}(a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(x))))), a_{1}(b_{0}(a_{1}(b_{0}(a_{1}(y))))))

f_{00}(a_{0}(x), a_{0}(y)) -> a_{0}(f_{00}(x,y))

f_{00}(a_{0}(x), a_{1}(y)) -> a_{1}(f_{01}(x,y))

f_{00}(a_{1}(x), a_{0}(y)) -> a_{0}(f_{10}(x,y))

f_{00}(a_{1}(x), a_{1}(y)) -> a_{1}(f_{11}(x,y))

f_{00}(b_{1}(x), b_{1}(y)) -> b_{1}(f_{11}(x,y))

f_{01}(b_{1}(x), b_{0}(y)) -> b_{0}(f_{10}(x,y))

f_{10}(b_{0}(x), b_{1}(y)) -> b_{1}(f_{01}(x,y))

f_{11}(b_{0}(x), b_{0}(y)) -> b_{0}(f_{00}(x,y))

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(b_0(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(F_01(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(F_10(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(b_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_{10}(b_{0}(x), b_{1}(y)) -> F_{01}(x,y)

F_{01}(b_{1}(x), b_{0}(y)) -> F_{10}(x,y)

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:50 minutes