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

(0) Obligation:

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

active(f(X, X)) → mark(f(a, b))
active(b) → mark(a)
active(f(X1, X2)) → f(active(X1), X2)
f(mark(X1), X2) → mark(f(X1, X2))
proper(f(X1, X2)) → f(proper(X1), proper(X2))
proper(a) → ok(a)
proper(b) → ok(b)
f(ok(X1), ok(X2)) → ok(f(X1, X2))
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(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(z0, z0)) → c(F(a, b))
ACTIVE(f(z0, z1)) → c2(F(active(z0), z1), ACTIVE(z0))
F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))

S tuples:

ACTIVE(f(z0, z0)) → c(F(a, b))
ACTIVE(f(z0, z1)) → c2(F(active(z0), z1), ACTIVE(z0))
F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
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, f, proper, top

Defined Pair Symbols:

ACTIVE, F, PROPER, TOP

Compound Symbols:

c, c2, c3, c4, c5, c8, c9

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

Removed 1 trailing nodes:

ACTIVE(f(z0, z0)) → c(F(a, b))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(z0, z1)) → c2(F(active(z0), z1), ACTIVE(z0))
F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))

S tuples:

ACTIVE(f(z0, z1)) → c2(F(active(z0), z1), ACTIVE(z0))
F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
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, f, proper, top

Defined Pair Symbols:

ACTIVE, F, PROPER, TOP

Compound Symbols:

c2, c3, c4, c5, c8, c9

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

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

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

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
ACTIVE(f(x0, x1)) → c2

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
ACTIVE(f(x0, x1)) → c2

K tuples:none
Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, PROPER, TOP, ACTIVE

Compound Symbols:

c3, c4, c5, c8, c9, c2, c2

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

Removed 1 trailing nodes:

ACTIVE(f(x0, x1)) → c2

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))

K tuples:none
Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, PROPER, TOP, ACTIVE

Compound Symbols:

c3, c4, c5, c8, c9, c2

(9) 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(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))

We considered the (Usable) Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)

And the Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))

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

POL(ACTIVE(x₁)) = x₁   
POL(F(x₁, x₂)) = 0   
POL(PROPER(x₁)) = 0   
POL(TOP(x₁)) = x₁   
POL(a) = 0   
POL(active(x₁)) = 0   
POL(b) = [1]   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c5(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c8(x₁, x₂)) = x₁ + x₂   
POL(c9(x₁, x₂)) = x₁ + x₂   
POL(f(x₁, x₂)) = [2]x₁   
POL(mark(x₁)) = x₁   
POL(ok(x₁)) = x₁   
POL(proper(x₁)) = x₁   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))

K tuples:

ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, PROPER, TOP, ACTIVE

Compound Symbols:

c3, c4, c5, c8, c9, c2

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

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

PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
PROPER(f(x0, x1)) → c5

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
PROPER(f(x0, x1)) → c5

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
PROPER(f(x0, x1)) → c5

K tuples:

ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, TOP, ACTIVE, PROPER

Compound Symbols:

c3, c4, c8, c9, c2, c5, c5

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

Removed 1 trailing nodes:

PROPER(f(x0, x1)) → c5

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))

K tuples:

ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, TOP, ACTIVE, PROPER

Compound Symbols:

c3, c4, c8, c9, c2, c5

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

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

TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a))
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))
TOP(mark(x0)) → c8

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a))
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))
TOP(mark(x0)) → c8

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a))
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))
TOP(mark(x0)) → c8

K tuples:

ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, TOP, ACTIVE, PROPER

Compound Symbols:

c3, c4, c9, c2, c5, c8, c8

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

Removed 1 trailing nodes:

TOP(mark(x0)) → c8

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a))
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a))
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))

K tuples:

ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, TOP, ACTIVE, PROPER

Compound Symbols:

c3, c4, c9, c2, c5, c8

(19) 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(b)) → c8(TOP(ok(b)), PROPER(b))

We considered the (Usable) Rules:

proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)

And the Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a))
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))

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

POL(ACTIVE(x₁)) = 0   
POL(F(x₁, x₂)) = 0   
POL(PROPER(x₁)) = 0   
POL(TOP(x₁)) = [2]x₁   
POL(a) = 0   
POL(active(x₁)) = 0   
POL(b) = [2]   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c5(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c8(x₁, x₂)) = x₁ + x₂   
POL(c9(x₁, x₂)) = x₁ + x₂   
POL(f(x₁, x₂)) = 0   
POL(mark(x₁)) = x₁   
POL(ok(x₁)) = 0   
POL(proper(x₁)) = 0   

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a))
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a))

K tuples:

ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, TOP, ACTIVE, PROPER

Compound Symbols:

c3, c4, c9, c2, c5, c8

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

TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a))

We considered the (Usable) Rules:

proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)

And the Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a))
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))

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

POL(ACTIVE(x₁)) = 0   
POL(F(x₁, x₂)) = 0   
POL(PROPER(x₁)) = 0   
POL(TOP(x₁)) = [2]x₁   
POL(a) = 0   
POL(active(x₁)) = x₁   
POL(b) = [1]   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c5(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c8(x₁, x₂)) = x₁ + x₂   
POL(c9(x₁, x₂)) = x₁ + x₂   
POL(f(x₁, x₂)) = [1]   
POL(mark(x₁)) = [1]   
POL(ok(x₁)) = x₁   
POL(proper(x₁)) = 0   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a))
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))

K tuples:

ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, TOP, ACTIVE, PROPER

Compound Symbols:

c3, c4, c9, c2, c5, c8

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

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

TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(b)) → c9(TOP(mark(a)), ACTIVE(b))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
TOP(ok(x0)) → c9

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a))
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(b)) → c9(TOP(mark(a)), ACTIVE(b))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
TOP(ok(x0)) → c9

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(b)) → c9(TOP(mark(a)), ACTIVE(b))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
TOP(ok(x0)) → c9

K tuples:

ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, ACTIVE, PROPER, TOP

Compound Symbols:

c3, c4, c2, c5, c8, c9, c9

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

Removed 4 trailing nodes:

TOP(ok(x0)) → c9
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a))
TOP(ok(b)) → c9(TOP(mark(a)), ACTIVE(b))
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))

K tuples:

ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, ACTIVE, PROPER, TOP

Compound Symbols:

c3, c4, c2, c5, c8, c9

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

