74.71/26.85 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml

74.71/26.85

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

0 CpxTRS

74.71/26.85

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

74.71/26.85

↳2 CdtProblem

74.71/26.85

↳3 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

74.71/26.85

↳4 CdtProblem

74.71/26.85

↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

74.71/26.85

↳6 CdtProblem

74.71/26.85

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

74.71/26.85

↳8 CdtProblem

74.71/26.85

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

74.71/26.85

↳10 CdtProblem

74.71/26.85

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

74.71/26.85

↳12 CdtProblem

74.71/26.85

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

74.71/26.85

↳14 CdtProblem

74.71/26.85

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

74.71/26.85

↳16 CdtProblem

74.71/26.85

↳17 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

74.71/26.85

↳18 CdtProblem

74.71/26.85

↳19 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

74.71/26.85

↳20 CdtProblem

74.71/26.85

↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

74.71/26.85

↳22 CdtProblem

74.71/26.85

↳23 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

74.71/26.85

↳24 CdtProblem

74.71/26.85

↳25 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

74.71/26.85

↳26 CdtProblem

74.71/26.85

↳27 CdtUnreachableProof (⇔)

74.71/26.85

↳28 CdtProblem

74.71/26.85

↳29 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

74.71/26.85

↳30 CdtProblem

74.71/26.85

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

74.71/26.85

↳32 CdtProblem

74.71/26.85

↳33 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))

74.71/26.85

↳34 CdtProblem

74.71/26.85

↳35 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))

74.71/26.85

↳36 CdtProblem

74.71/26.85

↳37 SIsEmptyProof (BOTH BOUNDS(ID, ID))

74.71/26.85

↳38 BOUNDS(O(1), O(1))

74.71/26.85

74.71/26.85 74.71/26.85

74.71/26.85

(0) Obligation:

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

active(f(b, c, x)) → mark(f(x, x, x)) 74.71/26.85
active(f(x, y, z)) → f(x, y, active(z)) 74.71/26.85
active(d) → m(b) 74.71/26.85
f(x, y, mark(z)) → mark(f(x, y, z)) 74.71/26.85
active(d) → mark(c) 74.71/26.85
proper(b) → ok(b) 74.71/26.85
proper(c) → ok(c) 74.71/26.85
proper(d) → ok(d) 74.71/26.85
proper(f(x, y, z)) → f(proper(x), proper(y), proper(z)) 74.71/26.85
f(ok(x), ok(y), ok(z)) → ok(f(x, y, z)) 74.71/26.85
top(mark(x)) → top(proper(x)) 74.71/26.85
top(ok(x)) → top(active(x))

Rewrite Strategy: INNERMOST

74.71/26.88

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

Converted CpxTRS to CDT

74.71/26.88

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 74.71/26.88
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 74.71/26.88
active(d) → m(b) 74.71/26.88
active(d) → mark(c) 74.71/26.88
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 74.71/26.88
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 74.71/26.88
proper(b) → ok(b) 74.71/26.88
proper(c) → ok(c) 74.71/26.88
proper(d) → ok(d) 74.71/26.88
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 74.71/26.88
top(mark(z0)) → top(proper(z0)) 74.71/26.88
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 74.71/26.88
ACTIVE(f(z0, z1, z2)) → c2(F(z0, z1, active(z2)), ACTIVE(z2)) 74.71/26.88
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 74.71/26.88
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 74.71/26.88
PROPER(f(z0, z1, z2)) → c10(F(proper(z0), proper(z1), proper(z2)), PROPER(z0), PROPER(z1), PROPER(z2)) 74.71/26.88
TOP(mark(z0)) → c11(TOP(proper(z0)), PROPER(z0)) 74.71/26.88
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0))

S tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 74.71/26.88
ACTIVE(f(z0, z1, z2)) → c2(F(z0, z1, active(z2)), ACTIVE(z2)) 74.71/26.88
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 74.71/26.88
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 74.71/26.88
PROPER(f(z0, z1, z2)) → c10(F(proper(z0), proper(z1), proper(z2)), PROPER(z0), PROPER(z1), PROPER(z2)) 74.71/26.88
TOP(mark(z0)) → c11(TOP(proper(z0)), PROPER(z0)) 74.71/26.88
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0))

K tuples:none
Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

ACTIVE, F, PROPER, TOP

Compound Symbols:

c1, c2, c5, c6, c10, c11, c12

74.71/26.88

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

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

ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 74.71/26.88
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 74.71/26.88
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, m(b)), ACTIVE(d)) 74.71/26.88
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c)), ACTIVE(d))

74.71/26.88

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 74.71/26.88
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 74.71/26.88
active(d) → m(b) 74.71/26.88
active(d) → mark(c) 74.71/26.88
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 74.71/26.88
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 74.71/26.88
proper(b) → ok(b) 74.71/26.88
proper(c) → ok(c) 74.71/26.88
proper(d) → ok(d) 74.71/26.88
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 74.71/26.88
top(mark(z0)) → top(proper(z0)) 74.71/26.88
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 74.71/26.90
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 74.71/26.90
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 74.71/26.90
PROPER(f(z0, z1, z2)) → c10(F(proper(z0), proper(z1), proper(z2)), PROPER(z0), PROPER(z1), PROPER(z2)) 74.71/26.90
TOP(mark(z0)) → c11(TOP(proper(z0)), PROPER(z0)) 74.71/26.90
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 74.71/26.90
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 74.71/26.90
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 74.71/26.90
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, m(b)), ACTIVE(d)) 74.71/26.90
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c)), ACTIVE(d))

S tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 74.71/26.90
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 74.71/26.90
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 74.71/26.90
PROPER(f(z0, z1, z2)) → c10(F(proper(z0), proper(z1), proper(z2)), PROPER(z0), PROPER(z1), PROPER(z2)) 74.71/26.90
TOP(mark(z0)) → c11(TOP(proper(z0)), PROPER(z0)) 74.71/26.90
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 74.71/26.90
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 74.71/26.90
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 74.71/26.90
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, m(b)), ACTIVE(d)) 74.71/26.90
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c)), ACTIVE(d))

K tuples:none
Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

ACTIVE, F, PROPER, TOP

Compound Symbols:

c1, c5, c6, c10, c11, c12, c2

74.71/26.90

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

Removed 3 trailing tuple parts

74.71/26.90

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 74.71/26.90
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 74.71/26.90
active(d) → m(b) 74.71/26.90
active(d) → mark(c) 74.71/26.90
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 74.71/26.90
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 74.71/26.90
proper(b) → ok(b) 74.71/26.90
proper(c) → ok(c) 74.71/26.90
proper(d) → ok(d) 74.71/26.90
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 74.71/26.90
top(mark(z0)) → top(proper(z0)) 74.71/26.90
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 74.71/26.90
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 74.71/26.90
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 74.71/26.90
PROPER(f(z0, z1, z2)) → c10(F(proper(z0), proper(z1), proper(z2)), PROPER(z0), PROPER(z1), PROPER(z2)) 74.71/26.90
TOP(mark(z0)) → c11(TOP(proper(z0)), PROPER(z0)) 74.71/26.90
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 74.71/26.90
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 74.71/26.90
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 74.71/26.90
ACTIVE(f(x0, x1, d)) → c2 74.71/26.90
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c)))

S tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 74.71/26.90
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 74.71/26.90
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 74.71/26.90
PROPER(f(z0, z1, z2)) → c10(F(proper(z0), proper(z1), proper(z2)), PROPER(z0), PROPER(z1), PROPER(z2)) 74.71/26.90
TOP(mark(z0)) → c11(TOP(proper(z0)), PROPER(z0)) 74.71/26.90
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 74.71/26.90
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 74.71/26.90
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 74.71/26.90
ACTIVE(f(x0, x1, d)) → c2 74.71/26.90
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c)))

K tuples:none
Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

ACTIVE, F, PROPER, TOP

Compound Symbols:

c1, c5, c6, c10, c11, c12, c2, c2, c2

74.71/26.90

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

Removed 1 trailing nodes:

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

74.71/26.90

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 74.71/26.90
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 74.71/26.90
active(d) → m(b) 74.71/26.90
active(d) → mark(c) 74.71/26.90
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 74.71/26.90
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 74.71/26.90
proper(b) → ok(b) 74.71/26.90
proper(c) → ok(c) 74.71/26.90
proper(d) → ok(d) 74.71/26.90
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 74.71/26.90
top(mark(z0)) → top(proper(z0)) 74.71/26.90
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 74.71/26.90
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 74.71/26.90
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 74.71/26.90
PROPER(f(z0, z1, z2)) → c10(F(proper(z0), proper(z1), proper(z2)), PROPER(z0), PROPER(z1), PROPER(z2)) 74.71/26.90
TOP(mark(z0)) → c11(TOP(proper(z0)), PROPER(z0)) 74.71/26.90
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 74.71/26.90
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 74.71/26.90
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 74.71/26.90
ACTIVE(f(x0, x1, d)) → c2 74.71/26.90
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c)))

S tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 74.71/26.90
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 74.71/26.90
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 74.71/26.90
PROPER(f(z0, z1, z2)) → c10(F(proper(z0), proper(z1), proper(z2)), PROPER(z0), PROPER(z1), PROPER(z2)) 74.71/26.90
TOP(mark(z0)) → c11(TOP(proper(z0)), PROPER(z0)) 74.71/26.90
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 74.71/26.90
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 74.71/26.90
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 74.71/26.90
ACTIVE(f(x0, x1, d)) → c2 74.71/26.90
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c)))

K tuples:none
Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

ACTIVE, F, PROPER, TOP

Compound Symbols:

c1, c5, c6, c10, c11, c12, c2, c2, c2

74.71/26.90

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

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

PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1), PROPER(b)) 74.71/26.90
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1), PROPER(c)) 74.71/26.90
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1), PROPER(d)) 74.71/26.90
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 74.71/26.90
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(b), PROPER(x2)) 74.71/26.90
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(c), PROPER(x2)) 74.71/26.90
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(d), PROPER(x2)) 74.71/26.90
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 74.71/26.90
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(b), PROPER(x1), PROPER(x2)) 74.71/26.90
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(c), PROPER(x1), PROPER(x2)) 74.71/26.90
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(d), PROPER(x1), PROPER(x2)) 74.71/26.90
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2))

