YES Termination w.r.t. Q proof of Transformed_CSR_04_Ex1_Zan97_GM.ari

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

0 QTRS
↳1 RFCMatchBoundsTRSProof (⇔, 0 ms)
↳2 YES

(0) Obligation:

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

a__g(X) → a__h(X)
a__c → d
a__h(d) → a__g(c)
mark(g(X)) → a__g(X)
mark(h(X)) → a__h(X)
mark(c) → a__c
mark(d) → d
a__g(X) → g(X)
a__h(X) → h(X)
a__c → c

Q is empty.

(1) RFCMatchBoundsTRSProof (EQUIVALENT transformation)

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

a__g(X) → a__h(X)
a__c → d
a__h(d) → a__g(c)
mark(g(X)) → a__g(X)
mark(h(X)) → a__h(X)
mark(c) → a__c
mark(d) → d
a__g(X) → g(X)
a__h(X) → h(X)
a__c → c

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

1, 3, 6, 7

Node 1 is start node and node 3 is final node.

Those nodes are connected through the following edges:

  • 1 to 3 labelled a__h_1(0), d(0), a__g_1(0), a__c(0), g_1(0), h_1(0), c(0), h_1(1), a__h_1(1), g_1(1), d(1), c(1), h_1(2)
  • 1 to 6 labelled a__g_1(0), a__h_1(1), g_1(1), h_1(2)
  • 1 to 1 labelled a__g_1(1), a__h_1(2), g_1(2), h_1(3)
  • 1 to 7 labelled a__g_1(2), a__h_1(3), g_1(3), h_1(4)
  • 3 to 3 labelled #_1(0)
  • 6 to 3 labelled c(0)
  • 7 to 3 labelled c(2)

(2) YES