(1) QTRS Reverse (EQUIVALENT transformation)

We applied the QTRS Reverse Processor [REVERSE].

(3) RFCMatchBoundsTRSProof (EQUIVALENT transformation)

Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 3. This implies Q-termination of R.
The following rules were used to construct the certificate:

a__c'(x) → c'(g(a__f(x)))
g(a__f(X)) → g(X)
c'(mark(x)) → a__c'(x)
f(mark(X)) → a__f(X)
g(mark(X)) → g(X)
a__c'(x) → c'(x)
a__f(X) → f(X)

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

2, 4, 7, 8, 9, 10, 13, 14

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

Those nodes are connected through the following edges:

• 2 to 7 labelled c'_1(0)
• 2 to 4 labelled g_1(0), a__c'_1(0), a__f_1(0), c'_1(0), f_1(0), c'_1(1), f_1(1), g_1(1), a__c'_1(1), a__f_1(1), c'_1(2), f_1(2)
• 2 to 9 labelled c'_1(1)
• 2 to 13 labelled c'_1(2)
• 4 to 4 labelled #_1(0)
• 7 to 8 labelled g_1(0)
• 7 to 4 labelled g_1(1)
• 8 to 4 labelled a__f_1(0), f_1(1), a__f_1(1), f_1(2)
• 9 to 10 labelled g_1(1)
• 9 to 4 labelled g_1(2), g_1(1)
• 10 to 4 labelled a__f_1(1), f_1(2)
• 13 to 14 labelled g_1(2)
• 13 to 4 labelled g_1(3), g_1(1), g_1(2)
• 14 to 4 labelled a__f_1(2), f_1(3), a__f_1(1), f_1(2)