YES Termination proof of rt3-4.trs

Termination of the given RelTRS could be proven:

0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPDepGraphProof (⇔, 0 ms)
↳4 RelADPP
↳5 RelADPReductionPairProof (⇔, 47 ms)
↳6 RelADPP
↳7 RelADPReductionPairProof (⇔, 0 ms)
↳8 RelADPP
↳9 DAbsisEmptyProof (⇔, 0 ms)
↳10 YES

(0) Obligation:

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

f(a, g(y), z) → f(b, g(y), g(y))
f(b, g(y), z) → f(a, y, z)
a → b

The relative TRS consists of the following S rules:

f(x, y, z) → f(x, y, g(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(a, g(y), z) → F(b, g(y), g(y))
f(b, g(y), z) → F(a, y, z)
f(b, g(y), z) → f(A, y, z)
a → b

and relative ADPs:

f(x, y, z) → F(x, y, g(z))

(3) RelADPDepGraphProof (EQUIVALENT transformation)

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

(4) Obligation:

Relative ADP Problem with
absolute ADPs:

f(a, g(y), z) → F(b, g(y), g(y))
f(b, g(y), z) → F(a, y, z)
a → b
f(b, g(y), z) → f(a, y, z)

and relative ADPs:

f(x, y, z) → F(x, y, g(z))

(5) 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(b, g(y), z) → F(a, y, z)
a → b
f(b, g(y), z) → f(a, y, z)


The remaining rules can at least be oriented weakly:
Absolute ADPs:

f(a, g(y), z) → F(b, g(y), g(y))

Relative ADPs:

f(x, y, z) → F(x, y, g(z))


Ordered with Polynomial interpretation [POLO]:

POL(A) = 2   
POL(F(x1, x2, x3)) = 2 + 3·x1 + 2·x2   
POL(a) = 2   
POL(b) = 2   
POL(f(x1, x2, x3)) = x2   
POL(g(x1)) = 1 + 2·x1   

(6) Obligation:

Relative ADP Problem with
absolute ADPs:

f(a, g(y), z) → F(b, g(y), g(y))

and relative ADPs:

a → b
f(x, y, z) → F(x, y, g(z))
f(b, g(y), z) → f(a, y, z)

(7) 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(a, g(y), z) → F(b, g(y), g(y))

Relative ADPs:

a → b
f(b, g(y), z) → f(a, y, z)


The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(A) = 3   
POL(F(x1, x2, x3)) = 2 + 2·x1 + 2·x2   
POL(a) = 3   
POL(b) = 0   
POL(f(x1, x2, x3)) = x2   
POL(g(x1)) = 1 + 3·x1   

(8) Obligation:

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

a → b
f(x, y, z) → F(x, y, g(z))
f(a, g(y), z) → f(b, g(y), g(y))
f(b, g(y), z) → f(a, y, z)

(9) DAbsisEmptyProof (EQUIVALENT transformation)

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

(10) YES