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))
Innermost 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:
86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 126, 127, 128, 129, 130, 131, 132, 133, 134, 135, 136
Node 86 is start node and node 87 is final node.
Those nodes are connect through the following edges:
- 87 to 87 labelled #(0)
- 86 to 88 labelled h'(0)
- 88 to 87 labelled ok'(0)
- 86 to 89 labelled active'(0)
- 89 to 87 labelled f'(0)
- 86 to 90 labelled proper'(0)
- 90 to 87 labelled g'(0)
- 86 to 91 labelled active'(0)
- 91 to 87 labelled top'(0)
- 86 to 92 labelled active'(0)
- 92 to 87 labelled h'(0)
- 86 to 88 labelled g'(0)
- 86 to 92 labelled proper'(0)
- 86 to 88 labelled f'(0)
- 86 to 93 labelled f'(0)
- 93 to 87 labelled mark'(0)
- 86 to 91 labelled proper'(0)
- 86 to 94 labelled f'(0)
- 94 to 95 labelled h'(0)
- 95 to 96 labelled g'(0)
- 96 to 87 labelled mark'(0)
- 86 to 89 labelled proper'(0)
- 86 to 93 labelled h'(0)
- 96 to 97 labelled proper'(1)
- 97 to 87 labelled top'(1)
- 96 to 98 labelled h'(1)
- 98 to 87 labelled mark'(1)
- 96 to 98 labelled f'(1)
- 88 to 99 labelled h'(1)
- 99 to 87 labelled ok'(1)
- 88 to 97 labelled active'(1)
- 88 to 99 labelled g'(1)
- 88 to 99 labelled f'(1)
- 89 to 100 labelled f'(1)
- 100 to 101 labelled h'(1)
- 101 to 102 labelled g'(1)
- 102 to 87 labelled mark'(1)
- 89 to 103 labelled proper'(1)
- 103 to 87 labelled f'(1)
- 89 to 103 labelled active'(1)
- 92 to 104 labelled active'(1)
- 104 to 87 labelled h'(1)
- 92 to 104 labelled proper'(1)
- 93 to 97 labelled proper'(1)
- 93 to 98 labelled h'(1)
- 93 to 98 labelled f'(1)
- 90 to 105 labelled proper'(1)
- 105 to 87 labelled g'(1)
- 86 to 106 labelled active'(1)
- 106 to 97 labelled f'(1)
- 86 to 107 labelled f'(1)
- 107 to 108 labelled h'(1)
- 108 to 109 labelled g'(1)
- 109 to 97 labelled mark'(1)
- 106 to 97 labelled h'(1)
- 104 to 104 labelled active'(1)
- 104 to 104 labelled proper'(1)
- 98 to 97 labelled proper'(1)
- 98 to 98 labelled h'(1)
- 98 to 98 labelled f'(1)
- 103 to 100 labelled f'(1)
- 103 to 103 labelled proper'(1)
- 103 to 103 labelled active'(1)
- 99 to 99 labelled h'(1)
- 99 to 97 labelled active'(1)
- 99 to 99 labelled g'(1)
- 99 to 99 labelled f'(1)
- 102 to 97 labelled proper'(1)
- 102 to 98 labelled h'(1)
- 102 to 98 labelled f'(1)
- 105 to 105 labelled proper'(1)
- 95 to 110 labelled proper'(1)
- 110 to 97 labelled g'(1)
- 86 to 106 labelled proper'(1)
- 88 to 111 labelled active'(2)
- 111 to 97 labelled h'(2)
- 99 to 111 labelled active'(2)
- 111 to 97 labelled f'(2)
- 99 to 112 labelled f'(2)
- 112 to 113 labelled h'(2)
- 113 to 114 labelled g'(2)
- 114 to 97 labelled mark'(2)
- 88 to 112 labelled f'(2)
- 93 to 111 labelled proper'(2)
- 98 to 111 labelled proper'(2)
- 96 to 111 labelled proper'(2)
- 102 to 111 labelled proper'(2)
- 101 to 115 labelled proper'(2)
- 115 to 97 labelled g'(2)
- 109 to 116 labelled proper'(2)
- 116 to 87 labelled top'(2)
- 94 to 117 labelled proper'(1)
- 117 to 110 labelled h'(1)
- 111 to 111 labelled h'(2)
- 111 to 111 labelled f'(2)
- 106 to 111 labelled f'(1)
- 106 to 111 labelled h'(1)
- 100 to 118 labelled proper'(2)
- 118 to 115 labelled h'(2)
- 110 to 111 labelled g'(1)
- 109 to 111 labelled mark'(1)
- 115 to 111 labelled g'(2)
- 106 to 117 labelled f'(1)
- 114 to 116 labelled proper'(2)
- 108 to 119 labelled proper'(2)
- 119 to 116 labelled g'(2)
- 114 to 111 labelled mark'(2)
- 107 to 126 labelled proper'(2)
- 126 to 119 labelled h'(2)
- 113 to 127 labelled proper'(3)
- 127 to 116 labelled g'(3)
- 114 to 128 labelled f'(3)
- 128 to 97 labelled mark'(3)
- 109 to 114 labelled f'(2)
- 114 to 128 labelled h'(3)
- 109 to 114 labelled h'(2)
- 103 to 129 labelled proper'(2)
- 129 to 118 labelled f'(2)
- 89 to 129 labelled proper'(2)
- 128 to 111 labelled mark'(3)
- 112 to 130 labelled proper'(3)
- 130 to 127 labelled h'(3)
- 109 to 131 labelled proper'(3)
- 131 to 116 labelled h'(3)
- 131 to 116 labelled f'(3)
- 128 to 128 labelled f'(3)
- 128 to 128 labelled h'(3)
- 86 to 132 labelled proper'(2)
- 132 to 126 labelled f'(2)
- 128 to 116 labelled proper'(2)
- 119 to 131 labelled g'(2)
- 128 to 131 labelled proper'(3)
- 114 to 131 labelled proper'(3)
- 88 to 133 labelled proper'(3)
- 133 to 130 labelled f'(3)
- 99 to 133 labelled proper'(3)
- 106 to 133 labelled g'(1)
- 106 to 133 labelled f'(1)
- 106 to 133 labelled h'(1)
- 99 to 134 labelled proper'(2)
- 134 to 133 labelled h'(2)
- 88 to 135 labelled proper'(2)
- 135 to 133 labelled g'(2)
- 135 to 133 labelled f'(2)
- 99 to 135 labelled proper'(2)
- 88 to 134 labelled proper'(2)
- 131 to 131 labelled h'(3)
- 127 to 131 labelled g'(3)
- 131 to 131 labelled f'(3)
- 128 to 136 labelled proper'(4)
- 136 to 131 labelled f'(4)
- 114 to 136 labelled proper'(4)
- 136 to 131 labelled h'(4)
- 134 to 134 labelled h'(2)
- 135 to 134 labelled g'(2)
- 135 to 134 labelled f'(2)
- 134 to 135 labelled h'(2)
- 135 to 135 labelled g'(2)
- 135 to 135 labelled f'(2)
- 136 to 136 labelled f'(4)
- 136 to 136 labelled h'(4)
- 106 to 135 labelled g'(1)
- 106 to 135 labelled f'(1)
- 106 to 135 labelled h'(1)
- 131 to 136 labelled h'(3)
- 127 to 136 labelled g'(3)
- 131 to 136 labelled f'(3)
- 106 to 134 labelled g'(1)
- 106 to 134 labelled f'(1)
- 106 to 134 labelled h'(1)
Innermost Termination of R successfully shown.
Duration:
0:06 minutes