Use narrowing to replace ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b)) by

ACTIVE(f(b, x0)) → c2(F(mark(a), x0))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
ACTIVE(f(b, x0)) → c2(F(mark(a), x0))

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))

K tuples:

ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, ACTIVE, PROPER, TOP

Compound Symbols:

c3, c4, c2, c5, c8, c9, c2

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

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

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

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
ACTIVE(f(b, x0)) → c2(F(mark(a), x0))
ACTIVE(f(f(f(z0, z0), x1), x2)) → c2(F(f(mark(f(a, b)), x1), x2), ACTIVE(f(f(z0, z0), x1)))
ACTIVE(f(f(b, x1), x2)) → c2(F(f(mark(a), x1), x2), ACTIVE(f(b, x1)))
ACTIVE(f(f(f(z0, z1), x1), x2)) → c2(F(f(f(active(z0), z1), x1), x2), ACTIVE(f(f(z0, z1), x1)))
ACTIVE(f(f(x0, x1), x2)) → c2

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
ACTIVE(f(f(f(z0, z0), x1), x2)) → c2(F(f(mark(f(a, b)), x1), x2), ACTIVE(f(f(z0, z0), x1)))
ACTIVE(f(f(b, x1), x2)) → c2(F(f(mark(a), x1), x2), ACTIVE(f(b, x1)))
ACTIVE(f(f(f(z0, z1), x1), x2)) → c2(F(f(f(active(z0), z1), x1), x2), ACTIVE(f(f(z0, z1), x1)))
ACTIVE(f(f(x0, x1), x2)) → c2

K tuples:

ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, ACTIVE, PROPER, TOP

Compound Symbols:

c3, c4, c2, c5, c8, c9, c2, c2

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

Removed 1 trailing nodes:

ACTIVE(f(f(x0, x1), x2)) → c2

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
ACTIVE(f(b, x0)) → c2(F(mark(a), x0))
ACTIVE(f(f(f(z0, z0), x1), x2)) → c2(F(f(mark(f(a, b)), x1), x2), ACTIVE(f(f(z0, z0), x1)))
ACTIVE(f(f(b, x1), x2)) → c2(F(f(mark(a), x1), x2), ACTIVE(f(b, x1)))
ACTIVE(f(f(f(z0, z1), x1), x2)) → c2(F(f(f(active(z0), z1), x1), x2), ACTIVE(f(f(z0, z1), x1)))

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
ACTIVE(f(f(f(z0, z0), x1), x2)) → c2(F(f(mark(f(a, b)), x1), x2), ACTIVE(f(f(z0, z0), x1)))
ACTIVE(f(f(b, x1), x2)) → c2(F(f(mark(a), x1), x2), ACTIVE(f(b, x1)))
ACTIVE(f(f(f(z0, z1), x1), x2)) → c2(F(f(f(active(z0), z1), x1), x2), ACTIVE(f(f(z0, z1), x1)))

K tuples:none
Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, ACTIVE, PROPER, TOP

Compound Symbols:

c3, c4, c2, c5, c8, c9, c2

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

ACTIVE(f(f(b, x1), x2)) → c2(F(f(mark(a), x1), x2), ACTIVE(f(b, x1)))

We considered the (Usable) Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)

And the Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
ACTIVE(f(b, x0)) → c2(F(mark(a), x0))
ACTIVE(f(f(f(z0, z0), x1), x2)) → c2(F(f(mark(f(a, b)), x1), x2), ACTIVE(f(f(z0, z0), x1)))
ACTIVE(f(f(b, x1), x2)) → c2(F(f(mark(a), x1), x2), ACTIVE(f(b, x1)))
ACTIVE(f(f(f(z0, z1), x1), x2)) → c2(F(f(f(active(z0), z1), x1), x2), ACTIVE(f(f(z0, z1), x1)))

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

