YES
0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPReductionPairProof (⇔, 0 ms)
↳4 RelADPP
↳5 DAbsisEmptyProof (⇔, 0 ms)
↳6 YES
f(g(x)) → x
a → h(g(f(a)))
We upgrade the RelTRS problem to an equivalent Relative ADP Problem [IJCAR24].
f(g(x)) → x
a → h(g(F(A)))
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
POL(A) = 0
POL(F(x1)) = x1
POL(a) = 0
POL(f(x1)) = x1
POL(g(x1)) = 1 + x1
POL(h(x1)) = 0
a → h(g(F(A)))
f(g(x)) → x