(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)) → a__f(g(f(a)))
mark(f(X)) → a__f(X)
mark(a) → a
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:
8688865, 8688866, 8688867, 8688868, 8688869, 8688870, 8688871, 8688874, 8688873, 8688872
Node 8688865 is start node and node 8688866 is final node.
Those nodes are connect through the following edges:
- 8688865 to 8688866 labelled a__f_1(0), a(0), f_1(0), f_1(1)
- 8688865 to 8688867 labelled g_1(0)
- 8688865 to 8688868 labelled a__f_1(0), f_1(1)
- 8688865 to 8688872 labelled a__f_1(1), f_1(2)
- 8688866 to 8688866 labelled #_1(0)
- 8688867 to 8688866 labelled mark_1(0), a__f_1(1), a(1), f_1(2)
- 8688867 to 8688871 labelled g_1(1)
- 8688867 to 8688872 labelled a__f_1(1), f_1(2)
- 8688868 to 8688869 labelled g_1(0)
- 8688869 to 8688870 labelled f_1(0)
- 8688870 to 8688866 labelled a(0)
- 8688871 to 8688866 labelled mark_1(1), a__f_1(1), a(1), f_1(2)
- 8688871 to 8688871 labelled g_1(1)
- 8688871 to 8688872 labelled a__f_1(1), f_1(2)
- 8688874 to 8688866 labelled a(1)
- 8688873 to 8688874 labelled f_1(1)
- 8688872 to 8688873 labelled g_1(1)