POL(ACTIVE(x₁)) = x₁   
POL(F(x₁, x₂)) = 0   
POL(PROPER(x₁)) = 0   
POL(TOP(x₁)) = x₁   
POL(a) = 0   
POL(active(x₁)) = 0   
POL(b) = [4]   
POL(c2(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c5(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(c8(x₁, x₂)) = x₁ + x₂   
POL(c9(x₁, x₂)) = x₁ + x₂   
POL(f(x₁, x₂)) = [4]x₁   
POL(mark(x₁)) = x₁   
POL(ok(x₁)) = x₁   
POL(proper(x₁)) = x₁   

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
ACTIVE(f(b, x0)) → c2(F(mark(a), x0))
ACTIVE(f(f(f(z0, z0), x1), x2)) → c2(F(f(mark(f(a, b)), x1), x2), ACTIVE(f(f(z0, z0), x1)))
ACTIVE(f(f(b, x1), x2)) → c2(F(f(mark(a), x1), x2), ACTIVE(f(b, x1)))
ACTIVE(f(f(f(z0, z1), x1), x2)) → c2(F(f(f(active(z0), z1), x1), x2), ACTIVE(f(f(z0, z1), x1)))

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
ACTIVE(f(f(f(z0, z0), x1), x2)) → c2(F(f(mark(f(a, b)), x1), x2), ACTIVE(f(f(z0, z0), x1)))
ACTIVE(f(f(f(z0, z1), x1), x2)) → c2(F(f(f(active(z0), z1), x1), x2), ACTIVE(f(f(z0, z1), x1)))

K tuples:

ACTIVE(f(f(b, x1), x2)) → c2(F(f(mark(a), x1), x2), ACTIVE(f(b, x1)))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, ACTIVE, PROPER, TOP

Compound Symbols:

c3, c4, c2, c5, c8, c9, c2

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

Use narrowing to replace PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) by

PROPER(f(x0, f(x1, f(z0, z1)))) → c5(F(proper(x0), f(proper(x1), f(proper(z0), proper(z1)))), PROPER(x0), PROPER(f(x1, f(z0, z1))))
PROPER(f(x0, f(x1, a))) → c5(F(proper(x0), f(proper(x1), ok(a))), PROPER(x0), PROPER(f(x1, a)))
PROPER(f(x0, f(x1, b))) → c5(F(proper(x0), f(proper(x1), ok(b))), PROPER(x0), PROPER(f(x1, b)))
PROPER(f(x0, f(f(z0, z1), x2))) → c5(F(proper(x0), f(f(proper(z0), proper(z1)), proper(x2))), PROPER(x0), PROPER(f(f(z0, z1), x2)))
PROPER(f(x0, f(a, x2))) → c5(F(proper(x0), f(ok(a), proper(x2))), PROPER(x0), PROPER(f(a, x2)))
PROPER(f(x0, f(b, x2))) → c5(F(proper(x0), f(ok(b), proper(x2))), PROPER(x0), PROPER(f(b, x2)))
PROPER(f(f(z0, z1), f(x1, x2))) → c5(F(f(proper(z0), proper(z1)), f(proper(x1), proper(x2))), PROPER(f(z0, z1)), PROPER(f(x1, x2)))
PROPER(f(a, f(x1, x2))) → c5(F(ok(a), f(proper(x1), proper(x2))), PROPER(a), PROPER(f(x1, x2)))
PROPER(f(b, f(x1, x2))) → c5(F(ok(b), f(proper(x1), proper(x2))), PROPER(b), PROPER(f(x1, x2)))
PROPER(f(x0, f(x1, x2))) → c5

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
ACTIVE(f(b, x0)) → c2(F(mark(a), x0))
ACTIVE(f(f(f(z0, z0), x1), x2)) → c2(F(f(mark(f(a, b)), x1), x2), ACTIVE(f(f(z0, z0), x1)))
ACTIVE(f(f(b, x1), x2)) → c2(F(f(mark(a), x1), x2), ACTIVE(f(b, x1)))
ACTIVE(f(f(f(z0, z1), x1), x2)) → c2(F(f(f(active(z0), z1), x1), x2), ACTIVE(f(f(z0, z1), x1)))
PROPER(f(x0, f(x1, f(z0, z1)))) → c5(F(proper(x0), f(proper(x1), f(proper(z0), proper(z1)))), PROPER(x0), PROPER(f(x1, f(z0, z1))))
PROPER(f(x0, f(x1, a))) → c5(F(proper(x0), f(proper(x1), ok(a))), PROPER(x0), PROPER(f(x1, a)))
PROPER(f(x0, f(x1, b))) → c5(F(proper(x0), f(proper(x1), ok(b))), PROPER(x0), PROPER(f(x1, b)))
PROPER(f(x0, f(f(z0, z1), x2))) → c5(F(proper(x0), f(f(proper(z0), proper(z1)), proper(x2))), PROPER(x0), PROPER(f(f(z0, z1), x2)))
PROPER(f(x0, f(a, x2))) → c5(F(proper(x0), f(ok(a), proper(x2))), PROPER(x0), PROPER(f(a, x2)))
PROPER(f(x0, f(b, x2))) → c5(F(proper(x0), f(ok(b), proper(x2))), PROPER(x0), PROPER(f(b, x2)))
PROPER(f(f(z0, z1), f(x1, x2))) → c5(F(f(proper(z0), proper(z1)), f(proper(x1), proper(x2))), PROPER(f(z0, z1)), PROPER(f(x1, x2)))
PROPER(f(a, f(x1, x2))) → c5(F(ok(a), f(proper(x1), proper(x2))), PROPER(a), PROPER(f(x1, x2)))
PROPER(f(b, f(x1, x2))) → c5(F(ok(b), f(proper(x1), proper(x2))), PROPER(b), PROPER(f(x1, x2)))
PROPER(f(x0, f(x1, x2))) → c5

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
ACTIVE(f(f(f(z0, z0), x1), x2)) → c2(F(f(mark(f(a, b)), x1), x2), ACTIVE(f(f(z0, z0), x1)))
ACTIVE(f(f(f(z0, z1), x1), x2)) → c2(F(f(f(active(z0), z1), x1), x2), ACTIVE(f(f(z0, z1), x1)))
PROPER(f(x0, f(x1, f(z0, z1)))) → c5(F(proper(x0), f(proper(x1), f(proper(z0), proper(z1)))), PROPER(x0), PROPER(f(x1, f(z0, z1))))
PROPER(f(x0, f(x1, a))) → c5(F(proper(x0), f(proper(x1), ok(a))), PROPER(x0), PROPER(f(x1, a)))
PROPER(f(x0, f(x1, b))) → c5(F(proper(x0), f(proper(x1), ok(b))), PROPER(x0), PROPER(f(x1, b)))
PROPER(f(x0, f(f(z0, z1), x2))) → c5(F(proper(x0), f(f(proper(z0), proper(z1)), proper(x2))), PROPER(x0), PROPER(f(f(z0, z1), x2)))
PROPER(f(x0, f(a, x2))) → c5(F(proper(x0), f(ok(a), proper(x2))), PROPER(x0), PROPER(f(a, x2)))
PROPER(f(x0, f(b, x2))) → c5(F(proper(x0), f(ok(b), proper(x2))), PROPER(x0), PROPER(f(b, x2)))
PROPER(f(f(z0, z1), f(x1, x2))) → c5(F(f(proper(z0), proper(z1)), f(proper(x1), proper(x2))), PROPER(f(z0, z1)), PROPER(f(x1, x2)))
PROPER(f(a, f(x1, x2))) → c5(F(ok(a), f(proper(x1), proper(x2))), PROPER(a), PROPER(f(x1, x2)))
PROPER(f(b, f(x1, x2))) → c5(F(ok(b), f(proper(x1), proper(x2))), PROPER(b), PROPER(f(x1, x2)))
PROPER(f(x0, f(x1, x2))) → c5

K tuples:

ACTIVE(f(f(b, x1), x2)) → c2(F(f(mark(a), x1), x2), ACTIVE(f(b, x1)))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, ACTIVE, PROPER, TOP

Compound Symbols:

c3, c4, c2, c5, c8, c9, c2, c5

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

Removed 1 trailing nodes:

PROPER(f(x0, f(x1, x2))) → c5

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
ACTIVE(f(b, x0)) → c2(F(mark(a), x0))
ACTIVE(f(f(f(z0, z0), x1), x2)) → c2(F(f(mark(f(a, b)), x1), x2), ACTIVE(f(f(z0, z0), x1)))
ACTIVE(f(f(b, x1), x2)) → c2(F(f(mark(a), x1), x2), ACTIVE(f(b, x1)))
ACTIVE(f(f(f(z0, z1), x1), x2)) → c2(F(f(f(active(z0), z1), x1), x2), ACTIVE(f(f(z0, z1), x1)))
PROPER(f(x0, f(x1, f(z0, z1)))) → c5(F(proper(x0), f(proper(x1), f(proper(z0), proper(z1)))), PROPER(x0), PROPER(f(x1, f(z0, z1))))
PROPER(f(x0, f(x1, a))) → c5(F(proper(x0), f(proper(x1), ok(a))), PROPER(x0), PROPER(f(x1, a)))
PROPER(f(x0, f(x1, b))) → c5(F(proper(x0), f(proper(x1), ok(b))), PROPER(x0), PROPER(f(x1, b)))
PROPER(f(x0, f(f(z0, z1), x2))) → c5(F(proper(x0), f(f(proper(z0), proper(z1)), proper(x2))), PROPER(x0), PROPER(f(f(z0, z1), x2)))
PROPER(f(x0, f(a, x2))) → c5(F(proper(x0), f(ok(a), proper(x2))), PROPER(x0), PROPER(f(a, x2)))
PROPER(f(x0, f(b, x2))) → c5(F(proper(x0), f(ok(b), proper(x2))), PROPER(x0), PROPER(f(b, x2)))
PROPER(f(f(z0, z1), f(x1, x2))) → c5(F(f(proper(z0), proper(z1)), f(proper(x1), proper(x2))), PROPER(f(z0, z1)), PROPER(f(x1, x2)))
PROPER(f(a, f(x1, x2))) → c5(F(ok(a), f(proper(x1), proper(x2))), PROPER(a), PROPER(f(x1, x2)))
PROPER(f(b, f(x1, x2))) → c5(F(ok(b), f(proper(x1), proper(x2))), PROPER(b), PROPER(f(x1, x2)))

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
ACTIVE(f(f(f(z0, z0), x1), x2)) → c2(F(f(mark(f(a, b)), x1), x2), ACTIVE(f(f(z0, z0), x1)))
ACTIVE(f(f(f(z0, z1), x1), x2)) → c2(F(f(f(active(z0), z1), x1), x2), ACTIVE(f(f(z0, z1), x1)))
PROPER(f(x0, f(x1, f(z0, z1)))) → c5(F(proper(x0), f(proper(x1), f(proper(z0), proper(z1)))), PROPER(x0), PROPER(f(x1, f(z0, z1))))
PROPER(f(x0, f(x1, a))) → c5(F(proper(x0), f(proper(x1), ok(a))), PROPER(x0), PROPER(f(x1, a)))
PROPER(f(x0, f(x1, b))) → c5(F(proper(x0), f(proper(x1), ok(b))), PROPER(x0), PROPER(f(x1, b)))
PROPER(f(x0, f(f(z0, z1), x2))) → c5(F(proper(x0), f(f(proper(z0), proper(z1)), proper(x2))), PROPER(x0), PROPER(f(f(z0, z1), x2)))
PROPER(f(x0, f(a, x2))) → c5(F(proper(x0), f(ok(a), proper(x2))), PROPER(x0), PROPER(f(a, x2)))
PROPER(f(x0, f(b, x2))) → c5(F(proper(x0), f(ok(b), proper(x2))), PROPER(x0), PROPER(f(b, x2)))
PROPER(f(f(z0, z1), f(x1, x2))) → c5(F(f(proper(z0), proper(z1)), f(proper(x1), proper(x2))), PROPER(f(z0, z1)), PROPER(f(x1, x2)))
PROPER(f(a, f(x1, x2))) → c5(F(ok(a), f(proper(x1), proper(x2))), PROPER(a), PROPER(f(x1, x2)))
PROPER(f(b, f(x1, x2))) → c5(F(ok(b), f(proper(x1), proper(x2))), PROPER(b), PROPER(f(x1, x2)))

K tuples:

ACTIVE(f(f(b, x1), x2)) → c2(F(f(mark(a), x1), x2), ACTIVE(f(b, x1)))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, ACTIVE, PROPER, TOP

Compound Symbols:

c3, c4, c2, c5, c8, c9, c2

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

Use narrowing to replace PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a)) by

