Runtime Complexity (innermost) proof of /tmp/tmplhBJCk/Ex23_Luc06

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))), 668 ms)

    ↳6 CdtProblem

    ↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳8 CdtProblem

    ↳9 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳10 CdtProblem

    ↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 166 ms)

    ↳12 CdtProblem

    ↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳14 CdtProblem

    ↳15 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳16 CdtProblem

    ↳17 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 1392 ms)

    ↳18 CdtProblem

    ↳19 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳20 CdtProblem

    ↳21 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳22 CdtProblem

    ↳23 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳24 CdtProblem

    ↳25 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 691 ms)

    ↳26 CdtProblem

    ↳27 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳28 CdtProblem

    ↳29 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳30 CdtProblem

    ↳31 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳32 CdtProblem

    ↳33 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 826 ms)

    ↳34 CdtProblem

    ↳35 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 8 ms)

    ↳36 CdtProblem

    ↳37 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳38 CdtProblem

    ↳39 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳40 CdtProblem

    ↳41 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 806 ms)

    ↳42 CdtProblem

    ↳43 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳44 CdtProblem

    ↳45 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳46 CdtProblem

    ↳47 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳48 CdtProblem

↳49 CpxTrsMatchBoundsProof (⇔, 0 ms)

↳50 BOUNDS(O(1), O(n^1))

(0) Obligation:

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

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(X)) → f(active(X))
active(g(X)) → g(active(X))
f(mark(X)) → mark(f(X))
g(mark(X)) → mark(g(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(c(X)) → c(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
c(ok(X)) → ok(c(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Rewrite Strategy: INNERMOST

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

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(f(a))) → c1(C(f(g(f(a)))), F(g(f(a))), G(f(a)), F(a))
ACTIVE(f(z0)) → c2(F(active(z0)), ACTIVE(z0))
ACTIVE(g(z0)) → c3(G(active(z0)), ACTIVE(z0))
F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))

S tuples:

ACTIVE(f(f(a))) → c1(C(f(g(f(a)))), F(g(f(a))), G(f(a)), F(a))
ACTIVE(f(z0)) → c2(F(active(z0)), ACTIVE(z0))
ACTIVE(g(z0)) → c3(G(active(z0)), ACTIVE(z0))
F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))

K tuples:none
Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, C, TOP

Compound Symbols:

c1, c2, c3, c4, c5, c6, c7, c8, c10, c11, c12, c13, c14

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

Removed 1 trailing nodes:

ACTIVE(f(f(a))) → c1(C(f(g(f(a)))), F(g(f(a))), G(f(a)), F(a))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(z0)) → c2(F(active(z0)), ACTIVE(z0))
ACTIVE(g(z0)) → c3(G(active(z0)), ACTIVE(z0))
F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))

S tuples:

ACTIVE(f(z0)) → c2(F(active(z0)), ACTIVE(z0))
ACTIVE(g(z0)) → c3(G(active(z0)), ACTIVE(z0))
F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))

K tuples:none
Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, C, TOP

Compound Symbols:

c2, c3, c4, c5, c6, c7, c8, c10, c11, c12, c13, c14

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

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))

We considered the (Usable) Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))

And the Tuples:

ACTIVE(f(z0)) → c2(F(active(z0)), ACTIVE(z0))
ACTIVE(g(z0)) → c3(G(active(z0)), ACTIVE(z0))
F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))

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

POL(ACTIVE(x₁)) = 0
POL(C(x₁)) = 0
POL(F(x₁)) = 0
POL(G(x₁)) = 0
POL(PROPER(x₁)) = 0
POL(TOP(x₁)) = [2]x₁
POL(a) = [2]
POL(active(x₁)) = x₁
POL(c(x₁)) = 0
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(f(x₁)) = [2]x₁
POL(g(x₁)) = [4]x₁
POL(mark(x₁)) = [1] + x₁
POL(ok(x₁)) = x₁
POL(proper(x₁)) = x₁

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(z0)) → c2(F(active(z0)), ACTIVE(z0))
ACTIVE(g(z0)) → c3(G(active(z0)), ACTIVE(z0))
F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))

S tuples:

ACTIVE(f(z0)) → c2(F(active(z0)), ACTIVE(z0))
ACTIVE(g(z0)) → c3(G(active(z0)), ACTIVE(z0))
F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, C, TOP

Compound Symbols:

c2, c3, c4, c5, c6, c7, c8, c10, c11, c12, c13, c14

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

Use narrowing to replace ACTIVE(f(z0)) → c2(F(active(z0)), ACTIVE(z0)) by

ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(f(x0)) → c2

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(g(z0)) → c3(G(active(z0)), ACTIVE(z0))
F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(f(x0)) → c2

S tuples:

ACTIVE(g(z0)) → c3(G(active(z0)), ACTIVE(z0))
F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(f(x0)) → c2

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, C, TOP

Compound Symbols:

c3, c4, c5, c6, c7, c8, c10, c11, c12, c13, c14, c2, c2

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

Removed 1 trailing nodes:

ACTIVE(f(x0)) → c2

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(g(z0)) → c3(G(active(z0)), ACTIVE(z0))
F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))

S tuples:

ACTIVE(g(z0)) → c3(G(active(z0)), ACTIVE(z0))
F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, C, TOP

Compound Symbols:

c3, c4, c5, c6, c7, c8, c10, c11, c12, c13, c14, 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.

ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))

We considered the (Usable) Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))

And the Tuples:

ACTIVE(g(z0)) → c3(G(active(z0)), ACTIVE(z0))
F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))

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

POL(ACTIVE(x₁)) = x₁
POL(C(x₁)) = 0
POL(F(x₁)) = 0
POL(G(x₁)) = 0
POL(PROPER(x₁)) = 0
POL(TOP(x₁)) = [4]x₁
POL(a) = [4]
POL(active(x₁)) = 0
POL(c(x₁)) = 0
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(f(x₁)) = [2]x₁
POL(g(x₁)) = x₁
POL(mark(x₁)) = x₁
POL(ok(x₁)) = x₁
POL(proper(x₁)) = x₁

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(g(z0)) → c3(G(active(z0)), ACTIVE(z0))
F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))

S tuples:

ACTIVE(g(z0)) → c3(G(active(z0)), ACTIVE(z0))
F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, C, TOP

Compound Symbols:

c3, c4, c5, c6, c7, c8, c10, c11, c12, c13, c14, c2

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

Use narrowing to replace ACTIVE(g(z0)) → c3(G(active(z0)), ACTIVE(z0)) by

ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(x0)) → c3

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(x0)) → c3

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(x0)) → c3

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, PROPER, C, TOP, ACTIVE

Compound Symbols:

c4, c5, c6, c7, c8, c10, c11, c12, c13, c14, c2, c3, c3

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

Removed 1 trailing nodes:

ACTIVE(g(x0)) → c3

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, PROPER, C, TOP, ACTIVE

Compound Symbols:

c4, c5, c6, c7, c8, c10, c11, c12, c13, c14, c2, c3

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

ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))

We considered the (Usable) Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))

And the Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))

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

POL(ACTIVE(x₁)) = [4]x₁
POL(C(x₁)) = 0
POL(F(x₁)) = 0
POL(G(x₁)) = 0
POL(PROPER(x₁)) = 0
POL(TOP(x₁)) = [4]x₁
POL(a) = [4]
POL(active(x₁)) = 0
POL(c(x₁)) = 0
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(f(x₁)) = [4]x₁
POL(g(x₁)) = [4]x₁
POL(mark(x₁)) = x₁
POL(ok(x₁)) = x₁
POL(proper(x₁)) = x₁

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, PROPER, C, TOP, ACTIVE

Compound Symbols:

c4, c5, c6, c7, c8, c10, c11, c12, c13, c14, c2, c3

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

Use narrowing to replace PROPER(f(z0)) → c8(F(proper(z0)), PROPER(z0)) by

PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(a)) → c8(F(ok(a)), PROPER(a))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(x0)) → c8

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(a)) → c8(F(ok(a)), PROPER(a))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(x0)) → c8

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(a)) → c8(F(ok(a)), PROPER(a))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(x0)) → c8

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, PROPER, C, TOP, ACTIVE

Compound Symbols:

c4, c5, c6, c7, c10, c11, c12, c13, c14, c2, c3, c8, c8

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

Removed 1 trailing nodes:

PROPER(f(x0)) → c8

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(a)) → c8(F(ok(a)), PROPER(a))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(a)) → c8(F(ok(a)), PROPER(a))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, PROPER, C, TOP, ACTIVE

Compound Symbols:

c4, c5, c6, c7, c10, c11, c12, c13, c14, c2, c3, c8

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

Removed 1 trailing tuple parts

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, PROPER, C, TOP, ACTIVE

Compound Symbols:

c4, c5, c6, c7, c10, c11, c12, c13, c14, c2, c3, c8, c8

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

PROPER(f(a)) → c8(F(ok(a)))

We considered the (Usable) Rules:

proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
c(ok(z0)) → ok(c(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))

And the Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))

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

POL(ACTIVE(x₁)) = 0
POL(C(x₁)) = 0
POL(F(x₁)) = 0
POL(G(x₁)) = 0
POL(PROPER(x₁)) = [1]
POL(TOP(x₁)) = [2]x₁
POL(a) = [1]
POL(active(x₁)) = x₁
POL(c(x₁)) = 0
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(f(x₁)) = [2]x₁
POL(g(x₁)) = [4]x₁
POL(mark(x₁)) = [1] + x₁
POL(ok(x₁)) = x₁
POL(proper(x₁)) = x₁

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
PROPER(f(a)) → c8(F(ok(a)))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, PROPER, C, TOP, ACTIVE

Compound Symbols:

c4, c5, c6, c7, c10, c11, c12, c13, c14, c2, c3, c8, c8

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

Use narrowing to replace PROPER(c(z0)) → c10(C(proper(z0)), PROPER(z0)) by

PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(a)) → c10(C(ok(a)), PROPER(a))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(c(x0)) → c10

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(a)) → c10(C(ok(a)), PROPER(a))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(c(x0)) → c10

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(a)) → c10(C(ok(a)), PROPER(a))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(c(x0)) → c10

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
PROPER(f(a)) → c8(F(ok(a)))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, PROPER, C, TOP, ACTIVE

Compound Symbols:

c4, c5, c6, c7, c11, c12, c13, c14, c2, c3, c8, c8, c10, c10

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

Removed 1 trailing nodes:

PROPER(c(x0)) → c10

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(a)) → c10(C(ok(a)), PROPER(a))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(a)) → c10(C(ok(a)), PROPER(a))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
PROPER(f(a)) → c8(F(ok(a)))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, PROPER, C, TOP, ACTIVE

Compound Symbols:

c4, c5, c6, c7, c11, c12, c13, c14, c2, c3, c8, c8, c10

(31) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(c(a)) → c10(C(ok(a)))

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(c(a)) → c10(C(ok(a)))

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
PROPER(f(a)) → c8(F(ok(a)))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, PROPER, C, TOP, ACTIVE

Compound Symbols:

c4, c5, c6, c7, c11, c12, c13, c14, c2, c3, c8, c8, c10, c10

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

PROPER(c(a)) → c10(C(ok(a)))

We considered the (Usable) Rules:

proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
c(ok(z0)) → ok(c(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))

And the Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(c(a)) → c10(C(ok(a)))

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

