f(f(a, b),

f(f(b, a),

f(

R

↳Dependency Pair Analysis

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

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

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

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

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

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

Furthermore,

R

↳DPs

→DP Problem 1

↳Modular Removal of Rules

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

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

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

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

innermost

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(f(b, a),x) -> f(b, f(b,x))

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

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

Polynomial interpretation:

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

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

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

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

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

F(f(a, b),x) -> F(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

↳Instantiation Transformation

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

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

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

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

innermost

On this DP problem, an Instantiation SCC transformation can be performed.

As a result of transforming the rule

two new Dependency Pairs are created:

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

F(a, f(y',z')) -> F(f(a,y'),z')

F(b, f(y',z')) -> F(f(b,y'),z')

The transformation is resulting in two new DP problems:

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳Inst

...

→DP Problem 3

↳Semantic Labelling

**F(b, f( y', z')) -> F(f(b, y'), z')**

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

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

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

innermost

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

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

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

R

↳DPs

→DP Problem 1

↳MRR

→DP Problem 2

↳Inst

...

→DP Problem 4

↳Semantic Labelling

**F(a, f( y', z')) -> F(f(a, y'), z')**

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

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

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

innermost

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

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

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

Duration:

0:16 minutes