YES Termination proof of AProVE_24_divMinusExchange.ari

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 (⇔, 46 ms)
        ↳7 RelADPP
        ↳8 DAbsisEmptyProof (⇔, 0 ms)
        ↳9 YES
    ↳10 RelADPP
        ↳11 RelADPReductionPairProof (⇔, 51 ms)
        ↳12 RelADPP
        ↳13 DAbsisEmptyProof (⇔, 0 ms)
        ↳14 YES

(0) Obligation:

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

minus1(x, 0) → x
minus1(s(x), s(y)) → minus1(x, y)
div1(0, s(y)) → 0
div1(s(x), s(y)) → s(div1(minus1(x, y), s(y)))
minus2(0, x) → x
minus2(s(x), s(y)) → minus2(x, y)
div2(s(y), 0) → 0
div2(s(x), s(y)) → s(div2(s(x), minus2(x, y)))

The relative TRS consists of the following S rules:

minus2(x, y) → minus1(y, x)
div2(x, y) → div1(y, x)
minus1(x, y) → minus2(y, x)
div1(x, y) → div2(y, x)

(1) RelTRStoRelADPProof (EQUIVALENT transformation)

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

(2) Obligation:

Relative ADP Problem with
absolute ADPs:

minus1(x, 0) → x
minus1(s(x), s(y)) → MINUS1(x, y)
div1(0, s(y)) → 0
div1(s(x), s(y)) → s(DIV1(minus1(x, y), s(y)))
div1(s(x), s(y)) → s(div1(MINUS1(x, y), s(y)))
minus2(0, x) → x
minus2(s(x), s(y)) → MINUS2(x, y)
div2(s(y), 0) → 0
div2(s(x), s(y)) → s(DIV2(s(x), minus2(x, y)))
div2(s(x), s(y)) → s(div2(s(x), MINUS2(x, y)))

and relative ADPs:

minus2(x, y) → MINUS1(y, x)
div2(x, y) → DIV1(y, x)
minus1(x, y) → MINUS2(y, x)
div1(x, y) → DIV2(y, x)

(3) RelADPDepGraphProof (EQUIVALENT transformation)

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

(4) Complex Obligation (AND)

(5) Obligation:

Relative ADP Problem with
absolute ADPs:

minus1(s(x), s(y)) → MINUS1(x, y)
minus2(s(x), s(y)) → MINUS2(x, y)

and relative ADPs:

div2(s(y), 0) → 0
minus1(x, 0) → x
div2(x, y) → div1(y, x)
minus2(x, y) → MINUS1(y, x)
div1(0, s(y)) → 0
minus1(x, y) → MINUS2(y, x)
minus2(0, x) → x
div1(s(x), s(y)) → s(div1(minus1(x, y), s(y)))
div2(s(x), s(y)) → s(div2(s(x), minus2(x, y)))
div1(x, y) → div2(y, x)

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


minus1(s(x), s(y)) → MINUS1(x, y)
minus2(s(x), s(y)) → MINUS2(x, y)

Relative ADPs:

div2(s(y), 0) → 0
minus1(x, 0) → x
div2(x, y) → div1(y, x)
div1(0, s(y)) → 0
minus2(0, x) → x
div1(s(x), s(y)) → s(div1(minus1(x, y), s(y)))
div2(s(x), s(y)) → s(div2(s(x), minus2(x, y)))
div1(x, y) → div2(y, x)


The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(0) = 0   
POL(DIV1(x1, x2)) = 2   
POL(DIV2(x1, x2)) = 2   
POL(MINUS1(x1, x2)) = x1   
POL(MINUS2(x1, x2)) = x2   
POL(div1(x1, x2)) = x1 + 2·x2   
POL(div2(x1, x2)) = 2·x1 + x2   
POL(minus1(x1, x2)) = x1   
POL(minus2(x1, x2)) = x2   
POL(s(x1)) = 3 + x1   

(7) Obligation:

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

div2(s(y), 0) → 0
minus1(x, 0) → x
div2(x, y) → div1(y, x)
minus2(x, y) → MINUS1(y, x)
div1(0, s(y)) → 0
minus1(x, y) → MINUS2(y, x)
minus1(s(x), s(y)) → minus1(x, y)
minus2(s(x), s(y)) → minus2(x, y)
minus2(0, x) → x
div1(s(x), s(y)) → s(div1(minus1(x, y), s(y)))
div2(s(x), s(y)) → s(div2(s(x), minus2(x, y)))
div1(x, y) → div2(y, x)

(8) DAbsisEmptyProof (EQUIVALENT transformation)

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

(9) YES

(10) Obligation:

Relative ADP Problem with
absolute ADPs:

div1(s(x), s(y)) → s(DIV1(minus1(x, y), s(y)))
div2(s(x), s(y)) → s(DIV2(s(x), minus2(x, y)))

and relative ADPs:

div2(x, y) → DIV1(y, x)
div2(s(y), 0) → 0
minus2(x, y) → minus1(y, x)
minus1(x, 0) → x
div1(0, s(y)) → 0
minus1(s(x), s(y)) → minus1(x, y)
minus2(0, x) → x
minus2(s(x), s(y)) → minus2(x, y)
minus1(x, y) → minus2(y, x)
div1(x, y) → DIV2(y, x)
div1(s(x), s(y)) → s(div1(minus1(x, y), s(y)))
div2(s(x), s(y)) → s(div2(s(x), minus2(x, y)))

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


div1(s(x), s(y)) → s(DIV1(minus1(x, y), s(y)))
div2(s(x), s(y)) → s(DIV2(s(x), minus2(x, y)))

Relative ADPs:

div2(s(y), 0) → 0
minus2(x, y) → minus1(y, x)
minus1(x, 0) → x
div1(0, s(y)) → 0
minus1(s(x), s(y)) → minus1(x, y)
minus2(0, x) → x
minus2(s(x), s(y)) → minus2(x, y)
minus1(x, y) → minus2(y, x)
div1(s(x), s(y)) → s(div1(minus1(x, y), s(y)))
div2(s(x), s(y)) → s(div2(s(x), minus2(x, y)))


The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(0) = 0   
POL(DIV1(x1, x2)) = 3 + 2·x1   
POL(DIV2(x1, x2)) = 3 + 2·x2   
POL(MINUS1(x1, x2)) = 2   
POL(MINUS2(x1, x2)) = 2   
POL(div1(x1, x2)) = x1   
POL(div2(x1, x2)) = x2   
POL(minus1(x1, x2)) = x1   
POL(minus2(x1, x2)) = x2   
POL(s(x1)) = 3 + 2·x1   

(12) Obligation:

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

div2(x, y) → DIV1(y, x)
div2(s(y), 0) → 0
minus2(x, y) → minus1(y, x)
minus1(x, 0) → x
div1(0, s(y)) → 0
minus1(s(x), s(y)) → minus1(x, y)
minus2(0, x) → x
minus2(s(x), s(y)) → minus2(x, y)
minus1(x, y) → minus2(y, x)
div1(x, y) → DIV2(y, x)
div1(s(x), s(y)) → s(div1(minus1(x, y), s(y)))
div2(s(x), s(y)) → s(div2(s(x), minus2(x, y)))

(13) DAbsisEmptyProof (EQUIVALENT transformation)

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

(14) YES