Term Rewriting System R:

   [X]
   a__g(X) -> a__h(X)
   a__g(X) -> g(X)
   a__c -> d
   a__c -> c
   a__h(d) -> a__g(c)
   a__h(X) -> h(X)
   mark(g(X)) -> a__g(X)
   mark(h(X)) -> a__h(X)
   mark(c) -> a__c
   mark(d) -> d

Termination of R to be shown.


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:
1, 2, 3

Node 1 is start node and node 2 is final node.

Those nodes are connect through the following edges:

* 2 to 2 labelled #(0)
* 1 to 2 labelled a__h(0)
* 1 to 2 labelled g(0)
* 1 to 2 labelled d(0)
* 1 to 2 labelled c(0)
* 1 to 1 labelled a__g(0)
* 1 to 2 labelled h(0)
* 1 to 2 labelled a__g(0)
* 1 to 2 labelled a__c(0)
* 1 to 1 labelled a__h(1)
* 1 to 1 labelled g(1)
* 1 to 2 labelled c(1)
* 1 to 2 labelled d(1)
* 1 to 2 labelled a__h(1)
* 1 to 2 labelled g(1)
* 1 to 2 labelled h(1)
* 1 to 1 labelled h(2)
* 1 to 2 labelled h(2)
* 1 to 1 labelled a__g(1)
* 1 to 3 labelled a__g(2)
* 3 to 2 labelled c(2)
* 1 to 1 labelled a__h(2)
* 1 to 1 labelled g(2)
* 1 to 3 labelled a__h(3)
* 1 to 3 labelled g(3)
* 1 to 1 labelled h(3)
* 1 to 3 labelled h(4)




Termination of R successfully shown.


Duration: 0.351 seconds.