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

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

Additionally, the following usable rules w.r.t. to the implicit 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: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(I(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(i(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(e)= 0 _{ }^{ }_{ }^{ }POL(DIV(x)_{1}, x_{2})= x _{1}_{ }^{ }_{ }^{ }POL(div(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Polo

→DP Problem 2

↳Dependency Graph

**DIV( X, e) -> 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)

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:00 minutes