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

(0) Obligation:

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

f(g(X)) → g(f(f(X)))
f(h(X)) → h(g(X))

Q is empty.

(1) QTRS Reverse (EQUIVALENT transformation)

We applied the QTRS Reverse Processor [REVERSE].

(2) Obligation:

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

g(f(x)) → f(f(g(x)))
h(f(x)) → g(h(x))

Q is empty.

(3) RFCMatchBoundsTRSProof (EQUIVALENT transformation)

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

g(f(x)) → f(f(g(x)))
h(f(x)) → g(h(x))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

1210314, 1210315, 1210317, 1210316, 1210318, 1210319, 1210320, 1210321

Node 1210314 is start node and node 1210315 is final node.

Those nodes are connect through the following edges:

• 1210314 to 1210316 labelled f_1(0)
• 1210314 to 1210318 labelled g_1(0)
• 1210315 to 1210315 labelled #_1(0)
• 1210317 to 1210315 labelled g_1(0)
• 1210317 to 1210320 labelled f_1(1)
• 1210316 to 1210317 labelled f_1(0)
• 1210318 to 1210315 labelled h_1(0)
• 1210318 to 1210319 labelled g_1(1)
• 1210319 to 1210315 labelled h_1(1)
• 1210319 to 1210319 labelled g_1(1)
• 1210320 to 1210321 labelled f_1(1)
• 1210321 to 1210315 labelled g_1(1)
• 1210321 to 1210320 labelled f_1(1)

(4) TRUE