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:

f(f(x)) → f(c(f(x)))
f(f(x)) → f(d(f(x)))
g(c(x)) → x
g(d(x)) → x
g(c(h(0))) → g(d(1))
g(c(1)) → g(d(h(0)))
g(h(x)) → g(x)

Q is empty.

(1) RFCMatchBoundsTRSProof (EQUIVALENT transformation)

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

f(f(x)) → f(c(f(x)))
f(f(x)) → f(d(f(x)))
g(c(x)) → x
g(d(x)) → x
g(c(h(0))) → g(d(1))
g(c(1)) → g(d(h(0)))
g(h(x)) → g(x)

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

1355281, 1355282, 1355283, 1355284, 1355285, 1355286, 1355287, 1355288, 1355289, 1355291, 1355290, 1355293, 1355292, 1355295, 1355296, 1355294

Node 1355281 is start node and node 1355282 is final node.

Those nodes are connect through the following edges:

  • 1355281 to 1355282 labelled f_1(0), h_1(0), 1(0), c_1(0), g_1(0), 0(0), d_1(0), f_1(1), h_1(1), 1(1), c_1(1), g_1(1), 0(1), d_1(1), 1(2)
  • 1355281 to 1355283 labelled g_1(0)
  • 1355281 to 1355286 labelled f_1(0)
  • 1355281 to 1355288 labelled f_1(0)
  • 1355281 to 1355294 labelled g_1(1)
  • 1355281 to 1355290 labelled f_1(1)
  • 1355281 to 1355292 labelled f_1(1)
  • 1355281 to 1355285 labelled h_1(1)
  • 1355281 to 1355296 labelled h_1(2)
  • 1355282 to 1355282 labelled #_1(0)
  • 1355283 to 1355284 labelled d_1(0)
  • 1355284 to 1355285 labelled h_1(0)
  • 1355284 to 1355282 labelled 1(0)
  • 1355285 to 1355282 labelled 0(0)
  • 1355286 to 1355287 labelled c_1(0)
  • 1355287 to 1355282 labelled f_1(0)
  • 1355287 to 1355290 labelled f_1(1)
  • 1355287 to 1355292 labelled f_1(1)
  • 1355288 to 1355289 labelled d_1(0)
  • 1355289 to 1355282 labelled f_1(0)
  • 1355289 to 1355290 labelled f_1(1)
  • 1355289 to 1355292 labelled f_1(1)
  • 1355291 to 1355282 labelled f_1(1)
  • 1355291 to 1355290 labelled f_1(1)
  • 1355291 to 1355292 labelled f_1(1)
  • 1355290 to 1355291 labelled c_1(1)
  • 1355293 to 1355282 labelled f_1(1)
  • 1355293 to 1355290 labelled f_1(1)
  • 1355293 to 1355292 labelled f_1(1)
  • 1355292 to 1355293 labelled d_1(1)
  • 1355295 to 1355296 labelled h_1(1)
  • 1355295 to 1355282 labelled 1(1)
  • 1355296 to 1355282 labelled 0(1)
  • 1355294 to 1355295 labelled d_1(1)

(2) TRUE