YES Termination proof of AProVE_24_shuffle_a2.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 RelADPDerelatifyingProof (⇔, 0 ms)
        ↳7 QDP
        ↳8 MRRProof (⇔, 0 ms)
        ↳9 QDP
        ↳10 PisEmptyProof (⇔, 0 ms)
        ↳11 YES
    ↳12 RelADPP
        ↳13 RelADPDerelatifyingProof (⇔, 0 ms)
        ↳14 QDP
        ↳15 MRRProof (⇔, 14 ms)
        ↳16 QDP
        ↳17 PisEmptyProof (⇔, 0 ms)
        ↳18 YES
    ↳19 RelADPP
        ↳20 RelADPReductionPairProof (⇔, 47 ms)
        ↳21 RelADPP
        ↳22 DAbsisEmptyProof (⇔, 0 ms)
        ↳23 YES
    ↳24 RelADPP
        ↳25 RelADPReductionPairProof (⇔, 51 ms)
        ↳26 RelADPP
        ↳27 DAbsisEmptyProof (⇔, 0 ms)
        ↳28 YES
    ↳29 RelADPP
        ↳30 RelADPReductionPairProof (⇔, 53 ms)
        ↳31 RelADPP
        ↳32 DAbsisEmptyProof (⇔, 0 ms)
        ↳33 YES
    ↳34 RelADPP
        ↳35 RelADPReductionPairProof (⇔, 49 ms)
        ↳36 RelADPP
        ↳37 DAbsisEmptyProof (⇔, 0 ms)
        ↳38 YES

(0) Obligation:

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

app(nil, y) → y
app(cons(n, x), y) → cons(n, app(x, y))
reverse(nil) → nil
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
shuffle(nil) → nil
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))

The relative TRS consists of the following S rules:

shuffle(cons(x, xs)) → shuffle(consSwap(x, xs))
consSwap(x, xs) → cons(x, xs)
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))

(1) RelTRStoRelADPProof (EQUIVALENT transformation)

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

(2) Obligation:

Relative ADP Problem with
absolute ADPs:

app(nil, y) → y
app(cons(n, x), y) → cons(n, APP(x, y))
reverse(nil) → nil
reverse(cons(n, x)) → APP(reverse(x), cons(n, nil))
reverse(cons(n, x)) → app(REVERSE(x), cons(n, nil))
shuffle(nil) → nil
shuffle(cons(n, x)) → cons(n, SHUFFLE(reverse(x)))
shuffle(cons(n, x)) → cons(n, shuffle(REVERSE(x)))

and relative ADPs:

shuffle(cons(x, xs)) → SHUFFLE(CONSSWAP(x, xs))
consSwap(x, xs) → cons(x, xs)
consSwap(x, cons(y, xs)) → cons(y, CONSSWAP(x, xs))

(3) RelADPDepGraphProof (EQUIVALENT transformation)

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

(4) Complex Obligation (AND)

(5) Obligation:

Relative ADP Problem with
absolute ADPs:

app(cons(n, x), y) → cons(n, APP(x, y))

and relative ADPs:

shuffle(cons(x, xs)) → shuffle(consSwap(x, xs))
reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
shuffle(nil) → nil

(6) RelADPDerelatifyingProof (EQUIVALENT transformation)

We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP(cons(n, x), y) → APP(x, y)

The TRS R consists of the following rules:

shuffle(cons(x, xs)) → shuffle(consSwap(x, xs))
reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
shuffle(nil) → nil

Q is empty.
We have to consider all (P,Q,R)-chains.

(8) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

APP(cons(n, x), y) → APP(x, y)

Strictly oriented rules of the TRS R:

shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
shuffle(nil) → nil

Used ordering: Polynomial interpretation [POLO]:

POL(APP(x1, x2)) = x1 + x2   
POL(app(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = 1 + x1 + x2   
POL(consSwap(x1, x2)) = x1 + 2·x2   
POL(nil) = 0   
POL(reverse(x1)) = x1   
POL(shuffle(x1)) = 1 + 2·x1   
POL(xs) = 1   

(9) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

shuffle(cons(x, xs)) → shuffle(consSwap(x, xs))
reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y

Q is empty.
We have to consider all (P,Q,R)-chains.

(10) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(11) YES

(12) Obligation:

Relative ADP Problem with
absolute ADPs:

reverse(cons(n, x)) → app(REVERSE(x), cons(n, nil))

and relative ADPs:

shuffle(cons(x, xs)) → shuffle(consSwap(x, xs))
reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
shuffle(nil) → nil

(13) RelADPDerelatifyingProof (EQUIVALENT transformation)

We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REVERSE(cons(n, x)) → REVERSE(x)

The TRS R consists of the following rules:

shuffle(cons(x, xs)) → shuffle(consSwap(x, xs))
reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
shuffle(nil) → nil

Q is empty.
We have to consider all (P,Q,R)-chains.

(15) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

REVERSE(cons(n, x)) → REVERSE(x)

Strictly oriented rules of the TRS R:

shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
shuffle(nil) → nil

Used ordering: Polynomial interpretation [POLO]:

POL(REVERSE(x1)) = x1   
POL(app(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = 1 + x1 + x2   
POL(consSwap(x1, x2)) = x1 + 2·x2   
POL(nil) = 0   
POL(reverse(x1)) = x1   
POL(shuffle(x1)) = 1 + 2·x1   
POL(xs) = 1   

(16) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

shuffle(cons(x, xs)) → shuffle(consSwap(x, xs))
reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y

Q is empty.
We have to consider all (P,Q,R)-chains.

(17) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(18) YES

(19) Obligation:

Relative ADP Problem with
absolute ADPs:

shuffle(cons(n, x)) → cons(n, SHUFFLE(reverse(x)))

and relative ADPs:

reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y
shuffle(cons(x, xs)) → SHUFFLE(CONSSWAP(x, xs))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
shuffle(nil) → nil

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


shuffle(cons(n, x)) → cons(n, SHUFFLE(reverse(x)))

Relative ADPs:

reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
shuffle(nil) → nil


The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(APP(x1, x2)) = x1   
POL(CONSSWAP(x1, x2)) = 0   
POL(REVERSE(x1)) = x12   
POL(SHUFFLE(x1)) = 2 + x1   
POL(app(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = 3 + x2   
POL(consSwap(x1, x2)) = 3 + x2   
POL(nil) = 0   
POL(reverse(x1)) = x1   
POL(shuffle(x1)) = 1 + 2·x1   
POL(xs) = 2   

(21) Obligation:

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

reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y
shuffle(cons(x, xs)) → SHUFFLE(CONSSWAP(x, xs))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
shuffle(nil) → nil

(22) DAbsisEmptyProof (EQUIVALENT transformation)

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

(23) YES

(24) Obligation:

Relative ADP Problem with
absolute ADPs:

shuffle(cons(n, x)) → cons(n, SHUFFLE(reverse(x)))

and relative ADPs:

reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y
shuffle(cons(x, xs)) → SHUFFLE(CONSSWAP(x, xs))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
shuffle(nil) → nil

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


shuffle(cons(n, x)) → cons(n, SHUFFLE(reverse(x)))

Relative ADPs:

reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
shuffle(nil) → nil


The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(APP(x1, x2)) = x1   
POL(CONSSWAP(x1, x2)) = 0   
POL(REVERSE(x1)) = x12   
POL(SHUFFLE(x1)) = 2 + x1   
POL(app(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = 3 + x2   
POL(consSwap(x1, x2)) = 3 + x2   
POL(nil) = 0   
POL(reverse(x1)) = x1   
POL(shuffle(x1)) = 1 + 2·x1   
POL(xs) = 2   

(26) Obligation:

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

reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y
shuffle(cons(x, xs)) → SHUFFLE(CONSSWAP(x, xs))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
shuffle(nil) → nil

(27) DAbsisEmptyProof (EQUIVALENT transformation)

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

(28) YES

(29) Obligation:

Relative ADP Problem with
absolute ADPs:

shuffle(cons(n, x)) → cons(n, shuffle(REVERSE(x)))

and relative ADPs:

reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y
shuffle(cons(x, xs)) → SHUFFLE(CONSSWAP(x, xs))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
shuffle(nil) → nil

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


shuffle(cons(n, x)) → cons(n, shuffle(REVERSE(x)))

Relative ADPs:

reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
shuffle(nil) → nil


The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(APP(x1, x2)) = 2·x1·x2   
POL(CONSSWAP(x1, x2)) = 0   
POL(REVERSE(x1)) = 2·x1   
POL(SHUFFLE(x1)) = 2·x1   
POL(app(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = 3 + x2   
POL(consSwap(x1, x2)) = 1 + 2·x2   
POL(nil) = 0   
POL(reverse(x1)) = x1   
POL(shuffle(x1)) = x1   
POL(xs) = 2   

(31) Obligation:

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

reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y
shuffle(cons(x, xs)) → SHUFFLE(CONSSWAP(x, xs))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
shuffle(nil) → nil

(32) DAbsisEmptyProof (EQUIVALENT transformation)

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

(33) YES

(34) Obligation:

Relative ADP Problem with
absolute ADPs:

shuffle(nil) → nil

and relative ADPs:

reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y
shuffle(cons(x, xs)) → SHUFFLE(CONSSWAP(x, xs))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))

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


shuffle(nil) → nil

Relative ADPs:

reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))


The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(APP(x1, x2)) = 2 + 2·x2   
POL(CONSSWAP(x1, x2)) = 0   
POL(REVERSE(x1)) = 2 + 2·x12   
POL(SHUFFLE(x1)) = 1 + 3·x1   
POL(app(x1, x2)) = x1 + x2   
POL(cons(x1, x2)) = 3 + 3·x1 + x2   
POL(consSwap(x1, x2)) = 3 + 3·x1 + x2   
POL(nil) = 0   
POL(reverse(x1)) = x1   
POL(shuffle(x1)) = 2 + 3·x1   
POL(xs) = 3   

(36) Obligation:

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

reverse(nil) → nil
consSwap(x, xs) → cons(x, xs)
app(cons(n, x), y) → cons(n, app(x, y))
shuffle(cons(n, x)) → cons(n, shuffle(reverse(x)))
reverse(cons(n, x)) → app(reverse(x), cons(n, nil))
app(nil, y) → y
shuffle(cons(x, xs)) → SHUFFLE(CONSSWAP(x, xs))
consSwap(x, cons(y, xs)) → cons(y, consSwap(x, xs))
shuffle(nil) → nil

(37) DAbsisEmptyProof (EQUIVALENT transformation)

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

(38) YES