Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
↳ QTRS
↳ DependencyPairsProof
↳ QTRS Reverse
Q restricted rewrite system:
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
PROPER(g(X)) → PROPER(X)
PROPER(f(X)) → F(proper(X))
TOP(mark(X)) → PROPER(X)
TOP(mark(X)) → TOP(proper(X))
F(ok(X)) → F(X)
ACTIVE(c) → F(g(c))
G(ok(X)) → G(X)
PROPER(g(X)) → G(proper(X))
ACTIVE(c) → G(c)
PROPER(f(X)) → PROPER(X)
TOP(ok(X)) → ACTIVE(X)
TOP(ok(X)) → TOP(active(X))
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
PROPER(g(X)) → PROPER(X)
PROPER(f(X)) → F(proper(X))
TOP(mark(X)) → PROPER(X)
TOP(mark(X)) → TOP(proper(X))
F(ok(X)) → F(X)
ACTIVE(c) → F(g(c))
G(ok(X)) → G(X)
PROPER(g(X)) → G(proper(X))
ACTIVE(c) → G(c)
PROPER(f(X)) → PROPER(X)
TOP(ok(X)) → ACTIVE(X)
TOP(ok(X)) → TOP(active(X))
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 4 SCCs with 6 less nodes.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
G(ok(X)) → G(X)
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
G(ok(X)) → G(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
G(ok(X)) → G(X)
No rules are removed from R.
Used ordering: POLO with Polynomial interpretation [25]:
POL(G(x1)) = 2·x1
POL(ok(x1)) = 2·x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ PisEmptyProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
G(ok(X)) → G(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
F(ok(X)) → F(X)
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
F(ok(X)) → F(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
F(ok(X)) → F(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
F(ok(X)) → F(X)
No rules are removed from R.
Used ordering: POLO with Polynomial interpretation [25]:
POL(F(x1)) = 2·x1
POL(ok(x1)) = 2·x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QTRS Reverse
Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
PROPER(g(X)) → PROPER(X)
PROPER(f(X)) → PROPER(X)
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
PROPER(g(X)) → PROPER(X)
PROPER(f(X)) → PROPER(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
PROPER(g(X)) → PROPER(X)
PROPER(f(X)) → PROPER(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the usable rules with reduction pair processor [15] with a polynomial ordering [25], all dependency pairs and the corresponding usable rules [17] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
PROPER(g(X)) → PROPER(X)
PROPER(f(X)) → PROPER(X)
No rules are removed from R.
Used ordering: POLO with Polynomial interpretation [25]:
POL(PROPER(x1)) = 2·x1
POL(f(x1)) = 2·x1
POL(g(x1)) = 2·x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QTRS Reverse
Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
TOP(mark(X)) → TOP(proper(X))
TOP(ok(X)) → TOP(active(X))
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ UsableRulesProof
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
TOP(mark(X)) → TOP(proper(X))
TOP(ok(X)) → TOP(active(X))
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
g(ok(X)) → ok(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ UsableRulesProof
↳ QDP
↳ QTRS Reverse
Q DP problem:
The TRS P consists of the following rules:
TOP(mark(X)) → TOP(proper(X))
TOP(ok(X)) → TOP(active(X))
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
g(ok(X)) → ok(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We have reversed the following QTRS:
The set of rules R is
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The set Q is empty.
We have obtained the following QTRS:
c'(active(x)) → c'(g(f(mark(x))))
g(f(active(x))) → g(mark(x))
c'(proper(x)) → c'(ok(x))
f(proper(x)) → proper(f(x))
g(proper(x)) → proper(g(x))
ok(f(x)) → f(ok(x))
ok(g(x)) → g(ok(x))
mark(top(x)) → proper(top(x))
ok(top(x)) → active(top(x))
The set Q is empty.
↳ QTRS
↳ DependencyPairsProof
↳ QTRS Reverse
↳ QTRS
↳ RFCMatchBoundsTRSProof
Q restricted rewrite system:
The TRS R consists of the following rules:
c'(active(x)) → c'(g(f(mark(x))))
g(f(active(x))) → g(mark(x))
c'(proper(x)) → c'(ok(x))
f(proper(x)) → proper(f(x))
g(proper(x)) → proper(g(x))
ok(f(x)) → f(ok(x))
ok(g(x)) → g(ok(x))
mark(top(x)) → proper(top(x))
ok(top(x)) → active(top(x))
Q is empty.
Termination of the TRS R could be shown with a Match Bound [6,7] of 6. This implies Q-termination of R.
The following rules were used to construct the certificate:
c'(active(x)) → c'(g(f(mark(x))))
g(f(active(x))) → g(mark(x))
c'(proper(x)) → c'(ok(x))
f(proper(x)) → proper(f(x))
g(proper(x)) → proper(g(x))
ok(f(x)) → f(ok(x))
ok(g(x)) → g(ok(x))
mark(top(x)) → proper(top(x))
ok(top(x)) → active(top(x))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
196, 197, 198, 199, 200, 201, 203, 202, 204, 205, 206, 207, 208, 209, 210, 212, 211, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248
Node 196 is start node and node 197 is final node.
Those nodes are connect through the following edges:
- 196 to 198 labelled proper_1(0)
- 196 to 199 labelled active_1(0), proper_1(0)
- 196 to 200 labelled g_1(0), f_1(0), c'_1(0)
- 196 to 201 labelled c'_1(0)
- 196 to 209 labelled c'_1(1)
- 196 to 208 labelled proper_1(1)
- 196 to 210 labelled c'_1(1)
- 196 to 212 labelled g_1(1)
- 196 to 218 labelled proper_1(2)
- 196 to 219 labelled c'_1(2)
- 196 to 231 labelled c'_1(3)
- 196 to 246 labelled c'_1(4)
- 197 to 197 labelled #_1(0)
- 198 to 197 labelled g_1(0), f_1(0)
- 198 to 205 labelled proper_1(1)
- 198 to 206 labelled g_1(1)
- 198 to 214 labelled proper_1(2)
- 199 to 197 labelled top_1(0)
- 200 to 197 labelled ok_1(0), mark_1(0)
- 200 to 204 labelled proper_1(1), active_1(1)
- 200 to 207 labelled g_1(1), f_1(1)
- 200 to 216 labelled g_1(2)
- 200 to 223 labelled proper_1(3)
- 200 to 227 labelled proper_1(2)
- 201 to 202 labelled g_1(0)
- 201 to 215 labelled proper_1(1)
- 203 to 197 labelled mark_1(0)
- 203 to 204 labelled proper_1(1)
- 202 to 203 labelled f_1(0)
- 202 to 208 labelled proper_1(1)
- 204 to 197 labelled top_1(1)
- 205 to 197 labelled g_1(1), f_1(1)
- 205 to 205 labelled proper_1(1)
- 205 to 206 labelled g_1(1)
- 205 to 214 labelled proper_1(2)
- 206 to 197 labelled mark_1(1)
- 206 to 204 labelled proper_1(1)
- 207 to 197 labelled ok_1(1)
- 207 to 204 labelled active_1(1)
- 207 to 207 labelled g_1(1), f_1(1)
- 207 to 216 labelled g_1(2)
- 207 to 223 labelled proper_1(3)
- 207 to 227 labelled proper_1(2)
- 208 to 204 labelled f_1(1), g_1(1)
- 208 to 223 labelled f_1(1), g_1(1)
- 208 to 227 labelled g_1(1), f_1(1)
- 209 to 204 labelled ok_1(1)
- 209 to 213 labelled active_1(2)
- 209 to 215 labelled ok_1(1)
- 209 to 225 labelled g_1(2)
- 209 to 223 labelled ok_1(1)
- 209 to 227 labelled ok_1(1)
- 209 to 233 labelled f_1(2), g_1(2)
- 209 to 228 labelled f_1(2), g_1(2)
- 209 to 234 labelled g_1(3)
- 209 to 237 labelled proper_1(4)
- 210 to 211 labelled g_1(1)
- 210 to 222 labelled proper_1(2)
- 212 to 204 labelled mark_1(1)
- 212 to 213 labelled proper_1(2)
- 211 to 212 labelled f_1(1)
- 211 to 217 labelled proper_1(2)
- 213 to 197 labelled top_1(2)
- 214 to 204 labelled g_1(2)
- 215 to 208 labelled g_1(1)
- 216 to 204 labelled mark_1(2)
- 216 to 213 labelled proper_1(2)
- 217 to 213 labelled f_1(2)
- 218 to 213 labelled g_1(2)
- 219 to 220 labelled g_1(2)
- 219 to 222 labelled ok_1(2)
- 219 to 229 labelled proper_1(3)
- 219 to 230 labelled g_1(3)
- 219 to 240 labelled g_1(4)
- 219 to 237 labelled ok_1(2)
- 219 to 242 labelled proper_1(5)
- 220 to 221 labelled f_1(2)
- 220 to 226 labelled proper_1(3)
- 221 to 213 labelled mark_1(2)
- 221 to 224 labelled proper_1(3)
- 222 to 217 labelled g_1(2)
- 223 to 213 labelled g_1(3)
- 224 to 197 labelled top_1(3)
- 225 to 208 labelled ok_1(2)
- 225 to 228 labelled f_1(2), g_1(2)
- 225 to 213 labelled ok_1(2)
- 225 to 224 labelled active_1(3)
- 225 to 233 labelled f_1(2), g_1(2)
- 226 to 224 labelled f_1(3)
- 227 to 223 labelled f_1(2), g_1(2)
- 227 to 227 labelled g_1(2), f_1(2)
- 228 to 204 labelled ok_1(2)
- 228 to 213 labelled active_1(2)
- 228 to 223 labelled ok_1(2)
- 228 to 232 labelled g_1(3)
- 229 to 226 labelled g_1(3)
- 230 to 217 labelled ok_1(3)
- 230 to 232 labelled f_1(3)
- 230 to 224 labelled ok_1(3)
- 230 to 241 labelled active_1(4)
- 231 to 229 labelled ok_1(3)
- 231 to 236 labelled g_1(4)
- 231 to 243 labelled g_1(5)
- 231 to 242 labelled ok_1(3)
- 231 to 245 labelled proper_1(6)
- 232 to 213 labelled ok_1(3)
- 232 to 224 labelled active_1(3)
- 233 to 227 labelled ok_1(2)
- 233 to 235 labelled f_1(3), g_1(3)
- 234 to 213 labelled mark_1(3)
- 234 to 224 labelled proper_1(3)
- 235 to 227 labelled ok_1(3)
- 235 to 223 labelled ok_1(3)
- 235 to 235 labelled f_1(3), g_1(3)
- 235 to 239 labelled g_1(4)
- 236 to 226 labelled ok_1(4)
- 236 to 238 labelled f_1(4)
- 236 to 241 labelled ok_1(4)
- 236 to 244 labelled active_1(5)
- 237 to 224 labelled g_1(4)
- 238 to 224 labelled ok_1(4)
- 238 to 241 labelled active_1(4)
- 239 to 213 labelled ok_1(4)
- 239 to 224 labelled active_1(3)
- 240 to 224 labelled mark_1(4)
- 240 to 241 labelled proper_1(4)
- 241 to 197 labelled top_1(4)
- 242 to 241 labelled g_1(5)
- 243 to 241 labelled mark_1(5)
- 243 to 244 labelled proper_1(5)
- 244 to 197 labelled top_1(5)
- 245 to 244 labelled g_1(6)
- 246 to 245 labelled ok_1(4)
- 246 to 247 labelled g_1(5)
- 247 to 244 labelled ok_1(5)
- 247 to 248 labelled active_1(6)
- 248 to 197 labelled top_1(6)