YES(O(1), O(n^1)) 52.85/20.35 YES(O(1), O(n^1)) 52.85/20.39 52.85/20.39 52.85/20.39 52.85/20.39 52.85/20.39 52.85/20.39 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 52.85/20.39 52.85/20.39 52.85/20.39
52.85/20.39
52.85/20.39
52.85/20.39
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
52.85/20.39 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
52.85/20.39 
↳2 CdtProblem
52.85/20.39 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
52.85/20.39 
↳4 CdtProblem
52.85/20.39 
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
52.85/20.39 
↳6 CdtProblem
52.85/20.39 
↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
52.85/20.39 
↳8 CdtProblem
52.85/20.39 
↳9 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
52.85/20.39 
↳10 CdtProblem
52.85/20.39 
↳11 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
52.85/20.39 
↳12 CdtProblem
52.85/20.39 
↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
52.85/20.39 
↳14 CdtProblem
52.85/20.39 
↳15 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
52.85/20.39 
↳16 CdtProblem
52.85/20.39 
↳17 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
52.85/20.39 
↳18 CdtProblem
52.85/20.39 
↳19 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
52.85/20.39 
↳20 CdtProblem
52.85/20.39 
↳21 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
52.85/20.39 
↳22 CdtProblem
52.85/20.39 
↳23 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
52.85/20.39 
↳24 CdtProblem
52.85/20.39 
↳25 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
52.85/20.39 
↳26 CdtProblem
52.85/20.39 
↳27 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
52.85/20.39 
↳28 CdtProblem
52.85/20.39 
↳29 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
52.85/20.39 
↳30 CdtProblem
52.85/20.39 
↳31 CdtUnreachableProof (⇔)
52.85/20.39 
↳32 CdtProblem
52.85/20.39 
↳33 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
52.85/20.39 
↳34 CdtProblem
52.85/20.39 
↳35 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
52.85/20.39 
↳36 CdtProblem
52.85/20.39 
↳37 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
52.85/20.39 
↳38 CdtProblem
52.85/20.39 
↳39 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
52.85/20.39 
↳40 CdtProblem
52.85/20.39 
↳41 SIsEmptyProof (BOTH BOUNDS(ID, ID))
52.85/20.39 
↳42 BOUNDS(O(1), O(1))
52.85/20.39
52.85/20.39 52.85/20.39
52.85/20.39
52.85/20.39

(0) Obligation:

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

active(g(X)) → mark(h(X)) 52.85/20.39
active(c) → mark(d) 52.85/20.39
active(h(d)) → mark(g(c)) 52.85/20.39
proper(g(X)) → g(proper(X)) 52.85/20.39
proper(h(X)) → h(proper(X)) 52.85/20.39
proper(c) → ok(c) 52.85/20.39
proper(d) → ok(d) 52.85/20.39
g(ok(X)) → ok(g(X)) 52.85/20.39
h(ok(X)) → ok(h(X)) 52.85/20.39
top(mark(X)) → top(proper(X)) 52.85/20.39
top(ok(X)) → top(active(X))

Rewrite Strategy: INNERMOST
52.85/20.39
52.85/20.39

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

Converted CpxTRS to CDT
52.85/20.39
52.85/20.39

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 52.85/20.39
active(c) → mark(d) 52.85/20.39
active(h(d)) → mark(g(c)) 52.85/20.39
proper(g(z0)) → g(proper(z0)) 52.85/20.39
proper(h(z0)) → h(proper(z0)) 52.85/20.39
proper(c) → ok(c) 52.85/20.39
proper(d) → ok(d) 52.85/20.39
g(ok(z0)) → ok(g(z0)) 52.85/20.39
h(ok(z0)) → ok(h(z0)) 52.85/20.39
top(mark(z0)) → top(proper(z0)) 52.85/20.39
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 52.85/20.39
ACTIVE(h(d)) → c3(G(c)) 52.85/20.39
PROPER(g(z0)) → c4(G(proper(z0)), PROPER(z0)) 52.85/20.39
PROPER(h(z0)) → c5(H(proper(z0)), PROPER(z0)) 52.85/20.39
G(ok(z0)) → c8(G(z0)) 52.85/20.39
H(ok(z0)) → c9(H(z0)) 52.85/20.39
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 52.85/20.39
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0))
S tuples:

