(1) RFCMatchBoundsTRSProof (EQUIVALENT transformation)
Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 2. This implies Q-termination of R.
The following rules were used to construct the certificate:
a__f(f(a)) → c(f(g(f(a))))
mark(f(X)) → a__f(mark(X))
mark(a) → a
mark(c(X)) → c(X)
mark(g(X)) → g(mark(X))
a__f(X) → f(X)
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
10122763, 10122764, 10122765, 10122766, 10122767, 10122768, 10122769, 10122770, 10122772, 10122773, 10122774, 10122771, 10122775, 10122776, 10122778, 10122777
Node 10122763 is start node and node 10122764 is final node.
Those nodes are connect through the following edges:
- 10122763 to 10122764 labelled c_1(0), a(0), f_1(0)
- 10122763 to 10122765 labelled a__f_1(0), g_1(0), f_1(1)
- 10122763 to 10122766 labelled c_1(0)
- 10122763 to 10122771 labelled c_1(1)
- 10122764 to 10122764 labelled #_1(0)
- 10122765 to 10122764 labelled mark_1(0), c_1(1), a(1)
- 10122765 to 10122770 labelled a__f_1(1), g_1(1), f_1(2)
- 10122765 to 10122775 labelled c_1(2)
- 10122766 to 10122767 labelled f_1(0)
- 10122767 to 10122768 labelled g_1(0)
- 10122768 to 10122769 labelled f_1(0)
- 10122769 to 10122764 labelled a(0)
- 10122770 to 10122764 labelled mark_1(1), c_1(1), a(1)
- 10122770 to 10122770 labelled a__f_1(1), g_1(1), f_1(2)
- 10122770 to 10122775 labelled c_1(2)
- 10122772 to 10122773 labelled g_1(1)
- 10122773 to 10122774 labelled f_1(1)
- 10122774 to 10122764 labelled a(1)
- 10122771 to 10122772 labelled f_1(1)
- 10122775 to 10122776 labelled f_1(2)
- 10122776 to 10122777 labelled g_1(2)
- 10122778 to 10122764 labelled a(2)
- 10122777 to 10122778 labelled f_1(2)