POL(ACTIVE(x₁)) = 0
POL(C(x₁)) = 0
POL(F(x₁)) = 0
POL(G(x₁)) = 0
POL(PROPER(x₁)) = [1]
POL(TOP(x₁)) = [4]x₁
POL(a) = [4]
POL(active(x₁)) = x₁
POL(c(x₁)) = 0
POL(c10(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(f(x₁)) = [4]x₁
POL(g(x₁)) = [4]x₁
POL(mark(x₁)) = [2] + x₁
POL(ok(x₁)) = x₁
POL(proper(x₁)) = x₁

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(c(a)) → c10(C(ok(a)))

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(a)) → c10(C(ok(a)))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, PROPER, C, TOP, ACTIVE

Compound Symbols:

c4, c5, c6, c7, c11, c12, c13, c14, c2, c3, c8, c8, c10, c10

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

Use narrowing to replace PROPER(g(z0)) → c11(G(proper(z0)), PROPER(z0)) by

PROPER(g(f(z0))) → c11(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(a)) → c11(G(ok(a)), PROPER(a))
PROPER(g(c(z0))) → c11(G(c(proper(z0))), PROPER(c(z0)))
PROPER(g(g(z0))) → c11(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(x0)) → c11

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(c(a)) → c10(C(ok(a)))
PROPER(g(f(z0))) → c11(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(a)) → c11(G(ok(a)), PROPER(a))
PROPER(g(c(z0))) → c11(G(c(proper(z0))), PROPER(c(z0)))
PROPER(g(g(z0))) → c11(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(x0)) → c11

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c11(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(a)) → c11(G(ok(a)), PROPER(a))
PROPER(g(c(z0))) → c11(G(c(proper(z0))), PROPER(c(z0)))
PROPER(g(g(z0))) → c11(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(x0)) → c11

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(a)) → c10(C(ok(a)))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, C, TOP, ACTIVE, PROPER

Compound Symbols:

c4, c5, c6, c7, c12, c13, c14, c2, c3, c8, c8, c10, c10, c11, c11

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

Removed 1 trailing nodes:

PROPER(g(x0)) → c11

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(c(a)) → c10(C(ok(a)))
PROPER(g(f(z0))) → c11(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(a)) → c11(G(ok(a)), PROPER(a))
PROPER(g(c(z0))) → c11(G(c(proper(z0))), PROPER(c(z0)))
PROPER(g(g(z0))) → c11(G(g(proper(z0))), PROPER(g(z0)))

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c11(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(a)) → c11(G(ok(a)), PROPER(a))
PROPER(g(c(z0))) → c11(G(c(proper(z0))), PROPER(c(z0)))
PROPER(g(g(z0))) → c11(G(g(proper(z0))), PROPER(g(z0)))

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(a)) → c10(C(ok(a)))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, C, TOP, ACTIVE, PROPER

Compound Symbols:

c4, c5, c6, c7, c12, c13, c14, c2, c3, c8, c8, c10, c10, c11

(39) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(c(a)) → c10(C(ok(a)))
PROPER(g(f(z0))) → c11(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(c(z0))) → c11(G(c(proper(z0))), PROPER(c(z0)))
PROPER(g(g(z0))) → c11(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(a)) → c11(G(ok(a)))

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c11(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(c(z0))) → c11(G(c(proper(z0))), PROPER(c(z0)))
PROPER(g(g(z0))) → c11(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(a)) → c11(G(ok(a)))

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(a)) → c10(C(ok(a)))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, C, TOP, ACTIVE, PROPER

Compound Symbols:

c4, c5, c6, c7, c12, c13, c14, c2, c3, c8, c8, c10, c10, c11, c11

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

PROPER(g(a)) → c11(G(ok(a)))

We considered the (Usable) Rules:

proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
c(ok(z0)) → ok(c(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))

And the Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(c(a)) → c10(C(ok(a)))
PROPER(g(f(z0))) → c11(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(c(z0))) → c11(G(c(proper(z0))), PROPER(c(z0)))
PROPER(g(g(z0))) → c11(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(a)) → c11(G(ok(a)))

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

