Term Rewriting System R:
[X]
active(f(X)) -> mark(g(h(f(X))))
active(f(X)) -> f(active(X))
active(h(X)) -> h(active(X))
f(mark(X)) -> mark(f(X))
f(ok(X)) -> ok(f(X))
h(mark(X)) -> mark(h(X))
h(ok(X)) -> ok(h(X))
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
proper(h(X)) -> h(proper(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
↳Reversing
Rule(s) before reversing:
active(f(X)) -> mark(g(h(f(X))))
active(f(X)) -> f(active(X))
active(h(X)) -> h(active(X))
f(mark(X)) -> mark(f(X))
f(ok(X)) -> ok(f(X))
h(mark(X)) -> mark(h(X))
h(ok(X)) -> ok(h(X))
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
proper(h(X)) -> h(proper(X))
g(ok(X)) -> ok(g(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))
Rule(s) after reversing:
f'(active'(x)) -> f'(h'(g'(mark'(x))))
f'(active'(x)) -> active'(f'(x))
f'(proper'(x)) -> proper'(f'(x))
h'(active'(x)) -> active'(h'(x))
h'(proper'(x)) -> proper'(h'(x))
g'(proper'(x)) -> proper'(g'(x))
mark'(f'(x)) -> f'(mark'(x))
mark'(h'(x)) -> h'(mark'(x))
mark'(top'(x)) -> proper'(top'(x))
ok'(f'(x)) -> f'(ok'(x))
ok'(h'(x)) -> h'(ok'(x))
ok'(g'(x)) -> g'(ok'(x))
ok'(top'(x)) -> active'(top'(x))
TRS
↳Rev
→TRS2
↳RFC Match Bounds
Termination could be shown with a Match Bound of 4.
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94
Node 51 is start node and node 52 is final node.
Those nodes are connect through the following edges:
- 52 to 52 labelled #(0)
- 51 to 53 labelled h'(0)
- 53 to 52 labelled ok'(0)
- 51 to 54 labelled active'(0)
- 54 to 52 labelled f'(0)
- 51 to 55 labelled proper'(0)
- 55 to 52 labelled g'(0)
- 51 to 56 labelled active'(0)
- 56 to 52 labelled top'(0)
- 51 to 57 labelled active'(0)
- 57 to 52 labelled h'(0)
- 51 to 53 labelled g'(0)
- 51 to 57 labelled proper'(0)
- 51 to 53 labelled f'(0)
- 51 to 58 labelled f'(0)
- 58 to 52 labelled mark'(0)
- 51 to 56 labelled proper'(0)
- 51 to 59 labelled f'(0)
- 59 to 60 labelled h'(0)
- 60 to 61 labelled g'(0)
- 61 to 52 labelled mark'(0)
- 51 to 54 labelled proper'(0)
- 51 to 58 labelled h'(0)
- 53 to 62 labelled h'(1)
- 62 to 52 labelled ok'(1)
- 53 to 63 labelled active'(1)
- 63 to 52 labelled top'(1)
- 53 to 62 labelled g'(1)
- 53 to 62 labelled f'(1)
- 58 to 63 labelled proper'(1)
- 58 to 64 labelled h'(1)
- 64 to 52 labelled mark'(1)
- 58 to 64 labelled f'(1)
- 55 to 65 labelled proper'(1)
- 65 to 52 labelled g'(1)
- 57 to 66 labelled active'(1)
- 66 to 52 labelled h'(1)
- 57 to 66 labelled proper'(1)
- 54 to 67 labelled f'(1)
- 67 to 68 labelled h'(1)
- 68 to 69 labelled g'(1)
- 69 to 52 labelled mark'(1)
- 54 to 70 labelled proper'(1)
- 70 to 52 labelled f'(1)
- 54 to 70 labelled active'(1)
- 61 to 63 labelled proper'(1)
- 61 to 64 labelled h'(1)
- 61 to 64 labelled f'(1)
- 51 to 71 labelled active'(1)
- 71 to 63 labelled f'(1)
- 51 to 72 labelled f'(1)
- 72 to 73 labelled h'(1)
- 73 to 74 labelled g'(1)
- 74 to 63 labelled mark'(1)
- 71 to 63 labelled h'(1)
- 60 to 75 labelled proper'(1)
- 75 to 63 labelled g'(1)
- 65 to 65 labelled proper'(1)
- 66 to 66 labelled active'(1)
- 66 to 66 labelled proper'(1)
- 62 to 62 labelled h'(1)
- 62 to 63 labelled active'(1)
- 62 to 62 labelled g'(1)
- 62 to 62 labelled f'(1)
- 70 to 67 labelled f'(1)
- 70 to 70 labelled proper'(1)
- 70 to 70 labelled active'(1)
- 69 to 63 labelled proper'(1)
- 69 to 64 labelled h'(1)
- 69 to 64 labelled f'(1)
- 64 to 63 labelled proper'(1)
- 64 to 64 labelled h'(1)
- 64 to 64 labelled f'(1)
- 51 to 71 labelled proper'(1)
- 62 to 76 labelled active'(2)
- 76 to 63 labelled h'(2)
- 53 to 76 labelled active'(2)
- 76 to 63 labelled f'(2)
- 62 to 77 labelled f'(2)
- 77 to 78 labelled h'(2)
- 78 to 79 labelled g'(2)
- 79 to 63 labelled mark'(2)
- 53 to 77 labelled f'(2)
- 58 to 76 labelled proper'(2)
- 61 to 76 labelled proper'(2)
- 64 to 76 labelled proper'(2)
- 69 to 76 labelled proper'(2)
- 59 to 80 labelled proper'(1)
- 80 to 75 labelled h'(1)
- 68 to 81 labelled proper'(2)
- 81 to 63 labelled g'(2)
- 74 to 82 labelled proper'(2)
- 82 to 52 labelled top'(2)
- 71 to 80 labelled f'(1)
- 71 to 76 labelled f'(1)
- 71 to 76 labelled h'(1)
- 79 to 82 labelled proper'(2)
- 67 to 83 labelled proper'(2)
- 83 to 81 labelled h'(2)
- 76 to 76 labelled f'(2)
- 79 to 76 labelled mark'(2)
- 76 to 76 labelled h'(2)
- 74 to 76 labelled mark'(1)
- 81 to 76 labelled g'(2)
- 75 to 76 labelled g'(1)
- 73 to 84 labelled proper'(2)
- 84 to 82 labelled g'(2)
- 72 to 85 labelled proper'(2)
- 85 to 84 labelled h'(2)
- 78 to 86 labelled proper'(3)
- 86 to 82 labelled g'(3)
- 54 to 87 labelled proper'(2)
- 87 to 83 labelled f'(2)
- 70 to 87 labelled proper'(2)
- 74 to 79 labelled f'(2)
- 79 to 88 labelled f'(3)
- 88 to 63 labelled mark'(3)
- 74 to 79 labelled h'(2)
- 79 to 88 labelled h'(3)
- 88 to 76 labelled mark'(3)
- 51 to 89 labelled proper'(2)
- 89 to 85 labelled f'(2)
- 88 to 82 labelled proper'(2)
- 74 to 90 labelled proper'(3)
- 90 to 82 labelled f'(3)
- 90 to 82 labelled h'(3)
- 77 to 91 labelled proper'(3)
- 91 to 86 labelled h'(3)
- 88 to 88 labelled f'(3)
- 88 to 88 labelled h'(3)
- 88 to 90 labelled proper'(3)
- 79 to 90 labelled proper'(3)
- 62 to 92 labelled proper'(3)
- 92 to 91 labelled f'(3)
- 53 to 92 labelled proper'(3)
- 84 to 90 labelled g'(2)
- 90 to 90 labelled f'(3)
- 86 to 90 labelled g'(3)
- 90 to 90 labelled h'(3)
- 88 to 93 labelled proper'(4)
- 93 to 90 labelled f'(4)
- 93 to 90 labelled h'(4)
- 79 to 93 labelled proper'(4)
- 53 to 94 labelled proper'(2)
- 94 to 92 labelled f'(2)
- 62 to 94 labelled proper'(2)
- 94 to 92 labelled g'(2)
- 94 to 92 labelled h'(2)
- 71 to 92 labelled g'(1)
- 71 to 92 labelled f'(1)
- 71 to 92 labelled h'(1)
- 90 to 93 labelled f'(3)
- 86 to 93 labelled g'(3)
- 90 to 93 labelled h'(3)
- 71 to 94 labelled g'(1)
- 71 to 94 labelled f'(1)
- 71 to 94 labelled h'(1)
- 94 to 94 labelled f'(2)
- 94 to 94 labelled g'(2)
- 94 to 94 labelled h'(2)
- 93 to 93 labelled f'(4)
- 93 to 93 labelled h'(4)
Termination of R successfully shown.
Duration:
0:00 minutes