YES Termination proof of rt1-4.trs

Termination of the given RelTRS could be proven:

0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPDepGraphProof (⇔, 0 ms)
↳4 AND
    ↳5 RelADPP
        ↳6 RelADPReductionPairProof (⇔, 29 ms)
        ↳7 RelADPP
        ↳8 RelADPReductionPairProof (⇔, 0 ms)
        ↳9 RelADPP
        ↳10 DAbsisEmptyProof (⇔, 0 ms)
        ↳11 YES
    ↳12 RelADPP
        ↳13 RelADPReductionPairProof (⇔, 26 ms)
        ↳14 RelADPP
        ↳15 RelADPReductionPairProof (⇔, 0 ms)
        ↳16 RelADPP
        ↳17 DAbsisEmptyProof (⇔, 0 ms)
        ↳18 YES
    ↳19 RelADPP
        ↳20 RelADPReductionPairProof (⇔, 36 ms)
        ↳21 RelADPP
        ↳22 DAbsisEmptyProof (⇔, 0 ms)
        ↳23 YES

(0) Obligation:

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

f(el(x), y) → f(x, el(y))

The relative TRS consists of the following S rules:

l(el(x)) → el(l(x))
f(x, y) → f(l(x), y)
el(r(x)) → r(el(x))
f(x, y) → f(x, r(y))

(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(el(x), y) → F(x, el(y))
f(el(x), y) → f(x, EL(y))

and relative ADPs:

l(el(x)) → EL(L(x))
f(x, y) → F(L(x), y)
el(r(x)) → r(EL(x))
f(x, y) → F(x, r(y))

(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,
2 Lassos,
Result: This relative DT problem is equivalent to 3 subproblems.

(4) Complex Obligation (AND)

(5) Obligation:

Relative ADP Problem with
absolute ADPs:

f(el(x), y) → f(x, el(y))
f(el(x), y) → F(x, el(y))

and relative ADPs:

f(x, y) → F(x, r(y))
l(el(x)) → el(l(x))
el(r(x)) → r(el(x))
f(x, y) → F(L(x), y)

(6) 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(el(x), y) → f(x, el(y))

Relative ADPs:

l(el(x)) → el(l(x))
el(r(x)) → r(el(x))


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

f(el(x), y) → F(x, el(y))

Relative ADPs:

f(x, y) → F(x, r(y))
f(x, y) → F(L(x), y)


Ordered with Polynomial interpretation [POLO]:

POL(EL(x1)) = 0   
POL(F(x1, x2)) = 1   
POL(L(x1)) = 0   
POL(el(x1)) = 3 + x1   
POL(f(x1, x2)) = 0   
POL(l(x1)) = 3 + x1   
POL(r(x1)) = 0   

(7) Obligation:

Relative ADP Problem with
absolute ADPs:

f(el(x), y) → F(x, el(y))

and relative ADPs:

f(el(x), y) → f(x, el(y))
f(x, y) → F(x, r(y))
l(el(x)) → el(l(x))
el(r(x)) → r(el(x))
f(x, y) → F(L(x), y)

(8) 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(el(x), y) → F(x, el(y))

Relative ADPs:

f(el(x), y) → f(x, el(y))
l(el(x)) → el(l(x))
el(r(x)) → r(el(x))


The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(EL(x1)) = 2 + x12   
POL(F(x1, x2)) = 2 + x1   
POL(L(x1)) = 0   
POL(el(x1)) = 1 + x1   
POL(f(x1, x2)) = 0   
POL(l(x1)) = x1   
POL(r(x1)) = 2   

(9) Obligation:

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

f(el(x), y) → f(x, el(y))
f(x, y) → F(x, r(y))
l(el(x)) → el(l(x))
el(r(x)) → r(el(x))
f(x, y) → F(L(x), y)

(10) DAbsisEmptyProof (EQUIVALENT transformation)

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

(11) YES

(12) Obligation:

Relative ADP Problem with
absolute ADPs:

f(el(x), y) → f(x, el(y))
f(el(x), y) → F(x, el(y))

and relative ADPs:

f(x, y) → F(x, r(y))
l(el(x)) → el(l(x))
el(r(x)) → r(el(x))
f(x, y) → F(L(x), y)

(13) 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(el(x), y) → f(x, el(y))

Relative ADPs:

l(el(x)) → el(l(x))
el(r(x)) → r(el(x))


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

f(el(x), y) → F(x, el(y))

Relative ADPs:

f(x, y) → F(x, r(y))
f(x, y) → F(L(x), y)


Ordered with Polynomial interpretation [POLO]:

POL(EL(x1)) = 0   
POL(F(x1, x2)) = 1   
POL(L(x1)) = 0   
POL(el(x1)) = 3 + x1   
POL(f(x1, x2)) = 0   
POL(l(x1)) = 3 + x1   
POL(r(x1)) = 0   

(14) Obligation:

Relative ADP Problem with
absolute ADPs:

f(el(x), y) → F(x, el(y))

and relative ADPs:

f(el(x), y) → f(x, el(y))
f(x, y) → F(x, r(y))
l(el(x)) → el(l(x))
el(r(x)) → r(el(x))
f(x, y) → F(L(x), y)

(15) 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(el(x), y) → F(x, el(y))

Relative ADPs:

f(el(x), y) → f(x, el(y))
l(el(x)) → el(l(x))
el(r(x)) → r(el(x))


The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(EL(x1)) = 2 + x12   
POL(F(x1, x2)) = 2 + x1   
POL(L(x1)) = 0   
POL(el(x1)) = 1 + x1   
POL(f(x1, x2)) = 0   
POL(l(x1)) = x1   
POL(r(x1)) = 2   

(16) Obligation:

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

f(el(x), y) → f(x, el(y))
f(x, y) → F(x, r(y))
l(el(x)) → el(l(x))
el(r(x)) → r(el(x))
f(x, y) → F(L(x), y)

(17) DAbsisEmptyProof (EQUIVALENT transformation)

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

(18) YES

(19) Obligation:

Relative ADP Problem with
absolute ADPs:

f(el(x), y) → f(x, el(y))
f(el(x), y) → f(x, EL(y))

and relative ADPs:

f(x, y) → F(x, r(y))
l(el(x)) → el(l(x))
el(r(x)) → r(el(x))
f(x, y) → F(L(x), y)

(20) 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(el(x), y) → f(x, el(y))
f(el(x), y) → f(x, EL(y))

Relative ADPs:

l(el(x)) → el(l(x))
el(r(x)) → r(el(x))


The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(EL(x1)) = 3   
POL(F(x1, x2)) = 3 + 3·x1   
POL(L(x1)) = 0   
POL(el(x1)) = 3 + 3·x1   
POL(f(x1, x2)) = 0   
POL(l(x1)) = x1   
POL(r(x1)) = 2   

(21) Obligation:

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

f(el(x), y) → f(x, el(y))
f(x, y) → F(x, r(y))
l(el(x)) → el(l(x))
el(r(x)) → r(el(x))
f(x, y) → F(L(x), y)

(22) DAbsisEmptyProof (EQUIVALENT transformation)

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

(23) YES