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:



Innermost Termination of R successfully shown.
Duration:
0:06 minutes