ACTIVE(g(z0)) → c1(H(z0)) 52.85/20.39
ACTIVE(h(d)) → c3(G(c)) 52.85/20.39
PROPER(g(z0)) → c4(G(proper(z0)), PROPER(z0)) 52.85/20.39
PROPER(h(z0)) → c5(H(proper(z0)), PROPER(z0)) 52.85/20.39
G(ok(z0)) → c8(G(z0)) 52.85/20.39
H(ok(z0)) → c9(H(z0)) 52.85/20.39
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 52.85/20.39
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0))
K tuples:none
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

ACTIVE, PROPER, G, H, TOP

Compound Symbols:

c1, c3, c4, c5, c8, c9, c10, c11

52.85/20.39
52.85/20.39

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

Removed 1 trailing tuple parts
52.85/20.39
52.85/20.39

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 52.85/20.39
active(c) → mark(d) 52.85/20.39
active(h(d)) → mark(g(c)) 52.85/20.39
proper(g(z0)) → g(proper(z0)) 52.85/20.40
proper(h(z0)) → h(proper(z0)) 52.85/20.40
proper(c) → ok(c) 52.85/20.40
proper(d) → ok(d) 52.85/20.40
g(ok(z0)) → ok(g(z0)) 52.85/20.40
h(ok(z0)) → ok(h(z0)) 52.85/20.40
top(mark(z0)) → top(proper(z0)) 52.85/20.40
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 52.85/20.40
PROPER(g(z0)) → c4(G(proper(z0)), PROPER(z0)) 52.85/20.40
PROPER(h(z0)) → c5(H(proper(z0)), PROPER(z0)) 52.85/20.40
G(ok(z0)) → c8(G(z0)) 52.85/20.40
H(ok(z0)) → c9(H(z0)) 52.85/20.40
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 52.85/20.40
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 52.85/20.40
ACTIVE(h(d)) → c3
S tuples:

ACTIVE(g(z0)) → c1(H(z0)) 52.85/20.40
PROPER(g(z0)) → c4(G(proper(z0)), PROPER(z0)) 52.85/20.40
PROPER(h(z0)) → c5(H(proper(z0)), PROPER(z0)) 52.85/20.40
G(ok(z0)) → c8(G(z0)) 52.85/20.40
H(ok(z0)) → c9(H(z0)) 52.85/20.40
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 52.85/20.40
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 52.85/20.40
ACTIVE(h(d)) → c3
K tuples:none
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

ACTIVE, PROPER, G, H, TOP

Compound Symbols:

c1, c4, c5, c8, c9, c10, c11, c3

52.85/20.40
52.85/20.40

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

Removed 1 trailing nodes:

ACTIVE(h(d)) → c3
52.85/20.40
52.85/20.40

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 52.85/20.40
active(c) → mark(d) 52.85/20.40
active(h(d)) → mark(g(c)) 52.85/20.40
proper(g(z0)) → g(proper(z0)) 52.85/20.40
proper(h(z0)) → h(proper(z0)) 52.85/20.40
proper(c) → ok(c) 52.85/20.40
proper(d) → ok(d) 52.85/20.40
g(ok(z0)) → ok(g(z0)) 52.85/20.40
h(ok(z0)) → ok(h(z0)) 52.85/20.40
top(mark(z0)) → top(proper(z0)) 52.85/20.40
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 52.85/20.40
PROPER(g(z0)) → c4(G(proper(z0)), PROPER(z0)) 52.85/20.40
PROPER(h(z0)) → c5(H(proper(z0)), PROPER(z0)) 52.85/20.40
G(ok(z0)) → c8(G(z0)) 52.85/20.40
H(ok(z0)) → c9(H(z0)) 52.85/20.40
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 52.85/20.40
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 52.85/20.40
ACTIVE(h(d)) → c3
S tuples:

ACTIVE(g(z0)) → c1(H(z0)) 52.85/20.40
PROPER(g(z0)) → c4(G(proper(z0)), PROPER(z0)) 52.85/20.40
PROPER(h(z0)) → c5(H(proper(z0)), PROPER(z0)) 52.85/20.40
G(ok(z0)) → c8(G(z0)) 52.85/20.40
H(ok(z0)) → c9(H(z0)) 52.85/20.40
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 52.85/20.40
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 52.85/20.40
ACTIVE(h(d)) → c3
K tuples:none
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