74.71/26.90

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 74.71/26.90
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 74.71/26.90
active(d) → m(b) 74.71/26.90
active(d) → mark(c) 74.71/26.90
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 74.71/26.90
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 74.71/26.90
proper(b) → ok(b) 74.71/26.90
proper(c) → ok(c) 74.71/26.90
proper(d) → ok(d) 74.71/26.90
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 74.71/26.90
top(mark(z0)) → top(proper(z0)) 74.71/26.90
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 74.71/26.90
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 74.71/26.90
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 74.71/26.90
TOP(mark(z0)) → c11(TOP(proper(z0)), PROPER(z0)) 74.71/26.90
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 74.71/26.90
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 74.71/26.90
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 74.71/26.90
ACTIVE(f(x0, x1, d)) → c2 74.71/26.90
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 74.71/26.90
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1), PROPER(b)) 74.71/26.90
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1), PROPER(c)) 74.71/26.90
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1), PROPER(d)) 74.71/26.90
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 74.71/26.90
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(b), PROPER(x2)) 74.71/26.90
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(c), PROPER(x2)) 74.71/26.90
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(d), PROPER(x2)) 74.71/26.90
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 74.71/26.90
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(b), PROPER(x1), PROPER(x2)) 74.71/26.90
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(c), PROPER(x1), PROPER(x2)) 74.71/26.90
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(d), PROPER(x1), PROPER(x2)) 74.71/26.90
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2))

S tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 74.71/26.90
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 74.71/26.90
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 74.71/26.90
TOP(mark(z0)) → c11(TOP(proper(z0)), PROPER(z0)) 74.71/26.90
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 74.71/26.90
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 74.71/26.90
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 74.71/26.90
ACTIVE(f(x0, x1, d)) → c2 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.91
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1), PROPER(b)) 75.08/26.91
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1), PROPER(c)) 75.08/26.91
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1), PROPER(d)) 75.08/26.91
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.91
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(b), PROPER(x2)) 75.08/26.91
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(c), PROPER(x2)) 75.08/26.91
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(d), PROPER(x2)) 75.08/26.91
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.91
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(b), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(c), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(d), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2))

K tuples:none
Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

ACTIVE, F, TOP, PROPER

Compound Symbols:

c1, c5, c6, c11, c12, c2, c2, c2, c10

75.08/26.91

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

Removed 9 trailing tuple parts

75.08/26.91

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 75.08/26.91
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 75.08/26.91
active(d) → m(b) 75.08/26.91
active(d) → mark(c) 75.08/26.91
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 75.08/26.91
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 75.08/26.91
proper(b) → ok(b) 75.08/26.91
proper(c) → ok(c) 75.08/26.91
proper(d) → ok(d) 75.08/26.91
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 75.08/26.91
top(mark(z0)) → top(proper(z0)) 75.08/26.91
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.91
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.91
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.91
TOP(mark(z0)) → c11(TOP(proper(z0)), PROPER(z0)) 75.08/26.91
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 75.08/26.91
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.91
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.91
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.91
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.91
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2))

S tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.91
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.91
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.91
TOP(mark(z0)) → c11(TOP(proper(z0)), PROPER(z0)) 75.08/26.91
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 75.08/26.91
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.91
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.91
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.91
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.91
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2))

K tuples:none
Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

ACTIVE, F, TOP, PROPER

Compound Symbols:

c1, c5, c6, c11, c12, c2, c2, c2, c10, c10

75.08/26.91

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

Removed 1 trailing nodes:

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

75.08/26.91

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 75.08/26.91
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 75.08/26.91
active(d) → m(b) 75.08/26.91
active(d) → mark(c) 75.08/26.91
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 75.08/26.91
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 75.08/26.91
proper(b) → ok(b) 75.08/26.91
proper(c) → ok(c) 75.08/26.91
proper(d) → ok(d) 75.08/26.91
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 75.08/26.91
top(mark(z0)) → top(proper(z0)) 75.08/26.91
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.91
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.91
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.91
TOP(mark(z0)) → c11(TOP(proper(z0)), PROPER(z0)) 75.08/26.91
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 75.08/26.91
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.91
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.91
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.91
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.91
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2))

S tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.91
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.91
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.91
TOP(mark(z0)) → c11(TOP(proper(z0)), PROPER(z0)) 75.08/26.91
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 75.08/26.91
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.91
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.91
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.91
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.91
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2))

K tuples:none
Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

ACTIVE, F, TOP, PROPER

Compound Symbols:

c1, c5, c6, c11, c12, c2, c2, c2, c10, c10

75.08/26.91

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

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

TOP(mark(b)) → c11(TOP(ok(b)), PROPER(b)) 75.08/26.91
TOP(mark(c)) → c11(TOP(ok(c)), PROPER(c)) 75.08/26.91
TOP(mark(d)) → c11(TOP(ok(d)), PROPER(d)) 75.08/26.91
TOP(mark(f(z0, z1, z2))) → c11(TOP(f(proper(z0), proper(z1), proper(z2))), PROPER(f(z0, z1, z2)))

