div(

div(div(

i(div(

R

↳Dependency Pair Analysis

DIV(X, e) -> I(X)

DIV(div(X,Y),Z) -> DIV(Y, div(i(X),Z))

DIV(div(X,Y),Z) -> DIV(i(X),Z)

DIV(div(X,Y),Z) -> I(X)

I(div(X,Y)) -> DIV(Y,X)

Furthermore,

R

↳DPs

→DP Problem 1

↳Argument Filtering and Ordering

**DIV(div( X, Y), Z) -> I(X)**

div(X, e) -> i(X)

div(div(X,Y),Z) -> div(Y, div(i(X),Z))

i(div(X,Y)) -> div(Y,X)

The following dependency pairs can be strictly oriented:

DIV(div(X,Y),Z) -> I(X)

DIV(div(X,Y),Z) -> DIV(i(X),Z)

DIV(div(X,Y),Z) -> DIV(Y, div(i(X),Z))

I(div(X,Y)) -> DIV(Y,X)

DIV(X, e) -> I(X)

The following usable rules w.r.t. to the AFS can be oriented:

i(div(X,Y)) -> div(Y,X)

div(X, e) -> i(X)

div(div(X,Y),Z) -> div(Y, div(i(X),Z))

Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

{i, I, div, DIV}

resulting in one new DP problem.

Used Argument Filtering System:

DIV(x,_{1}x) -> DIV(_{2}x,_{1}x)_{2}

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

div(x,_{1}x) -> div(_{2}x,_{1}x)_{2}

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

R

↳DPs

→DP Problem 1

↳AFS

→DP Problem 2

↳Dependency Graph

div(X, e) -> i(X)

div(div(X,Y),Z) -> div(Y, div(i(X),Z))

i(div(X,Y)) -> div(Y,X)

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:00 minutes