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

↳Argument Filtering and Ordering

→DP Problem 2

↳AFS

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

The following dependency pair can be strictly oriented:

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

There are no usable rules for innermost that need to be oriented.

Used ordering: Homeomorphic Embedding Order with EMB

resulting in one new DP problem.

Used Argument Filtering System:

V(x) -> V(_{1}x)_{1}

a(x) -> a(_{1}x)_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 3

↳Dependency Graph

→DP Problem 2

↳AFS

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

↳AFS

→DP Problem 2

↳Argument Filtering and 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)

innermost

The following dependency pair can be strictly oriented:

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

There are no usable rules for innermost that need to be oriented.

Used ordering: Homeomorphic Embedding Order with EMB

resulting in one new DP problem.

Used Argument Filtering System:

W(x) -> W(_{1}x)_{1}

a(x) -> a(_{1}x)_{1}

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳AFS

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

innermost

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:00 minutes