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

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

(0) Obligation:

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

active(f(f(a))) → mark(f(g(f(a)))) 106.60/33.00
active(g(X)) → g(active(X)) 106.60/33.00
g(mark(X)) → mark(g(X)) 106.60/33.00
proper(f(X)) → f(proper(X)) 106.60/33.00
proper(a) → ok(a) 106.60/33.00
proper(g(X)) → g(proper(X)) 106.60/33.00
f(ok(X)) → ok(f(X)) 106.60/33.00
g(ok(X)) → ok(g(X)) 106.60/33.00
top(mark(X)) → top(proper(X)) 106.60/33.00
top(ok(X)) → top(active(X))

Rewrite Strategy: INNERMOST
106.60/33.00
106.60/33.00

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

Converted CpxTRS to CDT
106.60/33.00
106.60/33.00

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.60/33.00
active(g(z0)) → g(active(z0)) 106.60/33.00
g(mark(z0)) → mark(g(z0)) 106.60/33.00
g(ok(z0)) → ok(g(z0)) 106.60/33.00
proper(f(z0)) → f(proper(z0)) 106.60/33.00
proper(a) → ok(a) 106.60/33.00
proper(g(z0)) → g(proper(z0)) 106.60/33.00
f(ok(z0)) → ok(f(z0)) 106.60/33.00
top(mark(z0)) → top(proper(z0)) 106.60/33.00
top(ok(z0)) → top(active(z0))
Tuples:

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

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

active, g, proper, f, top

Defined Pair Symbols:

ACTIVE, G, PROPER, F, TOP

Compound Symbols:

c, c1, c2, c3, c4, c6, c7, c8, c9

106.60/33.00
106.60/33.00

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

Removed 3 trailing tuple parts
106.60/33.00
106.60/33.00

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.60/33.00
active(g(z0)) → g(active(z0)) 106.60/33.00
g(mark(z0)) → mark(g(z0)) 106.60/33.00
g(ok(z0)) → ok(g(z0)) 106.60/33.00
proper(f(z0)) → f(proper(z0)) 106.60/33.00
proper(a) → ok(a) 106.60/33.00
proper(g(z0)) → g(proper(z0)) 106.60/33.00
f(ok(z0)) → ok(f(z0)) 106.60/33.00
top(mark(z0)) → top(proper(z0)) 106.60/33.00
top(ok(z0)) → top(active(z0))
Tuples:

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

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

active, g, proper, f, top

Defined Pair Symbols:

ACTIVE, G, PROPER, F, TOP

Compound Symbols:

c1, c2, c3, c4, c6, c7, c8, c9, c

106.60/33.01
106.60/33.01

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

Removed 1 trailing nodes:

ACTIVE(f(f(a))) → c
106.60/33.01
106.60/33.01

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.60/33.01
active(g(z0)) → g(active(z0)) 106.60/33.01
g(mark(z0)) → mark(g(z0)) 106.60/33.01
g(ok(z0)) → ok(g(z0)) 106.60/33.01
proper(f(z0)) → f(proper(z0)) 106.60/33.01
proper(a) → ok(a) 106.60/33.01
proper(g(z0)) → g(proper(z0)) 106.60/33.01
f(ok(z0)) → ok(f(z0)) 106.60/33.01
top(mark(z0)) → top(proper(z0)) 106.60/33.01
top(ok(z0)) → top(active(z0))
Tuples:

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

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

active, g, proper, f, top

Defined Pair Symbols:

ACTIVE, G, PROPER, F, TOP

Compound Symbols:

c1, c2, c3, c4, c6, c7, c8, c9, c

106.94/33.01
106.94/33.01

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

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

