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

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
    ↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 466 ms)
    ↳6 CdtProblem
    ↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 495 ms)
    ↳8 CdtProblem
    ↳9 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 103 ms)
    ↳12 CdtProblem
    ↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 116 ms)
    ↳14 CdtProblem
    ↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳16 CdtProblem
    ↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳18 CdtProblem
    ↳19 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳20 CdtProblem
    ↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 204 ms)
    ↳22 CdtProblem
    ↳23 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳24 CdtProblem
    ↳25 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳26 CdtProblem
    ↳27 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳28 CdtProblem
↳29 CpxTrsMatchBoundsTAProof (⇔, 227 ms)
↳30 BOUNDS(O(1), O(n^1))

(0) Obligation:

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

active(f(a, X, X)) → mark(f(X, b, b))
active(b) → mark(a)
mark(f(X1, X2, X3)) → active(f(X1, mark(X2), X3))
mark(a) → active(a)
mark(b) → active(b)
f(mark(X1), X2, X3) → f(X1, X2, X3)
f(X1, mark(X2), X3) → f(X1, X2, X3)
f(X1, X2, mark(X3)) → f(X1, X2, X3)
f(active(X1), X2, X3) → f(X1, X2, X3)
f(X1, active(X2), X3) → f(X1, X2, X3)
f(X1, X2, active(X3)) → f(X1, X2, X3)

Rewrite Strategy: INNERMOST

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

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
ACTIVE(b) → c1(MARK(a))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, mark(z1), z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(a) → c3(ACTIVE(a))
MARK(b) → c4(ACTIVE(b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
S tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
ACTIVE(b) → c1(MARK(a))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, mark(z1), z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(a) → c3(ACTIVE(a))
MARK(b) → c4(ACTIVE(b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
K tuples:none
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, MARK, F

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 3 trailing nodes:

MARK(a) → c3(ACTIVE(a))
ACTIVE(b) → c1(MARK(a))
MARK(b) → c4(ACTIVE(b))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, mark(z1), z2)), F(z0, mark(z1), z2), MARK(z1))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
S tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, mark(z1), z2)), F(z0, mark(z1), z2), MARK(z1))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
K tuples:none
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, MARK, F

Compound Symbols:

c, c2, c5, c6, c7, c8, c9, c10

(5) 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.

F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
We considered the (Usable) Rules:

mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
And the Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, mark(z1), z2)), F(z0, mark(z1), z2), MARK(z1))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1, x2, x3)) = x3   
POL(MARK(x1)) = [2]x1   
POL(a) = 0   
POL(active(x1)) = [1] + [2]x1   
POL(b) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c10(x1)) = x1   
POL(c2(x1, x2, x3)) = x1 + x2 + x3   
POL(c5(x1)) = x1   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c9(x1)) = x1   
POL(f(x1, x2, x3)) = x2 + [4]x3   
POL(mark(x1)) = [2]x1   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, mark(z1), z2)), F(z0, mark(z1), z2), MARK(z1))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
S tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, mark(z1), z2)), F(z0, mark(z1), z2), MARK(z1))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
K tuples:

F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, MARK, F

Compound Symbols:

c, c2, c5, c6, c7, c8, c9, c10

(7) 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.

F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
We considered the (Usable) Rules:

mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
And the Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, mark(z1), z2)), F(z0, mark(z1), z2), MARK(z1))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1, x2, x3)) = [2]x3   
POL(MARK(x1)) = x1   
POL(a) = 0   
POL(active(x1)) = [4]x1   
POL(b) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c10(x1)) = x1   
POL(c2(x1, x2, x3)) = x1 + x2 + x3   
POL(c5(x1)) = x1   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c9(x1)) = x1   
POL(f(x1, x2, x3)) = x2 + [2]x3   
POL(mark(x1)) = [1] + [2]x1   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, mark(z1), z2)), F(z0, mark(z1), z2), MARK(z1))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
S tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, mark(z1), z2)), F(z0, mark(z1), z2), MARK(z1))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
K tuples:

F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, MARK, F

Compound Symbols:

c, c2, c5, c6, c7, c8, c9, c10

(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, mark(z1), z2)), F(z0, mark(z1), z2), MARK(z1)) by

MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, f(z0, z1, z2), x2)) → c2(ACTIVE(f(x0, active(f(z0, mark(z1), z2)), x2)), F(x0, mark(f(z0, z1, z2)), x2), MARK(f(z0, z1, z2)))
MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a))
MARK(f(x0, b, x2)) → c2(ACTIVE(f(x0, active(b), x2)), F(x0, mark(b), x2), MARK(b))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, f(z0, z1, z2), x2)) → c2(ACTIVE(f(x0, active(f(z0, mark(z1), z2)), x2)), F(x0, mark(f(z0, z1, z2)), x2), MARK(f(z0, z1, z2)))
MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a))
MARK(f(x0, b, x2)) → c2(ACTIVE(f(x0, active(b), x2)), F(x0, mark(b), x2), MARK(b))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
S tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, f(z0, z1, z2), x2)) → c2(ACTIVE(f(x0, active(f(z0, mark(z1), z2)), x2)), F(x0, mark(f(z0, z1, z2)), x2), MARK(f(z0, z1, z2)))
MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a))
MARK(f(x0, b, x2)) → c2(ACTIVE(f(x0, active(b), x2)), F(x0, mark(b), x2), MARK(b))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
K tuples:

F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, F, MARK

Compound Symbols:

c, c5, c6, c7, c8, c9, c10, c2, c2

(11) 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.

MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a))
We considered the (Usable) Rules:

mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
And the Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, f(z0, z1, z2), x2)) → c2(ACTIVE(f(x0, active(f(z0, mark(z1), z2)), x2)), F(x0, mark(f(z0, z1, z2)), x2), MARK(f(z0, z1, z2)))
MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a))
MARK(f(x0, b, x2)) → c2(ACTIVE(f(x0, active(b), x2)), F(x0, mark(b), x2), MARK(b))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1, x2, x3)) = [2]x3   
POL(MARK(x1)) = [2]x1   
POL(a) = [4]   
POL(active(x1)) = [3] + [2]x1   
POL(b) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c10(x1)) = x1   
POL(c2(x1)) = x1   
POL(c2(x1, x2, x3)) = x1 + x2 + x3   
POL(c5(x1)) = x1   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c9(x1)) = x1   
POL(f(x1, x2, x3)) = [5]x2 + x3   
POL(mark(x1)) = [3] + [4]x1   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, f(z0, z1, z2), x2)) → c2(ACTIVE(f(x0, active(f(z0, mark(z1), z2)), x2)), F(x0, mark(f(z0, z1, z2)), x2), MARK(f(z0, z1, z2)))
MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a))
MARK(f(x0, b, x2)) → c2(ACTIVE(f(x0, active(b), x2)), F(x0, mark(b), x2), MARK(b))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
S tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, f(z0, z1, z2), x2)) → c2(ACTIVE(f(x0, active(f(z0, mark(z1), z2)), x2)), F(x0, mark(f(z0, z1, z2)), x2), MARK(f(z0, z1, z2)))
MARK(f(x0, b, x2)) → c2(ACTIVE(f(x0, active(b), x2)), F(x0, mark(b), x2), MARK(b))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
K tuples:

F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, F, MARK

Compound Symbols:

c, c5, c6, c7, c8, c9, c10, c2, c2

(13) 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.

MARK(f(x0, f(z0, z1, z2), x2)) → c2(ACTIVE(f(x0, active(f(z0, mark(z1), z2)), x2)), F(x0, mark(f(z0, z1, z2)), x2), MARK(f(z0, z1, z2)))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
We considered the (Usable) Rules:

mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
And the Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, f(z0, z1, z2), x2)) → c2(ACTIVE(f(x0, active(f(z0, mark(z1), z2)), x2)), F(x0, mark(f(z0, z1, z2)), x2), MARK(f(z0, z1, z2)))
MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a))
MARK(f(x0, b, x2)) → c2(ACTIVE(f(x0, active(b), x2)), F(x0, mark(b), x2), MARK(b))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = [4]   
POL(F(x1, x2, x3)) = 0   
POL(MARK(x1)) = [2]x1   
POL(a) = 0   
POL(active(x1)) = [4]x1   
POL(b) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c10(x1)) = x1   
POL(c2(x1)) = x1   
POL(c2(x1, x2, x3)) = x1 + x2 + x3   
POL(c5(x1)) = x1   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c9(x1)) = x1   
POL(f(x1, x2, x3)) = [2] + [2]x2   
POL(mark(x1)) = 0   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, f(z0, z1, z2), x2)) → c2(ACTIVE(f(x0, active(f(z0, mark(z1), z2)), x2)), F(x0, mark(f(z0, z1, z2)), x2), MARK(f(z0, z1, z2)))
MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a))
MARK(f(x0, b, x2)) → c2(ACTIVE(f(x0, active(b), x2)), F(x0, mark(b), x2), MARK(b))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
S tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, b, x2)) → c2(ACTIVE(f(x0, active(b), x2)), F(x0, mark(b), x2), MARK(b))
K tuples:

F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a))
MARK(f(x0, f(z0, z1, z2), x2)) → c2(ACTIVE(f(x0, active(f(z0, mark(z1), z2)), x2)), F(x0, mark(f(z0, z1, z2)), x2), MARK(f(z0, z1, z2)))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, F, MARK

Compound Symbols:

c, c5, c6, c7, c8, c9, c10, c2, c2

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(f(x0, f(z0, z1, z2), x2)) → c2(ACTIVE(f(x0, active(f(z0, mark(z1), z2)), x2)), F(x0, mark(f(z0, z1, z2)), x2), MARK(f(z0, z1, z2))) by

MARK(f(z0, f(x1, x2, x3), z2)) → c2(ACTIVE(f(z0, f(x1, mark(x2), x3), z2)), F(z0, mark(f(x1, x2, x3)), z2), MARK(f(x1, x2, x3)))
MARK(f(x0, f(z0, z1, z2), x4)) → c2(ACTIVE(f(x0, active(f(z0, z1, z2)), x4)), F(x0, mark(f(z0, z1, z2)), x4), MARK(f(z0, z1, z2)))
MARK(f(x0, f(x1, f(z0, z1, z2), x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(f(z0, mark(z1), z2)), x3)), x4)), F(x0, mark(f(x1, f(z0, z1, z2), x3)), x4), MARK(f(x1, f(z0, z1, z2), x3)))
MARK(f(x0, f(x1, a, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(a), x3)), x4)), F(x0, mark(f(x1, a, x3)), x4), MARK(f(x1, a, x3)))
MARK(f(x0, f(x1, b, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(b), x3)), x4)), F(x0, mark(f(x1, b, x3)), x4), MARK(f(x1, b, x3)))
MARK(f(x0, f(x1, x2, x3), x4)) → c2(F(x0, mark(f(x1, x2, x3)), x4))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a))
MARK(f(x0, b, x2)) → c2(ACTIVE(f(x0, active(b), x2)), F(x0, mark(b), x2), MARK(b))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
MARK(f(z0, f(x1, x2, x3), z2)) → c2(ACTIVE(f(z0, f(x1, mark(x2), x3), z2)), F(z0, mark(f(x1, x2, x3)), z2), MARK(f(x1, x2, x3)))
MARK(f(x0, f(z0, z1, z2), x4)) → c2(ACTIVE(f(x0, active(f(z0, z1, z2)), x4)), F(x0, mark(f(z0, z1, z2)), x4), MARK(f(z0, z1, z2)))
MARK(f(x0, f(x1, f(z0, z1, z2), x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(f(z0, mark(z1), z2)), x3)), x4)), F(x0, mark(f(x1, f(z0, z1, z2), x3)), x4), MARK(f(x1, f(z0, z1, z2), x3)))
MARK(f(x0, f(x1, a, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(a), x3)), x4)), F(x0, mark(f(x1, a, x3)), x4), MARK(f(x1, a, x3)))
MARK(f(x0, f(x1, b, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(b), x3)), x4)), F(x0, mark(f(x1, b, x3)), x4), MARK(f(x1, b, x3)))
MARK(f(x0, f(x1, x2, x3), x4)) → c2(F(x0, mark(f(x1, x2, x3)), x4))
S tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, b, x2)) → c2(ACTIVE(f(x0, active(b), x2)), F(x0, mark(b), x2), MARK(b))
K tuples:

F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a))
MARK(f(x0, f(z0, z1, z2), x2)) → c2(ACTIVE(f(x0, active(f(z0, mark(z1), z2)), x2)), F(x0, mark(f(z0, z1, z2)), x2), MARK(f(z0, z1, z2)))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, F, MARK

Compound Symbols:

c, c5, c6, c7, c8, c9, c10, c2, c2

(17) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a)) by

MARK(f(z0, a, z2)) → c2(ACTIVE(f(z0, a, z2)), F(z0, mark(a), z2), MARK(a))
MARK(f(x0, a, x1)) → c2(F(x0, mark(a), x1))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, b, x2)) → c2(ACTIVE(f(x0, active(b), x2)), F(x0, mark(b), x2), MARK(b))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
MARK(f(z0, f(x1, x2, x3), z2)) → c2(ACTIVE(f(z0, f(x1, mark(x2), x3), z2)), F(z0, mark(f(x1, x2, x3)), z2), MARK(f(x1, x2, x3)))
MARK(f(x0, f(z0, z1, z2), x4)) → c2(ACTIVE(f(x0, active(f(z0, z1, z2)), x4)), F(x0, mark(f(z0, z1, z2)), x4), MARK(f(z0, z1, z2)))
MARK(f(x0, f(x1, f(z0, z1, z2), x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(f(z0, mark(z1), z2)), x3)), x4)), F(x0, mark(f(x1, f(z0, z1, z2), x3)), x4), MARK(f(x1, f(z0, z1, z2), x3)))
MARK(f(x0, f(x1, a, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(a), x3)), x4)), F(x0, mark(f(x1, a, x3)), x4), MARK(f(x1, a, x3)))
MARK(f(x0, f(x1, b, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(b), x3)), x4)), F(x0, mark(f(x1, b, x3)), x4), MARK(f(x1, b, x3)))
MARK(f(x0, f(x1, x2, x3), x4)) → c2(F(x0, mark(f(x1, x2, x3)), x4))
MARK(f(z0, a, z2)) → c2(ACTIVE(f(z0, a, z2)), F(z0, mark(a), z2), MARK(a))
MARK(f(x0, a, x1)) → c2(F(x0, mark(a), x1))
S tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, b, x2)) → c2(ACTIVE(f(x0, active(b), x2)), F(x0, mark(b), x2), MARK(b))
K tuples:

F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a))
MARK(f(x0, f(z0, z1, z2), x2)) → c2(ACTIVE(f(x0, active(f(z0, mark(z1), z2)), x2)), F(x0, mark(f(z0, z1, z2)), x2), MARK(f(z0, z1, z2)))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, F, MARK

Compound Symbols:

c, c5, c6, c7, c8, c9, c10, c2, c2

(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace MARK(f(x0, b, x2)) → c2(ACTIVE(f(x0, active(b), x2)), F(x0, mark(b), x2), MARK(b)) by

MARK(f(z0, b, z2)) → c2(ACTIVE(f(z0, b, z2)), F(z0, mark(b), z2), MARK(b))
MARK(f(x0, b, x1)) → c2(ACTIVE(f(x0, mark(a), x1)), F(x0, mark(b), x1), MARK(b))
MARK(f(x0, b, x1)) → c2

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
MARK(f(z0, f(x1, x2, x3), z2)) → c2(ACTIVE(f(z0, f(x1, mark(x2), x3), z2)), F(z0, mark(f(x1, x2, x3)), z2), MARK(f(x1, x2, x3)))
MARK(f(x0, f(z0, z1, z2), x4)) → c2(ACTIVE(f(x0, active(f(z0, z1, z2)), x4)), F(x0, mark(f(z0, z1, z2)), x4), MARK(f(z0, z1, z2)))
MARK(f(x0, f(x1, f(z0, z1, z2), x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(f(z0, mark(z1), z2)), x3)), x4)), F(x0, mark(f(x1, f(z0, z1, z2), x3)), x4), MARK(f(x1, f(z0, z1, z2), x3)))
MARK(f(x0, f(x1, a, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(a), x3)), x4)), F(x0, mark(f(x1, a, x3)), x4), MARK(f(x1, a, x3)))
MARK(f(x0, f(x1, b, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(b), x3)), x4)), F(x0, mark(f(x1, b, x3)), x4), MARK(f(x1, b, x3)))
MARK(f(x0, f(x1, x2, x3), x4)) → c2(F(x0, mark(f(x1, x2, x3)), x4))
MARK(f(z0, a, z2)) → c2(ACTIVE(f(z0, a, z2)), F(z0, mark(a), z2), MARK(a))
MARK(f(x0, a, x1)) → c2(F(x0, mark(a), x1))
MARK(f(z0, b, z2)) → c2(ACTIVE(f(z0, b, z2)), F(z0, mark(b), z2), MARK(b))
MARK(f(x0, b, x1)) → c2(ACTIVE(f(x0, mark(a), x1)), F(x0, mark(b), x1), MARK(b))
MARK(f(x0, b, x1)) → c2
S tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(z0, b, z2)) → c2(ACTIVE(f(z0, b, z2)), F(z0, mark(b), z2), MARK(b))
MARK(f(x0, b, x1)) → c2(ACTIVE(f(x0, mark(a), x1)), F(x0, mark(b), x1), MARK(b))
MARK(f(x0, b, x1)) → c2
K tuples:

F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a))
MARK(f(x0, f(z0, z1, z2), x2)) → c2(ACTIVE(f(x0, active(f(z0, mark(z1), z2)), x2)), F(x0, mark(f(z0, z1, z2)), x2), MARK(f(z0, z1, z2)))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, F, MARK

Compound Symbols:

c, c5, c6, c7, c8, c9, c10, c2, c2, c2

(21) 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.

MARK(f(x0, b, x1)) → c2
We considered the (Usable) Rules:

mark(a) → active(a)
mark(b) → active(b)
mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
active(b) → mark(a)
active(f(a, z0, z0)) → mark(f(z0, b, b))
And the Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
MARK(f(z0, f(x1, x2, x3), z2)) → c2(ACTIVE(f(z0, f(x1, mark(x2), x3), z2)), F(z0, mark(f(x1, x2, x3)), z2), MARK(f(x1, x2, x3)))
MARK(f(x0, f(z0, z1, z2), x4)) → c2(ACTIVE(f(x0, active(f(z0, z1, z2)), x4)), F(x0, mark(f(z0, z1, z2)), x4), MARK(f(z0, z1, z2)))
MARK(f(x0, f(x1, f(z0, z1, z2), x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(f(z0, mark(z1), z2)), x3)), x4)), F(x0, mark(f(x1, f(z0, z1, z2), x3)), x4), MARK(f(x1, f(z0, z1, z2), x3)))
MARK(f(x0, f(x1, a, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(a), x3)), x4)), F(x0, mark(f(x1, a, x3)), x4), MARK(f(x1, a, x3)))
MARK(f(x0, f(x1, b, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(b), x3)), x4)), F(x0, mark(f(x1, b, x3)), x4), MARK(f(x1, b, x3)))
MARK(f(x0, f(x1, x2, x3), x4)) → c2(F(x0, mark(f(x1, x2, x3)), x4))
MARK(f(z0, a, z2)) → c2(ACTIVE(f(z0, a, z2)), F(z0, mark(a), z2), MARK(a))
MARK(f(x0, a, x1)) → c2(F(x0, mark(a), x1))
MARK(f(z0, b, z2)) → c2(ACTIVE(f(z0, b, z2)), F(z0, mark(b), z2), MARK(b))
MARK(f(x0, b, x1)) → c2(ACTIVE(f(x0, mark(a), x1)), F(x0, mark(b), x1), MARK(b))
MARK(f(x0, b, x1)) → c2
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = [4]   
POL(F(x1, x2, x3)) = 0   
POL(MARK(x1)) = [2]x1   
POL(a) = 0   
POL(active(x1)) = [3]   
POL(b) = 0   
POL(c(x1, x2)) = x1 + x2   
POL(c10(x1)) = x1   
POL(c2) = 0   
POL(c2(x1)) = x1   
POL(c2(x1, x2, x3)) = x1 + x2 + x3   
POL(c5(x1)) = x1   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c9(x1)) = x1   
POL(f(x1, x2, x3)) = [2] + [4]x2   
POL(mark(x1)) = [2] + [2]x1   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
MARK(f(z0, f(x1, x2, x3), z2)) → c2(ACTIVE(f(z0, f(x1, mark(x2), x3), z2)), F(z0, mark(f(x1, x2, x3)), z2), MARK(f(x1, x2, x3)))
MARK(f(x0, f(z0, z1, z2), x4)) → c2(ACTIVE(f(x0, active(f(z0, z1, z2)), x4)), F(x0, mark(f(z0, z1, z2)), x4), MARK(f(z0, z1, z2)))
MARK(f(x0, f(x1, f(z0, z1, z2), x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(f(z0, mark(z1), z2)), x3)), x4)), F(x0, mark(f(x1, f(z0, z1, z2), x3)), x4), MARK(f(x1, f(z0, z1, z2), x3)))
MARK(f(x0, f(x1, a, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(a), x3)), x4)), F(x0, mark(f(x1, a, x3)), x4), MARK(f(x1, a, x3)))
MARK(f(x0, f(x1, b, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(b), x3)), x4)), F(x0, mark(f(x1, b, x3)), x4), MARK(f(x1, b, x3)))
MARK(f(x0, f(x1, x2, x3), x4)) → c2(F(x0, mark(f(x1, x2, x3)), x4))
MARK(f(z0, a, z2)) → c2(ACTIVE(f(z0, a, z2)), F(z0, mark(a), z2), MARK(a))
MARK(f(x0, a, x1)) → c2(F(x0, mark(a), x1))
MARK(f(z0, b, z2)) → c2(ACTIVE(f(z0, b, z2)), F(z0, mark(b), z2), MARK(b))
MARK(f(x0, b, x1)) → c2(ACTIVE(f(x0, mark(a), x1)), F(x0, mark(b), x1), MARK(b))
MARK(f(x0, b, x1)) → c2
S tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(mark(z0), z1, z2) → c5(F(z0, z1, z2))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(z0, b, z2)) → c2(ACTIVE(f(z0, b, z2)), F(z0, mark(b), z2), MARK(b))
MARK(f(x0, b, x1)) → c2(ACTIVE(f(x0, mark(a), x1)), F(x0, mark(b), x1), MARK(b))
K tuples:

