a(c(d(

u(b(d(d(

v(a(a(

v(a(c(

v(c(

w(a(a(

w(a(c(

w(c(

R

↳Dependency Pair Analysis

V(a(a(x))) -> U(v(x))

V(a(a(x))) -> V(x)

V(a(c(x))) -> U(b(d(x)))

W(a(a(x))) -> U(w(x))

W(a(a(x))) -> W(x)

W(a(c(x))) -> U(b(d(x)))

Furthermore,

R

↳DPs

→DP Problem 1

↳Forward Instantiation Transformation

→DP Problem 2

↳FwdInst

**V(a(a( x))) -> V(x)**

a(c(d(x))) -> c(x)

u(b(d(d(x)))) -> b(x)

v(a(a(x))) -> u(v(x))

v(a(c(x))) -> u(b(d(x)))

v(c(x)) -> b(x)

w(a(a(x))) -> u(w(x))

w(a(c(x))) -> u(b(d(x)))

w(c(x)) -> b(x)

innermost

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

As a result of transforming the rule

one new Dependency Pair is created:

V(a(a(x))) -> V(x)

V(a(a(a(a(x''))))) -> V(a(a(x'')))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳FwdInst

→DP Problem 3

↳Forward Instantiation Transformation

→DP Problem 2

↳FwdInst

**V(a(a(a(a( x''))))) -> V(a(a(x'')))**

a(c(d(x))) -> c(x)

u(b(d(d(x)))) -> b(x)

v(a(a(x))) -> u(v(x))

v(a(c(x))) -> u(b(d(x)))

v(c(x)) -> b(x)

w(a(a(x))) -> u(w(x))

w(a(c(x))) -> u(b(d(x)))

w(c(x)) -> b(x)

innermost

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

As a result of transforming the rule

one new Dependency Pair is created:

V(a(a(a(a(x''))))) -> V(a(a(x'')))

V(a(a(a(a(a(a(x''''))))))) -> V(a(a(a(a(x'''')))))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳FwdInst

→DP Problem 3

↳FwdInst

...

→DP Problem 4

↳Polynomial Ordering

→DP Problem 2

↳FwdInst

**V(a(a(a(a(a(a( x''''))))))) -> V(a(a(a(a(x'''')))))**

a(c(d(x))) -> c(x)

u(b(d(d(x)))) -> b(x)

v(a(a(x))) -> u(v(x))

v(a(c(x))) -> u(b(d(x)))

v(c(x)) -> b(x)

w(a(a(x))) -> u(w(x))

w(a(c(x))) -> u(b(d(x)))

w(c(x)) -> b(x)

innermost

The following dependency pair can be strictly oriented:

V(a(a(a(a(a(a(x''''))))))) -> V(a(a(a(a(x'''')))))

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

a(c(d(x))) -> c(x)

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(c(x)_{1})= 0 _{ }^{ }_{ }^{ }POL(V(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(d(x)_{1})= 0 _{ }^{ }_{ }^{ }POL(a(x)_{1})= 1 + x _{1}_{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳FwdInst

→DP Problem 3

↳FwdInst

...

→DP Problem 5

↳Dependency Graph

→DP Problem 2

↳FwdInst

a(c(d(x))) -> c(x)

u(b(d(d(x)))) -> b(x)

v(a(a(x))) -> u(v(x))

v(a(c(x))) -> u(b(d(x)))

v(c(x)) -> b(x)

w(a(a(x))) -> u(w(x))

w(a(c(x))) -> u(b(d(x)))

w(c(x)) -> b(x)

innermost

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳FwdInst

→DP Problem 2

↳Forward Instantiation Transformation

**W(a(a( x))) -> W(x)**

a(c(d(x))) -> c(x)

u(b(d(d(x)))) -> b(x)

v(a(a(x))) -> u(v(x))

v(a(c(x))) -> u(b(d(x)))

v(c(x)) -> b(x)

w(a(a(x))) -> u(w(x))

w(a(c(x))) -> u(b(d(x)))

w(c(x)) -> b(x)

innermost

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

As a result of transforming the rule

one new Dependency Pair is created:

W(a(a(x))) -> W(x)

W(a(a(a(a(x''))))) -> W(a(a(x'')))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳FwdInst

→DP Problem 2

↳FwdInst

→DP Problem 6

↳Forward Instantiation Transformation

**W(a(a(a(a( x''))))) -> W(a(a(x'')))**

a(c(d(x))) -> c(x)

u(b(d(d(x)))) -> b(x)

v(a(a(x))) -> u(v(x))

v(a(c(x))) -> u(b(d(x)))

v(c(x)) -> b(x)

w(a(a(x))) -> u(w(x))

w(a(c(x))) -> u(b(d(x)))

w(c(x)) -> b(x)

innermost

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

As a result of transforming the rule

one new Dependency Pair is created:

W(a(a(a(a(x''))))) -> W(a(a(x'')))

W(a(a(a(a(a(a(x''''))))))) -> W(a(a(a(a(x'''')))))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳FwdInst

→DP Problem 2

↳FwdInst

→DP Problem 6

↳FwdInst

...

→DP Problem 7

↳Polynomial Ordering

**W(a(a(a(a(a(a( x''''))))))) -> W(a(a(a(a(x'''')))))**

a(c(d(x))) -> c(x)

u(b(d(d(x)))) -> b(x)

v(a(a(x))) -> u(v(x))

v(a(c(x))) -> u(b(d(x)))

v(c(x)) -> b(x)

w(a(a(x))) -> u(w(x))

w(a(c(x))) -> u(b(d(x)))

w(c(x)) -> b(x)

innermost

The following dependency pair can be strictly oriented:

W(a(a(a(a(a(a(x''''))))))) -> W(a(a(a(a(x'''')))))

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

a(c(d(x))) -> c(x)

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(c(x)_{1})= 0 _{ }^{ }_{ }^{ }POL(d(x)_{1})= 0 _{ }^{ }_{ }^{ }POL(a(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(W(x)_{1})= 1 + x _{1}_{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳FwdInst

→DP Problem 2

↳FwdInst

→DP Problem 6

↳FwdInst

...

→DP Problem 8

↳Dependency Graph

a(c(d(x))) -> c(x)

u(b(d(d(x)))) -> b(x)

v(a(a(x))) -> u(v(x))

v(a(c(x))) -> u(b(d(x)))

v(c(x)) -> b(x)

w(a(a(x))) -> u(w(x))

w(a(c(x))) -> u(b(d(x)))

w(c(x)) -> b(x)

innermost

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:00 minutes