ACTIVE(g(f(f(a)))) → c1(G(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 106.94/33.01
ACTIVE(g(g(z0))) → c1(G(g(active(z0))), ACTIVE(g(z0)))
106.94/33.01
106.94/33.01

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.01
active(g(z0)) → g(active(z0)) 106.94/33.01
g(mark(z0)) → mark(g(z0)) 106.94/33.01
g(ok(z0)) → ok(g(z0)) 106.94/33.01
proper(f(z0)) → f(proper(z0)) 106.94/33.01
proper(a) → ok(a) 106.94/33.01
proper(g(z0)) → g(proper(z0)) 106.94/33.01
f(ok(z0)) → ok(f(z0)) 106.94/33.01
top(mark(z0)) → top(proper(z0)) 106.94/33.01
top(ok(z0)) → top(active(z0))
Tuples:

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

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

active, g, proper, f, top

Defined Pair Symbols:

G, PROPER, F, TOP, ACTIVE

Compound Symbols:

c2, c3, c4, c6, c7, c8, c9, c, c1

106.94/33.01
106.94/33.01

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

Split RHS of tuples not part of any SCC
106.94/33.01
106.94/33.01

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.01
active(g(z0)) → g(active(z0)) 106.94/33.01
g(mark(z0)) → mark(g(z0)) 106.94/33.01
g(ok(z0)) → ok(g(z0)) 106.94/33.01
proper(f(z0)) → f(proper(z0)) 106.94/33.01
proper(a) → ok(a) 106.94/33.01
proper(g(z0)) → g(proper(z0)) 106.94/33.01
f(ok(z0)) → ok(f(z0)) 106.94/33.01
top(mark(z0)) → top(proper(z0)) 106.94/33.01
top(ok(z0)) → top(active(z0))
Tuples:

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

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

active, g, proper, f, top

Defined Pair Symbols:

G, PROPER, F, TOP, ACTIVE

Compound Symbols:

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

106.94/33.01
106.94/33.01

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

Removed 2 trailing nodes:

ACTIVE(g(f(f(a)))) → c5(ACTIVE(f(f(a)))) 106.94/33.01
ACTIVE(f(f(a))) → c
106.94/33.01
106.94/33.01

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.01
active(g(z0)) → g(active(z0)) 106.94/33.01
g(mark(z0)) → mark(g(z0)) 106.94/33.01
g(ok(z0)) → ok(g(z0)) 106.94/33.01
proper(f(z0)) → f(proper(z0)) 106.94/33.01
proper(a) → ok(a) 106.94/33.01
proper(g(z0)) → g(proper(z0)) 106.94/33.01
f(ok(z0)) → ok(f(z0)) 106.94/33.01
top(mark(z0)) → top(proper(z0)) 106.94/33.01
top(ok(z0)) → top(active(z0))
Tuples:

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

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

active, g, proper, f, top

Defined Pair Symbols:

G, PROPER, F, TOP, ACTIVE

Compound Symbols:

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

106.94/33.01
106.94/33.01

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

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

PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 106.94/33.01
PROPER(f(a)) → c4(F(ok(a)), PROPER(a)) 106.94/33.01
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
106.94/33.01
106.94/33.01

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.01
active(g(z0)) → g(active(z0)) 106.94/33.01
g(mark(z0)) → mark(g(z0)) 106.94/33.01
g(ok(z0)) → ok(g(z0)) 106.94/33.01
proper(f(z0)) → f(proper(z0)) 106.94/33.01
proper(a) → ok(a) 106.94/33.01
proper(g(z0)) → g(proper(z0)) 106.94/33.01
f(ok(z0)) → ok(f(z0)) 106.94/33.01
top(mark(z0)) → top(proper(z0)) 106.94/33.01
top(ok(z0)) → top(active(z0))
Tuples:

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

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

active, g, proper, f, top

Defined Pair Symbols:

G, PROPER, F, TOP, ACTIVE

Compound Symbols:

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

106.94/33.01
106.94/33.01

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

Removed 1 trailing tuple parts
106.94/33.01
106.94/33.01

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.01
active(g(z0)) → g(active(z0)) 106.94/33.01
g(mark(z0)) → mark(g(z0)) 106.94/33.01
g(ok(z0)) → ok(g(z0)) 106.94/33.01
proper(f(z0)) → f(proper(z0)) 106.94/33.01
proper(a) → ok(a) 106.94/33.01
proper(g(z0)) → g(proper(z0)) 106.94/33.01
f(ok(z0)) → ok(f(z0)) 106.94/33.01
top(mark(z0)) → top(proper(z0)) 106.94/33.01
top(ok(z0)) → top(active(z0))
Tuples:

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

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

active, g, proper, f, top

Defined Pair Symbols:

G, PROPER, F, TOP, ACTIVE

Compound Symbols:

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

106.94/33.01
106.94/33.01

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

Removed 2 trailing nodes:

ACTIVE(g(f(f(a)))) → c5(ACTIVE(f(f(a)))) 106.94/33.01
ACTIVE(f(f(a))) → c
106.94/33.01
106.94/33.01

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.01
active(g(z0)) → g(active(z0)) 106.94/33.01
g(mark(z0)) → mark(g(z0)) 106.94/33.01
g(ok(z0)) → ok(g(z0)) 106.94/33.01
proper(f(z0)) → f(proper(z0)) 106.94/33.01
proper(a) → ok(a) 106.94/33.01
proper(g(z0)) → g(proper(z0)) 106.94/33.01
f(ok(z0)) → ok(f(z0)) 106.94/33.01
top(mark(z0)) → top(proper(z0)) 106.94/33.01
top(ok(z0)) → top(active(z0))
Tuples:

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

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

active, g, proper, f, top

Defined Pair Symbols:

G, PROPER, F, TOP, ACTIVE

Compound Symbols:

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

106.94/33.01
106.94/33.01

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

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

PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 106.94/33.01
PROPER(g(a)) → c6(G(ok(a)), PROPER(a)) 106.94/33.01
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0)))
106.94/33.01
106.94/33.01

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.01
active(g(z0)) → g(active(z0)) 106.94/33.01
g(mark(z0)) → mark(g(z0)) 106.94/33.01
g(ok(z0)) → ok(g(z0)) 106.94/33.01
proper(f(z0)) → f(proper(z0)) 106.94/33.01
proper(a) → ok(a) 106.94/33.01
proper(g(z0)) → g(proper(z0)) 106.94/33.01
f(ok(z0)) → ok(f(z0)) 106.94/33.01
top(mark(z0)) → top(proper(z0)) 106.94/33.01
top(ok(z0)) → top(active(z0))
Tuples:

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

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

