a(f, a(f, a(g, a(g,

R

↳Dependency Pair Analysis

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

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

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

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

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

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

Furthermore,

R

↳DPs

→DP Problem 1

↳Narrowing Transformation

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

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

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Narrowing Transformation

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

a(f, a(f, a(g, a(g,x)))) -> a(g, a(g, a(g, a(f, a(f, 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(f, a(f, a(g, a(g, a(g, a(g,x'')))))) -> A(f, a(g, a(g, a(g, a(f, a(f, a(f,x'')))))))

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 3

↳Rewriting Transformation

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

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

innermost

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

As a result of transforming the rule

one new Dependency Pair is created:

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 4

↳Forward Instantiation Transformation

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

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

innermost

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

As a result of transforming the rule

four new Dependency Pairs are created:

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

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

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

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

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

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 5

↳Polynomial Ordering

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

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

innermost

The following dependency pairs can be strictly oriented:

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

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

Additionally, the following usable rule for innermost w.r.t. to the implicit AFS can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(g)= 0 _{ }^{ }_{ }^{ }POL(a(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(f)= 1 _{ }^{ }_{ }^{ }POL(A(x)_{1}, x_{2})= x _{2}_{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Nar

...

→DP Problem 6

↳Remaining Obligation(s)

The following remains to be proven:

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

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

innermost

Duration:

0:01 minutes