F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a))
MARK(f(x0, f(z0, z1, z2), x2)) → c2(ACTIVE(f(x0, active(f(z0, mark(z1), z2)), x2)), F(x0, mark(f(z0, z1, z2)), x2), MARK(f(z0, z1, z2)))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
MARK(f(x0, b, x1)) → c2
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, F, MARK

Compound Symbols:

c, c5, c6, c7, c8, c9, c10, c2, c2, c2

(23) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(mark(z0), z1, z2) → c5(F(z0, z1, z2)) by

F(mark(mark(y0)), z1, z2) → c5(F(mark(y0), z1, z2))
F(mark(z0), mark(y1), z2) → c5(F(z0, mark(y1), z2))
F(mark(z0), z1, mark(y2)) → c5(F(z0, z1, mark(y2)))
F(mark(active(y0)), z1, z2) → c5(F(active(y0), z1, z2))
F(mark(z0), active(y1), z2) → c5(F(z0, active(y1), z2))
F(mark(z0), z1, active(y2)) → c5(F(z0, z1, active(y2)))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
MARK(f(z0, f(x1, x2, x3), z2)) → c2(ACTIVE(f(z0, f(x1, mark(x2), x3), z2)), F(z0, mark(f(x1, x2, x3)), z2), MARK(f(x1, x2, x3)))
MARK(f(x0, f(z0, z1, z2), x4)) → c2(ACTIVE(f(x0, active(f(z0, z1, z2)), x4)), F(x0, mark(f(z0, z1, z2)), x4), MARK(f(z0, z1, z2)))
MARK(f(x0, f(x1, f(z0, z1, z2), x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(f(z0, mark(z1), z2)), x3)), x4)), F(x0, mark(f(x1, f(z0, z1, z2), x3)), x4), MARK(f(x1, f(z0, z1, z2), x3)))
MARK(f(x0, f(x1, a, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(a), x3)), x4)), F(x0, mark(f(x1, a, x3)), x4), MARK(f(x1, a, x3)))
MARK(f(x0, f(x1, b, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(b), x3)), x4)), F(x0, mark(f(x1, b, x3)), x4), MARK(f(x1, b, x3)))
MARK(f(x0, f(x1, x2, x3), x4)) → c2(F(x0, mark(f(x1, x2, x3)), x4))
MARK(f(z0, a, z2)) → c2(ACTIVE(f(z0, a, z2)), F(z0, mark(a), z2), MARK(a))
MARK(f(x0, a, x1)) → c2(F(x0, mark(a), x1))
MARK(f(z0, b, z2)) → c2(ACTIVE(f(z0, b, z2)), F(z0, mark(b), z2), MARK(b))
MARK(f(x0, b, x1)) → c2(ACTIVE(f(x0, mark(a), x1)), F(x0, mark(b), x1), MARK(b))
MARK(f(x0, b, x1)) → c2
F(mark(mark(y0)), z1, z2) → c5(F(mark(y0), z1, z2))
F(mark(z0), mark(y1), z2) → c5(F(z0, mark(y1), z2))
F(mark(z0), z1, mark(y2)) → c5(F(z0, z1, mark(y2)))
F(mark(active(y0)), z1, z2) → c5(F(active(y0), z1, z2))
F(mark(z0), active(y1), z2) → c5(F(z0, active(y1), z2))
F(mark(z0), z1, active(y2)) → c5(F(z0, z1, active(y2)))
S tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(z0, b, z2)) → c2(ACTIVE(f(z0, b, z2)), F(z0, mark(b), z2), MARK(b))
MARK(f(x0, b, x1)) → c2(ACTIVE(f(x0, mark(a), x1)), F(x0, mark(b), x1), MARK(b))
F(mark(mark(y0)), z1, z2) → c5(F(mark(y0), z1, z2))
F(mark(z0), mark(y1), z2) → c5(F(z0, mark(y1), z2))
F(mark(z0), z1, mark(y2)) → c5(F(z0, z1, mark(y2)))
F(mark(active(y0)), z1, z2) → c5(F(active(y0), z1, z2))
F(mark(z0), active(y1), z2) → c5(F(z0, active(y1), z2))
F(mark(z0), z1, active(y2)) → c5(F(z0, z1, active(y2)))
K tuples:

F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
MARK(f(x0, a, x2)) → c2(ACTIVE(f(x0, active(a), x2)), F(x0, mark(a), x2), MARK(a))
MARK(f(x0, f(z0, z1, z2), x2)) → c2(ACTIVE(f(x0, active(f(z0, mark(z1), z2)), x2)), F(x0, mark(f(z0, z1, z2)), x2), MARK(f(z0, z1, z2)))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
MARK(f(x0, b, x1)) → c2
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, F, MARK

Compound Symbols:

c, c6, c7, c8, c9, c10, c2, c2, c2, c5

(25) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

