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))), 361 ms)
    ↳6 CdtProblem
    ↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳8 CdtProblem
    ↳9 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳12 CdtProblem
    ↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 151 ms)
    ↳14 CdtProblem
    ↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳16 CdtProblem
    ↳17 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳18 CdtProblem
    ↳19 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳20 CdtProblem
    ↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 138 ms)
    ↳22 CdtProblem
    ↳23 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳24 CdtProblem
    ↳25 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳26 CdtProblem
    ↳27 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳28 CdtProblem
    ↳29 CdtNarrowingProof (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))), 54 ms)
    ↳34 CdtProblem
    ↳35 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 42 ms)
    ↳36 CdtProblem
    ↳37 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 22 ms)
    ↳38 CdtProblem
    ↳39 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 102 ms)
    ↳40 CdtProblem
    ↳41 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳42 CdtProblem
    ↳43 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳44 CdtProblem
    ↳45 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 100 ms)
    ↳46 CdtProblem
    ↳47 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳48 CdtProblem
    ↳49 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳50 CdtProblem
    ↳51 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 398 ms)
    ↳52 CdtProblem
    ↳53 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳54 CdtProblem
    ↳55 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳56 CdtProblem
    ↳57 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 170 ms)
    ↳58 CdtProblem
↳59 CpxTrsMatchBoundsProof (⇔, 0 ms)
↳60 BOUNDS(O(1), O(n^1))

(0) Obligation:

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