75.08/26.91

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 75.08/26.91
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 75.08/26.91
active(d) → m(b) 75.08/26.91
active(d) → mark(c) 75.08/26.91
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 75.08/26.91
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 75.08/26.91
proper(b) → ok(b) 75.08/26.91
proper(c) → ok(c) 75.08/26.91
proper(d) → ok(d) 75.08/26.91
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 75.08/26.91
top(mark(z0)) → top(proper(z0)) 75.08/26.91
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.91
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.91
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.91
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 75.08/26.91
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.91
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.91
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.91
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.91
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
TOP(mark(b)) → c11(TOP(ok(b)), PROPER(b)) 75.08/26.91
TOP(mark(c)) → c11(TOP(ok(c)), PROPER(c)) 75.08/26.91
TOP(mark(d)) → c11(TOP(ok(d)), PROPER(d)) 75.08/26.91
TOP(mark(f(z0, z1, z2))) → c11(TOP(f(proper(z0), proper(z1), proper(z2))), PROPER(f(z0, z1, z2)))

S tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.91
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.91
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.91
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 75.08/26.91
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.91
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.91
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.91
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.91
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
TOP(mark(b)) → c11(TOP(ok(b)), PROPER(b)) 75.08/26.91
TOP(mark(c)) → c11(TOP(ok(c)), PROPER(c)) 75.08/26.91
TOP(mark(d)) → c11(TOP(ok(d)), PROPER(d)) 75.08/26.91
TOP(mark(f(z0, z1, z2))) → c11(TOP(f(proper(z0), proper(z1), proper(z2))), PROPER(f(z0, z1, z2)))

K tuples:none
Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

ACTIVE, F, TOP, PROPER

Compound Symbols:

c1, c5, c6, c12, c2, c2, c2, c10, c10, c11

75.08/26.91

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

Removed 3 trailing tuple parts

75.08/26.91

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 75.08/26.91
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 75.08/26.91
active(d) → m(b) 75.08/26.91
active(d) → mark(c) 75.08/26.91
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 75.08/26.91
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 75.08/26.91
proper(b) → ok(b) 75.08/26.91
proper(c) → ok(c) 75.08/26.91
proper(d) → ok(d) 75.08/26.91
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 75.08/26.91
top(mark(z0)) → top(proper(z0)) 75.08/26.91
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.91
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.91
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.91
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 75.08/26.91
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.91
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.91
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.91
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.91
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
TOP(mark(f(z0, z1, z2))) → c11(TOP(f(proper(z0), proper(z1), proper(z2))), PROPER(f(z0, z1, z2))) 75.08/26.91
TOP(mark(b)) → c11(TOP(ok(b))) 75.08/26.91
TOP(mark(c)) → c11(TOP(ok(c))) 75.08/26.91
TOP(mark(d)) → c11(TOP(ok(d)))

S tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.91
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.91
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.91
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 75.08/26.91
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.91
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.91
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.91
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.91
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
TOP(mark(f(z0, z1, z2))) → c11(TOP(f(proper(z0), proper(z1), proper(z2))), PROPER(f(z0, z1, z2))) 75.08/26.91
TOP(mark(b)) → c11(TOP(ok(b))) 75.08/26.91
TOP(mark(c)) → c11(TOP(ok(c))) 75.08/26.91
TOP(mark(d)) → c11(TOP(ok(d)))

K tuples:none
Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

ACTIVE, F, TOP, PROPER

Compound Symbols:

c1, c5, c6, c12, c2, c2, c2, c10, c10, c11, c11

75.08/26.91

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

Removed 1 trailing nodes:

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

75.08/26.91

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 75.08/26.91
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 75.08/26.91
active(d) → m(b) 75.08/26.91
active(d) → mark(c) 75.08/26.91
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 75.08/26.91
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 75.08/26.91
proper(b) → ok(b) 75.08/26.91
proper(c) → ok(c) 75.08/26.91
proper(d) → ok(d) 75.08/26.91
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 75.08/26.91
top(mark(z0)) → top(proper(z0)) 75.08/26.91
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.91
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.91
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.91
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 75.08/26.91
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.91
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2 75.08/26.91
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.91
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.91
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.91
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.91
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.91
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.91
TOP(mark(f(z0, z1, z2))) → c11(TOP(f(proper(z0), proper(z1), proper(z2))), PROPER(f(z0, z1, z2))) 75.08/26.91
TOP(mark(b)) → c11(TOP(ok(b))) 75.08/26.92
TOP(mark(c)) → c11(TOP(ok(c))) 75.08/26.92
TOP(mark(d)) → c11(TOP(ok(d)))

S tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.92
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.92
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.92
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 75.08/26.92
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.92
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.92
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.92
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.92
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
TOP(mark(f(z0, z1, z2))) → c11(TOP(f(proper(z0), proper(z1), proper(z2))), PROPER(f(z0, z1, z2))) 75.08/26.92
TOP(mark(b)) → c11(TOP(ok(b))) 75.08/26.92
TOP(mark(c)) → c11(TOP(ok(c))) 75.08/26.92
TOP(mark(d)) → c11(TOP(ok(d)))

K tuples:none
Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

ACTIVE, F, TOP, PROPER

Compound Symbols:

c1, c5, c6, c12, c2, c2, c2, c10, c10, c11, c11

75.08/26.92

(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(b)) → c11(TOP(ok(b))) 75.08/26.92
TOP(mark(c)) → c11(TOP(ok(c)))

We considered the (Usable) Rules:

proper(b) → ok(b) 75.08/26.92
proper(c) → ok(c) 75.08/26.92
proper(d) → ok(d) 75.08/26.92
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 75.08/26.92
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 75.08/26.92
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 75.08/26.92
active(f(b, c, z0)) → mark(f(z0, z0, z0)) 75.08/26.92
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 75.08/26.92
active(d) → m(b) 75.08/26.92
active(d) → mark(c)