active, g, proper, f, top

Defined Pair Symbols:

G, F, TOP, ACTIVE, PROPER

Compound Symbols:

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

106.94/33.02
106.94/33.02

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

Removed 1 trailing tuple parts
106.94/33.02
106.94/33.02

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.02
active(g(z0)) → g(active(z0)) 106.94/33.02
g(mark(z0)) → mark(g(z0)) 106.94/33.02
g(ok(z0)) → ok(g(z0)) 106.94/33.02
proper(f(z0)) → f(proper(z0)) 106.94/33.02
proper(a) → ok(a) 106.94/33.02
proper(g(z0)) → g(proper(z0)) 106.94/33.02
f(ok(z0)) → ok(f(z0)) 106.94/33.02
top(mark(z0)) → top(proper(z0)) 106.94/33.02
top(ok(z0)) → top(active(z0))
Tuples:

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

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

active, g, proper, f, top

Defined Pair Symbols:

G, F, TOP, ACTIVE, PROPER

Compound Symbols:

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

106.94/33.02
106.94/33.02

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

Removed 2 trailing nodes:

ACTIVE(g(f(f(a)))) → c5(ACTIVE(f(f(a)))) 106.94/33.02
ACTIVE(f(f(a))) → c
106.94/33.02
106.94/33.02

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.02
active(g(z0)) → g(active(z0)) 106.94/33.02
g(mark(z0)) → mark(g(z0)) 106.94/33.02
g(ok(z0)) → ok(g(z0)) 106.94/33.02
proper(f(z0)) → f(proper(z0)) 106.94/33.02
proper(a) → ok(a) 106.94/33.02
proper(g(z0)) → g(proper(z0)) 106.94/33.02
f(ok(z0)) → ok(f(z0)) 106.94/33.02
top(mark(z0)) → top(proper(z0)) 106.94/33.02
top(ok(z0)) → top(active(z0))
Tuples:

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

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

