YES Termination proof of rt2-4.trs

Termination of the given RelTRS could be proven:

0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPReductionPairProof (⇔, 49 ms)
↳4 RelADPP
↳5 DAbsisEmptyProof (⇔, 0 ms)
↳6 YES

(0) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

f(g(x)) → x

The relative TRS consists of the following S rules:

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

(1) RelTRStoRelADPProof (EQUIVALENT transformation)

We upgrade the RelTRS problem to an equivalent Relative ADP Problem [IJCAR24].

(2) Obligation:

Relative ADP Problem with
absolute ADPs:

f(g(x)) → x

and relative ADPs:

a → h(g(F(A)))

(3) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Absolute ADPs:


f(g(x)) → x


The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(A) = 0   
POL(F(x1)) = x1   
POL(a) = 0   
POL(f(x1)) = x1   
POL(g(x1)) = 1 + x1   
POL(h(x1)) = 0   

(4) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

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

(5) DAbsisEmptyProof (EQUIVALENT transformation)

The RDT Problem has an empty P_abs. Hence, no infinite chain exists.

(6) YES