YES(O(1), O(n^1)) 61.04/21.85 YES(O(1), O(n^1)) 61.04/21.88 61.04/21.88 61.04/21.88
61.04/21.88 61.04/21.880 CpxTRS61.04/21.88
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))61.04/21.88
↳2 CdtProblem61.04/21.88
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))61.04/21.88
↳4 CdtProblem61.04/21.88
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))61.04/21.88
↳6 CdtProblem61.04/21.88
↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID))61.04/21.88
↳8 CdtProblem61.04/21.88
↳9 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))61.04/21.88
↳10 CdtProblem61.04/21.88
↳11 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))61.04/21.88
↳12 CdtProblem61.04/21.88
↳13 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))61.04/21.88
↳14 CdtProblem61.04/21.88
↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID))61.04/21.88
↳16 CdtProblem61.04/21.88
↳17 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))61.04/21.88
↳18 CdtProblem61.04/21.88
↳19 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))61.04/21.88
↳20 CdtProblem61.04/21.88
↳21 CdtNarrowingProof (BOTH BOUNDS(ID, ID))61.04/21.88
↳22 CdtProblem61.04/21.88
↳23 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))61.04/21.88
↳24 CdtProblem61.04/21.88
↳25 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))61.04/21.88
↳26 CdtProblem61.04/21.88
↳27 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))61.04/21.88
↳28 CdtProblem61.04/21.88
↳29 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))61.04/21.88
↳30 CdtProblem61.04/21.88
↳31 CdtNarrowingProof (BOTH BOUNDS(ID, ID))61.04/21.88
↳32 CdtProblem61.04/21.88
↳33 CdtUnreachableProof (⇔)61.04/21.88
↳34 CdtProblem61.04/21.88
↳35 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))61.04/21.88
↳36 CdtProblem61.04/21.88
↳37 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))61.04/21.88
↳38 CdtProblem61.04/21.88
↳39 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))61.04/21.88
↳40 CdtProblem61.04/21.88
↳41 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))61.04/21.88
↳42 CdtProblem61.04/21.88
↳43 SIsEmptyProof (BOTH BOUNDS(ID, ID))61.04/21.88
↳44 BOUNDS(O(1), O(1))61.04/21.88
active(f(X, X)) → mark(f(a, b)) 61.04/21.88
active(b) → mark(a) 61.04/21.88
active(f(X1, X2)) → f(active(X1), X2) 61.04/21.88
f(mark(X1), X2) → mark(f(X1, X2)) 61.04/21.88
proper(f(X1, X2)) → f(proper(X1), proper(X2)) 61.04/21.88
proper(a) → ok(a) 61.04/21.88
proper(b) → ok(b) 61.04/21.88
f(ok(X1), ok(X2)) → ok(f(X1, X2)) 61.04/21.88
top(mark(X)) → top(proper(X)) 61.04/21.88
top(ok(X)) → top(active(X))
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.91
active(b) → mark(a) 61.35/21.91
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.91
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.91
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.91
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.91
proper(a) → ok(a) 61.35/21.91
proper(b) → ok(b) 61.35/21.91
top(mark(z0)) → top(proper(z0)) 61.35/21.91
top(ok(z0)) → top(active(z0))
S tuples:
ACTIVE(f(z0, z0)) → c(F(a, b)) 61.35/21.91
ACTIVE(f(z0, z1)) → c2(F(active(z0), z1), ACTIVE(z0)) 61.35/21.91
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.91
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.91
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1)) 61.35/21.91
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.91
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
K tuples:none
ACTIVE(f(z0, z0)) → c(F(a, b)) 61.35/21.91
ACTIVE(f(z0, z1)) → c2(F(active(z0), z1), ACTIVE(z0)) 61.35/21.91
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.91
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.91
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1)) 61.35/21.91
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.91
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
active, f, proper, top
ACTIVE, F, PROPER, TOP
c, c2, c3, c4, c5, c8, c9
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.91
active(b) → mark(a) 61.35/21.91
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.91
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.91
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.91
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.91
proper(a) → ok(a) 61.35/21.91
proper(b) → ok(b) 61.35/21.91
top(mark(z0)) → top(proper(z0)) 61.35/21.91
top(ok(z0)) → top(active(z0))
S tuples:
ACTIVE(f(z0, z1)) → c2(F(active(z0), z1), ACTIVE(z0)) 61.35/21.91
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.91
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.91
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1)) 61.35/21.91
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.91
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.91
ACTIVE(f(z0, z0)) → c
K tuples:none
ACTIVE(f(z0, z1)) → c2(F(active(z0), z1), ACTIVE(z0)) 61.35/21.91
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.91
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.91
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1)) 61.35/21.91
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.91
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.91
ACTIVE(f(z0, z0)) → c
active, f, proper, top
ACTIVE, F, PROPER, TOP
c2, c3, c4, c5, c8, c9, c
ACTIVE(f(z0, z0)) → c
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.93
active(b) → mark(a) 61.35/21.93
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.93
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.93
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.93
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.93
proper(a) → ok(a) 61.35/21.93
proper(b) → ok(b) 61.35/21.93
top(mark(z0)) → top(proper(z0)) 61.35/21.93
top(ok(z0)) → top(active(z0))
S tuples:
ACTIVE(f(z0, z1)) → c2(F(active(z0), z1), ACTIVE(z0)) 61.35/21.93
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.93
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.93
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1)) 61.35/21.93
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.93
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.93
ACTIVE(f(z0, z0)) → c
K tuples:none
ACTIVE(f(z0, z1)) → c2(F(active(z0), z1), ACTIVE(z0)) 61.35/21.93
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.93
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.93
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1)) 61.35/21.93
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.93
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.93
ACTIVE(f(z0, z0)) → c
active, f, proper, top
ACTIVE, F, PROPER, TOP
c2, c3, c4, c5, c8, c9, c
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.93
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b)) 61.35/21.93
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.93
active(b) → mark(a) 61.35/21.93
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.93
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.93
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.93
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.93
proper(a) → ok(a) 61.35/21.93
proper(b) → ok(b) 61.35/21.93
top(mark(z0)) → top(proper(z0)) 61.35/21.93
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.93
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.93
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1)) 61.35/21.93
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.93
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.93
ACTIVE(f(z0, z0)) → c 61.35/21.93
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.93
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b)) 61.35/21.93
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
K tuples:none
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.93
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.93
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1)) 61.35/21.93
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.93
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.93
ACTIVE(f(z0, z0)) → c 61.35/21.93
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.93
ACTIVE(f(b, x1)) → c2(F(mark(a), x1), ACTIVE(b)) 61.35/21.93
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
active, f, proper, top
F, PROPER, TOP, ACTIVE
c3, c4, c5, c8, c9, c, c2
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.93
active(b) → mark(a) 61.35/21.93
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.93
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.93
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.93
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.93
proper(a) → ok(a) 61.35/21.93
proper(b) → ok(b) 61.35/21.93
top(mark(z0)) → top(proper(z0)) 61.35/21.93
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.93
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.93
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1)) 61.35/21.93
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.93
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.93
ACTIVE(f(z0, z0)) → c 61.35/21.93
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.93
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.93
ACTIVE(f(b, x1)) → c2(F(mark(a), x1))
K tuples:none
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.93
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.93
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1)) 61.35/21.93
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.93
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.93
ACTIVE(f(z0, z0)) → c 61.35/21.93
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.93
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.93
ACTIVE(f(b, x1)) → c2(F(mark(a), x1))
active, f, proper, top
F, PROPER, TOP, ACTIVE
c3, c4, c5, c8, c9, c, c2, c2
ACTIVE(f(z0, z0)) → c
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.93
active(b) → mark(a) 61.35/21.93
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.93
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.93
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.93
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.93
proper(a) → ok(a) 61.35/21.93
proper(b) → ok(b) 61.35/21.93
top(mark(z0)) → top(proper(z0)) 61.35/21.93
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.93
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.93
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1)) 61.35/21.93
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.93
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.93
ACTIVE(f(z0, z0)) → c 61.35/21.93
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.93
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.93
ACTIVE(f(b, x1)) → c2(F(mark(a), x1))
K tuples:none
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.93
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.93
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1)) 61.35/21.93
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.93
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.93
ACTIVE(f(z0, z0)) → c 61.35/21.93
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.93
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.93
ACTIVE(f(b, x1)) → c2(F(mark(a), x1))
active, f, proper, top
F, PROPER, TOP, ACTIVE
c3, c4, c5, c8, c9, c, c2, c2
We considered the (Usable) Rules:
ACTIVE(f(b, x1)) → c2(F(mark(a), x1))
And the Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.93
active(b) → mark(a) 61.35/21.93
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.93
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.93
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.93
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.93
proper(a) → ok(a) 61.35/21.93
proper(b) → ok(b)
The order we found is given by the following interpretation:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.93
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.93
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1)) 61.35/21.93
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.93
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.93
ACTIVE(f(z0, z0)) → c 61.35/21.93
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.93
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.93
ACTIVE(f(b, x1)) → c2(F(mark(a), x1))
POL(ACTIVE(x1)) = x1 61.35/21.93
POL(F(x1, x2)) = 0 61.35/21.93
POL(PROPER(x1)) = 0 61.35/21.93
POL(TOP(x1)) = x1 61.35/21.93
POL(a) = 0 61.35/21.93
POL(active(x1)) = 0 61.35/21.93
POL(b) = [4] 61.35/21.93
POL(c) = 0 61.35/21.93
POL(c2(x1)) = x1 61.35/21.93
POL(c2(x1, x2)) = x1 + x2 61.35/21.93
POL(c3(x1)) = x1 61.35/21.93
POL(c4(x1)) = x1 61.35/21.93
POL(c5(x1, x2, x3)) = x1 + x2 + x3 61.35/21.93
POL(c8(x1, x2)) = x1 + x2 61.35/21.93
POL(c9(x1, x2)) = x1 + x2 61.35/21.93
POL(f(x1, x2)) = [4]x1 61.35/21.93
POL(mark(x1)) = x1 61.35/21.93
POL(ok(x1)) = x1 61.35/21.93
POL(proper(x1)) = x1
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.93
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
top(mark(z0)) → top(proper(z0)) 61.35/21.95
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1)) 61.35/21.95
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
ACTIVE(f(b, x1)) → c2(F(mark(a), x1))
K tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
PROPER(f(z0, z1)) → c5(F(proper(z0), proper(z1)), PROPER(z0), PROPER(z1)) 61.35/21.95
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1)))
Defined Rule Symbols:
ACTIVE(f(b, x1)) → c2(F(mark(a), x1))
active, f, proper, top
F, PROPER, TOP, ACTIVE
c3, c4, c5, c8, c9, c, c2, c2
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b)) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.95
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
top(mark(z0)) → top(proper(z0)) 61.35/21.95
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
ACTIVE(f(b, x1)) → c2(F(mark(a), x1)) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b)) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
K tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0), PROPER(a)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0), PROPER(b)) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(a), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(b), PROPER(x1))
Defined Rule Symbols:
ACTIVE(f(b, x1)) → c2(F(mark(a), x1))
active, f, proper, top
F, TOP, ACTIVE, PROPER
c3, c4, c8, c9, c, c2, c2, c5
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.95
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
top(mark(z0)) → top(proper(z0)) 61.35/21.95
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
ACTIVE(f(b, x1)) → c2(F(mark(a), x1)) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1))
K tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1))
Defined Rule Symbols:
ACTIVE(f(b, x1)) → c2(F(mark(a), x1))
active, f, proper, top
F, TOP, ACTIVE, PROPER
c3, c4, c8, c9, c, c2, c2, c5, c5
ACTIVE(f(z0, z0)) → c
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.95
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
top(mark(z0)) → top(proper(z0)) 61.35/21.95
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
ACTIVE(f(b, x1)) → c2(F(mark(a), x1)) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1))
K tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1))
Defined Rule Symbols:
ACTIVE(f(b, x1)) → c2(F(mark(a), x1))
active, f, proper, top
F, TOP, ACTIVE, PROPER
c3, c4, c8, c9, c, c2, c2, c5, c5
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1))) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a)) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.95
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
top(mark(z0)) → top(proper(z0)) 61.35/21.95
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
ACTIVE(f(b, x1)) → c2(F(mark(a), x1)) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1)) 61.35/21.95
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1))) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a)) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))
K tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1)) 61.35/21.95
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1))) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a)), PROPER(a)) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b)), PROPER(b))
Defined Rule Symbols:
ACTIVE(f(b, x1)) → c2(F(mark(a), x1))
active, f, proper, top
F, TOP, ACTIVE, PROPER
c3, c4, c9, c, c2, c2, c5, c5, c8
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.95
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
top(mark(z0)) → top(proper(z0)) 61.35/21.95
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
ACTIVE(f(b, x1)) → c2(F(mark(a), x1)) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1)) 61.35/21.95
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1))) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a))) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b)))
K tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1)) 61.35/21.95
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1))) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a))) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b)))
Defined Rule Symbols:
ACTIVE(f(b, x1)) → c2(F(mark(a), x1))
active, f, proper, top
F, TOP, ACTIVE, PROPER
c3, c4, c9, c, c2, c2, c5, c5, c8, c8
ACTIVE(f(z0, z0)) → c
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.95
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
top(mark(z0)) → top(proper(z0)) 61.35/21.95
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
ACTIVE(f(b, x1)) → c2(F(mark(a), x1)) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1)) 61.35/21.95
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1))) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a))) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b)))
K tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1)) 61.35/21.95
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1))) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a))) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b)))
Defined Rule Symbols:
ACTIVE(f(b, x1)) → c2(F(mark(a), x1))
active, f, proper, top
F, TOP, ACTIVE, PROPER
c3, c4, c9, c, c2, c2, c5, c5, c8, c8
We considered the (Usable) Rules:
TOP(mark(b)) → c8(TOP(ok(b)))
And the Tuples:
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.95
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1)
The order we found is given by the following interpretation:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
ACTIVE(f(b, x1)) → c2(F(mark(a), x1)) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1)) 61.35/21.95
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1))) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a))) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b)))
POL(ACTIVE(x1)) = 0 61.35/21.95
POL(F(x1, x2)) = 0 61.35/21.95
POL(PROPER(x1)) = 0 61.35/21.95
POL(TOP(x1)) = x1 61.35/21.95
POL(a) = 0 61.35/21.95
POL(active(x1)) = 0 61.35/21.95
POL(b) = [2] 61.35/21.95
POL(c) = 0 61.35/21.95
POL(c2(x1)) = x1 61.35/21.95
POL(c2(x1, x2)) = x1 + x2 61.35/21.95
POL(c3(x1)) = x1 61.35/21.95
POL(c4(x1)) = x1 61.35/21.95
POL(c5(x1, x2)) = x1 + x2 61.35/21.95
POL(c5(x1, x2, x3)) = x1 + x2 + x3 61.35/21.95
POL(c8(x1)) = x1 61.35/21.95
POL(c8(x1, x2)) = x1 + x2 61.35/21.95
POL(c9(x1, x2)) = x1 + x2 61.35/21.95
POL(f(x1, x2)) = 0 61.35/21.95
POL(mark(x1)) = x1 61.35/21.95
POL(ok(x1)) = 0 61.35/21.95
POL(proper(x1)) = 0
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.95
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
top(mark(z0)) → top(proper(z0)) 61.35/21.95
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
ACTIVE(f(b, x1)) → c2(F(mark(a), x1)) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1)) 61.35/21.95
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1))) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a))) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b)))
K tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1)) 61.35/21.95
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1))) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a)))
Defined Rule Symbols:
ACTIVE(f(b, x1)) → c2(F(mark(a), x1)) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b)))
active, f, proper, top
F, TOP, ACTIVE, PROPER
c3, c4, c9, c, c2, c2, c5, c5, c8, c8
We considered the (Usable) Rules:
TOP(mark(a)) → c8(TOP(ok(a)))
And the Tuples:
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.95
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1)
The order we found is given by the following interpretation:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
ACTIVE(f(b, x1)) → c2(F(mark(a), x1)) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1)) 61.35/21.95
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1))) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a))) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b)))
POL(ACTIVE(x1)) = 0 61.35/21.95
POL(F(x1, x2)) = 0 61.35/21.95
POL(PROPER(x1)) = 0 61.35/21.95
POL(TOP(x1)) = [2]x1 61.35/21.95
POL(a) = 0 61.35/21.95
POL(active(x1)) = x1 61.35/21.95
POL(b) = [4] 61.35/21.95
POL(c) = 0 61.35/21.95
POL(c2(x1)) = x1 61.35/21.95
POL(c2(x1, x2)) = x1 + x2 61.35/21.95
POL(c3(x1)) = x1 61.35/21.95
POL(c4(x1)) = x1 61.35/21.95
POL(c5(x1, x2)) = x1 + x2 61.35/21.95
POL(c5(x1, x2, x3)) = x1 + x2 + x3 61.35/21.95
POL(c8(x1)) = x1 61.35/21.95
POL(c8(x1, x2)) = x1 + x2 61.35/21.95
POL(c9(x1, x2)) = x1 + x2 61.35/21.95
POL(f(x1, x2)) = [4] 61.35/21.95
POL(mark(x1)) = [4] 61.35/21.95
POL(ok(x1)) = x1 61.35/21.95
POL(proper(x1)) = 0
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.95
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
top(mark(z0)) → top(proper(z0)) 61.35/21.95
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
ACTIVE(f(b, x1)) → c2(F(mark(a), x1)) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1)) 61.35/21.95
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1))) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a))) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b)))
K tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1)) 61.35/21.95
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1)))
Defined Rule Symbols:
ACTIVE(f(b, x1)) → c2(F(mark(a), x1)) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b))) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a)))
active, f, proper, top
F, TOP, ACTIVE, PROPER
c3, c4, c9, c, c2, c2, c5, c5, c8, c8
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0))) 61.35/21.95
TOP(ok(b)) → c9(TOP(mark(a)), ACTIVE(b)) 61.35/21.95
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.95
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
top(mark(z0)) → top(proper(z0)) 61.35/21.95
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
ACTIVE(f(b, x1)) → c2(F(mark(a), x1)) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1)) 61.35/21.95
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1))) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a))) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b))) 61.35/21.95
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0))) 61.35/21.95
TOP(ok(b)) → c9(TOP(mark(a)), ACTIVE(b)) 61.35/21.95
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
K tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1)) 61.35/21.95
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1))) 61.35/21.95
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0))) 61.35/21.95
TOP(ok(b)) → c9(TOP(mark(a)), ACTIVE(b)) 61.35/21.95
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
Defined Rule Symbols:
ACTIVE(f(b, x1)) → c2(F(mark(a), x1)) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b))) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a)))
active, f, proper, top
F, ACTIVE, PROPER, TOP
c3, c4, c, c2, c2, c5, c5, c8, c8, c9
ACTIVE(f(z0, z0)) → c 61.35/21.95
ACTIVE(f(f(z0, z0), x1)) → c2(F(mark(f(a, b)), x1), ACTIVE(f(z0, z0))) 61.35/21.95
ACTIVE(f(f(z0, z1), x1)) → c2(F(f(active(z0), z1), x1), ACTIVE(f(z0, z1))) 61.35/21.95
ACTIVE(f(b, x1)) → c2(F(mark(a), x1)) 61.35/21.95
PROPER(f(x0, f(z0, z1))) → c5(F(proper(x0), f(proper(z0), proper(z1))), PROPER(x0), PROPER(f(z0, z1))) 61.35/21.95
PROPER(f(f(z0, z1), x1)) → c5(F(f(proper(z0), proper(z1)), proper(x1)), PROPER(f(z0, z1)), PROPER(x1)) 61.35/21.95
PROPER(f(x0, a)) → c5(F(proper(x0), ok(a)), PROPER(x0)) 61.35/21.95
PROPER(f(x0, b)) → c5(F(proper(x0), ok(b)), PROPER(x0)) 61.35/21.95
PROPER(f(a, x1)) → c5(F(ok(a), proper(x1)), PROPER(x1)) 61.35/21.95
PROPER(f(b, x1)) → c5(F(ok(b), proper(x1)), PROPER(x1)) 61.35/21.95
TOP(mark(f(z0, z1))) → c8(TOP(f(proper(z0), proper(z1))), PROPER(f(z0, z1))) 61.35/21.95
TOP(ok(f(z0, z0))) → c9(TOP(mark(f(a, b))), ACTIVE(f(z0, z0))) 61.35/21.95
TOP(ok(f(z0, z1))) → c9(TOP(f(active(z0), z1)), ACTIVE(f(z0, z1)))
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.95
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
top(mark(z0)) → top(proper(z0)) 61.35/21.95
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a))) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b))) 61.35/21.95
TOP(ok(b)) → c9(TOP(mark(a)), ACTIVE(b))
K tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(ok(b)) → c9(TOP(mark(a)), ACTIVE(b))
Defined Rule Symbols:
TOP(mark(b)) → c8(TOP(ok(b))) 61.35/21.95
TOP(mark(a)) → c8(TOP(ok(a)))
active, f, proper, top
F, TOP
c3, c4, c8, c9
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.95
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
top(mark(z0)) → top(proper(z0)) 61.35/21.95
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b))) 61.35/21.95
TOP(mark(a)) → c8 61.35/21.95
TOP(ok(b)) → c9(TOP(mark(a)))
K tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1)) 61.35/21.95
TOP(ok(b)) → c9(TOP(mark(a)))
Defined Rule Symbols:
TOP(mark(b)) → c8(TOP(ok(b))) 61.35/21.95
TOP(mark(a)) → c8
active, f, proper, top
F, TOP
c3, c4, c8, c8, c9
TOP(mark(a)) → c8 61.35/21.95
TOP(ok(b)) → c9(TOP(mark(a))) 61.35/21.95
TOP(mark(b)) → c8(TOP(ok(b)))
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.95
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
top(mark(z0)) → top(proper(z0)) 61.35/21.95
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1))
K tuples:none
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1))
active, f, proper, top
F
c3, c4
We considered the (Usable) Rules:none
F(mark(z0), z1) → c3(F(z0, z1))
The order we found is given by the following interpretation:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1))
POL(F(x1, x2)) = [4]x1 61.35/21.95
POL(c3(x1)) = x1 61.35/21.95
POL(c4(x1)) = x1 61.35/21.95
POL(mark(x1)) = [4] + x1 61.35/21.95
POL(ok(x1)) = x1
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.95
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
top(mark(z0)) → top(proper(z0)) 61.35/21.95
top(ok(z0)) → top(active(z0))
S tuples:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1))
K tuples:
F(ok(z0), ok(z1)) → c4(F(z0, z1))
Defined Rule Symbols:
F(mark(z0), z1) → c3(F(z0, z1))
active, f, proper, top
F
c3, c4
We considered the (Usable) Rules:none
F(ok(z0), ok(z1)) → c4(F(z0, z1))
The order we found is given by the following interpretation:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1))
POL(F(x1, x2)) = x1 61.35/21.95
POL(c3(x1)) = x1 61.35/21.95
POL(c4(x1)) = x1 61.35/21.95
POL(mark(x1)) = x1 61.35/21.95
POL(ok(x1)) = [1] + x1
Tuples:
active(f(z0, z0)) → mark(f(a, b)) 61.35/21.95
active(b) → mark(a) 61.35/21.95
active(f(z0, z1)) → f(active(z0), z1) 61.35/21.95
f(mark(z0), z1) → mark(f(z0, z1)) 61.35/21.95
f(ok(z0), ok(z1)) → ok(f(z0, z1)) 61.35/21.95
proper(f(z0, z1)) → f(proper(z0), proper(z1)) 61.35/21.95
proper(a) → ok(a) 61.35/21.95
proper(b) → ok(b) 61.35/21.95
top(mark(z0)) → top(proper(z0)) 61.35/21.95
top(ok(z0)) → top(active(z0))
S tuples:none
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1))
Defined Rule Symbols:
F(mark(z0), z1) → c3(F(z0, z1)) 61.35/21.95
F(ok(z0), ok(z1)) → c4(F(z0, z1))
active, f, proper, top
F
c3, c4