YES(O(1), O(n^1)) 99.78/33.07 YES(O(1), O(n^1)) 99.78/33.09 99.78/33.09 99.78/33.09
99.78/33.09 99.78/33.090 CpxTRS99.78/33.09
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳2 CdtProblem99.78/33.09
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳4 CdtProblem99.78/33.09
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳6 CdtProblem99.78/33.09
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))99.78/33.09
↳8 CdtProblem99.78/33.09
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))99.78/33.09
↳10 CdtProblem99.78/33.09
↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳12 CdtProblem99.78/33.09
↳13 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳14 CdtProblem99.78/33.09
↳15 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))99.78/33.09
↳16 CdtProblem99.78/33.09
↳17 CdtNarrowingProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳18 CdtProblem99.78/33.09
↳19 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳20 CdtProblem99.78/33.09
↳21 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳22 CdtProblem99.78/33.09
↳23 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))99.78/33.09
↳24 CdtProblem99.78/33.09
↳25 CdtNarrowingProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳26 CdtProblem99.78/33.09
↳27 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳28 CdtProblem99.78/33.09
↳29 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳30 CdtProblem99.78/33.09
↳31 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))99.78/33.09
↳32 CdtProblem99.78/33.09
↳33 CdtNarrowingProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳34 CdtProblem99.78/33.09
↳35 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳36 CdtProblem99.78/33.09
↳37 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳38 CdtProblem99.78/33.09
↳39 CdtNarrowingProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳40 CdtProblem99.78/33.09
↳41 CdtUnreachableProof (⇔)99.78/33.09
↳42 CdtProblem99.78/33.09
↳43 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳44 CdtProblem99.78/33.09
↳45 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳46 CdtProblem99.78/33.09
↳47 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))99.78/33.09
↳48 CdtProblem99.78/33.09
↳49 SIsEmptyProof (BOTH BOUNDS(ID, ID))99.78/33.09
↳50 BOUNDS(O(1), O(1))99.78/33.09
active(f(f(a))) → mark(f(g(f(a)))) 99.78/33.09
active(f(X)) → f(active(X)) 99.78/33.09
f(mark(X)) → mark(f(X)) 99.78/33.09
proper(f(X)) → f(proper(X)) 99.78/33.09
proper(a) → ok(a) 99.78/33.09
proper(g(X)) → g(proper(X)) 99.78/33.09
f(ok(X)) → ok(f(X)) 99.78/33.09
g(ok(X)) → ok(g(X)) 99.78/33.09
top(mark(X)) → top(proper(X)) 99.78/33.09
top(ok(X)) → top(active(X))
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 99.78/33.09
active(f(z0)) → f(active(z0)) 99.78/33.09
f(mark(z0)) → mark(f(z0)) 99.78/33.09
f(ok(z0)) → ok(f(z0)) 99.78/33.09
proper(f(z0)) → f(proper(z0)) 99.78/33.09
proper(a) → ok(a) 99.78/33.09
proper(g(z0)) → g(proper(z0)) 99.78/33.09
g(ok(z0)) → ok(g(z0)) 99.78/33.09
top(mark(z0)) → top(proper(z0)) 99.78/33.09
top(ok(z0)) → top(active(z0))
S tuples:
ACTIVE(f(f(a))) → c(F(g(f(a))), G(f(a)), F(a)) 99.78/33.09
ACTIVE(f(z0)) → c1(F(active(z0)), ACTIVE(z0)) 99.78/33.09
F(mark(z0)) → c2(F(z0)) 99.78/33.09
F(ok(z0)) → c3(F(z0)) 99.78/33.09
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 99.78/33.09
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 99.78/33.09
G(ok(z0)) → c7(G(z0)) 99.78/33.09
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 99.78/33.09
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
K tuples:none
ACTIVE(f(f(a))) → c(F(g(f(a))), G(f(a)), F(a)) 99.78/33.09
ACTIVE(f(z0)) → c1(F(active(z0)), ACTIVE(z0)) 99.78/33.09
F(mark(z0)) → c2(F(z0)) 99.78/33.09
F(ok(z0)) → c3(F(z0)) 99.78/33.09
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 99.78/33.09
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 99.78/33.09
G(ok(z0)) → c7(G(z0)) 99.78/33.09
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 99.78/33.09
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
active, f, proper, g, top
ACTIVE, F, PROPER, G, TOP
c, c1, c2, c3, c4, c6, c7, c8, c9
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.12
active(f(z0)) → f(active(z0)) 100.00/33.12
f(mark(z0)) → mark(f(z0)) 100.00/33.12
f(ok(z0)) → ok(f(z0)) 100.00/33.12
proper(f(z0)) → f(proper(z0)) 100.00/33.12
proper(a) → ok(a) 100.00/33.12
proper(g(z0)) → g(proper(z0)) 100.00/33.12
g(ok(z0)) → ok(g(z0)) 100.00/33.12
top(mark(z0)) → top(proper(z0)) 100.00/33.12
top(ok(z0)) → top(active(z0))
S tuples:
ACTIVE(f(z0)) → c1(F(active(z0)), ACTIVE(z0)) 100.00/33.12
F(mark(z0)) → c2(F(z0)) 100.00/33.12
F(ok(z0)) → c3(F(z0)) 100.00/33.12
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.12
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.12
G(ok(z0)) → c7(G(z0)) 100.00/33.12
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.12
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.12
ACTIVE(f(f(a))) → c
K tuples:none
ACTIVE(f(z0)) → c1(F(active(z0)), ACTIVE(z0)) 100.00/33.12
F(mark(z0)) → c2(F(z0)) 100.00/33.12
F(ok(z0)) → c3(F(z0)) 100.00/33.12
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.12
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.12
G(ok(z0)) → c7(G(z0)) 100.00/33.12
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.12
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.12
ACTIVE(f(f(a))) → c
active, f, proper, g, top
ACTIVE, F, PROPER, G, TOP
c1, c2, c3, c4, c6, c7, c8, c9, c
ACTIVE(f(f(a))) → c
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.12
active(f(z0)) → f(active(z0)) 100.00/33.12
f(mark(z0)) → mark(f(z0)) 100.00/33.12
f(ok(z0)) → ok(f(z0)) 100.00/33.12
proper(f(z0)) → f(proper(z0)) 100.00/33.12
proper(a) → ok(a) 100.00/33.12
proper(g(z0)) → g(proper(z0)) 100.00/33.12
g(ok(z0)) → ok(g(z0)) 100.00/33.12
top(mark(z0)) → top(proper(z0)) 100.00/33.12
top(ok(z0)) → top(active(z0))
S tuples:
ACTIVE(f(z0)) → c1(F(active(z0)), ACTIVE(z0)) 100.00/33.12
F(mark(z0)) → c2(F(z0)) 100.00/33.12
F(ok(z0)) → c3(F(z0)) 100.00/33.12
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.12
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.12
G(ok(z0)) → c7(G(z0)) 100.00/33.12
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.12
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.12
ACTIVE(f(f(a))) → c
K tuples:none
ACTIVE(f(z0)) → c1(F(active(z0)), ACTIVE(z0)) 100.00/33.12
F(mark(z0)) → c2(F(z0)) 100.00/33.12
F(ok(z0)) → c3(F(z0)) 100.00/33.12
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.12
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.12
G(ok(z0)) → c7(G(z0)) 100.00/33.12
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.12
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.12
ACTIVE(f(f(a))) → c
active, f, proper, g, top
ACTIVE, F, PROPER, G, TOP
c1, c2, c3, c4, c6, c7, c8, c9, c
We considered the (Usable) Rules:
ACTIVE(f(f(a))) → c
And the Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.12
active(f(z0)) → f(active(z0)) 100.00/33.12
f(mark(z0)) → mark(f(z0)) 100.00/33.12
f(ok(z0)) → ok(f(z0)) 100.00/33.12
proper(f(z0)) → f(proper(z0)) 100.00/33.12
proper(a) → ok(a) 100.00/33.12
proper(g(z0)) → g(proper(z0)) 100.00/33.12
g(ok(z0)) → ok(g(z0))
The order we found is given by the following interpretation:
ACTIVE(f(z0)) → c1(F(active(z0)), ACTIVE(z0)) 100.00/33.12
F(mark(z0)) → c2(F(z0)) 100.00/33.12
F(ok(z0)) → c3(F(z0)) 100.00/33.12
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.12
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.12
G(ok(z0)) → c7(G(z0)) 100.00/33.12
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.12
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.12
ACTIVE(f(f(a))) → c
POL(ACTIVE(x1)) = x1 100.00/33.12
POL(F(x1)) = 0 100.00/33.12
POL(G(x1)) = 0 100.00/33.12
POL(PROPER(x1)) = 0 100.00/33.12
POL(TOP(x1)) = x1 100.00/33.12
POL(a) = [1] 100.00/33.12
POL(active(x1)) = 0 100.00/33.12
POL(c) = 0 100.00/33.12
POL(c1(x1, x2)) = x1 + x2 100.00/33.12
POL(c2(x1)) = x1 100.00/33.12
POL(c3(x1)) = x1 100.00/33.12
POL(c4(x1, x2)) = x1 + x2 100.00/33.12
POL(c6(x1, x2)) = x1 + x2 100.00/33.12
POL(c7(x1)) = x1 100.00/33.12
POL(c8(x1, x2)) = x1 + x2 100.00/33.12
POL(c9(x1, x2)) = x1 + x2 100.00/33.12
POL(f(x1)) = [4]x1 100.00/33.12
POL(g(x1)) = 0 100.00/33.12
POL(mark(x1)) = x1 100.00/33.12
POL(ok(x1)) = x1 100.00/33.12
POL(proper(x1)) = x1
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.12
active(f(z0)) → f(active(z0)) 100.00/33.12
f(mark(z0)) → mark(f(z0)) 100.00/33.12
f(ok(z0)) → ok(f(z0)) 100.00/33.12
proper(f(z0)) → f(proper(z0)) 100.00/33.12
proper(a) → ok(a) 100.00/33.12
proper(g(z0)) → g(proper(z0)) 100.00/33.12
g(ok(z0)) → ok(g(z0)) 100.00/33.12
top(mark(z0)) → top(proper(z0)) 100.00/33.12
top(ok(z0)) → top(active(z0))
S tuples:
ACTIVE(f(z0)) → c1(F(active(z0)), ACTIVE(z0)) 100.00/33.12
F(mark(z0)) → c2(F(z0)) 100.00/33.12
F(ok(z0)) → c3(F(z0)) 100.00/33.12
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.12
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.12
G(ok(z0)) → c7(G(z0)) 100.00/33.12
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.12
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.12
ACTIVE(f(f(a))) → c
K tuples:
ACTIVE(f(z0)) → c1(F(active(z0)), ACTIVE(z0)) 100.00/33.12
F(mark(z0)) → c2(F(z0)) 100.00/33.12
F(ok(z0)) → c3(F(z0)) 100.00/33.12
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.12
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.12
G(ok(z0)) → c7(G(z0)) 100.00/33.12
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.12
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c
active, f, proper, g, top
ACTIVE, F, PROPER, G, TOP
c1, c2, c3, c4, c6, c7, c8, c9, c
We considered the (Usable) Rules:
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
And the Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.12
active(f(z0)) → f(active(z0)) 100.00/33.12
f(mark(z0)) → mark(f(z0)) 100.00/33.12
f(ok(z0)) → ok(f(z0)) 100.00/33.12
proper(f(z0)) → f(proper(z0)) 100.00/33.12
proper(a) → ok(a) 100.00/33.12
proper(g(z0)) → g(proper(z0)) 100.00/33.12
g(ok(z0)) → ok(g(z0))
The order we found is given by the following interpretation:
ACTIVE(f(z0)) → c1(F(active(z0)), ACTIVE(z0)) 100.00/33.12
F(mark(z0)) → c2(F(z0)) 100.00/33.12
F(ok(z0)) → c3(F(z0)) 100.00/33.12
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.12
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.12
G(ok(z0)) → c7(G(z0)) 100.00/33.12
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.12
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.12
ACTIVE(f(f(a))) → c
POL(ACTIVE(x1)) = 0 100.00/33.12
POL(F(x1)) = 0 100.00/33.12
POL(G(x1)) = 0 100.00/33.12
POL(PROPER(x1)) = 0 100.00/33.12
POL(TOP(x1)) = [2]x1 100.00/33.12
POL(a) = [1] 100.00/33.12
POL(active(x1)) = x1 100.00/33.12
POL(c) = 0 100.00/33.12
POL(c1(x1, x2)) = x1 + x2 100.00/33.12
POL(c2(x1)) = x1 100.00/33.12
POL(c3(x1)) = x1 100.00/33.12
POL(c4(x1, x2)) = x1 + x2 100.00/33.12
POL(c6(x1, x2)) = x1 + x2 100.00/33.12
POL(c7(x1)) = x1 100.00/33.12
POL(c8(x1, x2)) = x1 + x2 100.00/33.12
POL(c9(x1, x2)) = x1 + x2 100.00/33.12
POL(f(x1)) = x1 100.00/33.12
POL(g(x1)) = 0 100.00/33.12
POL(mark(x1)) = [1] + x1 100.00/33.12
POL(ok(x1)) = x1 100.00/33.12
POL(proper(x1)) = x1
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.12
active(f(z0)) → f(active(z0)) 100.00/33.12
f(mark(z0)) → mark(f(z0)) 100.00/33.12
f(ok(z0)) → ok(f(z0)) 100.00/33.12
proper(f(z0)) → f(proper(z0)) 100.00/33.13
proper(a) → ok(a) 100.00/33.13
proper(g(z0)) → g(proper(z0)) 100.00/33.13
g(ok(z0)) → ok(g(z0)) 100.00/33.13
top(mark(z0)) → top(proper(z0)) 100.00/33.13
top(ok(z0)) → top(active(z0))
S tuples:
ACTIVE(f(z0)) → c1(F(active(z0)), ACTIVE(z0)) 100.00/33.13
F(mark(z0)) → c2(F(z0)) 100.00/33.13
F(ok(z0)) → c3(F(z0)) 100.00/33.13
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.13
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.13
G(ok(z0)) → c7(G(z0)) 100.00/33.13
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.13
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.13
ACTIVE(f(f(a))) → c
K tuples:
ACTIVE(f(z0)) → c1(F(active(z0)), ACTIVE(z0)) 100.00/33.13
F(mark(z0)) → c2(F(z0)) 100.00/33.13
F(ok(z0)) → c3(F(z0)) 100.00/33.13
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.13
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.13
G(ok(z0)) → c7(G(z0)) 100.00/33.13
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c 100.00/33.13
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
active, f, proper, g, top
ACTIVE, F, PROPER, G, TOP
c1, c2, c3, c4, c6, c7, c8, c9, c
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.13
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0)))
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.13
active(f(z0)) → f(active(z0)) 100.00/33.13
f(mark(z0)) → mark(f(z0)) 100.00/33.13
f(ok(z0)) → ok(f(z0)) 100.00/33.13
proper(f(z0)) → f(proper(z0)) 100.00/33.13
proper(a) → ok(a) 100.00/33.13
proper(g(z0)) → g(proper(z0)) 100.00/33.13
g(ok(z0)) → ok(g(z0)) 100.00/33.13
top(mark(z0)) → top(proper(z0)) 100.00/33.13
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.13
F(ok(z0)) → c3(F(z0)) 100.00/33.13
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.13
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.13
G(ok(z0)) → c7(G(z0)) 100.00/33.13
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.13
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.13
ACTIVE(f(f(a))) → c 100.00/33.13
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.13
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0)))
K tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.13
F(ok(z0)) → c3(F(z0)) 100.00/33.13
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.14
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0)))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
active, f, proper, g, top
F, PROPER, G, TOP, ACTIVE
c2, c3, c4, c6, c7, c8, c9, c, c1
ACTIVE(f(f(a))) → c
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0)) 100.00/33.14
top(mark(z0)) → top(proper(z0)) 100.00/33.14
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.14
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0)))
K tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.14
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0)))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
active, f, proper, g, top
F, PROPER, G, TOP, ACTIVE
c2, c3, c4, c6, c7, c8, c9, c, c1
We considered the (Usable) Rules:
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a))))
And the Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0))
The order we found is given by the following interpretation:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.14
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0)))
POL(ACTIVE(x1)) = [2]x1 100.00/33.14
POL(F(x1)) = 0 100.00/33.14
POL(G(x1)) = 0 100.00/33.14
POL(PROPER(x1)) = 0 100.00/33.14
POL(TOP(x1)) = [2]x1 100.00/33.14
POL(a) = [4] 100.00/33.14
POL(active(x1)) = 0 100.00/33.14
POL(c) = 0 100.00/33.14
POL(c1(x1, x2)) = x1 + x2 100.00/33.14
POL(c2(x1)) = x1 100.00/33.14
POL(c3(x1)) = x1 100.00/33.14
POL(c4(x1, x2)) = x1 + x2 100.00/33.14
POL(c6(x1, x2)) = x1 + x2 100.00/33.14
POL(c7(x1)) = x1 100.00/33.14
POL(c8(x1, x2)) = x1 + x2 100.00/33.14
POL(c9(x1, x2)) = x1 + x2 100.00/33.14
POL(f(x1)) = [4]x1 100.00/33.14
POL(g(x1)) = 0 100.00/33.14
POL(mark(x1)) = x1 100.00/33.14
POL(ok(x1)) = x1 100.00/33.14
POL(proper(x1)) = x1
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0)) 100.00/33.14
top(mark(z0)) → top(proper(z0)) 100.00/33.14
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.14
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0)))
K tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) 100.00/33.14
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0)))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a))))
active, f, proper, g, top
F, PROPER, G, TOP, ACTIVE
c2, c3, c4, c6, c7, c8, c9, c, c1
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a)), PROPER(a)) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0)) 100.00/33.14
top(mark(z0)) → top(proper(z0)) 100.00/33.14
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a)), PROPER(a)) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
K tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a)), PROPER(a)) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a))))
active, f, proper, g, top
F, PROPER, G, TOP, ACTIVE
c2, c3, c6, c7, c8, c9, c, c1, c4
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0)) 100.00/33.14
top(mark(z0)) → top(proper(z0)) 100.00/33.14
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a)))
K tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a)))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a))))
active, f, proper, g, top
F, PROPER, G, TOP, ACTIVE
c2, c3, c6, c7, c8, c9, c, c1, c4, c4
ACTIVE(f(f(a))) → c
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0)) 100.00/33.14
top(mark(z0)) → top(proper(z0)) 100.00/33.14
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a)))
K tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a)))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a))))
active, f, proper, g, top
F, PROPER, G, TOP, ACTIVE
c2, c3, c6, c7, c8, c9, c, c1, c4, c4
We considered the (Usable) Rules:
PROPER(f(a)) → c4(F(ok(a)))
And the Tuples:
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0))
The order we found is given by the following interpretation:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a)))
POL(ACTIVE(x1)) = 0 100.00/33.14
POL(F(x1)) = 0 100.00/33.14
POL(G(x1)) = 0 100.00/33.14
POL(PROPER(x1)) = [1] 100.00/33.14
POL(TOP(x1)) = x1 100.00/33.14
POL(a) = 0 100.00/33.14
POL(active(x1)) = x1 100.00/33.14
POL(c) = 0 100.00/33.14
POL(c1(x1, x2)) = x1 + x2 100.00/33.14
POL(c2(x1)) = x1 100.00/33.14
POL(c3(x1)) = x1 100.00/33.14
POL(c4(x1)) = x1 100.00/33.14
POL(c4(x1, x2)) = x1 + x2 100.00/33.14
POL(c6(x1, x2)) = x1 + x2 100.00/33.14
POL(c7(x1)) = x1 100.00/33.14
POL(c8(x1, x2)) = x1 + x2 100.00/33.14
POL(c9(x1, x2)) = x1 + x2 100.00/33.14
POL(f(x1)) = [4] + x1 100.00/33.14
POL(g(x1)) = 0 100.00/33.14
POL(mark(x1)) = [4] + x1 100.00/33.14
POL(ok(x1)) = x1 100.00/33.14
POL(proper(x1)) = x1
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0)) 100.00/33.14
top(mark(z0)) → top(proper(z0)) 100.00/33.14
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a)))
K tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
PROPER(g(z0)) → c6(G(proper(z0)), PROPER(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a)))
active, f, proper, g, top
F, PROPER, G, TOP, ACTIVE
c2, c3, c6, c7, c8, c9, c, c1, c4, c4
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a)), PROPER(a)) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0)))
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0)) 100.00/33.14
top(mark(z0)) → top(proper(z0)) 100.00/33.14
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a)), PROPER(a)) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0)))
K tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a)), PROPER(a)) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0)))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a)))
active, f, proper, g, top
F, G, TOP, ACTIVE, PROPER
c2, c3, c7, c8, c9, c, c1, c4, c4, c6
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0)) 100.00/33.14
top(mark(z0)) → top(proper(z0)) 100.00/33.14
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a)))
K tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a)))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a)))
active, f, proper, g, top
F, G, TOP, ACTIVE, PROPER
c2, c3, c7, c8, c9, c, c1, c4, c4, c6, c6
ACTIVE(f(f(a))) → c
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0)) 100.00/33.14
top(mark(z0)) → top(proper(z0)) 100.00/33.14
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a)))
K tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a)))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a)))
active, f, proper, g, top
F, G, TOP, ACTIVE, PROPER
c2, c3, c7, c8, c9, c, c1, c4, c4, c6, c6
We considered the (Usable) Rules:
PROPER(g(a)) → c6(G(ok(a)))
And the Tuples:
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0))
The order we found is given by the following interpretation:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a)))
POL(ACTIVE(x1)) = 0 100.00/33.14
POL(F(x1)) = 0 100.00/33.14
POL(G(x1)) = 0 100.00/33.14
POL(PROPER(x1)) = [1] 100.00/33.14
POL(TOP(x1)) = [2]x1 100.00/33.14
POL(a) = [1] 100.00/33.14
POL(active(x1)) = x1 100.00/33.14
POL(c) = 0 100.00/33.14
POL(c1(x1, x2)) = x1 + x2 100.00/33.14
POL(c2(x1)) = x1 100.00/33.14
POL(c3(x1)) = x1 100.00/33.14
POL(c4(x1)) = x1 100.00/33.14
POL(c4(x1, x2)) = x1 + x2 100.00/33.14
POL(c6(x1)) = x1 100.00/33.14
POL(c6(x1, x2)) = x1 + x2 100.00/33.14
POL(c7(x1)) = x1 100.00/33.14
POL(c8(x1, x2)) = x1 + x2 100.00/33.14
POL(c9(x1, x2)) = x1 + x2 100.00/33.14
POL(f(x1)) = [4]x1 100.00/33.14
POL(g(x1)) = 0 100.00/33.14
POL(mark(x1)) = [2] + x1 100.00/33.14
POL(ok(x1)) = x1 100.00/33.14
POL(proper(x1)) = x1
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0)) 100.00/33.14
top(mark(z0)) → top(proper(z0)) 100.00/33.14
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a)))
K tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0)))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a)))
active, f, proper, g, top
F, G, TOP, ACTIVE, PROPER
c2, c3, c7, c8, c9, c, c1, c4, c4, c6, c6
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a)) 100.00/33.14
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0)) 100.00/33.14
top(mark(z0)) → top(proper(z0)) 100.00/33.14
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a))) 100.00/33.14
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a)) 100.00/33.14
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
K tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0)))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a)))
active, f, proper, g, top
F, G, TOP, ACTIVE, PROPER
c2, c3, c7, c9, c, c1, c4, c4, c6, c6, c8
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0)) 100.00/33.14
top(mark(z0)) → top(proper(z0)) 100.00/33.14
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a))) 100.00/33.14
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
TOP(mark(a)) → c8(TOP(ok(a)))
K tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0)))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c 100.00/33.14
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a)))
active, f, proper, g, top
F, G, TOP, ACTIVE, PROPER
c2, c3, c7, c9, c, c1, c4, c4, c6, c6, c8, c8
ACTIVE(f(f(a))) → c
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0)) 100.00/33.14
top(mark(z0)) → top(proper(z0)) 100.00/33.14
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a))) 100.00/33.14
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
TOP(mark(a)) → c8(TOP(ok(a)))
K tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0)))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a)))
active, f, proper, g, top
F, G, TOP, ACTIVE, PROPER
c2, c3, c7, c9, c, c1, c4, c4, c6, c6, c8, c8
TOP(ok(f(f(a)))) → c9(TOP(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
TOP(ok(f(z0))) → c9(TOP(f(active(z0))), ACTIVE(f(z0)))
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.14
active(f(z0)) → f(active(z0)) 100.00/33.14
f(mark(z0)) → mark(f(z0)) 100.00/33.14
f(ok(z0)) → ok(f(z0)) 100.00/33.14
proper(f(z0)) → f(proper(z0)) 100.00/33.14
proper(a) → ok(a) 100.00/33.14
proper(g(z0)) → g(proper(z0)) 100.00/33.14
g(ok(z0)) → ok(g(z0)) 100.00/33.14
top(mark(z0)) → top(proper(z0)) 100.00/33.14
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a))) 100.00/33.14
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
TOP(mark(a)) → c8(TOP(ok(a))) 100.00/33.14
TOP(ok(f(f(a)))) → c9(TOP(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
TOP(ok(f(z0))) → c9(TOP(f(active(z0))), ACTIVE(f(z0)))
K tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.14
F(ok(z0)) → c3(F(z0)) 100.00/33.14
G(ok(z0)) → c7(G(z0)) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
TOP(ok(f(f(a)))) → c9(TOP(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
TOP(ok(f(z0))) → c9(TOP(f(active(z0))), ACTIVE(f(z0)))
Defined Rule Symbols:
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a))) 100.00/33.14
PROPER(g(a)) → c6(G(ok(a)))
active, f, proper, g, top
F, G, ACTIVE, PROPER, TOP
c2, c3, c7, c, c1, c4, c4, c6, c6, c8, c8, c9
ACTIVE(f(f(a))) → c 100.00/33.14
ACTIVE(f(f(f(a)))) → c1(F(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.14
ACTIVE(f(f(z0))) → c1(F(f(active(z0))), ACTIVE(f(z0))) 100.00/33.14
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) 100.00/33.14
PROPER(f(a)) → c4(F(ok(a))) 100.00/33.14
PROPER(g(f(z0))) → c6(G(f(proper(z0))), PROPER(f(z0))) 100.00/33.14
PROPER(g(g(z0))) → c6(G(g(proper(z0))), PROPER(g(z0))) 100.00/33.15
PROPER(g(a)) → c6(G(ok(a))) 100.00/33.15
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0))) 100.00/33.15
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0))) 100.00/33.15
TOP(ok(f(f(a)))) → c9(TOP(mark(f(g(f(a))))), ACTIVE(f(f(a)))) 100.00/33.15
TOP(ok(f(z0))) → c9(TOP(f(active(z0))), ACTIVE(f(z0)))
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.15
active(f(z0)) → f(active(z0)) 100.00/33.15
f(mark(z0)) → mark(f(z0)) 100.00/33.15
f(ok(z0)) → ok(f(z0)) 100.00/33.15
proper(f(z0)) → f(proper(z0)) 100.00/33.15
proper(a) → ok(a) 100.00/33.15
proper(g(z0)) → g(proper(z0)) 100.00/33.15
g(ok(z0)) → ok(g(z0)) 100.00/33.15
top(mark(z0)) → top(proper(z0)) 100.00/33.15
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.15
F(ok(z0)) → c3(F(z0)) 100.00/33.15
G(ok(z0)) → c7(G(z0)) 100.00/33.15
TOP(mark(a)) → c8(TOP(ok(a)))
K tuples:none
F(mark(z0)) → c2(F(z0)) 100.00/33.15
F(ok(z0)) → c3(F(z0)) 100.00/33.15
G(ok(z0)) → c7(G(z0))
active, f, proper, g, top
F, G, TOP
c2, c3, c7, c8
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.15
active(f(z0)) → f(active(z0)) 100.00/33.15
f(mark(z0)) → mark(f(z0)) 100.00/33.15
f(ok(z0)) → ok(f(z0)) 100.00/33.15
proper(f(z0)) → f(proper(z0)) 100.00/33.15
proper(a) → ok(a) 100.00/33.15
proper(g(z0)) → g(proper(z0)) 100.00/33.15
g(ok(z0)) → ok(g(z0)) 100.00/33.15
top(mark(z0)) → top(proper(z0)) 100.00/33.15
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.15
F(ok(z0)) → c3(F(z0)) 100.00/33.15
G(ok(z0)) → c7(G(z0)) 100.00/33.15
TOP(mark(a)) → c8
K tuples:none
F(mark(z0)) → c2(F(z0)) 100.00/33.15
F(ok(z0)) → c3(F(z0)) 100.00/33.15
G(ok(z0)) → c7(G(z0))
active, f, proper, g, top
F, G, TOP
c2, c3, c7, c8
TOP(mark(a)) → c8
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.15
active(f(z0)) → f(active(z0)) 100.00/33.15
f(mark(z0)) → mark(f(z0)) 100.00/33.15
f(ok(z0)) → ok(f(z0)) 100.00/33.15
proper(f(z0)) → f(proper(z0)) 100.00/33.15
proper(a) → ok(a) 100.00/33.15
proper(g(z0)) → g(proper(z0)) 100.00/33.15
g(ok(z0)) → ok(g(z0)) 100.00/33.15
top(mark(z0)) → top(proper(z0)) 100.00/33.15
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0)) → c2(F(z0)) 100.00/33.15
F(ok(z0)) → c3(F(z0)) 100.00/33.15
G(ok(z0)) → c7(G(z0))
K tuples:none
F(mark(z0)) → c2(F(z0)) 100.00/33.15
F(ok(z0)) → c3(F(z0)) 100.00/33.15
G(ok(z0)) → c7(G(z0))
active, f, proper, g, top
F, G
c2, c3, c7
We considered the (Usable) Rules:none
F(mark(z0)) → c2(F(z0)) 100.00/33.15
F(ok(z0)) → c3(F(z0)) 100.00/33.15
G(ok(z0)) → c7(G(z0))
The order we found is given by the following interpretation:
F(mark(z0)) → c2(F(z0)) 100.00/33.15
F(ok(z0)) → c3(F(z0)) 100.00/33.15
G(ok(z0)) → c7(G(z0))
POL(F(x1)) = [3]x1 100.00/33.15
POL(G(x1)) = [3]x1 100.00/33.15
POL(c2(x1)) = x1 100.00/33.15
POL(c3(x1)) = x1 100.00/33.15
POL(c7(x1)) = x1 100.00/33.15
POL(mark(x1)) = [2] + x1 100.00/33.15
POL(ok(x1)) = [3] + x1
Tuples:
active(f(f(a))) → mark(f(g(f(a)))) 100.00/33.15
active(f(z0)) → f(active(z0)) 100.00/33.15
f(mark(z0)) → mark(f(z0)) 100.00/33.15
f(ok(z0)) → ok(f(z0)) 100.00/33.15
proper(f(z0)) → f(proper(z0)) 100.00/33.15
proper(a) → ok(a) 100.00/33.15
proper(g(z0)) → g(proper(z0)) 100.00/33.15
g(ok(z0)) → ok(g(z0)) 100.00/33.15
top(mark(z0)) → top(proper(z0)) 100.00/33.15
top(ok(z0)) → top(active(z0))
S tuples:none
F(mark(z0)) → c2(F(z0)) 100.00/33.15
F(ok(z0)) → c3(F(z0)) 100.00/33.15
G(ok(z0)) → c7(G(z0))
Defined Rule Symbols:
F(mark(z0)) → c2(F(z0)) 100.00/33.15
F(ok(z0)) → c3(F(z0)) 100.00/33.15
G(ok(z0)) → c7(G(z0))
active, f, proper, g, top
F, G
c2, c3, c7