MARK(f(x0, b, x1)) → c2

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
MARK(f(z0, f(x1, x2, x3), z2)) → c2(ACTIVE(f(z0, f(x1, mark(x2), x3), z2)), F(z0, mark(f(x1, x2, x3)), z2), MARK(f(x1, x2, x3)))
MARK(f(x0, f(z0, z1, z2), x4)) → c2(ACTIVE(f(x0, active(f(z0, z1, z2)), x4)), F(x0, mark(f(z0, z1, z2)), x4), MARK(f(z0, z1, z2)))
MARK(f(x0, f(x1, f(z0, z1, z2), x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(f(z0, mark(z1), z2)), x3)), x4)), F(x0, mark(f(x1, f(z0, z1, z2), x3)), x4), MARK(f(x1, f(z0, z1, z2), x3)))
MARK(f(x0, f(x1, a, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(a), x3)), x4)), F(x0, mark(f(x1, a, x3)), x4), MARK(f(x1, a, x3)))
MARK(f(x0, f(x1, b, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(b), x3)), x4)), F(x0, mark(f(x1, b, x3)), x4), MARK(f(x1, b, x3)))
MARK(f(x0, f(x1, x2, x3), x4)) → c2(F(x0, mark(f(x1, x2, x3)), x4))
MARK(f(z0, a, z2)) → c2(ACTIVE(f(z0, a, z2)), F(z0, mark(a), z2), MARK(a))
MARK(f(x0, a, x1)) → c2(F(x0, mark(a), x1))
MARK(f(z0, b, z2)) → c2(ACTIVE(f(z0, b, z2)), F(z0, mark(b), z2), MARK(b))
MARK(f(x0, b, x1)) → c2(ACTIVE(f(x0, mark(a), x1)), F(x0, mark(b), x1), MARK(b))
F(mark(mark(y0)), z1, z2) → c5(F(mark(y0), z1, z2))
F(mark(z0), mark(y1), z2) → c5(F(z0, mark(y1), z2))
F(mark(z0), z1, mark(y2)) → c5(F(z0, z1, mark(y2)))
F(mark(active(y0)), z1, z2) → c5(F(active(y0), z1, z2))
F(mark(z0), active(y1), z2) → c5(F(z0, active(y1), z2))
F(mark(z0), z1, active(y2)) → c5(F(z0, z1, active(y2)))
S tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(z0, mark(z1), z2) → c6(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(z0, b, z2)) → c2(ACTIVE(f(z0, b, z2)), F(z0, mark(b), z2), MARK(b))
MARK(f(x0, b, x1)) → c2(ACTIVE(f(x0, mark(a), x1)), F(x0, mark(b), x1), MARK(b))
F(mark(mark(y0)), z1, z2) → c5(F(mark(y0), z1, z2))
F(mark(z0), mark(y1), z2) → c5(F(z0, mark(y1), z2))
F(mark(z0), z1, mark(y2)) → c5(F(z0, z1, mark(y2)))
F(mark(active(y0)), z1, z2) → c5(F(active(y0), z1, z2))
F(mark(z0), active(y1), z2) → c5(F(z0, active(y1), z2))
F(mark(z0), z1, active(y2)) → c5(F(z0, z1, active(y2)))
K tuples:

F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, F, MARK

Compound Symbols:

c, c6, c7, c8, c9, c10, c2, c2, c5

(27) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(z0, mark(z1), z2) → c6(F(z0, z1, z2)) by

F(z0, mark(mark(y1)), z2) → c6(F(z0, mark(y1), z2))
F(z0, mark(z1), mark(y2)) → c6(F(z0, z1, mark(y2)))
F(active(y0), mark(z1), z2) → c6(F(active(y0), z1, z2))
F(z0, mark(active(y1)), z2) → c6(F(z0, active(y1), z2))
F(z0, mark(z1), active(y2)) → c6(F(z0, z1, active(y2)))
F(mark(mark(y0)), mark(z1), z2) → c6(F(mark(mark(y0)), z1, z2))
F(mark(y0), mark(mark(y1)), z2) → c6(F(mark(y0), mark(y1), z2))
F(mark(y0), mark(z1), mark(y2)) → c6(F(mark(y0), z1, mark(y2)))
F(mark(active(y0)), mark(z1), z2) → c6(F(mark(active(y0)), z1, z2))
F(mark(y0), mark(active(y1)), z2) → c6(F(mark(y0), active(y1), z2))
F(mark(y0), mark(z1), active(y2)) → c6(F(mark(y0), z1, active(y2)))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(a, z0, z0)) → mark(f(z0, b, b))
active(b) → mark(a)
mark(f(z0, z1, z2)) → active(f(z0, mark(z1), z2))
mark(a) → active(a)
mark(b) → active(b)
f(mark(z0), z1, z2) → f(z0, z1, z2)
f(z0, mark(z1), z2) → f(z0, z1, z2)
f(z0, z1, mark(z2)) → f(z0, z1, z2)
f(active(z0), z1, z2) → f(z0, z1, z2)
f(z0, active(z1), z2) → f(z0, z1, z2)
f(z0, z1, active(z2)) → f(z0, z1, z2)
Tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
MARK(f(z0, f(x1, x2, x3), z2)) → c2(ACTIVE(f(z0, f(x1, mark(x2), x3), z2)), F(z0, mark(f(x1, x2, x3)), z2), MARK(f(x1, x2, x3)))
MARK(f(x0, f(z0, z1, z2), x4)) → c2(ACTIVE(f(x0, active(f(z0, z1, z2)), x4)), F(x0, mark(f(z0, z1, z2)), x4), MARK(f(z0, z1, z2)))
MARK(f(x0, f(x1, f(z0, z1, z2), x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(f(z0, mark(z1), z2)), x3)), x4)), F(x0, mark(f(x1, f(z0, z1, z2), x3)), x4), MARK(f(x1, f(z0, z1, z2), x3)))
MARK(f(x0, f(x1, a, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(a), x3)), x4)), F(x0, mark(f(x1, a, x3)), x4), MARK(f(x1, a, x3)))
MARK(f(x0, f(x1, b, x3), x4)) → c2(ACTIVE(f(x0, active(f(x1, active(b), x3)), x4)), F(x0, mark(f(x1, b, x3)), x4), MARK(f(x1, b, x3)))
MARK(f(x0, f(x1, x2, x3), x4)) → c2(F(x0, mark(f(x1, x2, x3)), x4))
MARK(f(z0, a, z2)) → c2(ACTIVE(f(z0, a, z2)), F(z0, mark(a), z2), MARK(a))
MARK(f(x0, a, x1)) → c2(F(x0, mark(a), x1))
MARK(f(z0, b, z2)) → c2(ACTIVE(f(z0, b, z2)), F(z0, mark(b), z2), MARK(b))
MARK(f(x0, b, x1)) → c2(ACTIVE(f(x0, mark(a), x1)), F(x0, mark(b), x1), MARK(b))
F(mark(mark(y0)), z1, z2) → c5(F(mark(y0), z1, z2))
F(mark(z0), mark(y1), z2) → c5(F(z0, mark(y1), z2))
F(mark(z0), z1, mark(y2)) → c5(F(z0, z1, mark(y2)))
F(mark(active(y0)), z1, z2) → c5(F(active(y0), z1, z2))
F(mark(z0), active(y1), z2) → c5(F(z0, active(y1), z2))
F(mark(z0), z1, active(y2)) → c5(F(z0, z1, active(y2)))
F(z0, mark(mark(y1)), z2) → c6(F(z0, mark(y1), z2))
F(z0, mark(z1), mark(y2)) → c6(F(z0, z1, mark(y2)))
F(active(y0), mark(z1), z2) → c6(F(active(y0), z1, z2))
F(z0, mark(active(y1)), z2) → c6(F(z0, active(y1), z2))
F(z0, mark(z1), active(y2)) → c6(F(z0, z1, active(y2)))
F(mark(mark(y0)), mark(z1), z2) → c6(F(mark(mark(y0)), z1, z2))
F(mark(y0), mark(mark(y1)), z2) → c6(F(mark(y0), mark(y1), z2))
F(mark(y0), mark(z1), mark(y2)) → c6(F(mark(y0), z1, mark(y2)))
F(mark(active(y0)), mark(z1), z2) → c6(F(mark(active(y0)), z1, z2))
F(mark(y0), mark(active(y1)), z2) → c6(F(mark(y0), active(y1), z2))
F(mark(y0), mark(z1), active(y2)) → c6(F(mark(y0), z1, active(y2)))
S tuples:

ACTIVE(f(a, z0, z0)) → c(MARK(f(z0, b, b)), F(z0, b, b))
F(active(z0), z1, z2) → c8(F(z0, z1, z2))
F(z0, active(z1), z2) → c9(F(z0, z1, z2))
MARK(f(z0, z1, z2)) → c2(ACTIVE(f(z0, z1, z2)), F(z0, mark(z1), z2), MARK(z1))
MARK(f(z0, b, z2)) → c2(ACTIVE(f(z0, b, z2)), F(z0, mark(b), z2), MARK(b))
MARK(f(x0, b, x1)) → c2(ACTIVE(f(x0, mark(a), x1)), F(x0, mark(b), x1), MARK(b))
F(mark(mark(y0)), z1, z2) → c5(F(mark(y0), z1, z2))
F(mark(z0), mark(y1), z2) → c5(F(z0, mark(y1), z2))
F(mark(z0), z1, mark(y2)) → c5(F(z0, z1, mark(y2)))
F(mark(active(y0)), z1, z2) → c5(F(active(y0), z1, z2))
F(mark(z0), active(y1), z2) → c5(F(z0, active(y1), z2))
F(mark(z0), z1, active(y2)) → c5(F(z0, z1, active(y2)))
F(z0, mark(mark(y1)), z2) → c6(F(z0, mark(y1), z2))
F(z0, mark(z1), mark(y2)) → c6(F(z0, z1, mark(y2)))
F(active(y0), mark(z1), z2) → c6(F(active(y0), z1, z2))
F(z0, mark(active(y1)), z2) → c6(F(z0, active(y1), z2))
F(z0, mark(z1), active(y2)) → c6(F(z0, z1, active(y2)))
F(mark(mark(y0)), mark(z1), z2) → c6(F(mark(mark(y0)), z1, z2))
F(mark(y0), mark(mark(y1)), z2) → c6(F(mark(y0), mark(y1), z2))
F(mark(y0), mark(z1), mark(y2)) → c6(F(mark(y0), z1, mark(y2)))
F(mark(active(y0)), mark(z1), z2) → c6(F(mark(active(y0)), z1, z2))
F(mark(y0), mark(active(y1)), z2) → c6(F(mark(y0), active(y1), z2))
F(mark(y0), mark(z1), active(y2)) → c6(F(mark(y0), z1, active(y2)))
K tuples:

F(z0, z1, active(z2)) → c10(F(z0, z1, z2))
F(z0, z1, mark(z2)) → c7(F(z0, z1, z2))
MARK(f(x0, x1, x2)) → c2(F(x0, mark(x1), x2))
Defined Rule Symbols:

active, mark, f

Defined Pair Symbols:

ACTIVE, F, MARK

Compound Symbols:

c, c7, c8, c9, c10, c2, c2, c5, c6

(29) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match(-raise)-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 3.

