Term Rewriting System R:

   [x]
   a(d(x)) -> d(c(b(a(x))))
   a(c(x)) -> x
   b(c(x)) -> c(d(a(b(x))))
   b(d(x)) -> x

Innermost Termination of R to be shown.


R contains the following Dependency Pairs: 


   B(c(x)) -> A(b(x))
   B(c(x)) -> B(x)
   A(d(x)) -> B(a(x))
   A(d(x)) -> A(x)

Furthermore, R contains one SCC.


SCC1:

A(d(x)) -> A(x)
B(c(x)) -> B(x)
A(d(x)) -> B(a(x))
B(c(x)) -> A(b(x))

Using RFC Match Bounds, the Scc could be solved. The Match Bound was 2.
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47

Node 33 is start node and node 34 is final node.

Those nodes are connect through the following edges:

* 34 to 34 labelled #(0)
* 33 to 34 labelled A(0)
* 33 to 34 labelled B(0)
* 33 to 35 labelled B(0)
* 35 to 34 labelled a(0)
* 33 to 36 labelled A(0)
* 36 to 34 labelled b(0)
* 33 to 37 labelled B(1)
* 37 to 34 labelled a(1)
* 33 to 34 labelled A(1)
* 34 to 34 labelled b(1)
* 33 to 34 labelled B(1)
* 36 to 38 labelled c(1)
* 38 to 39 labelled d(1)
* 39 to 40 labelled a(1)
* 40 to 34 labelled b(1)
* 35 to 41 labelled d(1)
* 41 to 42 labelled c(1)
* 42 to 43 labelled b(1)
* 43 to 34 labelled a(1)
* 40 to 38 labelled c(1)
* 43 to 41 labelled d(1)
* 34 to 38 labelled c(1)
* 37 to 41 labelled d(1)
* 33 to 44 labelled A(2)
* 44 to 38 labelled b(2)
* 33 to 38 labelled B(2)
* 40 to 38 labelled b(1)
* 40 to 45 labelled c(2)
* 45 to 46 labelled d(2)
* 46 to 47 labelled a(2)
* 47 to 38 labelled b(2)
* 33 to 40 labelled A(1)
* 33 to 38 labelled B(1)
* 34 to 45 labelled c(2)
* 44 to 45 labelled b(2)
* 33 to 45 labelled B(2)
* 40 to 45 labelled b(1)
* 47 to 45 labelled b(2)
* 33 to 45 labelled B(1)




Innermost Termination of R successfully shown.


Duration: 10.914 seconds.