Term Rewriting System R:
[X]
f(g(X)) -> g(f(f(X)))
f(h(X)) -> h(g(X))
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:
123, 124, 125, 126, 127, 128, 129, 130
Node 123 is start node and node 124 is final node.
Those nodes are connect through the following edges:
- 124 to 124 labelled #(0)
- 123 to 125 labelled f'(0)
- 125 to 126 labelled f'(0)
- 126 to 124 labelled g'(0)
- 123 to 127 labelled g'(0)
- 127 to 124 labelled h'(0)
- 127 to 128 labelled g'(1)
- 128 to 124 labelled h'(1)
- 126 to 129 labelled f'(1)
- 129 to 130 labelled f'(1)
- 130 to 124 labelled g'(1)
- 130 to 129 labelled f'(1)
- 128 to 128 labelled g'(1)
Termination of R successfully shown.
Duration:
0:00 minutes