YES Termination proof of rt3-2.trs

Termination of the given RelTRS could be proven:

0 RelTRS
↳1 RelTRStoRelADPProof (⇔, 0 ms)
↳2 RelADPP
↳3 RelADPReductionPairProof (⇔, 56 ms)
↳4 RelADPP
↳5 RelADPRuleRemovalProof (⇔, 0 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:

p(0, y) → y
p(s(x), y) → s(p(x, y))

The relative TRS consists of the following S rules:

p(x, y) → p(x, s(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:

p(0, y) → y
p(s(x), y) → s(P(x, y))

and relative ADPs:

p(x, y) → P(x, s(y))

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


p(0, y) → y


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

p(s(x), y) → s(P(x, y))

Relative ADPs:

p(x, y) → P(x, s(y))


Ordered with Polynomial interpretation [POLO]:

POL(0) = 1   
POL(P(x1, x2)) = x1   
POL(p(x1, x2)) = x2   
POL(s(x1)) = x1   

(4) Obligation:

Relative ADP Problem with
absolute ADPs:

p(s(x), y) → s(P(x, y))

and relative ADPs:

p(0, y) → y
p(x, y) → P(x, s(y))

(5) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:


p(0, y) → y

c:

p(s(x), y) → s(P(x, y))

p(x, y) → P(x, s(y))

Ordered with Polynomial interpretation [POLO]:

POL(0) = 1   
POL(P(x1, x2)) = 2·x1 + x2   
POL(p(x1, x2)) = 1 + 2·x1 + x2   
POL(s(x1)) = x1   

(6) Obligation:

Relative ADP Problem with
absolute ADPs:

p(s(x), y) → s(P(x, y))

and relative ADPs:

p(x, y) → P(x, s(y))

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


p(s(x), y) → s(P(x, y))


The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(P(x1, x2)) = 3·x1   
POL(p(x1, x2)) = 2 + 2·x1   
POL(s(x1)) = 2 + x1   

(8) Obligation:

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

p(s(x), y) → s(p(x, y))
p(x, y) → P(x, s(y))

(9) DAbsisEmptyProof (EQUIVALENT transformation)

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

(10) YES