active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(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(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(c) → c1(F(g(c)), G(c))
ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
S tuples:

ACTIVE(c) → c1(F(g(c)), G(c))
ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
K tuples:none
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, PROPER, F, G, TOP

Compound Symbols:

c1, c2, c4, c5, c6, c7, c8, c9

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

Removed 1 trailing nodes:

ACTIVE(c) → c1(F(g(c)), G(c))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
K tuples:none
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, PROPER, F, G, TOP

Compound Symbols:

c2, c4, c5, c6, c7, c8, c9

(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)) → c8(TOP(proper(z0)), PROPER(z0))
We considered the (Usable) Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = 0   
POL(TOP(x1)) = x1   
POL(active(x1)) = x1   
POL(c) = [2]   
POL(c2(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = [1]   
POL(g(x1)) = 0   
POL(mark(x1)) = [1] + x1   
POL(ok(x1)) = x1   
POL(proper(x1)) = x1   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
K tuples:

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, PROPER, F, G, TOP

Compound Symbols:

c2, c4, c5, c6, c7, c8, c9

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

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

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

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(x0)) → c4
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(x0)) → c4
K tuples:

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, PROPER, F, G, TOP

Compound Symbols:

c2, c5, c6, c7, c8, c9, c4, c4

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

Removed 1 trailing nodes:

PROPER(f(x0)) → c4

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
K tuples:

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, PROPER, F, G, TOP

Compound Symbols:

c2, c5, c6, c7, c8, c9, c4

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

Removed 1 trailing tuple parts

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
K tuples:

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, PROPER, F, G, TOP

Compound Symbols:

c2, c5, c6, c7, c8, c9, c4, c4

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

PROPER(f(c)) → c4(F(ok(c)))
We considered the (Usable) Rules:

proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = [1]   
POL(TOP(x1)) = [2]x1   
POL(active(x1)) = x1   
POL(c) = [5]   
POL(c2(x1)) = x1   
POL(c4(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = [4]x1   
POL(g(x1)) = [1]   
POL(mark(x1)) = [1] + x1   
POL(ok(x1)) = x1   
POL(proper(x1)) = x1   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
K tuples:

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
PROPER(f(c)) → c4(F(ok(c)))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, PROPER, F, G, TOP

Compound Symbols:

c2, c5, c6, c7, c8, c9, c4, c4

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

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

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

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(x0)) → c5
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(x0)) → c5
K tuples:

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
PROPER(f(c)) → c4(F(ok(c)))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, TOP, PROPER

Compound Symbols:

c2, c6, c7, c8, c9, c4, c4, c5, c5

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

Removed 1 trailing nodes:

PROPER(g(x0)) → c5

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
K tuples:

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
PROPER(f(c)) → c4(F(ok(c)))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, TOP, PROPER

Compound Symbols:

c2, c6, c7, c8, c9, c4, c4, c5

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

Removed 1 trailing tuple parts

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
K tuples:

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
PROPER(f(c)) → c4(F(ok(c)))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, TOP, PROPER

Compound Symbols:

c2, c6, c7, c8, c9, c4, c4, c5, c5

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

PROPER(g(c)) → c5(G(ok(c)))
We considered the (Usable) Rules:

proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = [1]   
POL(TOP(x1)) = x1   
POL(active(x1)) = x1   
POL(c) = [2]   
POL(c2(x1)) = x1   
POL(c4(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = [1]   
POL(g(x1)) = 0   
POL(mark(x1)) = [1] + x1   
POL(ok(x1)) = x1   
POL(proper(x1)) = x1   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
K tuples:

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, TOP, PROPER

Compound Symbols:

c2, c6, c7, c8, c9, c4, c4, c5, c5

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

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

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

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(x0)) → c8
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
K tuples:

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, TOP, PROPER

Compound Symbols:

c2, c6, c7, c9, c4, c4, c5, c5, c8, c8

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

Removed 1 trailing nodes:

TOP(mark(x0)) → c8

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, TOP, PROPER

Compound Symbols:

c2, c6, c7, c9, c4, c4, c5, c5, c8

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

Removed 1 trailing tuple parts

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, TOP, PROPER

Compound Symbols:

c2, c6, c7, c9, c4, c4, c5, c5, c8, c8

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

Use narrowing to replace TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) by

TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c4, c5, c5, c8, c8, c9, c9

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

Removed 1 trailing tuple parts

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c4, c5, c5, c8, c8, c9, c9, c9

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

TOP(ok(x0)) → c9
We considered the (Usable) Rules:

proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = 0   
POL(TOP(x1)) = [4]   
POL(c) = [4]   
POL(c2(x1)) = x1   
POL(c4(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9) = 0   
POL(c9(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = [4] + [4]x1   
POL(g(x1)) = [1] + [3]x1   
POL(mark(x1)) = [3]   
POL(ok(x1)) = [5]   
POL(proper(x1)) = [2]x1   

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(ok(x0)) → c9
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c4, c5, c5, c8, c8, c9, c9, c9

(35) 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(g(z0))) → c2(G(z0))
We considered the (Usable) Rules:

proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = [4]x1   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = 0   
POL(TOP(x1)) = [4]x1   
POL(c) = [4]   
POL(c2(x1)) = x1   
POL(c4(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9) = 0   
POL(c9(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = [4]   
POL(g(x1)) = 0   
POL(mark(x1)) = x1   
POL(ok(x1)) = x1   
POL(proper(x1)) = [4] + [4]x1   

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(ok(x0)) → c9
ACTIVE(f(g(z0))) → c2(G(z0))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c4, c5, c5, c8, c8, c9, c9, c9

(37) 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(ok(c)) → c9(TOP(mark(f(g(c)))))
We considered the (Usable) Rules:

proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = 0   
POL(TOP(x1)) = x1   
POL(c) = [1]   
POL(c2(x1)) = x1   
POL(c4(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9) = 0   
POL(c9(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = 0   
POL(g(x1)) = 0   
POL(mark(x1)) = x1   
POL(ok(x1)) = x1   
POL(proper(x1)) = [2] + [4]x1   

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(ok(x0)) → c9
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c4, c5, c5, c8, c8, c9, c9, c9

(39) 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(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
We considered the (Usable) Rules:

proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = 0   
POL(TOP(x1)) = [4]x1   
POL(c) = [5]   
POL(c2(x1)) = x1   
POL(c4(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9) = 0   
POL(c9(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = [2]x1   
POL(g(x1)) = [2]   
POL(mark(x1)) = x1   
POL(ok(x1)) = x1   
POL(proper(x1)) = x1   

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(ok(x0)) → c9
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c4, c5, c5, c8, c8, c9, c9, c9

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

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

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

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(f(x0))) → c4
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(f(x0))) → c4
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(ok(x0)) → c9
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c4, c5, c5, c8, c8, c9, c9, c9, c4

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

Removed 1 trailing nodes:

TOP(ok(x0)) → c9

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(f(x0))) → c4
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(f(x0))) → c4
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c4, c5, c5, c8, c8, c9, c9, c4

(45) 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(f(x0))) → c4
We considered the (Usable) Rules:

proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(f(x0))) → c4
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = [4] + x1   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = [1]   
POL(TOP(x1)) = [4]x1   
POL(c) = [5]   
POL(c2(x1)) = x1   
POL(c4) = 0   
POL(c4(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = [4]   
POL(g(x1)) = 0   
POL(mark(x1)) = [1] + x1   
POL(ok(x1)) = x1   
POL(proper(x1)) = 0   

(46) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(f(x0))) → c4
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(f(x0))) → c4
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c4, c5, c5, c8, c8, c9, c9, c4

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

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

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

(48) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(f(x0))) → c4
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(f(g(x0))) → c4
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(f(g(x0))) → c4
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(f(x0))) → c4
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c5, c5, c8, c8, c9, c9, c4, c4

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

Removed 1 trailing nodes:

PROPER(f(f(x0))) → c4

(50) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(f(g(x0))) → c4
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(f(g(x0))) → c4
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c5, c5, c8, c8, c9, c9, c4, c4

(51) 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(g(x0))) → c4
We considered the (Usable) Rules:

proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(f(g(x0))) → c4
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = [2]   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = [1]   
POL(TOP(x1)) = [2]x1   
POL(c) = [4]   
POL(c2(x1)) = x1   
POL(c4) = 0   
POL(c4(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = [2]   
POL(g(x1)) = 0   
POL(mark(x1)) = [1] + x1   
POL(ok(x1)) = x1   
POL(proper(x1)) = 0   

(52) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(f(g(x0))) → c4
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(g(x0))) → c4
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c5, c5, c8, c8, c9, c9, c4, c4

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

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

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

(54) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(f(g(x0))) → c4
PROPER(g(f(c))) → c5(G(f(ok(c))), PROPER(f(c)))
PROPER(g(f(f(z0)))) → c5(G(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(g(f(g(z0)))) → c5(G(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(g(f(x0))) → c5
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(g(f(c))) → c5(G(f(ok(c))), PROPER(f(c)))
PROPER(g(f(f(z0)))) → c5(G(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(g(f(g(z0)))) → c5(G(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(g(f(x0))) → c5
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(g(x0))) → c4
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c5, c5, c8, c8, c9, c9, c4, c4, c5

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

Removed 1 trailing nodes:

PROPER(f(g(x0))) → c4

(56) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(g(f(c))) → c5(G(f(ok(c))), PROPER(f(c)))
PROPER(g(f(f(z0)))) → c5(G(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(g(f(g(z0)))) → c5(G(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(g(f(x0))) → c5
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(g(f(c))) → c5(G(f(ok(c))), PROPER(f(c)))
PROPER(g(f(f(z0)))) → c5(G(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(g(f(g(z0)))) → c5(G(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(g(f(x0))) → c5
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c5, c5, c8, c8, c9, c9, c4, c5

(57) 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(f(x0))) → c5
We considered the (Usable) Rules:

proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(g(f(c))) → c5(G(f(ok(c))), PROPER(f(c)))
PROPER(g(f(f(z0)))) → c5(G(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(g(f(g(z0)))) → c5(G(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(g(f(x0))) → c5
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = [4]   
POL(TOP(x1)) = [2]x1   
POL(c) = [4]   
POL(c2(x1)) = x1   
POL(c4(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5) = 0   
POL(c5(x1)) = x1   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9(x1)) = x1   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = [2]   
POL(g(x1)) = 0   
POL(mark(x1)) = [2] + x1   
POL(ok(x1)) = x1   
POL(proper(x1)) = 0   

(58) Obligation:

Complexity Dependency Tuples Problem
Rules:

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

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(g(f(c))) → c5(G(f(ok(c))), PROPER(f(c)))
PROPER(g(f(f(z0)))) → c5(G(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(g(f(g(z0)))) → c5(G(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(g(f(x0))) → c5
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(g(f(c))) → c5(G(f(ok(c))), PROPER(f(c)))
PROPER(g(f(f(z0)))) → c5(G(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(g(f(g(z0)))) → c5(G(f(g(proper(z0)))), PROPER(f(g(z0))))
K tuples:

PROPER(f(c)) → c4(F(ok(c)))
PROPER(g(c)) → c5(G(ok(c)))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(g(f(x0))) → c5
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c5, c5, c8, c8, c9, c9, c4, c5

(59) 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 6.
The certificate found is represented by the following graph.
Start state: 2933
Accept states: [2934, 2935, 2936, 2937, 2938]
Transitions:
2933→2934[active_1|0]
2933→2935[proper_1|0]
2933→2936[f_1|0]
2933→2937[g_1|0]
2933→2938[top_1|0]
2933→2933[c|0, mark_1|0, ok_1|0]
2933→2939[c|1]
2933→2942[c|1]
2933→2943[f_1|1]
2933→2944[g_1|1]
2933→2945[active_1|1]
2933→2946[proper_1|1]
2933→2949[c|2]
2933→2955[c|2]
2933→2959[c|3]
2933→2971[c|4]
2939→2940[g_1|1]
2939→2953[proper_1|2]
2940→2941[f_1|1]
2940→2952[proper_1|2]
2941→2934[mark_1|1]
2941→2945[mark_1|1]
2941→2947[proper_1|2]
2942→2935[ok_1|1]
2942→2946[ok_1|1]
2942→2948[active_1|2]
2943→2936[ok_1|1]
2943→2943[ok_1|1]
2944→2937[ok_1|1]
2944→2944[ok_1|1]
2945→2938[top_1|1]
2946→2938[top_1|1]
2947→2938[top_1|2]
2948→2938[top_1|2]
2949→2950[g_1|2]
2949→2957[proper_1|3]
2950→2951[f_1|2]
2950→2956[proper_1|3]
2951→2948[mark_1|2]
2951→2954[proper_1|3]
2952→2947[f_1|2]
2953→2952[g_1|2]
2954→2938[top_1|3]
2955→2953[ok_1|2]
2955→2958[g_1|3]
2955→2963[g_1|4]
2955→2967[proper_1|5]
2956→2954[f_1|3]
2957→2956[g_1|3]
2958→2952[ok_1|3]
2958→2960[f_1|3]
2959→2957[ok_1|3]
2959→2961[g_1|4]
2959→2968[g_1|5]
2959→2967[ok_1|3]
2959→2970[proper_1|6]
2960→2947[ok_1|3]
2960→2962[active_1|3]
2961→2956[ok_1|4]
2961→2964[f_1|4]
2961→2965[ok_1|4]
2961→2972[active_1|5]
2962→2938[top_1|3]
2963→2962[mark_1|4]
2963→2965[proper_1|4]
2964→2954[ok_1|4]
2964→2966[active_1|4]
2965→2938[top_1|4]
2966→2938[top_1|4]
2967→2965[g_1|5]
2968→2966[mark_1|5]
2968→2969[proper_1|5]
2969→2938[top_1|5]
2970→2969[g_1|6]
2971→2970[ok_1|4]
2971→2973[g_1|5]
2972→2938[top_1|5]
2973→2969[ok_1|5]
2973→2974[active_1|6]
2974→2938[top_1|6]

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