active, g, proper, f, top

Defined Pair Symbols:

G, F, TOP, ACTIVE, PROPER

Compound Symbols:

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

106.94/33.02
106.94/33.02

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

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

TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0))) 106.94/33.02
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a)) 106.94/33.02
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
106.94/33.02
106.94/33.02

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.02
active(g(z0)) → g(active(z0)) 106.94/33.02
g(mark(z0)) → mark(g(z0)) 106.94/33.02
g(ok(z0)) → ok(g(z0)) 106.94/33.02
proper(f(z0)) → f(proper(z0)) 106.94/33.02
proper(a) → ok(a) 106.94/33.02
proper(g(z0)) → g(proper(z0)) 106.94/33.02
f(ok(z0)) → ok(f(z0)) 106.94/33.02
top(mark(z0)) → top(proper(z0)) 106.94/33.02
top(ok(z0)) → top(active(z0))
Tuples:

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

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

active, g, proper, f, top

Defined Pair Symbols:

G, F, TOP, ACTIVE, PROPER

Compound Symbols:

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

106.94/33.03
106.94/33.03

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

Removed 1 trailing tuple parts
106.94/33.03
106.94/33.03

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.03
active(g(z0)) → g(active(z0)) 106.94/33.03
g(mark(z0)) → mark(g(z0)) 106.94/33.03
g(ok(z0)) → ok(g(z0)) 106.94/33.03
proper(f(z0)) → f(proper(z0)) 106.94/33.03
proper(a) → ok(a) 106.94/33.03
proper(g(z0)) → g(proper(z0)) 106.94/33.03
f(ok(z0)) → ok(f(z0)) 106.94/33.03
top(mark(z0)) → top(proper(z0)) 106.94/33.03
top(ok(z0)) → top(active(z0))
Tuples:

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

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

active, g, proper, f, top

Defined Pair Symbols:

G, F, TOP, ACTIVE, PROPER

Compound Symbols:

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

106.94/33.03
106.94/33.03

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

Removed 2 trailing nodes:

ACTIVE(g(f(f(a)))) → c5(ACTIVE(f(f(a)))) 106.94/33.03
ACTIVE(f(f(a))) → c
106.94/33.03
106.94/33.03

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.03
active(g(z0)) → g(active(z0)) 106.94/33.03
g(mark(z0)) → mark(g(z0)) 106.94/33.03
g(ok(z0)) → ok(g(z0)) 106.94/33.03
proper(f(z0)) → f(proper(z0)) 106.94/33.03
proper(a) → ok(a) 106.94/33.03
proper(g(z0)) → g(proper(z0)) 106.94/33.03
f(ok(z0)) → ok(f(z0)) 106.94/33.03
top(mark(z0)) → top(proper(z0)) 106.94/33.03
top(ok(z0)) → top(active(z0))
Tuples:

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

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

active, g, proper, f, top

Defined Pair Symbols:

G, F, TOP, ACTIVE, PROPER

Compound Symbols:

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

106.94/33.03
106.94/33.03

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

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

TOP(mark(a)) → c8(TOP(ok(a)))
We considered the (Usable) Rules:

proper(f(z0)) → f(proper(z0)) 106.94/33.03
proper(a) → ok(a) 106.94/33.03
proper(g(z0)) → g(proper(z0)) 106.94/33.03
g(mark(z0)) → mark(g(z0)) 106.94/33.03
g(ok(z0)) → ok(g(z0)) 106.94/33.03
f(ok(z0)) → ok(f(z0)) 106.94/33.03
active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.03
active(g(z0)) → g(active(z0))
And the Tuples:

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

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

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.03
active(g(z0)) → g(active(z0)) 106.94/33.03
g(mark(z0)) → mark(g(z0)) 106.94/33.03
g(ok(z0)) → ok(g(z0)) 106.94/33.03
proper(f(z0)) → f(proper(z0)) 106.94/33.03
proper(a) → ok(a) 106.94/33.03
proper(g(z0)) → g(proper(z0)) 106.94/33.03
f(ok(z0)) → ok(f(z0)) 106.94/33.03
top(mark(z0)) → top(proper(z0)) 106.94/33.03
top(ok(z0)) → top(active(z0))
Tuples:

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

G(mark(z0)) → c2(G(z0)) 106.94/33.03
G(ok(z0)) → c3(G(z0)) 106.94/33.03
F(ok(z0)) → c7(F(z0)) 106.94/33.03
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 106.94/33.03
ACTIVE(f(f(a))) → c 106.94/33.03
ACTIVE(g(g(z0))) → c1(G(g(active(z0))), ACTIVE(g(z0))) 106.94/33.03
ACTIVE(g(f(f(a)))) → c5(G(mark(f(g(f(a)))))) 106.94/33.03
ACTIVE(g(f(f(a)))) → c5(ACTIVE(f(f(a)))) 106.94/33.03
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 106.94/33.03
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 106.94/33.03
PROPER(f(a)) → c4(F(ok(a))) 106.94/33.03
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 106.94/33.03
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0))) 106.94/33.03
PROPER(g(a)) → c6(G(ok(a))) 106.94/33.03
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0))) 106.94/33.03
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
K tuples:

TOP(mark(a)) → c8(TOP(ok(a)))
Defined Rule Symbols:

active, g, proper, f, top

Defined Pair Symbols:

G, F, TOP, ACTIVE, PROPER

Compound Symbols:

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

106.94/33.03
106.94/33.03

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

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

