The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

div(X, e) → i(X)
i(div(X, Y)) → div(Y, X)
div(div(X, Y), Z) → div(Y, div(i(X), Z))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

div(z0, e) → i(z0)
div(div(z0, z1), z2) → div(z1, div(i(z0), z2))
i(div(z0, z1)) → div(z1, z0)

Tuples:

DIV(z0, e) → c(I(z0))
DIV(div(z0, z1), z2) → c1(DIV(z1, div(i(z0), z2)), DIV(i(z0), z2), I(z0))
I(div(z0, z1)) → c2(DIV(z1, z0))

S tuples:

DIV(z0, e) → c(I(z0))
DIV(div(z0, z1), z2) → c1(DIV(z1, div(i(z0), z2)), DIV(i(z0), z2), I(z0))
I(div(z0, z1)) → c2(DIV(z1, z0))

K tuples:none
Defined Rule Symbols:

div, i

Defined Pair Symbols:

DIV, I

Compound Symbols:

c, c1, c2

(3) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

DIV(div(z0, z1), z2) → c1(DIV(z1, div(i(z0), z2)), DIV(i(z0), z2), I(z0))
I(div(z0, z1)) → c2(DIV(z1, z0))

We considered the (Usable) Rules:

i(div(z0, z1)) → div(z1, z0)
div(z0, e) → i(z0)
div(div(z0, z1), z2) → div(z1, div(i(z0), z2))

And the Tuples:

DIV(z0, e) → c(I(z0))
DIV(div(z0, z1), z2) → c1(DIV(z1, div(i(z0), z2)), DIV(i(z0), z2), I(z0))
I(div(z0, z1)) → c2(DIV(z1, z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(DIV(x₁, x₂)) = x₁   
POL(I(x₁)) = x₁   
POL(c(x₁)) = x₁   
POL(c1(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c2(x₁)) = x₁   
POL(div(x₁, x₂)) = [1] + [2]x₁ + x₂   
POL(e) = [3]   
POL(i(x₁)) = 0   

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

div(z0, e) → i(z0)
div(div(z0, z1), z2) → div(z1, div(i(z0), z2))
i(div(z0, z1)) → div(z1, z0)

Tuples:

DIV(z0, e) → c(I(z0))
DIV(div(z0, z1), z2) → c1(DIV(z1, div(i(z0), z2)), DIV(i(z0), z2), I(z0))
I(div(z0, z1)) → c2(DIV(z1, z0))

S tuples:

DIV(z0, e) → c(I(z0))

K tuples:

DIV(div(z0, z1), z2) → c1(DIV(z1, div(i(z0), z2)), DIV(i(z0), z2), I(z0))
I(div(z0, z1)) → c2(DIV(z1, z0))

Defined Rule Symbols:

div, i

Defined Pair Symbols:

DIV, I

Compound Symbols:

c, c1, c2

(5) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

DIV(z0, e) → c(I(z0))
I(div(z0, z1)) → c2(DIV(z1, z0))

Now S is empty

(6) BOUNDS(O(1), O(1))