PROPER(f(f(z0, z1), a)) → c5(F(f(proper(z0), proper(z1)), ok(a)), PROPER(f(z0, z1)), PROPER(a))
PROPER(f(a, a)) → c5(F(ok(a), ok(a)), PROPER(a), PROPER(a))
PROPER(f(b, a)) → c5(F(ok(b), ok(a)), PROPER(b), PROPER(a))
PROPER(f(x0, a)) → c5

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
ACTIVE(f(b, x0)) → c2(F(mark(a), x0))
ACTIVE(f(f(f(z0, z0), x1), x2)) → c2(F(f(mark(f(a, b)), x1), x2), ACTIVE(f(f(z0, z0), x1)))
ACTIVE(f(f(b, x1), x2)) → c2(F(f(mark(a), x1), x2), ACTIVE(f(b, x1)))
ACTIVE(f(f(f(z0, z1), x1), x2)) → c2(F(f(f(active(z0), z1), x1), x2), ACTIVE(f(f(z0, z1), x1)))
PROPER(f(x0, f(x1, f(z0, z1)))) → c5(F(proper(x0), f(proper(x1), f(proper(z0), proper(z1)))), PROPER(x0), PROPER(f(x1, f(z0, z1))))
PROPER(f(x0, f(x1, a))) → c5(F(proper(x0), f(proper(x1), ok(a))), PROPER(x0), PROPER(f(x1, a)))
PROPER(f(x0, f(x1, b))) → c5(F(proper(x0), f(proper(x1), ok(b))), PROPER(x0), PROPER(f(x1, b)))
PROPER(f(x0, f(f(z0, z1), x2))) → c5(F(proper(x0), f(f(proper(z0), proper(z1)), proper(x2))), PROPER(x0), PROPER(f(f(z0, z1), x2)))
PROPER(f(x0, f(a, x2))) → c5(F(proper(x0), f(ok(a), proper(x2))), PROPER(x0), PROPER(f(a, x2)))
PROPER(f(x0, f(b, x2))) → c5(F(proper(x0), f(ok(b), proper(x2))), PROPER(x0), PROPER(f(b, x2)))
PROPER(f(f(z0, z1), f(x1, x2))) → c5(F(f(proper(z0), proper(z1)), f(proper(x1), proper(x2))), PROPER(f(z0, z1)), PROPER(f(x1, x2)))
PROPER(f(a, f(x1, x2))) → c5(F(ok(a), f(proper(x1), proper(x2))), PROPER(a), PROPER(f(x1, x2)))
PROPER(f(b, f(x1, x2))) → c5(F(ok(b), f(proper(x1), proper(x2))), PROPER(b), PROPER(f(x1, x2)))
PROPER(f(f(z0, z1), a)) → c5(F(f(proper(z0), proper(z1)), ok(a)), PROPER(f(z0, z1)), PROPER(a))
PROPER(f(a, a)) → c5(F(ok(a), ok(a)), PROPER(a), PROPER(a))
PROPER(f(b, a)) → c5(F(ok(b), ok(a)), PROPER(b), PROPER(a))
PROPER(f(x0, a)) → c5

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
ACTIVE(f(f(f(z0, z0), x1), x2)) → c2(F(f(mark(f(a, b)), x1), x2), ACTIVE(f(f(z0, z0), x1)))
ACTIVE(f(f(f(z0, z1), x1), x2)) → c2(F(f(f(active(z0), z1), x1), x2), ACTIVE(f(f(z0, z1), x1)))
PROPER(f(x0, f(x1, f(z0, z1)))) → c5(F(proper(x0), f(proper(x1), f(proper(z0), proper(z1)))), PROPER(x0), PROPER(f(x1, f(z0, z1))))
PROPER(f(x0, f(x1, a))) → c5(F(proper(x0), f(proper(x1), ok(a))), PROPER(x0), PROPER(f(x1, a)))
PROPER(f(x0, f(x1, b))) → c5(F(proper(x0), f(proper(x1), ok(b))), PROPER(x0), PROPER(f(x1, b)))
PROPER(f(x0, f(f(z0, z1), x2))) → c5(F(proper(x0), f(f(proper(z0), proper(z1)), proper(x2))), PROPER(x0), PROPER(f(f(z0, z1), x2)))
PROPER(f(x0, f(a, x2))) → c5(F(proper(x0), f(ok(a), proper(x2))), PROPER(x0), PROPER(f(a, x2)))
PROPER(f(x0, f(b, x2))) → c5(F(proper(x0), f(ok(b), proper(x2))), PROPER(x0), PROPER(f(b, x2)))
PROPER(f(f(z0, z1), f(x1, x2))) → c5(F(f(proper(z0), proper(z1)), f(proper(x1), proper(x2))), PROPER(f(z0, z1)), PROPER(f(x1, x2)))
PROPER(f(a, f(x1, x2))) → c5(F(ok(a), f(proper(x1), proper(x2))), PROPER(a), PROPER(f(x1, x2)))
PROPER(f(b, f(x1, x2))) → c5(F(ok(b), f(proper(x1), proper(x2))), PROPER(b), PROPER(f(x1, x2)))
PROPER(f(f(z0, z1), a)) → c5(F(f(proper(z0), proper(z1)), ok(a)), PROPER(f(z0, z1)), PROPER(a))
PROPER(f(a, a)) → c5(F(ok(a), ok(a)), PROPER(a), PROPER(a))
PROPER(f(b, a)) → c5(F(ok(b), ok(a)), PROPER(b), PROPER(a))
PROPER(f(x0, a)) → c5

