YES Termination proof of rt2-3.trs

Termination of the given RelTRS could be proven:

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

(0) Obligation:

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

R(x, B2) → B2
W(x, B2) → B2

The relative TRS consists of the following S rules:

B1 → W(T, B1)
B1 → R(T, B1)

(1) RelTRStoRelADPProof (EQUIVALENT transformation)

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

(2) Obligation:

Relative ADP Problem with
absolute ADPs:

R(x, B2) → B2
W(x, B2) → B2

and relative ADPs:

B1 → W1(T, B11)
B1 → R1(T, B11)

(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:


R(x, B2) → B2


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

W(x, B2) → B2

Relative ADPs:

B1 → W1(T, B11)
B1 → R1(T, B11)


Ordered with Polynomial interpretation [POLO]:

POL(B1) = 0   
POL(B11) = 0   
POL(B2) = 1   
POL(R(x1, x2)) = x2   
POL(R1(x1, x2)) = x2   
POL(T) = 0   
POL(W(x1, x2)) = x2   
POL(W1(x1, x2)) = 0   

(4) Obligation:

Relative ADP Problem with
absolute ADPs:

W(x, B2) → B2

and relative ADPs:

B1 → W1(T, B11)
B1 → R1(T, B11)
R(x, B2) → B2

(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:


W(x, B2) → B2

Relative ADPs:

R(x, B2) → B2


The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(B1) = 0   
POL(B11) = 0   
POL(B2) = 1   
POL(R(x1, x2)) = x2   
POL(R1(x1, x2)) = 0   
POL(T) = 1   
POL(W(x1, x2)) = x2   
POL(W1(x1, x2)) = x2   

(6) Obligation:

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

B1 → W1(T, B11)
W(x, B2) → B2
B1 → R1(T, B11)
R(x, B2) → B2

(7) DAbsisEmptyProof (EQUIVALENT transformation)

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

(8) YES