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

(0) Obligation:

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

active(f(X)) → mark(g(h(f(X))))
mark(f(X)) → active(f(mark(X)))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(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:

active(f(X)) → mark(g(h(f(X))))
mark(f(X)) → active(f(mark(X)))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(X)) → h(X)

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

2, 3, 12, 13, 14, 15, 16, 17, 18, 19, 23, 24, 25, 30, 31, 32, 33, 34, 35, 36, 37, 42

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

Those nodes are connected through the following edges:

  • 2 to 12 labelled mark_1(0)
  • 2 to 15 labelled active_1(0)
  • 2 to 17 labelled active_1(0)
  • 2 to 3 labelled f_1(0), g_1(0), h_1(0), f_1(1), g_1(1), h_1(1)
  • 2 to 19 labelled active_1(1)
  • 2 to 23 labelled mark_1(1)
  • 2 to 37 labelled active_1(2)
  • 3 to 3 labelled #_1(0)
  • 12 to 13 labelled g_1(0)
  • 13 to 14 labelled h_1(0)
  • 14 to 3 labelled f_1(0), f_1(1)
  • 15 to 16 labelled f_1(0)
  • 15 to 3 labelled g_1(0), g_1(1), f_1(1)
  • 15 to 30 labelled f_1(1)
  • 15 to 15 labelled f_1(1)
  • 15 to 32 labelled f_1(1)
  • 15 to 23 labelled f_1(1)
  • 15 to 34 labelled f_1(1)
  • 15 to 37 labelled f_1(1)
  • 15 to 42 labelled f_1(1)
  • 16 to 3 labelled mark_1(0)
  • 16 to 30 labelled active_1(1)
  • 16 to 15 labelled active_1(1)
  • 16 to 32 labelled active_1(1)
  • 16 to 23 labelled mark_1(1)
  • 16 to 34 labelled mark_1(2)
  • 16 to 37 labelled active_1(2)
  • 16 to 42 labelled active_1(3)
  • 17 to 18 labelled h_1(0)
  • 17 to 3 labelled h_1(1)
  • 17 to 30 labelled h_1(1)
  • 17 to 15 labelled h_1(1)
  • 17 to 32 labelled h_1(1)
  • 17 to 23 labelled h_1(1)
  • 17 to 34 labelled h_1(1)
  • 17 to 37 labelled h_1(1)
  • 17 to 42 labelled h_1(1)
  • 18 to 3 labelled mark_1(0)
  • 18 to 30 labelled active_1(1)
  • 18 to 15 labelled active_1(1)
  • 18 to 32 labelled active_1(1)
  • 18 to 23 labelled mark_1(1)
  • 18 to 34 labelled mark_1(2)
  • 18 to 37 labelled active_1(2)
  • 18 to 42 labelled active_1(3)
  • 19 to 13 labelled g_1(1)
  • 23 to 24 labelled g_1(1)
  • 24 to 25 labelled h_1(1)
  • 25 to 16 labelled f_1(1)
  • 25 to 3 labelled f_1(1)
  • 25 to 30 labelled f_1(2), f_1(1)
  • 25 to 15 labelled f_1(2), f_1(1)
  • 25 to 32 labelled f_1(2), f_1(1)
  • 25 to 23 labelled f_1(2), f_1(1)
  • 25 to 34 labelled f_1(2), f_1(1)
  • 25 to 37 labelled f_1(2), f_1(1)
  • 25 to 42 labelled f_1(2), f_1(1)
  • 30 to 31 labelled f_1(1)
  • 30 to 3 labelled f_1(2), f_1(1)
  • 30 to 30 labelled f_1(2)
  • 30 to 15 labelled f_1(2)
  • 30 to 32 labelled f_1(2)
  • 30 to 23 labelled f_1(2)
  • 30 to 34 labelled f_1(2)
  • 30 to 37 labelled f_1(2)
  • 30 to 42 labelled f_1(2)
  • 31 to 3 labelled mark_1(1)
  • 31 to 30 labelled active_1(1)
  • 31 to 15 labelled active_1(1)
  • 31 to 32 labelled active_1(1)
  • 31 to 23 labelled mark_1(1)
  • 31 to 34 labelled mark_1(2)
  • 31 to 37 labelled active_1(2)
  • 31 to 42 labelled active_1(3)
  • 32 to 33 labelled h_1(1)
  • 32 to 3 labelled h_1(2), h_1(1)
  • 32 to 30 labelled h_1(2)
  • 32 to 15 labelled h_1(2)
  • 32 to 32 labelled h_1(2)
  • 32 to 23 labelled h_1(2)
  • 32 to 34 labelled h_1(2)
  • 32 to 37 labelled h_1(2)
  • 32 to 42 labelled h_1(2)
  • 33 to 3 labelled mark_1(1)
  • 33 to 30 labelled active_1(1)
  • 33 to 15 labelled active_1(1)
  • 33 to 32 labelled active_1(1)
  • 33 to 23 labelled mark_1(1)
  • 33 to 34 labelled mark_1(2)
  • 33 to 37 labelled active_1(2)
  • 33 to 42 labelled active_1(3)
  • 34 to 35 labelled g_1(2)
  • 35 to 36 labelled h_1(2)
  • 36 to 3 labelled f_1(2), f_1(1)
  • 36 to 31 labelled f_1(2)
  • 36 to 30 labelled f_1(2)
  • 36 to 15 labelled f_1(2)
  • 36 to 32 labelled f_1(2)
  • 36 to 23 labelled f_1(2)
  • 36 to 34 labelled f_1(2), f_1(3)
  • 36 to 37 labelled f_1(2), f_1(3)
  • 36 to 42 labelled f_1(2), f_1(3)
  • 37 to 24 labelled g_1(2)
  • 42 to 35 labelled g_1(3)

(2) YES