POL(ACTIVE(x₁)) = 0
POL(C(x₁)) = 0
POL(F(x₁)) = 0
POL(G(x₁)) = 0
POL(PROPER(x₁)) = [4]
POL(TOP(x₁)) = x₁
POL(a) = [1]
POL(active(x₁)) = x₁
POL(c(x₁)) = 0
POL(c10(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c12(x₁)) = x₁
POL(c13(x₁, x₂)) = x₁ + x₂
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c2(x₁, x₂)) = x₁ + x₂
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(c5(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(c7(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(c8(x₁, x₂)) = x₁ + x₂
POL(f(x₁)) = [2]x₁
POL(g(x₁)) = [2]x₁
POL(mark(x₁)) = [4] + x₁
POL(ok(x₁)) = x₁
POL(proper(x₁)) = x₁

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
C(ok(z0)) → c12(C(z0))
TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(c(a)) → c10(C(ok(a)))
PROPER(g(f(z0))) → c11(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(c(z0))) → c11(G(c(proper(z0))), PROPER(c(z0)))
PROPER(g(g(z0))) → c11(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(a)) → c11(G(ok(a)))

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c11(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(c(z0))) → c11(G(c(proper(z0))), PROPER(c(z0)))
PROPER(g(g(z0))) → c11(G(g(proper(z0))), PROPER(g(z0)))

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(a)) → c10(C(ok(a)))
PROPER(g(a)) → c11(G(ok(a)))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, C, TOP, ACTIVE, PROPER

Compound Symbols:

c4, c5, c6, c7, c12, c13, c14, c2, c3, c8, c8, c10, c10, c11, c11

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

Use narrowing to replace TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0)) by

TOP(mark(f(z0))) → c13(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(a)) → c13(TOP(ok(a)), PROPER(a))
TOP(mark(c(z0))) → c13(TOP(c(proper(z0))), PROPER(c(z0)))
TOP(mark(g(z0))) → c13(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(x0)) → c13

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(c(a)) → c10(C(ok(a)))
PROPER(g(f(z0))) → c11(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(c(z0))) → c11(G(c(proper(z0))), PROPER(c(z0)))
PROPER(g(g(z0))) → c11(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(a)) → c11(G(ok(a)))
TOP(mark(f(z0))) → c13(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(a)) → c13(TOP(ok(a)), PROPER(a))
TOP(mark(c(z0))) → c13(TOP(c(proper(z0))), PROPER(c(z0)))
TOP(mark(g(z0))) → c13(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(x0)) → c13

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c11(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(c(z0))) → c11(G(c(proper(z0))), PROPER(c(z0)))
PROPER(g(g(z0))) → c11(G(g(proper(z0))), PROPER(g(z0)))

K tuples:

TOP(mark(z0)) → c13(TOP(proper(z0)), PROPER(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(a)) → c10(C(ok(a)))
PROPER(g(a)) → c11(G(ok(a)))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, C, TOP, ACTIVE, PROPER

Compound Symbols:

c4, c5, c6, c7, c12, c14, c2, c3, c8, c8, c10, c10, c11, c11, c13, c13

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

Removed 1 trailing nodes:

TOP(mark(x0)) → c13

(46) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(c(a)) → c10(C(ok(a)))
PROPER(g(f(z0))) → c11(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(c(z0))) → c11(G(c(proper(z0))), PROPER(c(z0)))
PROPER(g(g(z0))) → c11(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(a)) → c11(G(ok(a)))
TOP(mark(f(z0))) → c13(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(a)) → c13(TOP(ok(a)), PROPER(a))
TOP(mark(c(z0))) → c13(TOP(c(proper(z0))), PROPER(c(z0)))
TOP(mark(g(z0))) → c13(TOP(g(proper(z0))), PROPER(g(z0)))

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c11(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(c(z0))) → c11(G(c(proper(z0))), PROPER(c(z0)))
PROPER(g(g(z0))) → c11(G(g(proper(z0))), PROPER(g(z0)))

K tuples:

ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(a)) → c10(C(ok(a)))
PROPER(g(a)) → c11(G(ok(a)))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, C, TOP, ACTIVE, PROPER

Compound Symbols:

c4, c5, c6, c7, c12, c14, c2, c3, c8, c8, c10, c10, c11, c11, c13

(47) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(48) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(z0)) → f(active(z0))
active(g(z0)) → g(active(z0))
f(mark(z0)) → mark(f(z0))
f(ok(z0)) → ok(f(z0))
g(mark(z0)) → mark(g(z0))
g(ok(z0)) → ok(g(z0))
proper(f(z0)) → f(proper(z0))
proper(a) → ok(a)
proper(c(z0)) → c(proper(z0))
proper(g(z0)) → g(proper(z0))
c(ok(z0)) → ok(c(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(c(a)) → c10(C(ok(a)))
PROPER(g(f(z0))) → c11(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(c(z0))) → c11(G(c(proper(z0))), PROPER(c(z0)))
PROPER(g(g(z0))) → c11(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(a)) → c11(G(ok(a)))
TOP(mark(f(z0))) → c13(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(c(z0))) → c13(TOP(c(proper(z0))), PROPER(c(z0)))
TOP(mark(g(z0))) → c13(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(a)) → c13(TOP(ok(a)))

S tuples:

F(mark(z0)) → c4(F(z0))
F(ok(z0)) → c5(F(z0))
G(mark(z0)) → c6(G(z0))
G(ok(z0)) → c7(G(z0))
C(ok(z0)) → c12(C(z0))
TOP(ok(z0)) → c14(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0))) → c2(F(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(f(g(z0))) → c2(F(g(active(z0))), ACTIVE(g(z0)))
ACTIVE(g(f(z0))) → c3(G(f(active(z0))), ACTIVE(f(z0)))
ACTIVE(g(g(z0))) → c3(G(g(active(z0))), ACTIVE(g(z0)))
PROPER(f(f(z0))) → c8(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(c(z0))) → c8(F(c(proper(z0))), PROPER(c(z0)))
PROPER(f(g(z0))) → c8(F(g(proper(z0))), PROPER(g(z0)))
PROPER(c(f(z0))) → c10(C(f(proper(z0))), PROPER(f(z0)))
PROPER(c(c(z0))) → c10(C(c(proper(z0))), PROPER(c(z0)))
PROPER(c(g(z0))) → c10(C(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c11(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(c(z0))) → c11(G(c(proper(z0))), PROPER(c(z0)))
PROPER(g(g(z0))) → c11(G(g(proper(z0))), PROPER(g(z0)))

K tuples:

ACTIVE(f(f(f(a)))) → c2(F(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
ACTIVE(g(f(f(a)))) → c3(G(mark(c(f(g(f(a)))))), ACTIVE(f(f(a))))
PROPER(f(a)) → c8(F(ok(a)))
PROPER(c(a)) → c10(C(ok(a)))
PROPER(g(a)) → c11(G(ok(a)))

Defined Rule Symbols:

active, f, g, proper, c, top

Defined Pair Symbols:

F, G, C, TOP, ACTIVE, PROPER

Compound Symbols:

c4, c5, c6, c7, c12, c14, c2, c3, c8, c8, c10, c10, c11, c11, c13, c13

(49) CpxTrsMatchBoundsProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 2.
The certificate found is represented by the following graph.

Start state: 3095
Accept states: [3096, 3097, 3098, 3099, 3100, 3101]
Transitions:
3095→3096[active_1|0]
3095→3097[f_1|0]
3095→3098[g_1|0]
3095→3099[proper_1|0]
3095→3100[c_1|0]
3095→3101[top_1|0]
3095→3095[a|0, mark_1|0, ok_1|0]
3095→3102[a|1]
3095→3103[f_1|1]
3095→3104[g_1|1]
3095→3105[proper_1|1]
3095→3106[f_1|1]
3095→3107[g_1|1]
3095→3108[c_1|1]
3095→3109[active_1|1]
3102→3099[ok_1|1]
3102→3105[ok_1|1]
3102→3110[active_1|2]
3103→3097[mark_1|1]
3103→3103[mark_1|1]
3103→3106[mark_1|1]
3104→3098[mark_1|1]
3104→3104[mark_1|1]
3104→3107[mark_1|1]
3105→3101[top_1|1]
3106→3097[ok_1|1]
3106→3103[ok_1|1]
3106→3106[ok_1|1]
3107→3098[ok_1|1]
3107→3104[ok_1|1]
3107→3107[ok_1|1]
3108→3100[ok_1|1]
3108→3108[ok_1|1]
3109→3101[top_1|1]
3110→3101[top_1|2]

(0) Obligation:

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

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

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

(12) Obligation:

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

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

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

(24) Obligation:

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

(26) Obligation:

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

(28) Obligation:

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

(30) Obligation:

(31) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(32) Obligation:

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

(34) Obligation:

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

(36) Obligation:

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

(38) Obligation:

(39) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(40) Obligation:

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

(42) Obligation:

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

(44) Obligation:

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

(46) Obligation:

(47) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(48) Obligation:

(49) CpxTrsMatchBoundsProof (EQUIVALENT transformation)

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