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(a) → g(h(a))
h(g(x)) → g(h(f(x)))
k(x, h(x), a) → h(x)
k(f(x), y, x) → f(x)

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(a) = 0   
POL(f(x₁)) = x₁   
POL(g(x₁)) = x₁   
POL(h(x₁)) = x₁   
POL(k(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

k(x, h(x), a) → h(x)
k(f(x), y, x) → f(x)

(2) Obligation:

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

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

Q is empty.

(3) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(4) Obligation:

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

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

The set Q consists of the following terms:

f(a)
h(g(x0))

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(6) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(a) → H(a)
H(g(x)) → H(f(x))
H(g(x)) → F(x)

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

f(a)
h(g(x0))

We have to consider all minimal (P,Q,R)-chains.

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(8) Obligation:

Q DP problem:
The TRS P consists of the following rules:

H(g(x)) → H(f(x))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

f(a)
h(g(x0))

We have to consider all minimal (P,Q,R)-chains.

(9) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

H(g(x)) → H(f(x))

The TRS R consists of the following rules:

f(a) → g(h(a))

The set Q consists of the following terms:

f(a)
h(g(x0))

We have to consider all minimal (P,Q,R)-chains.

(11) RFCMatchBoundsDPProof (EQUIVALENT transformation)

Finiteness of the DP problem can be shown by a matchbound of 1.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:

H(g(x)) → H(f(x))

To find matches we regarded all rules of R and P:

f(a) → g(h(a))
H(g(x)) → H(f(x))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

2623718, 2623719, 2623720, 2623721, 2623722, 2623723

Node 2623718 is start node and node 2623719 is final node.

Those nodes are connect through the following edges:

• 2623718 to 2623720 labelled H_1(0)
• 2623718 to 2623723 labelled H_1(1)
• 2623719 to 2623719 labelled #_1(0)
• 2623720 to 2623719 labelled f_1(0)
• 2623720 to 2623721 labelled g_1(1)
• 2623721 to 2623722 labelled h_1(1)
• 2623722 to 2623719 labelled a(1)
• 2623723 to 2623721 labelled f_1(1)

(12) TRUE