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(g(f(g(f(X)))))
f(g(f(X))) → f(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(g(f(g(f(X)))))
f(g(f(X))) → f(g(X))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

1210701, 1210702, 1210703, 1210704, 1210705, 1210707, 1210706, 1210708, 1210711, 1210712, 1210710, 1210709, 1210713, 1210714, 1210715

Node 1210701 is start node and node 1210702 is final node.

Those nodes are connect through the following edges:

  • 1210701 to 1210703 labelled f_1(0)
  • 1210701 to 1210704 labelled f_1(0)
  • 1210701 to 1210713 labelled f_1(1)
  • 1210701 to 1210708 labelled f_1(1)
  • 1210702 to 1210702 labelled #_1(0)
  • 1210703 to 1210702 labelled g_1(0)
  • 1210704 to 1210705 labelled g_1(0)
  • 1210705 to 1210706 labelled f_1(0)
  • 1210705 to 1210708 labelled f_1(1)
  • 1210705 to 1210713 labelled f_1(1)
  • 1210707 to 1210702 labelled f_1(0)
  • 1210707 to 1210708 labelled f_1(1)
  • 1210707 to 1210709 labelled f_1(1)
  • 1210707 to 1210715 labelled f_1(2)
  • 1210707 to 1210714 labelled f_1(2)
  • 1210706 to 1210707 labelled g_1(0)
  • 1210708 to 1210702 labelled g_1(1)
  • 1210708 to 1210709 labelled g_1(1)
  • 1210708 to 1210715 labelled g_1(1)
  • 1210708 to 1210714 labelled g_1(1)
  • 1210711 to 1210712 labelled g_1(1)
  • 1210712 to 1210702 labelled f_1(1)
  • 1210712 to 1210708 labelled f_1(1)
  • 1210712 to 1210709 labelled f_1(1)
  • 1210712 to 1210715 labelled f_1(2)
  • 1210712 to 1210714 labelled f_1(2)
  • 1210710 to 1210711 labelled f_1(1)
  • 1210710 to 1210714 labelled f_1(2)
  • 1210710 to 1210708 labelled f_1(1)
  • 1210710 to 1210715 labelled f_1(2)
  • 1210709 to 1210710 labelled g_1(1)
  • 1210713 to 1210706 labelled g_1(1)
  • 1210713 to 1210708 labelled g_1(1)
  • 1210713 to 1210713 labelled g_1(1)
  • 1210714 to 1210702 labelled g_1(2)
  • 1210714 to 1210708 labelled g_1(2)
  • 1210714 to 1210709 labelled g_1(2)
  • 1210714 to 1210715 labelled g_1(2)
  • 1210715 to 1210711 labelled g_1(2)
  • 1210715 to 1210714 labelled g_1(2)

(2) TRUE