YES Termination proof of AProVE_24_depGraph_2.ari

Termination of the given RelTRS could be proven:

0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPDepGraphProof (⇔, 0 ms)
↳4 TRUE

(0) Obligation:

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

f(s(x), s(y), s(z)) → f(g(z, s(x)), h(s(y), z), k(s(z), x, y))

The relative TRS consists of the following S rules:

g(s(x), s(y)) → h(s(s(y)), s(s(x)))
h(s(x), s(y)) → g(s(s(y)), s(s(x)))
k(x, y, z) → f(0, y, z)

(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(s(x), s(y), s(z)) → F(g(z, s(x)), h(s(y), z), k(s(z), x, y))
f(s(x), s(y), s(z)) → f(G(z, s(x)), h(s(y), z), k(s(z), x, y))
f(s(x), s(y), s(z)) → f(g(z, s(x)), H(s(y), z), k(s(z), x, y))
f(s(x), s(y), s(z)) → f(g(z, s(x)), h(s(y), z), K(s(z), x, y))

and relative ADPs:

g(s(x), s(y)) → H(s(s(y)), s(s(x)))
h(s(x), s(y)) → G(s(s(y)), s(s(x)))
k(x, y, z) → F(0, y, z)

(3) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
0 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 0 subproblems.

(4) TRUE