ACTIVE, PROPER, G, H, TOP

Compound Symbols:

c1, c4, c5, c8, c9, c10, c11, c3

52.85/20.40
52.85/20.40

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

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

PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 52.85/20.40
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 52.85/20.40
PROPER(g(c)) → c4(G(ok(c)), PROPER(c)) 52.85/20.40
PROPER(g(d)) → c4(G(ok(d)), PROPER(d))
52.85/20.40
52.85/20.40

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 52.85/20.40
active(c) → mark(d) 52.85/20.40
active(h(d)) → mark(g(c)) 52.85/20.40
proper(g(z0)) → g(proper(z0)) 52.85/20.40
proper(h(z0)) → h(proper(z0)) 52.85/20.40
proper(c) → ok(c) 52.85/20.40
proper(d) → ok(d) 52.85/20.40
g(ok(z0)) → ok(g(z0)) 52.85/20.40
h(ok(z0)) → ok(h(z0)) 52.85/20.40
top(mark(z0)) → top(proper(z0)) 52.85/20.40
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 52.85/20.40
PROPER(h(z0)) → c5(H(proper(z0)), PROPER(z0)) 52.85/20.40
G(ok(z0)) → c8(G(z0)) 52.85/20.40
H(ok(z0)) → c9(H(z0)) 52.85/20.40
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 52.85/20.40
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 52.85/20.40
ACTIVE(h(d)) → c3 52.85/20.40
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 52.85/20.40
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 52.85/20.40
PROPER(g(c)) → c4(G(ok(c)), PROPER(c)) 52.85/20.40
PROPER(g(d)) → c4(G(ok(d)), PROPER(d))
S tuples:

ACTIVE(g(z0)) → c1(H(z0)) 52.85/20.40
PROPER(h(z0)) → c5(H(proper(z0)), PROPER(z0)) 52.85/20.40
G(ok(z0)) → c8(G(z0)) 52.85/20.40
H(ok(z0)) → c9(H(z0)) 52.85/20.40
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 52.85/20.40
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 52.85/20.40
ACTIVE(h(d)) → c3 52.85/20.40
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 52.85/20.40
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 52.85/20.40
PROPER(g(c)) → c4(G(ok(c)), PROPER(c)) 52.85/20.40
PROPER(g(d)) → c4(G(ok(d)), PROPER(d))
K tuples:none
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

ACTIVE, PROPER, G, H, TOP

Compound Symbols:

c1, c5, c8, c9, c10, c11, c3, c4

53.10/20.41
53.10/20.41

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

Removed 2 trailing tuple parts
53.10/20.41
53.10/20.41

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c)) 53.10/20.41
proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
top(mark(z0)) → top(proper(z0)) 53.10/20.41
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
PROPER(h(z0)) → c5(H(proper(z0)), PROPER(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d)))
S tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
PROPER(h(z0)) → c5(H(proper(z0)), PROPER(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d)))
K tuples:none
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

ACTIVE, PROPER, G, H, TOP

Compound Symbols:

c1, c5, c8, c9, c10, c11, c3, c4, c4

53.10/20.41
53.10/20.41

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

Removed 1 trailing nodes:

ACTIVE(h(d)) → c3
53.10/20.41
53.10/20.41

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c)) 53.10/20.41
proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
top(mark(z0)) → top(proper(z0)) 53.10/20.41
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
PROPER(h(z0)) → c5(H(proper(z0)), PROPER(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d)))
S tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
PROPER(h(z0)) → c5(H(proper(z0)), PROPER(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d)))
K tuples:none
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

ACTIVE, PROPER, G, H, TOP

Compound Symbols:

c1, c5, c8, c9, c10, c11, c3, c4, c4

53.10/20.41
53.10/20.41

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

Use narrowing to replace PROPER(h(z0)) → c5(H(proper(z0)), PROPER(z0)) by

PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c)), PROPER(c)) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d)), PROPER(d))
53.10/20.41
53.10/20.41

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c)) 53.10/20.41
proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
top(mark(z0)) → top(proper(z0)) 53.10/20.41
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c)), PROPER(c)) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d)), PROPER(d))
S tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c)), PROPER(c)) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d)), PROPER(d))
K tuples:none
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

ACTIVE, G, H, TOP, PROPER

Compound Symbols:

