Termination proof of AProVE_24_shuffle

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 RelADPCleverAfsProof (⇒, 29 ms)

        ↳7 QDP

        ↳8 MRRProof (⇔, 0 ms)

        ↳9 QDP

        ↳10 PisEmptyProof (⇔, 0 ms)

        ↳11 YES

    ↳12 RelADPP

        ↳13 RelADPCleverAfsProof (⇒, 44 ms)

        ↳14 QDP

        ↳15 MRRProof (⇔, 0 ms)

        ↳16 QDP

        ↳17 PisEmptyProof (⇔, 0 ms)

        ↳18 YES

    ↳19 RelADPP

        ↳20 RelADPReductionPairProof (⇔, 0 ms)

        ↳21 RelADPP

        ↳22 DAbsisEmptyProof (⇔, 0 ms)

        ↳23 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(n, cons(m, x))) → shuffle(cons(m, cons(n, 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:

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(n, cons(m, x))) → SHUFFLE(cons(m, cons(n, x)))

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

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

(6) RelADPCleverAfsProof (SOUND 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.

Furthermore, We use an argument filter [LPAR04].
Filtering:reverse_1 = app_2 = cons_2 = 0 shuffle_1 = APP_2 = 1 nil =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
APP(x1, x2) = x1
cons(x1, x2) = cons(x2)

Recursive path order with status [RPO].
Quasi-Precedence:

trivial

Status:

cons₁: multiset

(7) Obligation:

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

APP(cons(x)) → APP(x)

The TRS R consists of the following rules:

reverse0(nil0) → nil0
shuffle0(cons(cons(x))) → shuffle0(cons(cons(x)))
app0(cons(x), y) → cons(app0(x, y))
shuffle0(cons(x)) → cons(shuffle0(reverse0(x)))
reverse0(cons(x)) → app0(reverse0(x), cons(nil0))
app0(nil0, y) → y
shuffle0(nil0) → nil0

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(x)) → APP(x)

Strictly oriented rules of the TRS R:

shuffle0(cons(x)) → cons(shuffle0(reverse0(x)))
shuffle0(nil0) → nil0

Used ordering: Polynomial interpretation [POLO]:

POL(APP(x₁)) = x₁
POL(app0(x₁, x₂)) = x₁ + x₂
POL(cons(x₁)) = 1 + x₁
POL(nil0) = 0
POL(reverse0(x₁)) = x₁
POL(shuffle0(x₁)) = 2 + 2·x₁

(9) Obligation:

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

reverse0(nil0) → nil0
shuffle0(cons(cons(x))) → shuffle0(cons(cons(x)))
app0(cons(x), y) → cons(app0(x, y))
reverse0(cons(x)) → app0(reverse0(x), cons(nil0))
app0(nil0, 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:

reverse(nil) → nil
shuffle(cons(n, cons(m, x))) → shuffle(cons(m, cons(n, x)))
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(nil) → nil

(13) RelADPCleverAfsProof (SOUND 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.

Furthermore, We use an argument filter [LPAR04].
Filtering:REVERSE_1 = reverse_1 = app_2 = cons_2 = 0 shuffle_1 = nil =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
REVERSE(x1) = REVERSE(x1)
cons(x1, x2) = cons(x2)

Recursive path order with status [RPO].
Quasi-Precedence:

[REVERSE₁, cons₁]

Status:

REVERSE₁: [1]
cons₁: multiset

(14) Obligation:

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

REVERSE0(cons(x)) → REVERSE0(x)

The TRS R consists of the following rules:

reverse0(nil0) → nil0
shuffle0(cons(cons(x))) → shuffle0(cons(cons(x)))
app0(cons(x), y) → cons(app0(x, y))
shuffle0(cons(x)) → cons(shuffle0(reverse0(x)))
reverse0(cons(x)) → app0(reverse0(x), cons(nil0))
app0(nil0, y) → y
shuffle0(nil0) → nil0

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

(15) MRRProof (EQUIVALENT transformation)

REVERSE0(cons(x)) → REVERSE0(x)

Strictly oriented rules of the TRS R:

shuffle0(cons(x)) → cons(shuffle0(reverse0(x)))
shuffle0(nil0) → nil0

Used ordering: Polynomial interpretation [POLO]:

POL(REVERSE0(x₁)) = x₁
POL(app0(x₁, x₂)) = x₁ + x₂
POL(cons(x₁)) = 1 + x₁
POL(nil0) = 0
POL(reverse0(x₁)) = x₁
POL(shuffle0(x₁)) = 2 + 2·x₁

(16) Obligation:

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

reverse0(nil0) → nil0
shuffle0(cons(cons(x))) → shuffle0(cons(cons(x)))
app0(cons(x), y) → cons(app0(x, y))
reverse0(cons(x)) → app0(reverse0(x), cons(nil0))
app0(nil0, 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
shuffle(cons(n, cons(m, x))) → SHUFFLE(cons(m, cons(n, x)))
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(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
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(nil) → nil

The remaining rules can at least be oriented weakly:

Ordered with Polynomial interpretation [POLO]:

POL(APP(x₁, x₂)) = 2·x₁·x₂ + 2·x₂
POL(REVERSE(x₁)) = 2 + x₁ + 2·x₁²
POL(SHUFFLE(x₁)) = 2 + x₁
POL(app(x₁, x₂)) = x₁ + x₂
POL(cons(x₁, x₂)) = 1 + x₂
POL(nil) = 0
POL(reverse(x₁)) = x₁
POL(shuffle(x₁)) = 3 + x₁

(21) Obligation:

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

reverse(nil) → nil
shuffle(cons(n, cons(m, x))) → SHUFFLE(cons(m, cons(n, x)))
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(nil) → nil

(22) DAbsisEmptyProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) RelTRStoRelADPProof (EQUIVALENT transformation)

(2) Obligation:

(3) RelADPDepGraphProof (EQUIVALENT transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) RelADPCleverAfsProof (SOUND transformation)

(7) Obligation:

(8) MRRProof (EQUIVALENT transformation)

(9) Obligation:

(10) PisEmptyProof (EQUIVALENT transformation)

(11) YES

(12) Obligation:

(13) RelADPCleverAfsProof (SOUND transformation)

(14) Obligation:

(15) MRRProof (EQUIVALENT transformation)

(16) Obligation:

(17) PisEmptyProof (EQUIVALENT transformation)

(18) YES

(19) Obligation:

(20) RelADPReductionPairProof (EQUIVALENT transformation)

(21) Obligation:

(22) DAbsisEmptyProof (EQUIVALENT transformation)

(23) YES