Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS
↳1 RFCMatchBoundsTRSProof (⇔)
↳2 TRUE

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

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)

Q is empty.

(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:

2340846, 2340847, 2340848, 2340849, 2340850, 2340851, 2340852, 2340853, 2340854, 2340855, 2340857, 2340856, 2340859, 2340860, 2340858

Node 2340846 is start node and node 2340847 is final node.

Those nodes are connect through the following edges:

  • 2340846 to 2340848 labelled a__h_1(0), a__f_1(0), h_1(1), f_1(1)
  • 2340846 to 2340847 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)
  • 2340846 to 2340846 labelled a__c_1(0), c_1(1), d_1(1)
  • 2340846 to 2340849 labelled a__c_1(0), c_1(1), d_1(1)
  • 2340846 to 2340852 labelled a__c_1(1), c_1(2), d_1(2)
  • 2340846 to 2340855 labelled a__c_1(1), c_1(2), d_1(2)
  • 2340847 to 2340847 labelled #_1(0)
  • 2340848 to 2340847 labelled mark_1(0), g_1(1), a__c_1(1), d_1(1), c_1(2), d_1(2)
  • 2340848 to 2340853 labelled a__h_1(1), a__f_1(1), f_1(2), h_1(2)
  • 2340848 to 2340854 labelled a__c_1(2), c_1(3), d_1(3)
  • 2340848 to 2340858 labelled a__c_1(2), c_1(3), d_1(3)
  • 2340849 to 2340850 labelled f_1(0)
  • 2340850 to 2340851 labelled g_1(0)
  • 2340851 to 2340847 labelled f_1(0)
  • 2340852 to 2340848 labelled d_1(1)
  • 2340853 to 2340847 labelled mark_1(1), g_1(1), a__c_1(1), d_1(1), c_1(2), d_1(2)
  • 2340853 to 2340853 labelled a__h_1(1), a__f_1(1), h_1(2), f_1(2)
  • 2340853 to 2340854 labelled a__c_1(2), c_1(3), d_1(3)
  • 2340853 to 2340858 labelled a__c_1(2), c_1(3), d_1(3)
  • 2340854 to 2340853 labelled d_1(2)
  • 2340855 to 2340856 labelled f_1(1)
  • 2340857 to 2340853 labelled f_1(1)
  • 2340856 to 2340857 labelled g_1(1)
  • 2340859 to 2340860 labelled g_1(2)
  • 2340860 to 2340853 labelled f_1(2)
  • 2340858 to 2340859 labelled f_1(2)

(2) TRUE