c1, c8, c9, c10, c11, c3, c4, c4, c5

53.10/20.41
53.10/20.41

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

Removed 2 trailing tuple parts
53.10/20.41
53.10/20.41

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c)) 53.10/20.41
proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
top(mark(z0)) → top(proper(z0)) 53.10/20.41
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d)))
S tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d)))
K tuples:none
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

ACTIVE, G, H, TOP, PROPER

Compound Symbols:

c1, c8, c9, c10, c11, c3, c4, c4, c5, c5

53.10/20.41
53.10/20.41

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

Removed 1 trailing nodes:

ACTIVE(h(d)) → c3
53.10/20.41
53.10/20.41

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c)) 53.10/20.41
proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
top(mark(z0)) → top(proper(z0)) 53.10/20.41
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d)))
S tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(mark(z0)) → c10(TOP(proper(z0)), PROPER(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d)))
K tuples:none
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

ACTIVE, G, H, TOP, PROPER

Compound Symbols:

c1, c8, c9, c10, c11, c3, c4, c4, c5, c5

53.10/20.41
53.10/20.41

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

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

TOP(mark(g(z0))) → c10(TOP(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
TOP(mark(h(z0))) → c10(TOP(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
TOP(mark(c)) → c10(TOP(ok(c)), PROPER(c)) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d)), PROPER(d))
53.10/20.41
53.10/20.41

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c)) 53.10/20.41
proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
top(mark(z0)) → top(proper(z0)) 53.10/20.41
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d))) 53.10/20.41
TOP(mark(g(z0))) → c10(TOP(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
TOP(mark(h(z0))) → c10(TOP(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
TOP(mark(c)) → c10(TOP(ok(c)), PROPER(c)) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d)), PROPER(d))
S tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d))) 53.10/20.41
TOP(mark(g(z0))) → c10(TOP(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
TOP(mark(h(z0))) → c10(TOP(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
TOP(mark(c)) → c10(TOP(ok(c)), PROPER(c)) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d)), PROPER(d))
K tuples:none
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

ACTIVE, G, H, TOP, PROPER

Compound Symbols:

c1, c8, c9, c11, c3, c4, c4, c5, c5, c10

53.10/20.41
53.10/20.41

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

Removed 2 trailing tuple parts
53.10/20.41
53.10/20.41

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c)) 53.10/20.41
proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
top(mark(z0)) → top(proper(z0)) 53.10/20.41
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d))) 53.10/20.41
TOP(mark(g(z0))) → c10(TOP(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
TOP(mark(h(z0))) → c10(TOP(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
TOP(mark(c)) → c10(TOP(ok(c))) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d)))
S tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d))) 53.10/20.41
TOP(mark(g(z0))) → c10(TOP(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
TOP(mark(h(z0))) → c10(TOP(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
TOP(mark(c)) → c10(TOP(ok(c))) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d)))
K tuples:none
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

ACTIVE, G, H, TOP, PROPER

Compound Symbols:

c1, c8, c9, c11, c3, c4, c4, c5, c5, c10, c10

53.10/20.41
53.10/20.41

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

Removed 1 trailing nodes:

ACTIVE(h(d)) → c3
53.10/20.41
53.10/20.41

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c)) 53.10/20.41
proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
top(mark(z0)) → top(proper(z0)) 53.10/20.41
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d))) 53.10/20.41
TOP(mark(g(z0))) → c10(TOP(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
TOP(mark(h(z0))) → c10(TOP(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
TOP(mark(c)) → c10(TOP(ok(c))) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d)))
S tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d))) 53.10/20.41
TOP(mark(g(z0))) → c10(TOP(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
TOP(mark(h(z0))) → c10(TOP(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
TOP(mark(c)) → c10(TOP(ok(c))) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d)))
K tuples:none
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

ACTIVE, G, H, TOP, PROPER

Compound Symbols:

c1, c8, c9, c11, c3, c4, c4, c5, c5, c10, c10

53.10/20.41
53.10/20.41

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

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

TOP(mark(c)) → c10(TOP(ok(c)))
We considered the (Usable) Rules:

proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c))
And the Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d))) 53.10/20.41
TOP(mark(g(z0))) → c10(TOP(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
TOP(mark(h(z0))) → c10(TOP(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
TOP(mark(c)) → c10(TOP(ok(c))) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d)))
The order we found is given by the following interpretation:
Polynomial interpretation : 53.10/20.41

POL(ACTIVE(x1)) = 0    53.10/20.41
POL(G(x1)) = 0    53.10/20.41
POL(H(x1)) = 0    53.10/20.41
POL(PROPER(x1)) = 0    53.10/20.41
POL(TOP(x1)) = x1    53.10/20.41
POL(active(x1)) = 0    53.10/20.41
POL(c) = [1]    53.10/20.41
POL(c1(x1)) = x1    53.10/20.41
POL(c10(x1)) = x1    53.10/20.41
POL(c10(x1, x2)) = x1 + x2    53.10/20.41
POL(c11(x1, x2)) = x1 + x2    53.10/20.41
POL(c3) = 0    53.10/20.41
POL(c4(x1)) = x1    53.10/20.41
POL(c4(x1, x2)) = x1 + x2    53.10/20.41
POL(c5(x1)) = x1    53.10/20.41
POL(c5(x1, x2)) = x1 + x2    53.10/20.41
POL(c8(x1)) = x1    53.10/20.41
POL(c9(x1)) = x1    53.10/20.41
POL(d) = 0    53.10/20.41
POL(g(x1)) = 0    53.10/20.41
POL(h(x1)) = 0    53.10/20.41
POL(mark(x1)) = x1    53.10/20.41
POL(ok(x1)) = 0    53.10/20.41
POL(proper(x1)) = 0   
53.10/20.41
53.10/20.41

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c)) 53.10/20.41
proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
top(mark(z0)) → top(proper(z0)) 53.10/20.41
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d))) 53.10/20.41
TOP(mark(g(z0))) → c10(TOP(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
TOP(mark(h(z0))) → c10(TOP(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
TOP(mark(c)) → c10(TOP(ok(c))) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d)))
S tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d))) 53.10/20.41
TOP(mark(g(z0))) → c10(TOP(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
TOP(mark(h(z0))) → c10(TOP(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d)))
K tuples:

TOP(mark(c)) → c10(TOP(ok(c)))
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

ACTIVE, G, H, TOP, PROPER

Compound Symbols:

c1, c8, c9, c11, c3, c4, c4, c5, c5, c10, c10

53.10/20.41
53.10/20.41

(27) 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)) → c10(TOP(ok(d)))
We considered the (Usable) Rules:

proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c))
And the Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d))) 53.10/20.41
TOP(mark(g(z0))) → c10(TOP(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
TOP(mark(h(z0))) → c10(TOP(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
TOP(mark(c)) → c10(TOP(ok(c))) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d)))
The order we found is given by the following interpretation:
Polynomial interpretation : 53.10/20.41

POL(ACTIVE(x1)) = 0    53.10/20.41
POL(G(x1)) = 0    53.10/20.41
POL(H(x1)) = 0    53.10/20.41
POL(PROPER(x1)) = 0    53.10/20.41
POL(TOP(x1)) = [4]x1    53.10/20.41
POL(active(x1)) = x1    53.10/20.41
POL(c) = [2]    53.10/20.41
POL(c1(x1)) = x1    53.10/20.41
POL(c10(x1)) = x1    53.10/20.41
POL(c10(x1, x2)) = x1 + x2    53.10/20.41
POL(c11(x1, x2)) = x1 + x2    53.10/20.41
POL(c3) = 0    53.10/20.41
POL(c4(x1)) = x1    53.10/20.41
POL(c4(x1, x2)) = x1 + x2    53.10/20.41
POL(c5(x1)) = x1    53.10/20.41
POL(c5(x1, x2)) = x1 + x2    53.10/20.41
POL(c8(x1)) = x1    53.10/20.41
POL(c9(x1)) = x1    53.10/20.41
POL(d) = 0    53.10/20.41
POL(g(x1)) = [2]    53.10/20.41
POL(h(x1)) = [2]    53.10/20.41
POL(mark(x1)) = [2]    53.10/20.41
POL(ok(x1)) = x1    53.10/20.41
POL(proper(x1)) = 0   
53.10/20.41
53.10/20.41

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c)) 53.10/20.41
proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
top(mark(z0)) → top(proper(z0)) 53.10/20.41
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d))) 53.10/20.41
TOP(mark(g(z0))) → c10(TOP(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
TOP(mark(h(z0))) → c10(TOP(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
TOP(mark(c)) → c10(TOP(ok(c))) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d)))
S tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(ok(z0)) → c11(TOP(active(z0)), ACTIVE(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d))) 53.10/20.41
TOP(mark(g(z0))) → c10(TOP(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
TOP(mark(h(z0))) → c10(TOP(h(proper(z0))), PROPER(h(z0)))
K tuples:

TOP(mark(c)) → c10(TOP(ok(c))) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d)))
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