TOP(ok(f(f(a)))) → c9(TOP(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 106.94/33.03
TOP(ok(g(z0))) → c9(TOP(g(active(z0))), ACTIVE(g(z0)))
106.94/33.03
106.94/33.03

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.03
active(g(z0)) → g(active(z0)) 106.94/33.03
g(mark(z0)) → mark(g(z0)) 106.94/33.03
g(ok(z0)) → ok(g(z0)) 106.94/33.03
proper(f(z0)) → f(proper(z0)) 106.94/33.03
proper(a) → ok(a) 106.94/33.03
proper(g(z0)) → g(proper(z0)) 106.94/33.03
f(ok(z0)) → ok(f(z0)) 106.94/33.03
top(mark(z0)) → top(proper(z0)) 106.94/33.03
top(ok(z0)) → top(active(z0))
Tuples:

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

G(mark(z0)) → c2(G(z0)) 106.94/33.03
G(ok(z0)) → c3(G(z0)) 106.94/33.03
F(ok(z0)) → c7(F(z0)) 106.94/33.03
ACTIVE(f(f(a))) → c 106.94/33.03
ACTIVE(g(g(z0))) → c1(G(g(active(z0))), ACTIVE(g(z0))) 106.94/33.03
ACTIVE(g(f(f(a)))) → c5(G(mark(f(g(f(a)))))) 106.94/33.03
ACTIVE(g(f(f(a)))) → c5(ACTIVE(f(f(a)))) 106.94/33.03
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 106.94/33.03
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 106.94/33.03
PROPER(f(a)) → c4(F(ok(a))) 106.94/33.03
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 106.94/33.03
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0))) 106.94/33.03
PROPER(g(a)) → c6(G(ok(a))) 106.94/33.03
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0))) 106.94/33.03
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0))) 106.94/33.03
TOP(ok(f(f(a)))) → c9(TOP(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 106.94/33.03
TOP(ok(g(z0))) → c9(TOP(g(active(z0))), ACTIVE(g(z0)))
K tuples:

TOP(mark(a)) → c8(TOP(ok(a)))
Defined Rule Symbols:

active, g, proper, f, top

Defined Pair Symbols:

G, F, ACTIVE, PROPER, TOP

Compound Symbols:

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

106.94/33.03
106.94/33.03

(35) CdtUnreachableProof (EQUIVALENT transformation)

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

ACTIVE(f(f(a))) → c 106.94/33.03
ACTIVE(g(g(z0))) → c1(G(g(active(z0))), ACTIVE(g(z0))) 106.94/33.03
ACTIVE(g(f(f(a)))) → c5(G(mark(f(g(f(a)))))) 106.94/33.03
ACTIVE(g(f(f(a)))) → c5(ACTIVE(f(f(a)))) 106.94/33.03
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 106.94/33.03
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 106.94/33.03
PROPER(f(a)) → c4(F(ok(a))) 106.94/33.03
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 106.94/33.03
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0))) 106.94/33.03
PROPER(g(a)) → c6(G(ok(a))) 106.94/33.03
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0))) 106.94/33.03
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0))) 106.94/33.03
TOP(ok(f(f(a)))) → c9(TOP(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 106.94/33.03
TOP(ok(g(z0))) → c9(TOP(g(active(z0))), ACTIVE(g(z0)))
106.94/33.03
106.94/33.03

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.03
active(g(z0)) → g(active(z0)) 106.94/33.03
g(mark(z0)) → mark(g(z0)) 106.94/33.03
g(ok(z0)) → ok(g(z0)) 106.94/33.03
proper(f(z0)) → f(proper(z0)) 106.94/33.03
proper(a) → ok(a) 106.94/33.03
proper(g(z0)) → g(proper(z0)) 106.94/33.03
f(ok(z0)) → ok(f(z0)) 106.94/33.03
top(mark(z0)) → top(proper(z0)) 106.94/33.03
top(ok(z0)) → top(active(z0))
Tuples:

G(mark(z0)) → c2(G(z0)) 106.94/33.03
G(ok(z0)) → c3(G(z0)) 106.94/33.03
F(ok(z0)) → c7(F(z0)) 106.94/33.03
TOP(mark(a)) → c8(TOP(ok(a)))
S tuples:

G(mark(z0)) → c2(G(z0)) 106.94/33.03
G(ok(z0)) → c3(G(z0)) 106.94/33.03
F(ok(z0)) → c7(F(z0))
K tuples:

TOP(mark(a)) → c8(TOP(ok(a)))
Defined Rule Symbols:

active, g, proper, f, top

Defined Pair Symbols:

G, F, TOP

Compound Symbols:

c2, c3, c7, c8

106.94/33.03
106.94/33.03

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

Removed 1 trailing tuple parts
106.94/33.03
106.94/33.03

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.03
active(g(z0)) → g(active(z0)) 106.94/33.03
g(mark(z0)) → mark(g(z0)) 106.94/33.03
g(ok(z0)) → ok(g(z0)) 106.94/33.03
proper(f(z0)) → f(proper(z0)) 106.94/33.03
proper(a) → ok(a) 106.94/33.03
proper(g(z0)) → g(proper(z0)) 106.94/33.03
f(ok(z0)) → ok(f(z0)) 106.94/33.03
top(mark(z0)) → top(proper(z0)) 106.94/33.03
top(ok(z0)) → top(active(z0))
Tuples:

G(mark(z0)) → c2(G(z0)) 106.94/33.03
G(ok(z0)) → c3(G(z0)) 106.94/33.03
F(ok(z0)) → c7(F(z0)) 106.94/33.03
TOP(mark(a)) → c8
S tuples:

G(mark(z0)) → c2(G(z0)) 106.94/33.03
G(ok(z0)) → c3(G(z0)) 106.94/33.03
F(ok(z0)) → c7(F(z0))
K tuples:

TOP(mark(a)) → c8
Defined Rule Symbols:

active, g, proper, f, top

Defined Pair Symbols:

G, F, TOP

Compound Symbols:

c2, c3, c7, c8

106.94/33.03
106.94/33.03

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

Removed 1 trailing nodes:

TOP(mark(a)) → c8
106.94/33.03
106.94/33.03

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.03
active(g(z0)) → g(active(z0)) 106.94/33.03
g(mark(z0)) → mark(g(z0)) 106.94/33.03
g(ok(z0)) → ok(g(z0)) 106.94/33.03
proper(f(z0)) → f(proper(z0)) 106.94/33.03
proper(a) → ok(a) 106.94/33.03
proper(g(z0)) → g(proper(z0)) 106.94/33.03
f(ok(z0)) → ok(f(z0)) 106.94/33.03
top(mark(z0)) → top(proper(z0)) 106.94/33.03
top(ok(z0)) → top(active(z0))
Tuples:

G(mark(z0)) → c2(G(z0)) 106.94/33.03
G(ok(z0)) → c3(G(z0)) 106.94/33.03
F(ok(z0)) → c7(F(z0))
S tuples:

G(mark(z0)) → c2(G(z0)) 106.94/33.03
G(ok(z0)) → c3(G(z0)) 106.94/33.03
F(ok(z0)) → c7(F(z0))
K tuples:none
Defined Rule Symbols:

active, g, proper, f, top

Defined Pair Symbols:

G, F

Compound Symbols:

c2, c3, c7

106.94/33.03
106.94/33.03

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

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

G(mark(z0)) → c2(G(z0)) 106.94/33.03
G(ok(z0)) → c3(G(z0)) 106.94/33.03
F(ok(z0)) → c7(F(z0))
We considered the (Usable) Rules:none
And the Tuples:

G(mark(z0)) → c2(G(z0)) 106.94/33.03
G(ok(z0)) → c3(G(z0)) 106.94/33.03
F(ok(z0)) → c7(F(z0))
The order we found is given by the following interpretation:
Polynomial interpretation : 106.94/33.03

POL(F(x1)) = [3]x1    106.94/33.03
POL(G(x1)) = [3]x1    106.94/33.03
POL(c2(x1)) = x1    106.94/33.03
POL(c3(x1)) = x1    106.94/33.03
POL(c7(x1)) = x1    106.94/33.03
POL(mark(x1)) = [2] + x1    106.94/33.03
POL(ok(x1)) = [3] + x1   
106.94/33.03
106.94/33.03

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(f(f(a))) → mark(f(g(f(a)))) 106.94/33.03
active(g(z0)) → g(active(z0)) 106.94/33.03
g(mark(z0)) → mark(g(z0)) 106.94/33.03
g(ok(z0)) → ok(g(z0)) 106.94/33.03
proper(f(z0)) → f(proper(z0)) 106.94/33.03
proper(a) → ok(a) 106.94/33.03
proper(g(z0)) → g(proper(z0)) 106.94/33.03
f(ok(z0)) → ok(f(z0)) 106.94/33.03
top(mark(z0)) → top(proper(z0)) 106.94/33.03
top(ok(z0)) → top(active(z0))
Tuples:

G(mark(z0)) → c2(G(z0)) 106.94/33.03
G(ok(z0)) → c3(G(z0)) 106.94/33.03
F(ok(z0)) → c7(F(z0))
S tuples:none
K tuples:

G(mark(z0)) → c2(G(z0)) 106.94/33.03
G(ok(z0)) → c3(G(z0)) 106.94/33.03
F(ok(z0)) → c7(F(z0))
Defined Rule Symbols:

active, g, proper, f, top

Defined Pair Symbols:

G, F

Compound Symbols:

c2, c3, c7

106.94/33.03
106.94/33.03

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

The set S is empty
106.94/33.03
106.94/33.03

(44) BOUNDS(O(1), O(1))

106.94/33.03
106.94/33.03
107.15/33.12 EOF