And the Tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.92
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.92
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.92
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 75.08/26.92
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.92
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.92
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.92
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.92
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
TOP(mark(f(z0, z1, z2))) → c11(TOP(f(proper(z0), proper(z1), proper(z2))), PROPER(f(z0, z1, z2))) 75.08/26.92
TOP(mark(b)) → c11(TOP(ok(b))) 75.08/26.92
TOP(mark(c)) → c11(TOP(ok(c))) 75.08/26.92
TOP(mark(d)) → c11(TOP(ok(d)))

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

POL(ACTIVE(x₁)) = 0 75.08/26.92
POL(F(x₁, x₂, x₃)) = 0 75.08/26.92
POL(PROPER(x₁)) = 0 75.08/26.92
POL(TOP(x₁)) = x₁ 75.08/26.92
POL(active(x₁)) = x₁ 75.08/26.92
POL(b) = 0 75.08/26.92
POL(c) = 0 75.08/26.92
POL(c1(x₁)) = x₁ 75.08/26.92
POL(c10(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 75.08/26.92
POL(c10(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄ 75.08/26.92
POL(c11(x₁)) = x₁ 75.08/26.92
POL(c11(x₁, x₂)) = x₁ + x₂ 75.08/26.92
POL(c12(x₁, x₂)) = x₁ + x₂ 75.08/26.92
POL(c2) = 0 75.08/26.92
POL(c2(x₁)) = x₁ 75.08/26.92
POL(c2(x₁, x₂)) = x₁ + x₂ 75.08/26.92
POL(c5(x₁)) = x₁ 75.08/26.92
POL(c6(x₁)) = x₁ 75.08/26.92
POL(d) = [2] 75.08/26.92
POL(f(x₁, x₂, x₃)) = [2] 75.08/26.92
POL(m(x₁)) = x₁ 75.08/26.92
POL(mark(x₁)) = [2] 75.08/26.92
POL(ok(x₁)) = x₁ 75.08/26.92
POL(proper(x₁)) = 0

75.08/26.92

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 75.08/26.92
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 75.08/26.92
active(d) → m(b) 75.08/26.92
active(d) → mark(c) 75.08/26.92
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 75.08/26.92
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 75.08/26.92
proper(b) → ok(b) 75.08/26.92
proper(c) → ok(c) 75.08/26.92
proper(d) → ok(d) 75.08/26.92
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 75.08/26.92
top(mark(z0)) → top(proper(z0)) 75.08/26.92
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.92
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.92
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.92
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 75.08/26.92
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.92
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.92
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.92
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.92
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
TOP(mark(f(z0, z1, z2))) → c11(TOP(f(proper(z0), proper(z1), proper(z2))), PROPER(f(z0, z1, z2))) 75.08/26.92
TOP(mark(b)) → c11(TOP(ok(b))) 75.08/26.92
TOP(mark(c)) → c11(TOP(ok(c))) 75.08/26.92
TOP(mark(d)) → c11(TOP(ok(d)))

S tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.92
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.92
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.92
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 75.08/26.92
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.92
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.92
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.92
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.92
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
TOP(mark(f(z0, z1, z2))) → c11(TOP(f(proper(z0), proper(z1), proper(z2))), PROPER(f(z0, z1, z2))) 75.08/26.92
TOP(mark(d)) → c11(TOP(ok(d)))

K tuples:

TOP(mark(b)) → c11(TOP(ok(b))) 75.08/26.92
TOP(mark(c)) → c11(TOP(ok(c)))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

ACTIVE, F, TOP, PROPER

Compound Symbols:

c1, c5, c6, c12, c2, c2, c2, c10, c10, c11, c11

75.08/26.92

(23) 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(d)) → c11(TOP(ok(d)))

We considered the (Usable) Rules:

proper(b) → ok(b) 75.08/26.92
proper(c) → ok(c) 75.08/26.92
proper(d) → ok(d) 75.08/26.92
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 75.08/26.92
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 75.08/26.92
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 75.08/26.92
active(f(b, c, z0)) → mark(f(z0, z0, z0)) 75.08/26.92
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 75.08/26.92
active(d) → m(b) 75.08/26.92
active(d) → mark(c)

And the Tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.92
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.92
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.92
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 75.08/26.92
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.92
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.92
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.92
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.92
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
TOP(mark(f(z0, z1, z2))) → c11(TOP(f(proper(z0), proper(z1), proper(z2))), PROPER(f(z0, z1, z2))) 75.08/26.92
TOP(mark(b)) → c11(TOP(ok(b))) 75.08/26.92
TOP(mark(c)) → c11(TOP(ok(c))) 75.08/26.92
TOP(mark(d)) → c11(TOP(ok(d)))

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

POL(ACTIVE(x₁)) = 0 75.08/26.92
POL(F(x₁, x₂, x₃)) = 0 75.08/26.92
POL(PROPER(x₁)) = 0 75.08/26.92
POL(TOP(x₁)) = [4]x₁ 75.08/26.92
POL(active(x₁)) = 0 75.08/26.92
POL(b) = 0 75.08/26.92
POL(c) = 0 75.08/26.92
POL(c1(x₁)) = x₁ 75.08/26.92
POL(c10(x₁, x₂, x₃)) = x₁ + x₂ + x₃ 75.08/26.92
POL(c10(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₃ + x₄ 75.08/26.92
POL(c11(x₁)) = x₁ 75.08/26.92
POL(c11(x₁, x₂)) = x₁ + x₂ 75.08/26.92
POL(c12(x₁, x₂)) = x₁ + x₂ 75.08/26.92
POL(c2) = 0 75.08/26.92
POL(c2(x₁)) = x₁ 75.08/26.92
POL(c2(x₁, x₂)) = x₁ + x₂ 75.08/26.92
POL(c5(x₁)) = x₁ 75.08/26.92
POL(c6(x₁)) = x₁ 75.08/26.92
POL(d) = [2] 75.08/26.92
POL(f(x₁, x₂, x₃)) = 0 75.08/26.92
POL(m(x₁)) = x₁ 75.08/26.92
POL(mark(x₁)) = x₁ 75.08/26.92
POL(ok(x₁)) = 0 75.08/26.92
POL(proper(x₁)) = 0

75.08/26.92

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 75.08/26.92
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 75.08/26.92
active(d) → m(b) 75.08/26.92
active(d) → mark(c) 75.08/26.92
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 75.08/26.92
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 75.08/26.92
proper(b) → ok(b) 75.08/26.92
proper(c) → ok(c) 75.08/26.92
proper(d) → ok(d) 75.08/26.92
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 75.08/26.92
top(mark(z0)) → top(proper(z0)) 75.08/26.92
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.92
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.92
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.92
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 75.08/26.92
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.92
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.92
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.92
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.92
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
TOP(mark(f(z0, z1, z2))) → c11(TOP(f(proper(z0), proper(z1), proper(z2))), PROPER(f(z0, z1, z2))) 75.08/26.92
TOP(mark(b)) → c11(TOP(ok(b))) 75.08/26.92
TOP(mark(c)) → c11(TOP(ok(c))) 75.08/26.92
TOP(mark(d)) → c11(TOP(ok(d)))

S tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.92
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.92
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.92
TOP(ok(z0)) → c12(TOP(active(z0)), ACTIVE(z0)) 75.08/26.92
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.92
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.92
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.92
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.92
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
TOP(mark(f(z0, z1, z2))) → c11(TOP(f(proper(z0), proper(z1), proper(z2))), PROPER(f(z0, z1, z2)))

K tuples:

TOP(mark(b)) → c11(TOP(ok(b))) 75.08/26.92
TOP(mark(c)) → c11(TOP(ok(c))) 75.08/26.92
TOP(mark(d)) → c11(TOP(ok(d)))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

ACTIVE, F, TOP, PROPER

Compound Symbols:

c1, c5, c6, c12, c2, c2, c2, c10, c10, c11, c11

75.08/26.92

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

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

TOP(ok(f(b, c, z0))) → c12(TOP(mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.92
TOP(ok(f(z0, z1, z2))) → c12(TOP(f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.92
TOP(ok(d)) → c12(TOP(m(b)), ACTIVE(d)) 75.08/26.92
TOP(ok(d)) → c12(TOP(mark(c)), ACTIVE(d))

75.08/26.92

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 75.08/26.92
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 75.08/26.92
active(d) → m(b) 75.08/26.92
active(d) → mark(c) 75.08/26.92
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 75.08/26.92
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 75.08/26.92
proper(b) → ok(b) 75.08/26.92
proper(c) → ok(c) 75.08/26.92
proper(d) → ok(d) 75.08/26.92
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 75.08/26.92
top(mark(z0)) → top(proper(z0)) 75.08/26.92
top(ok(z0)) → top(active(z0))

Tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.92
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.92
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.92
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.92
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.92
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.92
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.92
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.92
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.92
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.92
TOP(mark(f(z0, z1, z2))) → c11(TOP(f(proper(z0), proper(z1), proper(z2))), PROPER(f(z0, z1, z2))) 75.08/26.92
TOP(mark(b)) → c11(TOP(ok(b))) 75.08/26.92
TOP(mark(c)) → c11(TOP(ok(c))) 75.08/26.92
TOP(mark(d)) → c11(TOP(ok(d))) 75.08/26.92
TOP(ok(f(b, c, z0))) → c12(TOP(mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.92
TOP(ok(f(z0, z1, z2))) → c12(TOP(f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.92
TOP(ok(d)) → c12(TOP(m(b)), ACTIVE(d)) 75.08/26.92
TOP(ok(d)) → c12(TOP(mark(c)), ACTIVE(d))

S tuples:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.92
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.92
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.92
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.92
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2 75.08/26.92
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.92
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.92
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.92
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.93
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.93
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.93
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.93
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.93
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.93
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.93
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.93
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.93
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.93
TOP(mark(f(z0, z1, z2))) → c11(TOP(f(proper(z0), proper(z1), proper(z2))), PROPER(f(z0, z1, z2))) 75.08/26.93
TOP(ok(f(b, c, z0))) → c12(TOP(mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.93
TOP(ok(f(z0, z1, z2))) → c12(TOP(f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.93
TOP(ok(d)) → c12(TOP(m(b)), ACTIVE(d)) 75.08/26.93
TOP(ok(d)) → c12(TOP(mark(c)), ACTIVE(d))

K tuples:

TOP(mark(b)) → c11(TOP(ok(b))) 75.08/26.93
TOP(mark(c)) → c11(TOP(ok(c))) 75.08/26.93
TOP(mark(d)) → c11(TOP(ok(d)))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

ACTIVE, F, PROPER, TOP

Compound Symbols:

c1, c5, c6, c2, c2, c2, c10, c10, c11, c11, c12

75.08/26.93

(27) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

ACTIVE(f(b, c, z0)) → c1(F(z0, z0, z0)) 75.08/26.93
ACTIVE(f(x0, x1, f(b, c, z0))) → c2(F(x0, x1, mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.93
ACTIVE(f(x0, x1, f(z0, z1, z2))) → c2(F(x0, x1, f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2))) 75.08/26.93
ACTIVE(f(x0, x1, d)) → c2 75.08/26.93
ACTIVE(f(x0, x1, d)) → c2(F(x0, x1, mark(c))) 75.08/26.93
PROPER(f(x0, x1, f(z0, z1, z2))) → c10(F(proper(x0), proper(x1), f(proper(z0), proper(z1), proper(z2))), PROPER(x0), PROPER(x1), PROPER(f(z0, z1, z2))) 75.08/26.93
PROPER(f(x0, f(z0, z1, z2), x2)) → c10(F(proper(x0), f(proper(z0), proper(z1), proper(z2)), proper(x2)), PROPER(x0), PROPER(f(z0, z1, z2)), PROPER(x2)) 75.08/26.93
PROPER(f(f(z0, z1, z2), x1, x2)) → c10(F(f(proper(z0), proper(z1), proper(z2)), proper(x1), proper(x2)), PROPER(f(z0, z1, z2)), PROPER(x1), PROPER(x2)) 75.08/26.93
PROPER(f(x0, x1, b)) → c10(F(proper(x0), proper(x1), ok(b)), PROPER(x0), PROPER(x1)) 75.08/26.93
PROPER(f(x0, x1, c)) → c10(F(proper(x0), proper(x1), ok(c)), PROPER(x0), PROPER(x1)) 75.08/26.93
PROPER(f(x0, x1, d)) → c10(F(proper(x0), proper(x1), ok(d)), PROPER(x0), PROPER(x1)) 75.08/26.93
PROPER(f(x0, b, x2)) → c10(F(proper(x0), ok(b), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.93
PROPER(f(x0, c, x2)) → c10(F(proper(x0), ok(c), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.93
PROPER(f(x0, d, x2)) → c10(F(proper(x0), ok(d), proper(x2)), PROPER(x0), PROPER(x2)) 75.08/26.93
PROPER(f(b, x1, x2)) → c10(F(ok(b), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.93
PROPER(f(c, x1, x2)) → c10(F(ok(c), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.93
PROPER(f(d, x1, x2)) → c10(F(ok(d), proper(x1), proper(x2)), PROPER(x1), PROPER(x2)) 75.08/26.93
TOP(mark(f(z0, z1, z2))) → c11(TOP(f(proper(z0), proper(z1), proper(z2))), PROPER(f(z0, z1, z2))) 75.08/26.93
TOP(ok(f(b, c, z0))) → c12(TOP(mark(f(z0, z0, z0))), ACTIVE(f(b, c, z0))) 75.08/26.93
TOP(ok(f(z0, z1, z2))) → c12(TOP(f(z0, z1, active(z2))), ACTIVE(f(z0, z1, z2)))

75.08/26.93

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 75.08/26.93
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 75.08/26.93
active(d) → m(b) 75.08/26.93
active(d) → mark(c) 75.08/26.93
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 75.08/26.93
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 75.08/26.93
proper(b) → ok(b) 75.08/26.93
proper(c) → ok(c) 75.08/26.93
proper(d) → ok(d) 75.08/26.93
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 75.08/26.93
top(mark(z0)) → top(proper(z0)) 75.08/26.93
top(ok(z0)) → top(active(z0))

Tuples:

F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.93
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.93
TOP(mark(b)) → c11(TOP(ok(b))) 75.08/26.93
TOP(mark(c)) → c11(TOP(ok(c))) 75.08/26.93
TOP(mark(d)) → c11(TOP(ok(d))) 75.08/26.93
TOP(ok(d)) → c12(TOP(m(b)), ACTIVE(d)) 75.08/26.93
TOP(ok(d)) → c12(TOP(mark(c)), ACTIVE(d))

S tuples:

F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.93
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.93
TOP(ok(d)) → c12(TOP(m(b)), ACTIVE(d)) 75.08/26.93
TOP(ok(d)) → c12(TOP(mark(c)), ACTIVE(d))

K tuples:

TOP(mark(b)) → c11(TOP(ok(b))) 75.08/26.93
TOP(mark(c)) → c11(TOP(ok(c))) 75.08/26.93
TOP(mark(d)) → c11(TOP(ok(d)))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, TOP

Compound Symbols:

c5, c6, c11, c12

75.08/26.93

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

Removed 5 trailing tuple parts

75.08/26.93

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 75.08/26.93
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 75.08/26.93
active(d) → m(b) 75.08/26.93
active(d) → mark(c) 75.08/26.93
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 75.08/26.93
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 75.08/26.93
proper(b) → ok(b) 75.08/26.93
proper(c) → ok(c) 75.08/26.93
proper(d) → ok(d) 75.08/26.93
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 75.08/26.93
top(mark(z0)) → top(proper(z0)) 75.08/26.93
top(ok(z0)) → top(active(z0))

Tuples:

F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.93
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.93
TOP(mark(d)) → c11(TOP(ok(d))) 75.08/26.93
TOP(mark(b)) → c11 75.08/26.93
TOP(mark(c)) → c11 75.08/26.93
TOP(ok(d)) → c12 75.08/26.93
TOP(ok(d)) → c12(TOP(mark(c)))

S tuples:

F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.93
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.93
TOP(ok(d)) → c12 75.08/26.93
TOP(ok(d)) → c12(TOP(mark(c)))

K tuples:

TOP(mark(d)) → c11(TOP(ok(d))) 75.08/26.93
TOP(mark(b)) → c11 75.08/26.93
TOP(mark(c)) → c11

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F, TOP

Compound Symbols:

c5, c6, c11, c11, c12, c12

75.08/26.93

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

Removed 5 trailing nodes:

TOP(ok(d)) → c12 75.08/26.93
TOP(mark(c)) → c11 75.08/26.93
TOP(mark(b)) → c11 75.08/26.93
TOP(mark(d)) → c11(TOP(ok(d))) 75.08/26.93
TOP(ok(d)) → c12(TOP(mark(c)))

75.08/26.93

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 75.08/26.93
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 75.08/26.93
active(d) → m(b) 75.08/26.93
active(d) → mark(c) 75.08/26.93
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 75.08/26.93
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 75.08/26.93
proper(b) → ok(b) 75.08/26.93
proper(c) → ok(c) 75.08/26.93
proper(d) → ok(d) 75.08/26.93
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 75.08/26.93
top(mark(z0)) → top(proper(z0)) 75.08/26.93
top(ok(z0)) → top(active(z0))

Tuples:

F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.93
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2))

S tuples:

F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.93
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2))

K tuples:none
Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F

Compound Symbols:

c5, c6

75.08/26.93

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

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

F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2))

We considered the (Usable) Rules:none
And the Tuples:

F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.93
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2))

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

POL(F(x₁, x₂, x₃)) = x₂² 75.08/26.93
POL(c5(x₁)) = x₁ 75.08/26.93
POL(c6(x₁)) = x₁ 75.08/26.93
POL(mark(x₁)) = 0 75.08/26.93
POL(ok(x₁)) = [1] + x₁

75.08/26.93

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 75.08/26.93
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 75.08/26.93
active(d) → m(b) 75.08/26.93
active(d) → mark(c) 75.08/26.93
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 75.08/26.93
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 75.08/26.93
proper(b) → ok(b) 75.08/26.93
proper(c) → ok(c) 75.08/26.93
proper(d) → ok(d) 75.08/26.93
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 75.08/26.93
top(mark(z0)) → top(proper(z0)) 75.08/26.93
top(ok(z0)) → top(active(z0))

Tuples:

F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.93
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2))

S tuples:

F(z0, z1, mark(z2)) → c5(F(z0, z1, z2))

K tuples:

F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F

Compound Symbols:

c5, c6

75.08/26.93

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

F(z0, z1, mark(z2)) → c5(F(z0, z1, z2))

We considered the (Usable) Rules:none
And the Tuples:

F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.93
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2))

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

POL(F(x₁, x₂, x₃)) = [5]x₁ + [5]x₂ + [5]x₃ 75.08/26.93
POL(c5(x₁)) = x₁ 75.08/26.93
POL(c6(x₁)) = x₁ 75.08/26.93
POL(mark(x₁)) = [1] + x₁ 75.08/26.93
POL(ok(x₁)) = x₁

75.08/26.93

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(b, c, z0)) → mark(f(z0, z0, z0)) 75.08/26.93
active(f(z0, z1, z2)) → f(z0, z1, active(z2)) 75.08/26.93
active(d) → m(b) 75.08/26.93
active(d) → mark(c) 75.08/26.93
f(z0, z1, mark(z2)) → mark(f(z0, z1, z2)) 75.08/26.93
f(ok(z0), ok(z1), ok(z2)) → ok(f(z0, z1, z2)) 75.08/26.93
proper(b) → ok(b) 75.08/26.93
proper(c) → ok(c) 75.08/26.93
proper(d) → ok(d) 75.08/26.93
proper(f(z0, z1, z2)) → f(proper(z0), proper(z1), proper(z2)) 75.08/26.93
top(mark(z0)) → top(proper(z0)) 75.08/26.93
top(ok(z0)) → top(active(z0))

Tuples:

F(z0, z1, mark(z2)) → c5(F(z0, z1, z2)) 75.08/26.93
F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2))

S tuples:none
K tuples:

F(ok(z0), ok(z1), ok(z2)) → c6(F(z0, z1, z2)) 75.08/26.93
F(z0, z1, mark(z2)) → c5(F(z0, z1, z2))

Defined Rule Symbols:

active, f, proper, top

Defined Pair Symbols:

F

Compound Symbols:

c5, c6

75.08/26.93

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

The set S is empty

75.08/26.93

(38) BOUNDS(O(1), O(1))

75.08/26.93