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)

The following dependency pair can be strictly oriented:

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

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: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

{d, a} > u

{d, a} > b

{d, a} > v

w > u

c > b

resulting in one new DP problem.

Used Argument Filtering System:

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

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

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

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

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

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

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

w(x) -> w(_{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)

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)

The following dependency pair can be strictly oriented:

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

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: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

a > d

a > u

a > v > {w, b}

resulting in one new DP problem.

Used Argument Filtering System:

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

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

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

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

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

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

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

w(x) -> w(_{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)

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:00 minutes