(1) 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__f(f(X)) → a__c(f(g(f(X))))
a__c(X) → d(X)
a__h(X) → a__c(d(X))
mark(f(X)) → a__f(mark(X))
mark(c(X)) → a__c(X)
mark(h(X)) → a__h(mark(X))
mark(g(X)) → g(X)
mark(d(X)) → d(X)
a__f(X) → f(X)
a__c(X) → c(X)
a__h(X) → h(X)
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
488778, 488779, 488780, 488783, 488782, 488781, 488784, 488785, 488786, 488788, 488789, 488787, 488792, 488790, 488791
Node 488778 is start node and node 488779 is final node.
Those nodes are connect through the following edges:
- 488778 to 488780 labelled a__h_1(0), a__f_1(0), f_1(1), h_1(1)
- 488778 to 488779 labelled h_1(0), c_1(0), d_1(0), g_1(0), a__c_1(0), f_1(0), c_1(1), d_1(1)
- 488778 to 488778 labelled a__c_1(0), c_1(1), d_1(1)
- 488778 to 488781 labelled a__c_1(0), c_1(1), d_1(1)
- 488778 to 488784 labelled a__c_1(1), c_1(2), d_1(2)
- 488778 to 488787 labelled a__c_1(1), c_1(2), d_1(2)
- 488779 to 488779 labelled #_1(0)
- 488780 to 488779 labelled mark_1(0), g_1(1), a__c_1(1), d_1(1), c_1(2), d_1(2)
- 488780 to 488785 labelled a__h_1(1), a__f_1(1), h_1(2), f_1(2)
- 488780 to 488786 labelled a__c_1(2), c_1(3), d_1(3)
- 488780 to 488790 labelled a__c_1(2), c_1(3), d_1(3)
- 488783 to 488779 labelled f_1(0)
- 488782 to 488783 labelled g_1(0)
- 488781 to 488782 labelled f_1(0)
- 488784 to 488780 labelled d_1(1)
- 488785 to 488779 labelled mark_1(1), g_1(1), a__c_1(1), d_1(1), c_1(2), d_1(2)
- 488785 to 488785 labelled a__h_1(1), a__f_1(1), h_1(2), f_1(2)
- 488785 to 488786 labelled a__c_1(2), c_1(3), d_1(3)
- 488785 to 488790 labelled a__c_1(2), c_1(3), d_1(3)
- 488786 to 488785 labelled d_1(2)
- 488788 to 488789 labelled g_1(1)
- 488789 to 488785 labelled f_1(1)
- 488787 to 488788 labelled f_1(1)
- 488792 to 488785 labelled f_1(2)
- 488790 to 488791 labelled f_1(2)
- 488791 to 488792 labelled g_1(2)