K tuples:

ACTIVE(f(f(b, x1), x2)) → c2(F(f(mark(a), x1), x2), ACTIVE(f(b, x1)))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, ACTIVE, PROPER, TOP

Compound Symbols:

c3, c4, c2, c5, c8, c9, c2, c5

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

Removed 1 trailing nodes:

PROPER(f(x0, a)) → c5

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(z0, z0)) → mark(f(a, b))
active(b) → mark(a)
active(f(z0, z1)) → f(active(z0), z1)
f(mark(z0), z1) → mark(f(z0, z1))
f(ok(z0), ok(z1)) → ok(f(z0, z1))
proper(f(z0, z1)) → f(proper(z0), proper(z1))
proper(a) → ok(a)
proper(b) → ok(b)
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))

Tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
ACTIVE(f(b, x0)) → c2(F(mark(a), x0))
ACTIVE(f(f(f(z0, z0), x1), x2)) → c2(F(f(mark(f(a, b)), x1), x2), ACTIVE(f(f(z0, z0), x1)))
ACTIVE(f(f(b, x1), x2)) → c2(F(f(mark(a), x1), x2), ACTIVE(f(b, x1)))
ACTIVE(f(f(f(z0, z1), x1), x2)) → c2(F(f(f(active(z0), z1), x1), x2), ACTIVE(f(f(z0, z1), x1)))
PROPER(f(x0, f(x1, f(z0, z1)))) → c5(F(proper(x0), f(proper(x1), f(proper(z0), proper(z1)))), PROPER(x0), PROPER(f(x1, f(z0, z1))))
PROPER(f(x0, f(x1, a))) → c5(F(proper(x0), f(proper(x1), ok(a))), PROPER(x0), PROPER(f(x1, a)))
PROPER(f(x0, f(x1, b))) → c5(F(proper(x0), f(proper(x1), ok(b))), PROPER(x0), PROPER(f(x1, b)))
PROPER(f(x0, f(f(z0, z1), x2))) → c5(F(proper(x0), f(f(proper(z0), proper(z1)), proper(x2))), PROPER(x0), PROPER(f(f(z0, z1), x2)))
PROPER(f(x0, f(a, x2))) → c5(F(proper(x0), f(ok(a), proper(x2))), PROPER(x0), PROPER(f(a, x2)))
PROPER(f(x0, f(b, x2))) → c5(F(proper(x0), f(ok(b), proper(x2))), PROPER(x0), PROPER(f(b, x2)))
PROPER(f(f(z0, z1), f(x1, x2))) → c5(F(f(proper(z0), proper(z1)), f(proper(x1), proper(x2))), PROPER(f(z0, z1)), PROPER(f(x1, x2)))
PROPER(f(a, f(x1, x2))) → c5(F(ok(a), f(proper(x1), proper(x2))), PROPER(a), PROPER(f(x1, x2)))
PROPER(f(b, f(x1, x2))) → c5(F(ok(b), f(proper(x1), proper(x2))), PROPER(b), PROPER(f(x1, x2)))
PROPER(f(f(z0, z1), a)) → c5(F(f(proper(z0), proper(z1)), ok(a)), PROPER(f(z0, z1)), PROPER(a))
PROPER(f(a, a)) → c5(F(ok(a), ok(a)), PROPER(a), PROPER(a))
PROPER(f(b, a)) → c5(F(ok(b), ok(a)), PROPER(b), PROPER(a))