ACTIVE, G, H, TOP, PROPER

Compound Symbols:

c1, c8, c9, c11, c3, c4, c4, c5, c5, c10, c10

53.10/20.41
53.10/20.41

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

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

TOP(ok(g(z0))) → c11(TOP(mark(h(z0))), ACTIVE(g(z0))) 53.10/20.41
TOP(ok(c)) → c11(TOP(mark(d)), ACTIVE(c)) 53.10/20.41
TOP(ok(h(d))) → c11(TOP(mark(g(c))), ACTIVE(h(d)))
53.10/20.41
53.10/20.41

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c)) 53.10/20.41
proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
top(mark(z0)) → top(proper(z0)) 53.10/20.41
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d))) 53.10/20.41
TOP(mark(g(z0))) → c10(TOP(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
TOP(mark(h(z0))) → c10(TOP(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
TOP(mark(c)) → c10(TOP(ok(c))) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d))) 53.10/20.41
TOP(ok(g(z0))) → c11(TOP(mark(h(z0))), ACTIVE(g(z0))) 53.10/20.41
TOP(ok(c)) → c11(TOP(mark(d)), ACTIVE(c)) 53.10/20.41
TOP(ok(h(d))) → c11(TOP(mark(g(c))), ACTIVE(h(d)))
S tuples:

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d))) 53.10/20.41
TOP(mark(g(z0))) → c10(TOP(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
TOP(mark(h(z0))) → c10(TOP(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
TOP(ok(g(z0))) → c11(TOP(mark(h(z0))), ACTIVE(g(z0))) 53.10/20.41
TOP(ok(c)) → c11(TOP(mark(d)), ACTIVE(c)) 53.10/20.41
TOP(ok(h(d))) → c11(TOP(mark(g(c))), ACTIVE(h(d)))
K tuples:

TOP(mark(c)) → c10(TOP(ok(c))) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d)))
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

ACTIVE, G, H, PROPER, TOP

Compound Symbols:

c1, c8, c9, c3, c4, c4, c5, c5, c10, c10, c11

53.10/20.41
53.10/20.41

(31) CdtUnreachableProof (EQUIVALENT transformation)

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

ACTIVE(g(z0)) → c1(H(z0)) 53.10/20.41
ACTIVE(h(d)) → c3 53.10/20.41
PROPER(g(g(z0))) → c4(G(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(g(h(z0))) → c4(G(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(g(c)) → c4(G(ok(c))) 53.10/20.41
PROPER(g(d)) → c4(G(ok(d))) 53.10/20.41
PROPER(h(g(z0))) → c5(H(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
PROPER(h(h(z0))) → c5(H(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
PROPER(h(c)) → c5(H(ok(c))) 53.10/20.41
PROPER(h(d)) → c5(H(ok(d))) 53.10/20.41
TOP(mark(g(z0))) → c10(TOP(g(proper(z0))), PROPER(g(z0))) 53.10/20.41
TOP(mark(h(z0))) → c10(TOP(h(proper(z0))), PROPER(h(z0))) 53.10/20.41
TOP(ok(g(z0))) → c11(TOP(mark(h(z0))), ACTIVE(g(z0))) 53.10/20.41
TOP(ok(h(d))) → c11(TOP(mark(g(c))), ACTIVE(h(d)))
53.10/20.41
53.10/20.41

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c)) 53.10/20.41
proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
top(mark(z0)) → top(proper(z0)) 53.10/20.41
top(ok(z0)) → top(active(z0))
Tuples:

G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(mark(c)) → c10(TOP(ok(c))) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d))) 53.10/20.41
TOP(ok(c)) → c11(TOP(mark(d)), ACTIVE(c))
S tuples:

G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(ok(c)) → c11(TOP(mark(d)), ACTIVE(c))
K tuples:

TOP(mark(c)) → c10(TOP(ok(c))) 53.10/20.41
TOP(mark(d)) → c10(TOP(ok(d)))
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

G, H, TOP

Compound Symbols:

c8, c9, c10, c11

53.10/20.41
53.10/20.41

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

Removed 2 trailing tuple parts
53.10/20.41
53.10/20.41

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c)) 53.10/20.41
proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
top(mark(z0)) → top(proper(z0)) 53.10/20.41
top(ok(z0)) → top(active(z0))
Tuples:

G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(mark(c)) → c10(TOP(ok(c))) 53.10/20.41
TOP(mark(d)) → c10 53.10/20.41
TOP(ok(c)) → c11(TOP(mark(d)))
S tuples:

G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0)) 53.10/20.41
TOP(ok(c)) → c11(TOP(mark(d)))
K tuples:

