Term Rewriting System R:
[X]
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))
Termination of R to be shown.
TRS
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
ACTIVE(c) -> F(g(c))
ACTIVE(c) -> G(c)
PROPER(f(X)) -> F(proper(X))
PROPER(f(X)) -> PROPER(X)
PROPER(g(X)) -> G(proper(X))
PROPER(g(X)) -> PROPER(X)
F(ok(X)) -> F(X)
G(ok(X)) -> G(X)
TOP(mark(X)) -> TOP(proper(X))
TOP(mark(X)) -> PROPER(X)
TOP(ok(X)) -> TOP(active(X))
TOP(ok(X)) -> ACTIVE(X)
Furthermore, R contains four SCCs.
TRS
↳DPs
→DP Problem 1
↳Modular Removal of Rules
→DP Problem 2
↳MRR
→DP Problem 3
↳MRR
→DP Problem 4
↳MRR
Dependency Pair:
F(ok(X)) -> F(X)
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))
We have the following set of usable rules:
none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
| POL(ok(x1)) | = x1 |
| POL(F(x1)) | = x1 |
We have the following set D of usable symbols: {F}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
F(ok(X)) -> F(X)
No Rules can be deleted.
After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.
TRS
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳Modular Removal of Rules
→DP Problem 3
↳MRR
→DP Problem 4
↳MRR
Dependency Pair:
G(ok(X)) -> G(X)
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))
We have the following set of usable rules:
none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
| POL(G(x1)) | = x1 |
| POL(ok(x1)) | = x1 |
We have the following set D of usable symbols: {G}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
G(ok(X)) -> G(X)
No Rules can be deleted.
After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.
TRS
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳MRR
→DP Problem 3
↳Modular Removal of Rules
→DP Problem 4
↳MRR
Dependency Pairs:
PROPER(g(X)) -> PROPER(X)
PROPER(f(X)) -> PROPER(X)
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))
We have the following set of usable rules:
none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
| POL(g(x1)) | = x1 |
| POL(PROPER(x1)) | = x1 |
| POL(f(x1)) | = x1 |
We have the following set D of usable symbols: {PROPER}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:
PROPER(g(X)) -> PROPER(X)
PROPER(f(X)) -> PROPER(X)
No Rules can be deleted.
After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.
TRS
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳MRR
→DP Problem 3
↳MRR
→DP Problem 4
↳Modular Removal of Rules
Dependency Pairs:
TOP(ok(X)) -> TOP(active(X))
TOP(mark(X)) -> TOP(proper(X))
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))
We have the following set of usable 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))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
| POL(active(x1)) | = x1 |
| POL(proper(x1)) | = x1 |
| POL(c) | = 0 |
| POL(g(x1)) | = x1 |
| POL(mark(x1)) | = x1 |
| POL(TOP(x1)) | = x1 |
| POL(ok(x1)) | = x1 |
| POL(f(x1)) | = x1 |
We have the following set D of usable symbols: {active, proper, c, g, mark, TOP, ok, f}
No Dependency Pairs can be deleted.
2 non usable rules have been deleted.
The result of this processor delivers one new DP problem.
TRS
↳DPs
→DP Problem 1
↳MRR
→DP Problem 2
↳MRR
→DP Problem 3
↳MRR
→DP Problem 4
↳MRR
→DP Problem 5
↳RFC Match Bounds
Dependency Pairs:
TOP(ok(X)) -> TOP(active(X))
TOP(mark(X)) -> TOP(proper(X))
Rules:
active(c) -> mark(f(g(c)))
active(f(g(X))) -> mark(g(X))
f(ok(X)) -> ok(f(X))
g(ok(X)) -> ok(g(X))
proper(c) -> ok(c)
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
Using RFC Match Bounds, the DP problem could be solved. The Match Bound was 5.
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133
Node 99 is start node and node 100 is final node.
Those nodes are connect through the following edges:
- 100 to 100 labelled #(0)
- 99 to 101 labelled TOP(0)
- 101 to 100 labelled proper(0)
- 99 to 102 labelled TOP(0)
- 102 to 100 labelled active(0)
- 102 to 103 labelled mark(1)
- 103 to 104 labelled f(1)
- 104 to 105 labelled g(1)
- 105 to 100 labelled c(1)
- 103 to 100 labelled g(1)
- 101 to 105 labelled ok(1)
- 101 to 106 labelled f(1)
- 106 to 100 labelled proper(1)
- 101 to 106 labelled g(1)
- 99 to 107 labelled TOP(1)
- 107 to 105 labelled active(1)
- 107 to 103 labelled proper(1)
- 106 to 105 labelled ok(1)
- 106 to 106 labelled f(1)
- 106 to 106 labelled g(1)
- 103 to 103 labelled ok(1)
- 106 to 108 labelled ok(2)
- 108 to 105 labelled g(2)
- 101 to 109 labelled ok(2)
- 109 to 105 labelled f(2)
- 101 to 108 labelled ok(2)
- 106 to 109 labelled ok(2)
- 107 to 110 labelled f(2)
- 110 to 104 labelled proper(2)
- 107 to 111 labelled mark(2)
- 111 to 112 labelled f(2)
- 112 to 113 labelled g(2)
- 113 to 100 labelled c(2)
- 107 to 114 labelled g(2)
- 114 to 100 labelled proper(2)
- 108 to 109 labelled g(2)
- 109 to 109 labelled f(2)
- 110 to 115 labelled g(2)
- 115 to 105 labelled proper(2)
- 108 to 108 labelled g(2)
- 109 to 108 labelled f(2)
- 107 to 108 labelled active(1)
- 99 to 116 labelled TOP(2)
- 116 to 111 labelled proper(2)
- 114 to 105 labelled ok(1)
- 114 to 106 labelled f(1)
- 114 to 106 labelled g(1)
- 107 to 109 labelled active(1)
- 114 to 109 labelled ok(2)
- 114 to 108 labelled ok(2)
- 116 to 117 labelled f(3)
- 117 to 112 labelled proper(3)
- 107 to 108 labelled ok(2)
- 115 to 113 labelled ok(2)
- 107 to 108 labelled mark(2)
- 110 to 118 labelled ok(3)
- 118 to 113 labelled g(3)
- 107 to 119 labelled ok(3)
- 119 to 108 labelled g(3)
- 119 to 109 labelled g(3)
- 116 to 108 labelled proper(2)
- 116 to 108 labelled active(2)
- 117 to 120 labelled g(3)
- 120 to 113 labelled proper(3)
- 116 to 121 labelled g(3)
- 121 to 105 labelled proper(3)
- 120 to 122 labelled ok(3)
- 122 to 100 labelled c(3)
- 116 to 119 labelled active(2)
- 121 to 109 labelled proper(3)
- 121 to 108 labelled proper(3)
- 119 to 118 labelled f(3)
- 121 to 121 labelled g(3)
- 121 to 121 labelled f(3)
- 121 to 113 labelled ok(2)
- 117 to 123 labelled ok(4)
- 123 to 122 labelled g(4)
- 116 to 118 labelled mark(3)
- 121 to 124 labelled ok(3)
- 124 to 113 labelled f(3)
- 116 to 118 labelled ok(3)
- 121 to 118 labelled ok(3)
- 99 to 125 labelled TOP(3)
- 125 to 118 labelled proper(3)
- 116 to 126 labelled ok(4)
- 126 to 123 labelled f(4)
- 125 to 127 labelled g(4)
- 127 to 113 labelled proper(4)
- 125 to 118 labelled active(3)
- 121 to 128 labelled ok(4)
- 128 to 124 labelled f(4)
- 126 to 124 labelled g(4)
- 121 to 126 labelled ok(4)
- 125 to 126 labelled active(3)
- 128 to 118 labelled f(4)
- 126 to 118 labelled g(4)
- 127 to 122 labelled ok(3)
- 128 to 128 labelled f(4)
- 126 to 128 labelled g(4)
- 128 to 126 labelled f(4)
- 126 to 126 labelled g(4)
- 125 to 123 labelled mark(4)
- 125 to 123 labelled ok(4)
- 99 to 129 labelled TOP(4)
- 129 to 123 labelled proper(4)
- 129 to 130 labelled g(5)
- 130 to 122 labelled proper(5)
- 129 to 123 labelled active(4)
- 130 to 131 labelled ok(4)
- 131 to 100 labelled c(4)
- 129 to 132 labelled ok(5)
- 132 to 131 labelled g(5)
- 99 to 133 labelled TOP(5)
- 133 to 132 labelled active(5)
Termination of R successfully shown.
Duration:
0:03 minutes