S tuples:

F(mark(z0), z1) → c3(F(z0, z1))
F(ok(z0), ok(z1)) → c4(F(z0, z1))
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0)))
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b))
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1))
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1))
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0)))
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
ACTIVE(f(f(f(z0, z0), x1), x2)) → c2(F(f(mark(f(a, b)), x1), x2), ACTIVE(f(f(z0, z0), x1)))
ACTIVE(f(f(f(z0, z1), x1), x2)) → c2(F(f(f(active(z0), z1), x1), x2), ACTIVE(f(f(z0, z1), x1)))
PROPER(f(x0, f(x1, f(z0, z1)))) → c5(F(proper(x0), f(proper(x1), f(proper(z0), proper(z1)))), PROPER(x0), PROPER(f(x1, f(z0, z1))))
PROPER(f(x0, f(x1, a))) → c5(F(proper(x0), f(proper(x1), ok(a))), PROPER(x0), PROPER(f(x1, a)))
PROPER(f(x0, f(x1, b))) → c5(F(proper(x0), f(proper(x1), ok(b))), PROPER(x0), PROPER(f(x1, b)))
PROPER(f(x0, f(f(z0, z1), x2))) → c5(F(proper(x0), f(f(proper(z0), proper(z1)), proper(x2))), PROPER(x0), PROPER(f(f(z0, z1), x2)))
PROPER(f(x0, f(a, x2))) → c5(F(proper(x0), f(ok(a), proper(x2))), PROPER(x0), PROPER(f(a, x2)))
PROPER(f(x0, f(b, x2))) → c5(F(proper(x0), f(ok(b), proper(x2))), PROPER(x0), PROPER(f(b, x2)))
PROPER(f(f(z0, z1), f(x1, x2))) → c5(F(f(proper(z0), proper(z1)), f(proper(x1), proper(x2))), PROPER(f(z0, z1)), PROPER(f(x1, x2)))
PROPER(f(a, f(x1, x2))) → c5(F(ok(a), f(proper(x1), proper(x2))), PROPER(a), PROPER(f(x1, x2)))
PROPER(f(b, f(x1, x2))) → c5(F(ok(b), f(proper(x1), proper(x2))), PROPER(b), PROPER(f(x1, x2)))
PROPER(f(f(z0, z1), a)) → c5(F(f(proper(z0), proper(z1)), ok(a)), PROPER(f(z0, z1)), PROPER(a))
PROPER(f(a, a)) → c5(F(ok(a), ok(a)), PROPER(a), PROPER(a))
PROPER(f(b, a)) → c5(F(ok(b), ok(a)), PROPER(b), PROPER(a))

K tuples:

ACTIVE(f(f(b, x1), x2)) → c2(F(f(mark(a), x1), x2), ACTIVE(f(b, x1)))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, ACTIVE, PROPER, TOP

Compound Symbols:

c3, c4, c2, c5, c8, c9, c2

(43) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

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