The compatible tree automaton used to show the Match(-raise)-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 3, 11]
transitions:
active0(0) → 1
mark0(0) → 2
f0(0, 0, 0) → 3
mark1(4) → 1
active1(5) → 2
b1() → 6
active1(6) → 2
b1() → 0
b1() → 8
active0(7) → 1
active0(8) → 1
mark0(7) → 2
mark0(8) → 2
f0(7, 0, 0) → 3
f0(0, 7, 0) → 3
f0(0, 0, 7) → 3
f0(8, 0, 0) → 3
f0(0, 8, 0) → 3
f0(0, 0, 8) → 3
f0(7, 7, 0) → 3
f0(7, 0, 7) → 3
f0(7, 8, 0) → 3
f0(7, 0, 8) → 3
f0(0, 7, 7) → 3
f0(8, 7, 0) → 3
f0(0, 7, 8) → 3
f0(8, 0, 7) → 3
f0(0, 8, 7) → 3
f0(8, 8, 0) → 3
f0(8, 0, 8) → 3
f0(0, 8, 8) → 3
f0(7, 7, 7) → 3
f0(7, 7, 8) → 3
f0(7, 8, 7) → 3
f0(7, 8, 8) → 3
f0(8, 7, 7) → 3
f0(8, 7, 8) → 3
f0(8, 8, 7) → 3
f0(8, 8, 8) → 3
mark1(7) → 1
active1(7) → 2
active1(8) → 2
active1(7) → 1
active1(8) → 1
mark1(7) → 2
mark2(9) → 2
active2(10) → 1
mark1(7) → 11
active1(7) → 11
active1(8) → 11
active0(12) → 1
mark0(12) → 2
f0(12, 0, 0) → 3
f0(12, 7, 0) → 3
f0(12, 0, 7) → 3
f0(12, 8, 0) → 3
f0(12, 0, 8) → 3
f0(12, 7, 7) → 3
f0(12, 7, 8) → 3
f0(12, 8, 7) → 3
f0(12, 8, 8) → 3
f0(0, 12, 0) → 3
f0(7, 12, 0) → 3
f0(0, 12, 7) → 3
f0(8, 12, 0) → 3
f0(0, 12, 8) → 3
f0(7, 12, 7) → 3
f0(7, 12, 8) → 3
f0(8, 12, 7) → 3
f0(8, 12, 8) → 3
f0(0, 0, 12) → 3
f0(7, 0, 12) → 3
f0(0, 7, 12) → 3
f0(8, 0, 12) → 3
f0(0, 8, 12) → 3
f0(7, 7, 12) → 3
f0(7, 8, 12) → 3
f0(8, 7, 12) → 3
f0(8, 8, 12) → 3
f0(12, 12, 0) → 3
f0(12, 12, 7) → 3
f0(12, 12, 8) → 3
f0(12, 0, 12) → 3
f0(12, 7, 12) → 3
f0(12, 8, 12) → 3
f0(0, 12, 12) → 3
f0(7, 12, 12) → 3
f0(8, 12, 12) → 3
f0(12, 12, 12) → 3
mark1(12) → 11
active1(12) → 11
mark2(12) → 2
active2(12) → 1
active1(12) → 1
mark1(12) → 2
mark2(12) → 11
active2(12) → 11
a3() → 13
active3(13) → 2
a3() → 9
a3() → 4
a3() → 0
a3() → 5
a3() → 7
a3() → 10
a3() → 12
a3() → 14
active0(14) → 1
mark0(14) → 2
f0(14, 0, 0) → 3
f0(14, 7, 0) → 3
f0(14, 0, 7) → 3
f0(14, 8, 0) → 3
f0(14, 0, 8) → 3
f0(14, 7, 7) → 3
f0(14, 7, 8) → 3
f0(14, 8, 7) → 3
f0(14, 8, 8) → 3
f0(14, 12, 0) → 3
f0(14, 12, 7) → 3
f0(14, 12, 8) → 3
f0(14, 0, 12) → 3
f0(14, 7, 12) → 3
f0(14, 8, 12) → 3
f0(14, 12, 12) → 3
f0(0, 14, 0) → 3
f0(7, 14, 0) → 3
f0(0, 14, 7) → 3
f0(8, 14, 0) → 3
f0(0, 14, 8) → 3
f0(7, 14, 7) → 3
f0(7, 14, 8) → 3
f0(8, 14, 7) → 3
f0(8, 14, 8) → 3
f0(12, 14, 0) → 3
f0(12, 14, 7) → 3
f0(12, 14, 8) → 3
f0(0, 14, 12) → 3
f0(7, 14, 12) → 3
f0(8, 14, 12) → 3
f0(12, 14, 12) → 3
f0(0, 0, 14) → 3
f0(7, 0, 14) → 3
f0(0, 7, 14) → 3
f0(8, 0, 14) → 3
f0(0, 8, 14) → 3
f0(7, 7, 14) → 3
f0(7, 8, 14) → 3
f0(8, 7, 14) → 3
f0(8, 8, 14) → 3
f0(12, 0, 14) → 3
f0(12, 7, 14) → 3
f0(12, 8, 14) → 3
f0(0, 12, 14) → 3
f0(7, 12, 14) → 3
f0(8, 12, 14) → 3
f0(12, 12, 14) → 3
f0(14, 14, 0) → 3
f0(14, 14, 7) → 3
f0(14, 14, 8) → 3
f0(14, 14, 12) → 3
f0(14, 0, 14) → 3
f0(14, 7, 14) → 3
f0(14, 8, 14) → 3
f0(14, 12, 14) → 3
f0(0, 14, 14) → 3
f0(7, 14, 14) → 3
f0(8, 14, 14) → 3
f0(12, 14, 14) → 3
f0(14, 14, 14) → 3
mark1(14) → 11
active1(14) → 11
mark2(14) → 11
active2(14) → 11
active3(14) → 2
active1(14) → 1
active2(14) → 1
active3(14) → 1
mark1(14) → 2
mark2(14) → 2
active3(14) → 11

(30) BOUNDS(O(1), O(n^1))