TOP(mark(c)) → c10(TOP(ok(c))) 53.10/20.41
TOP(mark(d)) → c10
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

G, H, TOP

Compound Symbols:

c8, c9, c10, c10, c11

53.10/20.41
53.10/20.41

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

Removed 3 trailing nodes:

TOP(mark(d)) → c10 53.10/20.41
TOP(mark(c)) → c10(TOP(ok(c))) 53.10/20.41
TOP(ok(c)) → c11(TOP(mark(d)))
53.10/20.41
53.10/20.41

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c)) 53.10/20.41
proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
top(mark(z0)) → top(proper(z0)) 53.10/20.41
top(ok(z0)) → top(active(z0))
Tuples:

G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0))
S tuples:

G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0))
K tuples:none
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

G, H

Compound Symbols:

c8, c9

53.10/20.41
53.10/20.41

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

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

H(ok(z0)) → c9(H(z0))
We considered the (Usable) Rules:none
And the Tuples:

G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 53.10/20.41

POL(G(x1)) = 0    53.10/20.41
POL(H(x1)) = x1    53.10/20.41
POL(c8(x1)) = x1    53.10/20.41
POL(c9(x1)) = x1    53.10/20.41
POL(ok(x1)) = [1] + x1   
53.10/20.41
53.10/20.41

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c)) 53.10/20.41
proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
top(mark(z0)) → top(proper(z0)) 53.10/20.41
top(ok(z0)) → top(active(z0))
Tuples:

G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0))
S tuples:

G(ok(z0)) → c8(G(z0))
K tuples:

H(ok(z0)) → c9(H(z0))
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

G, H

Compound Symbols:

c8, c9

53.10/20.41
53.10/20.41

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

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

G(ok(z0)) → c8(G(z0))
We considered the (Usable) Rules:none
And the Tuples:

G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 53.10/20.41

POL(G(x1)) = [5]x1    53.10/20.41
POL(H(x1)) = [5]x1    53.10/20.41
POL(c8(x1)) = x1    53.10/20.41
POL(c9(x1)) = x1    53.10/20.41
POL(ok(x1)) = [1] + x1   
53.10/20.41
53.10/20.41

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(g(z0)) → mark(h(z0)) 53.10/20.41
active(c) → mark(d) 53.10/20.41
active(h(d)) → mark(g(c)) 53.10/20.41
proper(g(z0)) → g(proper(z0)) 53.10/20.41
proper(h(z0)) → h(proper(z0)) 53.10/20.41
proper(c) → ok(c) 53.10/20.41
proper(d) → ok(d) 53.10/20.41
g(ok(z0)) → ok(g(z0)) 53.10/20.41
h(ok(z0)) → ok(h(z0)) 53.10/20.41
top(mark(z0)) → top(proper(z0)) 53.10/20.41
top(ok(z0)) → top(active(z0))
Tuples:

G(ok(z0)) → c8(G(z0)) 53.10/20.41
H(ok(z0)) → c9(H(z0))
S tuples:none
K tuples:

H(ok(z0)) → c9(H(z0)) 53.10/20.41
G(ok(z0)) → c8(G(z0))
Defined Rule Symbols:

active, proper, g, h, top

Defined Pair Symbols:

G, H

Compound Symbols:

c8, c9

53.10/20.41
53.10/20.41

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

The set S is empty
53.10/20.41
53.10/20.41

(42) BOUNDS(O(1), O(1))

53.10/20.41
53.10/20.41
53.10/20.46 EOF