The compatible tree automaton used to show the Match(-raise)-Boundedness (for constructor-based start-terms) is represented by:
final states : [4, 1, 2, 3, 13, 15, 16, 20, 21, 28, 29, 30, 31, 32, 33, 34, 40, 41, 42, 43, 47, 48]
transitions:
mark0(0) → 0
ok0(0) → 0
top0(0) → 4
mark1(5) → 1
f1(0, 0) → 6
mark1(6) → 2
f1(0, 0) → 2
ok1(7) → 3
ok1(8) → 3
f1(0, 0) → 9
ok1(9) → 2
proper1(0) → 10
top1(10) → 4
proper1(0) → 3
active1(0) → 11
top1(11) → 4
active1(0) → 1
f1(0, 0) → 13
proper1(0) → 15
active1(0) → 16
mark0(12) → 0
mark0(14) → 0
ok0(12) → 0
ok0(14) → 0
top0(12) → 4
top0(14) → 4
mark1(12) → 1
mark1(13) → 2
f1(12, 0) → 13
f1(0, 12) → 13
f1(14, 0) → 13
f1(0, 14) → 13
f1(12, 12) → 13
f1(12, 14) → 13
f1(14, 12) → 13
f1(14, 14) → 13
ok1(12) → 3
ok1(13) → 2
ok1(14) → 3
top1(15) → 4
top1(16) → 4
proper1(12) → 15
proper1(14) → 15
active1(12) → 16
active1(14) → 16
mark1(12) → 0
ok1(12) → 0
ok1(14) → 0
mark2(17) → 16
mark1(6) → 13
f1(12, 0) → 6
f1(14, 0) → 6
f1(0, 12) → 6
f1(12, 12) → 6
f1(14, 12) → 6
f1(0, 14) → 6
f1(12, 14) → 6
f1(14, 14) → 6
ok2(18) → 15
b2() → 19
ok2(19) → 15
b2() → 8
b2() → 0
b2() → 14
ok1(9) → 13
f1(0, 12) → 9
f1(0, 14) → 9
f1(12, 0) → 9
f1(12, 12) → 9
f1(12, 14) → 9
f1(14, 0) → 9
f1(14, 12) → 9
f1(14, 14) → 9
mark1(12) → 20
ok1(12) → 21
ok1(14) → 21
b2() → 23
mark0(20) → 0
mark0(21) → 0
mark0(22) → 0
mark0(23) → 0
ok0(20) → 0
ok0(21) → 0
ok0(22) → 0
ok0(23) → 0
top0(20) → 4
top0(21) → 4
top0(22) → 4
top0(23) → 4
mark1(13) → 13
mark1(22) → 20
f1(20, 0) → 13
f1(20, 12) → 13
f1(20, 14) → 13
f1(0, 20) → 13
f1(12, 20) → 13
f1(14, 20) → 13
f1(21, 0) → 13
f1(21, 12) → 13
f1(21, 14) → 13
f1(0, 21) → 13
f1(12, 21) → 13
f1(14, 21) → 13
f1(22, 12) → 13
f1(22, 14) → 13
f1(0, 22) → 13
f1(12, 22) → 13
f1(14, 22) → 13
f1(23, 0) → 13
f1(23, 12) → 13
f1(23, 14) → 13
f1(0, 23) → 13
f1(12, 23) → 13
f1(14, 23) → 13
f1(20, 20) → 13
f1(20, 21) → 13
f1(20, 22) → 13
f1(20, 23) → 13
f1(21, 20) → 13
f1(23, 20) → 13
f1(21, 21) → 13
f1(21, 22) → 13
f1(21, 23) → 13
f1(23, 21) → 13
ok1(13) → 13
ok1(22) → 21
ok1(23) → 21
proper1(20) → 15
proper1(21) → 15
proper1(23) → 15
active1(20) → 16
active1(21) → 16
mark2(22) → 16
ok2(22) → 15
ok2(23) → 15
mark1(22) → 0
mark2(22) → 0
ok1(22) → 0
ok2(22) → 0
ok1(23) → 0
ok2(23) → 0
mark2(22) → 20
ok2(22) → 21
ok2(23) → 21
f2(22, 0) → 24
mark2(24) → 13
f2(22, 0) → 13
f2(22, 20) → 24
f2(22, 20) → 13
f2(22, 21) → 24
f2(22, 21) → 13
f2(22, 22) → 24
f2(22, 22) → 13
f2(22, 23) → 24
f2(22, 23) → 13
f2(22, 22) → 25
ok2(25) → 13
f2(22, 23) → 25
f2(23, 22) → 25
f2(23, 22) → 13
f2(23, 23) → 25
f2(23, 23) → 13
proper2(22) → 26
top2(26) → 4
proper2(22) → 15
active2(22) → 27
top2(27) → 4
active2(22) → 16
active2(23) → 27
active2(23) → 16
mark2(22) → 28
ok2(22) → 29
ok2(23) → 29
f2(22, 0) → 30
f2(22, 20) → 30
f2(22, 21) → 30
f2(22, 22) → 31
f2(22, 23) → 31
f2(23, 22) → 32
f2(23, 23) → 32
proper2(22) → 33
active2(22) → 34
active2(23) → 34
mark0(28) → 0
mark0(29) → 0
ok0(28) → 0
ok0(29) → 0
top0(28) → 4
top0(29) → 4
mark1(30) → 13
mark1(31) → 13
mark1(32) → 13
f1(22, 0) → 13
f1(22, 20) → 13
f1(22, 21) → 13
f1(22, 22) → 13
f1(22, 23) → 13
f1(23, 22) → 13
f1(23, 23) → 13
f1(28, 0) → 13
f1(28, 12) → 13
f1(28, 14) → 13
f1(28, 20) → 13
f1(28, 21) → 13
f1(28, 22) → 13
f1(28, 23) → 13
f1(0, 28) → 13
f1(12, 28) → 13
f1(14, 28) → 13
f1(20, 28) → 13
f1(21, 28) → 13
f1(23, 28) → 13
f1(29, 0) → 13
f1(29, 12) → 13
f1(29, 14) → 13
f1(29, 20) → 13
f1(29, 21) → 13
f1(29, 22) → 13
f1(29, 23) → 13
f1(0, 29) → 13
f1(12, 29) → 13
f1(14, 29) → 13
f1(20, 29) → 13
f1(21, 29) → 13
f1(23, 29) → 13
f1(22, 28) → 13
f1(22, 29) → 13
f1(28, 28) → 13
f1(28, 29) → 13
f1(29, 28) → 13
f1(29, 29) → 13
ok1(30) → 13
ok1(31) → 13
ok1(32) → 13
top1(28) → 4
top1(29) → 4
top1(33) → 4
top1(34) → 4
proper1(22) → 15
proper1(28) → 15
proper1(29) → 15
active1(22) → 16
active1(23) → 16
active1(28) → 16
active1(29) → 16
mark2(30) → 13
mark2(31) → 13
ok2(31) → 13
ok2(32) → 13
f2(22, 22) → 30
f2(22, 23) → 30
f2(22, 28) → 30
f2(22, 29) → 30
top2(33) → 4
top2(34) → 4
f2(22, 28) → 13
f2(22, 29) → 13
mark3(35) → 34
ok3(36) → 33
mark0(37) → 0
ok0(37) → 0
top0(37) → 4
mark1(37) → 20
f1(37, 0) → 13
f1(37, 12) → 13
f1(37, 14) → 13
f1(37, 20) → 13
f1(37, 21) → 13
f1(37, 22) → 13
f1(37, 23) → 13
f1(37, 28) → 13
f1(37, 29) → 13
f1(0, 37) → 13
f1(12, 37) → 13
f1(14, 37) → 13
f1(20, 37) → 13
f1(21, 37) → 13
f1(22, 37) → 13
f1(23, 37) → 13
f1(28, 37) → 13
f1(29, 37) → 13
f1(37, 37) → 13
ok1(37) → 21
mark2(37) → 28
ok2(37) → 29
f2(37, 0) → 30
f2(37, 20) → 30
f2(37, 21) → 30
f2(37, 22) → 31
f2(37, 23) → 31
f2(37, 28) → 30
f2(37, 29) → 30
f2(22, 37) → 31
f2(23, 37) → 32
f2(37, 23) → 30
f2(37, 37) → 31
mark3(37) → 34
ok3(37) → 33
mark1(37) → 0
mark2(37) → 0
mark3(37) → 0
ok1(37) → 0
ok2(37) → 0
ok3(37) → 0
mark2(37) → 20
mark3(37) → 20
f2(37, 0) → 13
f2(37, 20) → 13
f2(37, 21) → 13
f2(37, 22) → 13
f2(37, 23) → 13
f2(37, 28) → 13
f2(37, 29) → 13
f2(22, 37) → 13
f2(23, 37) → 13
f2(37, 37) → 13
ok2(37) → 21
ok3(37) → 21
mark3(37) → 28
ok3(37) → 29
proper3(37) → 38
top3(38) → 4
proper3(37) → 15
proper3(37) → 33
active3(37) → 39
top3(39) → 4
active3(37) → 16
active3(37) → 34
mark3(37) → 40
ok3(37) → 41
proper3(37) → 42
active3(37) → 43
mark0(40) → 0
mark0(41) → 0
ok0(40) → 0
ok0(41) → 0
top0(40) → 4
top0(41) → 4
f1(40, 0) → 13
f1(40, 12) → 13
f1(40, 14) → 13
f1(40, 20) → 13
f1(40, 21) → 13
f1(40, 22) → 13
f1(40, 23) → 13
f1(40, 28) → 13
f1(40, 29) → 13
f1(40, 37) → 13
f1(0, 40) → 13
f1(12, 40) → 13
f1(14, 40) → 13
f1(20, 40) → 13
f1(21, 40) → 13
f1(23, 40) → 13
f1(22, 40) → 13
f1(28, 40) → 13
f1(29, 40) → 13
f1(37, 40) → 13
f1(41, 0) → 13
f1(41, 12) → 13
f1(41, 14) → 13
f1(41, 20) → 13
f1(41, 21) → 13
f1(41, 22) → 13
f1(41, 23) → 13
f1(41, 28) → 13
f1(41, 29) → 13
f1(41, 37) → 13
f1(0, 41) → 13
f1(12, 41) → 13
f1(14, 41) → 13
f1(20, 41) → 13
f1(21, 41) → 13
f1(23, 41) → 13
f1(22, 41) → 13
f1(28, 41) → 13
f1(29, 41) → 13
f1(37, 41) → 13
f1(40, 40) → 13
f1(40, 41) → 13
f1(41, 40) → 13
f1(41, 41) → 13
top1(40) → 4
top1(41) → 4
top1(42) → 4
top1(43) → 4
proper1(37) → 15
proper1(40) → 15
proper1(41) → 15
active1(37) → 16
active1(40) → 16
active1(41) → 16
f2(22, 40) → 30
f2(37, 40) → 30
f2(22, 41) → 30
f2(37, 41) → 30
top2(40) → 4
top2(41) → 4
top2(42) → 4
top2(43) → 4
proper2(37) → 33
active2(37) → 34
top3(42) → 4
top3(43) → 4
f2(22, 40) → 13
f2(37, 40) → 13
f2(22, 41) → 13
f2(37, 41) → 13
proper2(37) → 15
active2(37) → 16
a4() → 44
ok4(44) → 42
a4() → 35
a4() → 17
a4() → 5
a4() → 0
a4() → 7
a4() → 12
a4() → 18
a4() → 22
a4() → 36
a4() → 37
a4() → 45
mark0(45) → 0
ok0(45) → 0
top0(45) → 4
mark1(45) → 20
f1(45, 0) → 13
f1(45, 12) → 13
f1(45, 14) → 13
f1(45, 20) → 13
f1(45, 21) → 13
f1(45, 22) → 13
f1(45, 23) → 13
f1(45, 28) → 13
f1(45, 29) → 13
f1(45, 37) → 13
f1(45, 40) → 13
f1(45, 41) → 13
f1(0, 45) → 13
f1(12, 45) → 13
f1(14, 45) → 13
f1(20, 45) → 13
f1(21, 45) → 13
f1(22, 45) → 13
f1(23, 45) → 13
f1(28, 45) → 13
f1(29, 45) → 13
f1(37, 45) → 13
f1(40, 45) → 13
f1(41, 45) → 13
f1(45, 45) → 13
ok1(45) → 21
proper1(45) → 15
mark2(45) → 28
ok2(45) → 29
f2(45, 0) → 30
f2(45, 20) → 30
f2(45, 21) → 30
f2(45, 22) → 31
f2(45, 23) → 31
f2(45, 28) → 30
f2(45, 29) → 30
f2(45, 37) → 31
f2(45, 40) → 30
f2(45, 41) → 30
f2(22, 45) → 31
f2(23, 45) → 32
f2(37, 45) → 31
f2(45, 23) → 30
f2(45, 45) → 31
proper2(45) → 33
mark3(45) → 40
ok3(45) → 41
proper3(45) → 42
ok4(45) → 42
mark1(45) → 0
mark2(45) → 0
mark3(45) → 0
ok1(45) → 0
ok2(45) → 0
ok3(45) → 0
ok4(45) → 0
mark2(45) → 20
mark3(45) → 20
f2(45, 0) → 13
f2(45, 20) → 13
f2(45, 21) → 13
f2(45, 22) → 13
f2(45, 23) → 13
f2(45, 28) → 13
f2(45, 29) → 13
f2(45, 37) → 13
f2(45, 40) → 13
f2(45, 41) → 13
f2(22, 45) → 13
f2(23, 45) → 13
f2(37, 45) → 13
f2(45, 45) → 13
ok2(45) → 21
ok3(45) → 21
ok4(45) → 21
proper2(45) → 15
proper3(45) → 15
mark3(45) → 28
ok3(45) → 29
ok4(45) → 29
proper3(45) → 33
ok4(45) → 41
active4(45) → 46
top4(46) → 4
active4(45) → 16
active4(45) → 34
active4(45) → 43
ok4(45) → 47
active4(45) → 48
mark0(47) → 0
ok0(47) → 0
top0(47) → 4
f1(47, 0) → 13
f1(47, 12) → 13
f1(47, 14) → 13
f1(47, 20) → 13
f1(47, 21) → 13
f1(47, 22) → 13
f1(47, 23) → 13
f1(47, 28) → 13
f1(47, 29) → 13
f1(47, 37) → 13
f1(47, 40) → 13
f1(47, 41) → 13
f1(47, 45) → 13
f1(0, 47) → 13
f1(12, 47) → 13
f1(14, 47) → 13
f1(20, 47) → 13
f1(21, 47) → 13
f1(23, 47) → 13
f1(22, 47) → 13
f1(28, 47) → 13
f1(29, 47) → 13
f1(37, 47) → 13
f1(40, 47) → 13
f1(41, 47) → 13
f1(45, 47) → 13
f1(47, 47) → 13
top1(47) → 4
top1(48) → 4
proper1(47) → 15
active1(45) → 16
active1(47) → 16
f2(22, 47) → 30
f2(37, 47) → 30
f2(45, 47) → 30
top2(47) → 4
top2(48) → 4
active2(45) → 34
top3(47) → 4
top3(48) → 4
active3(45) → 43
top4(48) → 4
f2(22, 47) → 13
f2(37, 47) → 13
f2(45, 47) → 13
active2(45) → 16
active3(45) → 16
active3(45) → 34

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