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

↳Polynomial Ordering

→DP Problem 2

↳Polo

**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)

The following dependency pair can be strictly oriented:

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

Additionally, the following rules can be oriented:

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)

Used ordering: Polynomial ordering with Polynomial interpretation:

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

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 3

↳Dependency Graph

→DP Problem 2

↳Polo

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)

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polynomial Ordering

**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)

The following dependency pair can be strictly oriented:

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

Additionally, the following rules can be oriented:

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)

Used ordering: Polynomial ordering with Polynomial interpretation:

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

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Polo

→DP Problem 4

↳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)

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:00 minutes