Term Rewriting System R:
[X]
f(g(X)) -> g(f(f(X)))
f(h(X)) -> h(g(X))
Innermost Termination of R to be shown.
TRS
↳Reversing
Rule(s) before reversing:
f(g(X)) -> g(f(f(X)))
f(h(X)) -> h(g(X))
Rule(s) after reversing:
g'(f'(x)) -> f'(f'(g'(x)))
h'(f'(x)) -> g'(h'(x))
TRS
↳Rev
→TRS2
↳RFC Match Bounds
Termination could be shown with a Match Bound of 1.
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
129, 130, 131, 132, 133, 134, 135, 136
Node 129 is start node and node 130 is final node.
Those nodes are connect through the following edges:
- 130 to 130 labelled #(0)
- 129 to 131 labelled f'(0)
- 131 to 132 labelled f'(0)
- 132 to 130 labelled g'(0)
- 129 to 133 labelled g'(0)
- 133 to 130 labelled h'(0)
- 133 to 134 labelled g'(1)
- 134 to 130 labelled h'(1)
- 132 to 135 labelled f'(1)
- 135 to 136 labelled f'(1)
- 136 to 130 labelled g'(1)
- 134 to 134 labelled g'(1)
- 136 to 135 labelled f'(1)
Innermost Termination of R successfully shown.
Duration:
0:00 minutes