a(f, a(f,

a(

R

↳Dependency Pair Analysis

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

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

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

A(x, g) -> A(f,x)

Furthermore,

R

↳DPs

→DP Problem 1

↳Narrowing Transformation

**A( x, g) -> A(f, x)**

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

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

innermost

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

As a result of transforming the rule

two new Dependency Pairs are created:

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

A(a(f,x''), g) -> A(f, a(g, a(x'', g)))

A(g, g) -> A(f, a(g, a(f, a(g, a(f, f)))))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Usable Rules (Innermost)

**A(f, a(f, x)) -> A(x, g)**

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

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

innermost

As we are in the innermost case, we can delete all 2 non-usable-rules.

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳UsableRules

...

→DP Problem 3

↳Modular Removal of Rules

**A(f, a(f, x)) -> A(x, g)**

none

innermost

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)= 0 _{ }^{ }_{ }^{ }POL(a(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(A(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(f)= 0 _{ }^{ }

We have the following set D of usable symbols: {g, A, f}

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

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

No Rules can be deleted.

The result of this processor delivers one new DP problem.

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳UsableRules

...

→DP Problem 4

↳Modular Removal of Rules

**A( x, g) -> A(f, x)**

none

innermost

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)= 0 _{ }^{ }_{ }^{ }POL(A(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(f)= 0 _{ }^{ }

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

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

A(x, g) -> A(f,x)

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.

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

Duration:

0:00 minutes