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

(0) Obligation:

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

:(x, x) → e
:(x, e) → x
i(:(x, y)) → :(y, x)
:(:(x, y), z) → :(x, :(z, i(y)))
:(e, x) → i(x)
i(i(x)) → x
i(e) → e
:(x, :(y, i(x))) → i(y)
:(x, :(y, :(i(x), z))) → :(i(z), y)
:(i(x), :(y, x)) → i(y)
:(i(x), :(y, :(x, z))) → :(i(z), y)

Rewrite Strategy: INNERMOST

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

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

:'(:(z0, z1), z2) → c2(:'(z0, :(z2, i(z1))), :'(z2, i(z1)), I(z1))
:'(e, z0) → c3(I(z0))
:'(z0, :(z1, i(z0))) → c4(I(z1))
:'(z0, :(z1, :(i(z0), z2))) → c5(:'(i(z2), z1), I(z2))
:'(i(z0), :(z1, z0)) → c6(I(z1))
:'(i(z0), :(z1, :(z0, z2))) → c7(:'(i(z2), z1), I(z2))
I(:(z0, z1)) → c8(:'(z1, z0))

S tuples:

:'(:(z0, z1), z2) → c2(:'(z0, :(z2, i(z1))), :'(z2, i(z1)), I(z1))
:'(e, z0) → c3(I(z0))
:'(z0, :(z1, i(z0))) → c4(I(z1))
:'(z0, :(z1, :(i(z0), z2))) → c5(:'(i(z2), z1), I(z2))
:'(i(z0), :(z1, z0)) → c6(I(z1))
:'(i(z0), :(z1, :(z0, z2))) → c7(:'(i(z2), z1), I(z2))
I(:(z0, z1)) → c8(:'(z1, z0))

K tuples:none
Defined Rule Symbols:

:, i

Defined Pair Symbols:

:', I

Compound Symbols:

c2, c3, c4, c5, c6, c7, c8

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

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

:'(:(z0, z1), z2) → c2(:'(z0, :(z2, i(z1))), :'(z2, i(z1)), I(z1))
:'(e, z0) → c3(I(z0))
:'(z0, :(z1, i(z0))) → c4(I(z1))
:'(z0, :(z1, :(i(z0), z2))) → c5(:'(i(z2), z1), I(z2))
:'(i(z0), :(z1, z0)) → c6(I(z1))
:'(i(z0), :(z1, :(z0, z2))) → c7(:'(i(z2), z1), I(z2))
I(:(z0, z1)) → c8(:'(z1, z0))

We considered the (Usable) Rules:

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

And the Tuples:

:'(:(z0, z1), z2) → c2(:'(z0, :(z2, i(z1))), :'(z2, i(z1)), I(z1))
:'(e, z0) → c3(I(z0))
:'(z0, :(z1, i(z0))) → c4(I(z1))
:'(z0, :(z1, :(i(z0), z2))) → c5(:'(i(z2), z1), I(z2))
:'(i(z0), :(z1, z0)) → c6(I(z1))
:'(i(z0), :(z1, :(z0, z2))) → c7(:'(i(z2), z1), I(z2))
I(:(z0, z1)) → c8(:'(z1, z0))

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

POL(:(x₁, x₂)) = [3] + [3]x₁ + [3]x₂ + [2]x₁·x₂   
POL(:'(x₁, x₂)) = [3]x₁ + x₂ + [2]x₁·x₂   
POL(I(x₁)) = [2]x₁   
POL(c2(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c5(x₁, x₂)) = x₁ + x₂   
POL(c6(x₁)) = x₁   
POL(c7(x₁, x₂)) = x₁ + x₂   
POL(c8(x₁)) = x₁   
POL(e) = [1]   
POL(i(x₁)) = x₁   

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

Tuples:

:'(:(z0, z1), z2) → c2(:'(z0, :(z2, i(z1))), :'(z2, i(z1)), I(z1))
:'(e, z0) → c3(I(z0))
:'(z0, :(z1, i(z0))) → c4(I(z1))
:'(z0, :(z1, :(i(z0), z2))) → c5(:'(i(z2), z1), I(z2))
:'(i(z0), :(z1, z0)) → c6(I(z1))
:'(i(z0), :(z1, :(z0, z2))) → c7(:'(i(z2), z1), I(z2))
I(:(z0, z1)) → c8(:'(z1, z0))

S tuples:none
K tuples:

:'(:(z0, z1), z2) → c2(:'(z0, :(z2, i(z1))), :'(z2, i(z1)), I(z1))
:'(e, z0) → c3(I(z0))
:'(z0, :(z1, i(z0))) → c4(I(z1))
:'(z0, :(z1, :(i(z0), z2))) → c5(:'(i(z2), z1), I(z2))
:'(i(z0), :(z1, z0)) → c6(I(z1))
:'(i(z0), :(z1, :(z0, z2))) → c7(:'(i(z2), z1), I(z2))
I(:(z0, z1)) → c8(:'(z1, z0))

Defined Rule Symbols:

:, i

Defined Pair Symbols:

:', I

Compound Symbols:

c2, c3, c4, c5, c6, c7, c8

(5) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

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