YES Termination proof of INVY_15_3.53_rand.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 RelADPCleverAfsProof (⇒, 26 ms)
        ↳7 QDP
        ↳8 MRRProof (⇔, 0 ms)
        ↳9 QDP
        ↳10 MRRProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 MRRProof (⇔, 0 ms)
        ↳13 QDP
        ↳14 MRRProof (⇔, 5 ms)
        ↳15 QDP
        ↳16 MRRProof (⇔, 0 ms)
        ↳17 QDP
        ↳18 MRRProof (⇔, 0 ms)
        ↳19 QDP
        ↳20 MRRProof (⇔, 0 ms)
        ↳21 QDP
        ↳22 QDPOrderProof (⇔, 0 ms)
        ↳23 QDP
        ↳24 PisEmptyProof (⇔, 0 ms)
        ↳25 YES
    ↳26 RelADPP
        ↳27 RelADPCleverAfsProof (⇒, 25 ms)
        ↳28 QDP
        ↳29 MRRProof (⇔, 0 ms)
        ↳30 QDP
        ↳31 PisEmptyProof (⇔, 0 ms)
        ↳32 YES
    ↳33 RelADPP
        ↳34 RelADPDerelatifyingProof (⇔, 0 ms)
        ↳35 QDP
        ↳36 QDPOrderProof (⇔, 14 ms)
        ↳37 QDP
        ↳38 PisEmptyProof (⇔, 0 ms)
        ↳39 YES
    ↳40 RelADPP
        ↳41 RelADPCleverAfsProof (⇒, 29 ms)
        ↳42 QDP
        ↳43 MRRProof (⇔, 0 ms)
        ↳44 QDP
        ↳45 MRRProof (⇔, 2 ms)
        ↳46 QDP
        ↳47 MRRProof (⇔, 0 ms)
        ↳48 QDP
        ↳49 MRRProof (⇔, 8 ms)
        ↳50 QDP
        ↳51 PisEmptyProof (⇔, 0 ms)
        ↳52 YES
    ↳53 RelADPP
        ↳54 RelADPCleverAfsProof (⇒, 23 ms)
        ↳55 QDP
        ↳56 MRRProof (⇔, 0 ms)
        ↳57 QDP
        ↳58 MRRProof (⇔, 2 ms)
        ↳59 QDP
        ↳60 MRRProof (⇔, 0 ms)
        ↳61 QDP
        ↳62 MRRProof (⇔, 5 ms)
        ↳63 QDP
        ↳64 MRRProof (⇔, 0 ms)
        ↳65 QDP
        ↳66 PisEmptyProof (⇔, 0 ms)
        ↳67 YES
    ↳68 RelADPP
        ↳69 RelADPDerelatifyingProof (⇔, 0 ms)
        ↳70 QDP
        ↳71 QDPOrderProof (⇔, 22 ms)
        ↳72 QDP
        ↳73 PisEmptyProof (⇔, 0 ms)
        ↳74 YES
    ↳75 RelADPP
        ↳76 RelADPCleverAfsProof (⇒, 26 ms)
        ↳77 QDP
        ↳78 MRRProof (⇔, 0 ms)
        ↳79 QDP
        ↳80 MRRProof (⇔, 1 ms)
        ↳81 QDP
        ↳82 MRRProof (⇔, 0 ms)
        ↳83 QDP
        ↳84 MRRProof (⇔, 5 ms)
        ↳85 QDP
        ↳86 MRRProof (⇔, 0 ms)
        ↳87 QDP
        ↳88 MRRProof (⇔, 0 ms)
        ↳89 QDP
        ↳90 QDPOrderProof (⇔, 0 ms)
        ↳91 QDP
        ↳92 PisEmptyProof (⇔, 0 ms)
        ↳93 YES

(0) Obligation:

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

minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
less_leaves(x, leaf) → false
less_leaves(leaf, cons(w, z)) → true
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z))

The relative TRS consists of the following S rules:

rand(x) → rand(s(x))
rand(x) → 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:

minus(x, 0) → x
minus(s(x), s(y)) → MINUS(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))
quot(s(x), s(y)) → s(quot(MINUS(x, y), s(y)))
app(nil, y) → y
app(add(n, x), y) → add(n, APP(x, y))
reverse(nil) → nil
reverse(add(n, x)) → APP(reverse(x), add(n, nil))
reverse(add(n, x)) → app(REVERSE(x), add(n, nil))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, SHUFFLE(reverse(x)))
shuffle(add(n, x)) → add(n, shuffle(REVERSE(x)))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, CONCAT(v, y))
less_leaves(x, leaf) → false
less_leaves(leaf, cons(w, z)) → true
less_leaves(cons(u, v), cons(w, z)) → LESS_LEAVES(concat(u, v), concat(w, z))
less_leaves(cons(u, v), cons(w, z)) → less_leaves(CONCAT(u, v), concat(w, z))
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), CONCAT(w, z))

and relative ADPs:

rand(x) → RAND(s(x))
rand(x) → x

(3) RelADPDepGraphProof (EQUIVALENT transformation)

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

(4) Complex Obligation (AND)

(5) Obligation:

Relative ADP Problem with
absolute ADPs:

minus(s(x), s(y)) → MINUS(x, y)

and relative ADPs:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
rand(x) → rand(s(x))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
quot(0, s(y)) → 0
reverse(nil) → nil
less_leaves(x, leaf) → false
app(add(n, x), y) → add(n, app(x, y))
less_leaves(leaf, cons(w, z)) → true
app(nil, y) → y
reverse(add(n, x)) → app(reverse(x), add(n, nil))
minus(x, 0) → x
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z))
rand(x) → x

(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:MINUS_2 = 0 true = less_leaves_2 = add_2 = app_2 = concat_2 = leaf = shuffle_1 = rand_1 = quot_2 = nil = false = s_1 = reverse_1 = 0 = minus_2 = 1 cons_2 =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
MINUS(x1, x2)  =  MINUS(x2)
s(x1)  =  s(x1)
quot(x1, x2)  =  quot(x1, x2)
minus(x1, x2)  =  minus(x1)
0  =  0

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

quot2 > [MINUS1, s1, 0] > minus1

Status:
MINUS1: multiset
s1: multiset
quot2: [2,1]
minus1: multiset
0: multiset

(7) Obligation:

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

MINUS(s0(y)) → MINUS(y)

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
concat0(leaf0, y) → y
concat0(cons0(u, v), y) → cons0(u, concat0(v, y))
rand0(x) → rand0(s0(x))
shuffle0(nil0) → nil0
shuffle0(add0(n, x)) → add0(n, shuffle0(reverse0(x)))
quot0(00, s0(y)) → 00
reverse0(nil0) → nil0
less_leaves0(x, leaf0) → false0
app0(add0(n, x), y) → add0(n, app0(x, y))
less_leaves0(leaf0, cons0(w, z)) → true0
app0(nil0, y) → y
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))
minus(s0(x)) → minus(x)
minus(x) → x
less_leaves0(cons0(u, v), cons0(w, z)) → less_leaves0(concat0(u, v), concat0(w, z))
rand0(x) → x

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 rules of the TRS R:

concat0(leaf0, y) → y
concat0(cons0(u, v), y) → cons0(u, concat0(v, y))
quot0(00, s0(y)) → 00
less_leaves0(leaf0, cons0(w, z)) → true0
less_leaves0(cons0(u, v), cons0(w, z)) → less_leaves0(concat0(u, v), concat0(w, z))
rand0(x) → x

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 0   
POL(MINUS(x1)) = x1   
POL(add0(x1, x2)) = x1 + x2   
POL(app0(x1, x2)) = x1 + x2   
POL(concat0(x1, x2)) = 2·x1 + x2   
POL(cons0(x1, x2)) = 2 + 2·x1 + x2   
POL(false0) = 2   
POL(leaf0) = 1   
POL(less_leaves0(x1, x2)) = 1 + 2·x1 + x2   
POL(minus(x1)) = x1   
POL(nil0) = 0   
POL(quot0(x1, x2)) = 1 + x1 + x2   
POL(rand0(x1)) = 2 + x1   
POL(reverse0(x1)) = x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = x1   
POL(true0) = 0   

(9) Obligation:

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

MINUS(s0(y)) → MINUS(y)

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
shuffle0(nil0) → nil0
shuffle0(add0(n, x)) → add0(n, shuffle0(reverse0(x)))
reverse0(nil0) → nil0
less_leaves0(x, leaf0) → false0
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))
minus(s0(x)) → minus(x)
minus(x) → x

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

(10) 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 rules of the TRS R:

reverse0(nil0) → nil0
less_leaves0(x, leaf0) → false0

Used ordering: Polynomial interpretation [POLO]:

POL(MINUS(x1)) = x1   
POL(add0(x1, x2)) = 2 + x1 + x2   
POL(app0(x1, x2)) = x1 + x2   
POL(false0) = 0   
POL(leaf0) = 0   
POL(less_leaves0(x1, x2)) = 1 + x1 + x2   
POL(minus(x1)) = x1   
POL(nil0) = 0   
POL(quot0(x1, x2)) = x1 + x2   
POL(rand0(x1)) = x1   
POL(reverse0(x1)) = 1 + x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = 2·x1   

(11) Obligation:

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

MINUS(s0(y)) → MINUS(y)

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
shuffle0(nil0) → nil0
shuffle0(add0(n, x)) → add0(n, shuffle0(reverse0(x)))
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))
minus(s0(x)) → minus(x)
minus(x) → x

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

(12) 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 rules of the TRS R:

shuffle0(nil0) → nil0

Used ordering: Polynomial interpretation [POLO]:

POL(MINUS(x1)) = 2·x1   
POL(add0(x1, x2)) = 2 + x1 + x2   
POL(app0(x1, x2)) = x1 + x2   
POL(minus(x1)) = x1   
POL(nil0) = 0   
POL(quot0(x1, x2)) = x1 + x2   
POL(rand0(x1)) = x1   
POL(reverse0(x1)) = 1 + x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = 2 + 2·x1   

(13) Obligation:

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

MINUS(s0(y)) → MINUS(y)

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
shuffle0(add0(n, x)) → add0(n, shuffle0(reverse0(x)))
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))
minus(s0(x)) → minus(x)
minus(x) → x

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

(14) 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 rules of the TRS R:

shuffle0(add0(n, x)) → add0(n, shuffle0(reverse0(x)))

Used ordering: Polynomial interpretation [POLO]:

POL(MINUS(x1)) = x1   
POL(add0(x1, x2)) = 1 + x1 + x2   
POL(app0(x1, x2)) = x1 + x2   
POL(minus(x1)) = x1   
POL(nil0) = 0   
POL(quot0(x1, x2)) = x1 + x2   
POL(rand0(x1)) = x1   
POL(reverse0(x1)) = x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = 2·x1   

(15) Obligation:

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

MINUS(s0(y)) → MINUS(y)

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))
minus(s0(x)) → minus(x)
minus(x) → x

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

(16) 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 rules of the TRS R:

reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))

Used ordering: Polynomial interpretation [POLO]:

POL(MINUS(x1)) = 2·x1   
POL(add0(x1, x2)) = 2 + x1 + x2   
POL(app0(x1, x2)) = x1 + x2   
POL(minus(x1)) = x1   
POL(nil0) = 0   
POL(quot0(x1, x2)) = x1 + x2   
POL(rand0(x1)) = x1   
POL(reverse0(x1)) = 2 + 2·x1   
POL(s0(x1)) = x1   

(17) Obligation:

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

MINUS(s0(y)) → MINUS(y)

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
minus(s0(x)) → minus(x)
minus(x) → x

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

(18) 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 rules of the TRS R:

app0(nil0, y) → y

Used ordering: Polynomial interpretation [POLO]:

POL(MINUS(x1)) = x1   
POL(add0(x1, x2)) = x1 + x2   
POL(app0(x1, x2)) = 2·x1 + x2   
POL(minus(x1)) = x1   
POL(nil0) = 2   
POL(quot0(x1, x2)) = x1 + x2   
POL(rand0(x1)) = x1   
POL(s0(x1)) = x1   

(19) Obligation:

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

MINUS(s0(y)) → MINUS(y)

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
app0(add0(n, x), y) → add0(n, app0(x, y))
minus(s0(x)) → minus(x)
minus(x) → x

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

(20) 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 rules of the TRS R:

app0(add0(n, x), y) → add0(n, app0(x, y))

Used ordering: Polynomial interpretation [POLO]:

POL(MINUS(x1)) = x1   
POL(add0(x1, x2)) = 2 + x1 + x2   
POL(app0(x1, x2)) = 2 + 2·x1 + x2   
POL(minus(x1)) = x1   
POL(quot0(x1, x2)) = x1 + x2   
POL(rand0(x1)) = x1   
POL(s0(x1)) = x1   

(21) Obligation:

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

MINUS(s0(y)) → MINUS(y)

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
minus(s0(x)) → minus(x)
minus(x) → x

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

(22) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MINUS(s0(y)) → MINUS(y)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( quot0(x1, x2) ) = 2x1

POL( s0(x1) ) = 2x1 + 1

POL( minus(x1) ) = x1

POL( rand0(x1) ) = max{0, -2}

POL( MINUS(x1) ) = x1


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
minus(s0(x)) → minus(x)
minus(x) → x

(23) Obligation:

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

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
minus(s0(x)) → minus(x)
minus(x) → x

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

(24) PisEmptyProof (EQUIVALENT transformation)

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

(25) YES

(26) Obligation:

Relative ADP Problem with
absolute ADPs:

concat(cons(u, v), y) → cons(u, CONCAT(v, y))

and relative ADPs:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
concat(leaf, y) → y
rand(x) → rand(s(x))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
quot(0, s(y)) → 0
reverse(nil) → nil
less_leaves(x, leaf) → false
app(add(n, x), y) → add(n, app(x, y))
less_leaves(leaf, cons(w, z)) → true
app(nil, y) → y
reverse(add(n, x)) → app(reverse(x), add(n, nil))
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z))
rand(x) → x

(27) 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:true = CONCAT_2 = less_leaves_2 = add_2 = app_2 = concat_2 = leaf = shuffle_1 = rand_1 = quot_2 = 0, 1 nil = false = s_1 = reverse_1 = 0 = minus_2 = 1 cons_2 =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
CONCAT(x1, x2)  =  CONCAT(x1, x2)
cons(x1, x2)  =  cons(x1, x2)
quot(x1, x2)  =  quot
s(x1)  =  x1
minus(x1, x2)  =  x1
0  =  0

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

cons2 > CONCAT2
[quot, 0]

Status:
CONCAT2: multiset
cons2: multiset
quot: []
0: multiset

(28) Obligation:

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

CONCAT0(cons0(u, v), y) → CONCAT0(v, y)

The TRS R consists of the following rules:

quot → s0(quot)
concat0(leaf0, y) → y
concat0(cons0(u, v), y) → cons0(u, concat0(v, y))
rand0(x) → rand0(s0(x))
shuffle0(nil0) → nil0
shuffle0(add0(n, x)) → add0(n, shuffle0(reverse0(x)))
quot → 00
reverse0(nil0) → nil0
less_leaves0(x, leaf0) → false0
app0(add0(n, x), y) → add0(n, app0(x, y))
less_leaves0(leaf0, cons0(w, z)) → true0
app0(nil0, y) → y
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))
minus(s0(x)) → minus(x)
minus(x) → x
less_leaves0(cons0(u, v), cons0(w, z)) → less_leaves0(concat0(u, v), concat0(w, z))
rand0(x) → x

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

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

CONCAT0(cons0(u, v), y) → CONCAT0(v, y)

Strictly oriented rules of the TRS R:

concat0(cons0(u, v), y) → cons0(u, concat0(v, y))
less_leaves0(leaf0, cons0(w, z)) → true0
minus(x) → x
less_leaves0(cons0(u, v), cons0(w, z)) → less_leaves0(concat0(u, v), concat0(w, z))
rand0(x) → x

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 0   
POL(CONCAT0(x1, x2)) = x1 + x2   
POL(add0(x1, x2)) = x1 + x2   
POL(app0(x1, x2)) = x1 + x2   
POL(concat0(x1, x2)) = 2·x1 + x2   
POL(cons0(x1, x2)) = 2 + 2·x1 + x2   
POL(false0) = 0   
POL(leaf0) = 0   
POL(less_leaves0(x1, x2)) = 2·x1 + x2   
POL(minus(x1)) = 2 + x1   
POL(nil0) = 0   
POL(quot) = 0   
POL(rand0(x1)) = 2 + x1   
POL(reverse0(x1)) = x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = x1   
POL(true0) = 0   

(30) Obligation:

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

quot → s0(quot)
concat0(leaf0, y) → y
rand0(x) → rand0(s0(x))
shuffle0(nil0) → nil0
shuffle0(add0(n, x)) → add0(n, shuffle0(reverse0(x)))
quot → 00
reverse0(nil0) → nil0
less_leaves0(x, leaf0) → false0
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))
minus(s0(x)) → minus(x)

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

(31) PisEmptyProof (EQUIVALENT transformation)

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

(32) YES

(33) Obligation:

Relative ADP Problem with
absolute ADPs:

less_leaves(cons(u, v), cons(w, z)) → LESS_LEAVES(concat(u, v), concat(w, z))

and relative ADPs:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
rand(x) → rand(s(x))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
quot(0, s(y)) → 0
reverse(nil) → nil
less_leaves(x, leaf) → false
app(add(n, x), y) → add(n, app(x, y))
less_leaves(leaf, cons(w, z)) → true
app(nil, y) → y
reverse(add(n, x)) → app(reverse(x), add(n, nil))
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z))
rand(x) → x

(34) 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.

(35) Obligation:

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

LESS_LEAVES(cons(u, v), cons(w, z)) → LESS_LEAVES(concat(u, v), concat(w, z))

The TRS R consists of the following rules:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
rand(x) → rand(s(x))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
quot(0, s(y)) → 0
reverse(nil) → nil
less_leaves(x, leaf) → false
app(add(n, x), y) → add(n, app(x, y))
less_leaves(leaf, cons(w, z)) → true
app(nil, y) → y
reverse(add(n, x)) → app(reverse(x), add(n, nil))
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z))
rand(x) → x

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

(36) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


LESS_LEAVES(cons(u, v), cons(w, z)) → LESS_LEAVES(concat(u, v), concat(w, z))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( quot(x1, x2) ) = x1 + x2 + 1

POL( s(x1) ) = x1

POL( minus(x1, x2) ) = x1

POL( concat(x1, x2) ) = 2x1 + x2 + 1

POL( leaf ) = 0

POL( cons(x1, x2) ) = 2x1 + x2 + 2

POL( rand(x1) ) = 2x1

POL( shuffle(x1) ) = 2x1

POL( nil ) = 1

POL( add(x1, x2) ) = 2

POL( reverse(x1) ) = 2x1 + 2

POL( 0 ) = 1

POL( less_leaves(x1, x2) ) = 2x1 + x2 + 1

POL( false ) = 0

POL( app(x1, x2) ) = 2x2 + 2

POL( true ) = 2

POL( LESS_LEAVES(x1, x2) ) = 2x1 + 2x2 + 2


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
rand(x) → rand(s(x))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
quot(0, s(y)) → 0
reverse(nil) → nil
less_leaves(x, leaf) → false
app(add(n, x), y) → add(n, app(x, y))
less_leaves(leaf, cons(w, z)) → true
app(nil, y) → y
reverse(add(n, x)) → app(reverse(x), add(n, nil))
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z))
rand(x) → x

(37) Obligation:

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

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
rand(x) → rand(s(x))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
quot(0, s(y)) → 0
reverse(nil) → nil
less_leaves(x, leaf) → false
app(add(n, x), y) → add(n, app(x, y))
less_leaves(leaf, cons(w, z)) → true
app(nil, y) → y
reverse(add(n, x)) → app(reverse(x), add(n, nil))
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z))
rand(x) → x

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

(38) PisEmptyProof (EQUIVALENT transformation)

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

(39) YES

(40) Obligation:

Relative ADP Problem with
absolute ADPs:

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

and relative ADPs:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
rand(x) → rand(s(x))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
quot(0, s(y)) → 0
reverse(nil) → nil
less_leaves(x, leaf) → false
less_leaves(leaf, cons(w, z)) → true
app(nil, y) → y
reverse(add(n, x)) → app(reverse(x), add(n, nil))
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z))
rand(x) → x

(41) 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:true = less_leaves_2 = app_2 = add_2 = concat_2 = leaf = shuffle_1 = rand_1 = APP_2 = quot_2 = 0, 1 nil = false = s_1 = reverse_1 = 0 = minus_2 = 1 cons_2 =
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)  =  APP(x1, x2)
add(x1, x2)  =  add(x1, x2)
quot(x1, x2)  =  quot
s(x1)  =  x1
minus(x1, x2)  =  x1
0  =  0

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

add2 > APP2
[quot, 0]

Status:
APP2: [2,1]
add2: multiset
quot: []
0: multiset

(42) Obligation:

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

APP0(add0(n, x), y) → APP0(x, y)

The TRS R consists of the following rules:

quot → s0(quot)
concat0(leaf0, y) → y
concat0(cons0(u, v), y) → cons0(u, concat0(v, y))
rand0(x) → rand0(s0(x))
shuffle0(nil0) → nil0
shuffle0(add0(n, x)) → add0(n, shuffle0(reverse0(x)))
quot → 00
reverse0(nil0) → nil0
less_leaves0(x, leaf0) → false0
app0(add0(n, x), y) → add0(n, app0(x, y))
less_leaves0(leaf0, cons0(w, z)) → true0
app0(nil0, y) → y
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))
minus(s0(x)) → minus(x)
minus(x) → x
less_leaves0(cons0(u, v), cons0(w, z)) → less_leaves0(concat0(u, v), concat0(w, z))
rand0(x) → x

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

(43) 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 rules of the TRS R:

concat0(cons0(u, v), y) → cons0(u, concat0(v, y))
less_leaves0(leaf0, cons0(w, z)) → true0
minus(x) → x
less_leaves0(cons0(u, v), cons0(w, z)) → less_leaves0(concat0(u, v), concat0(w, z))
rand0(x) → x

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 0   
POL(APP0(x1, x2)) = x1 + x2   
POL(add0(x1, x2)) = x1 + x2   
POL(app0(x1, x2)) = x1 + x2   
POL(concat0(x1, x2)) = 2·x1 + x2   
POL(cons0(x1, x2)) = 2 + 2·x1 + x2   
POL(false0) = 0   
POL(leaf0) = 0   
POL(less_leaves0(x1, x2)) = 2·x1 + x2   
POL(minus(x1)) = 2 + x1   
POL(nil0) = 0   
POL(quot) = 0   
POL(rand0(x1)) = 2 + x1   
POL(reverse0(x1)) = x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = x1   
POL(true0) = 0   

(44) Obligation:

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

APP0(add0(n, x), y) → APP0(x, y)

The TRS R consists of the following rules:

quot → s0(quot)
concat0(leaf0, y) → y
rand0(x) → rand0(s0(x))
shuffle0(nil0) → nil0
shuffle0(add0(n, x)) → add0(n, shuffle0(reverse0(x)))
quot → 00
reverse0(nil0) → nil0
less_leaves0(x, leaf0) → false0
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))
minus(s0(x)) → minus(x)

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

(45) 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 rules of the TRS R:

concat0(leaf0, y) → y

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 0   
POL(APP0(x1, x2)) = 2·x1 + x2   
POL(add0(x1, x2)) = x1 + x2   
POL(app0(x1, x2)) = x1 + x2   
POL(concat0(x1, x2)) = 2 + x1 + x2   
POL(false0) = 2   
POL(leaf0) = 1   
POL(less_leaves0(x1, x2)) = x1 + 2·x2   
POL(minus(x1)) = x1   
POL(nil0) = 0   
POL(quot) = 0   
POL(rand0(x1)) = x1   
POL(reverse0(x1)) = x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = 2·x1   

(46) Obligation:

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

APP0(add0(n, x), y) → APP0(x, y)

The TRS R consists of the following rules:

quot → s0(quot)
rand0(x) → rand0(s0(x))
shuffle0(nil0) → nil0
shuffle0(add0(n, x)) → add0(n, shuffle0(reverse0(x)))
quot → 00
reverse0(nil0) → nil0
less_leaves0(x, leaf0) → false0
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))
minus(s0(x)) → minus(x)

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

(47) 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 rules of the TRS R:

quot → 00

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 1   
POL(APP0(x1, x2)) = 2·x1 + x2   
POL(add0(x1, x2)) = x1 + x2   
POL(app0(x1, x2)) = x1 + x2   
POL(false0) = 1   
POL(leaf0) = 0   
POL(less_leaves0(x1, x2)) = 1 + x1 + x2   
POL(minus(x1)) = x1   
POL(nil0) = 0   
POL(quot) = 2   
POL(rand0(x1)) = x1   
POL(reverse0(x1)) = x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = 2·x1   

(48) Obligation:

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

APP0(add0(n, x), y) → APP0(x, y)

The TRS R consists of the following rules:

quot → s0(quot)
rand0(x) → rand0(s0(x))
shuffle0(nil0) → nil0
shuffle0(add0(n, x)) → add0(n, shuffle0(reverse0(x)))
reverse0(nil0) → nil0
less_leaves0(x, leaf0) → false0
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))
minus(s0(x)) → minus(x)

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

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

APP0(add0(n, x), y) → APP0(x, y)

Strictly oriented rules of the TRS R:

shuffle0(nil0) → nil0
shuffle0(add0(n, x)) → add0(n, shuffle0(reverse0(x)))
less_leaves0(x, leaf0) → false0

Used ordering: Polynomial interpretation [POLO]:

POL(APP0(x1, x2)) = x1 + x2   
POL(add0(x1, x2)) = 1 + x1 + x2   
POL(app0(x1, x2)) = x1 + x2   
POL(false0) = 1   
POL(leaf0) = 2   
POL(less_leaves0(x1, x2)) = 2 + x1 + 2·x2   
POL(minus(x1)) = x1   
POL(nil0) = 0   
POL(quot) = 0   
POL(rand0(x1)) = x1   
POL(reverse0(x1)) = x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = 2 + 2·x1   

(50) Obligation:

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

quot → s0(quot)
rand0(x) → rand0(s0(x))
reverse0(nil0) → nil0
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))
minus(s0(x)) → minus(x)

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

(51) PisEmptyProof (EQUIVALENT transformation)

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

(52) YES

(53) Obligation:

Relative ADP Problem with
absolute ADPs:

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

and relative ADPs:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
rand(x) → rand(s(x))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
quot(0, s(y)) → 0
reverse(nil) → nil
less_leaves(x, leaf) → false
app(add(n, x), y) → add(n, app(x, y))
less_leaves(leaf, cons(w, z)) → true
app(nil, y) → y
reverse(add(n, x)) → app(reverse(x), add(n, nil))
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z))
rand(x) → x

(54) 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:true = REVERSE_1 = less_leaves_2 = add_2 = 0 app_2 = concat_2 = leaf = shuffle_1 = rand_1 = nil = quot_2 = 0, 1 false = s_1 = reverse_1 = 0 = minus_2 = 1 cons_2 =
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)  =  x1
add(x1, x2)  =  add(x2)
quot(x1, x2)  =  quot
s(x1)  =  x1
minus(x1, x2)  =  x1
0  =  0

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

[quot, 0]

Status:
add1: multiset
quot: []
0: multiset

(55) Obligation:

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

REVERSE0(add(x)) → REVERSE0(x)

The TRS R consists of the following rules:

quot → s0(quot)
concat0(leaf0, y) → y
concat0(cons0(u, v), y) → cons0(u, concat0(v, y))
rand0(x) → rand0(s0(x))
shuffle0(nil0) → nil0
shuffle0(add(x)) → add(shuffle0(reverse0(x)))
quot → 00
reverse0(nil0) → nil0
less_leaves0(x, leaf0) → false0
app0(add(x), y) → add(app0(x, y))
less_leaves0(leaf0, cons0(w, z)) → true0
app0(nil0, y) → y
reverse0(add(x)) → app0(reverse0(x), add(nil0))
minus(s0(x)) → minus(x)
minus(x) → x
less_leaves0(cons0(u, v), cons0(w, z)) → less_leaves0(concat0(u, v), concat0(w, z))
rand0(x) → x

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

(56) 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 rules of the TRS R:

concat0(cons0(u, v), y) → cons0(u, concat0(v, y))
less_leaves0(x, leaf0) → false0
less_leaves0(leaf0, cons0(w, z)) → true0
minus(x) → x
less_leaves0(cons0(u, v), cons0(w, z)) → less_leaves0(concat0(u, v), concat0(w, z))
rand0(x) → x

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 0   
POL(REVERSE0(x1)) = x1   
POL(add(x1)) = x1   
POL(app0(x1, x2)) = x1 + x2   
POL(concat0(x1, x2)) = 2·x1 + x2   
POL(cons0(x1, x2)) = 2 + 2·x1 + x2   
POL(false0) = 0   
POL(leaf0) = 0   
POL(less_leaves0(x1, x2)) = 1 + 2·x1 + x2   
POL(minus(x1)) = 2 + 2·x1   
POL(nil0) = 0   
POL(quot) = 0   
POL(rand0(x1)) = 2 + x1   
POL(reverse0(x1)) = x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = x1   
POL(true0) = 2   

(57) Obligation:

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

REVERSE0(add(x)) → REVERSE0(x)

The TRS R consists of the following rules:

quot → s0(quot)
concat0(leaf0, y) → y
rand0(x) → rand0(s0(x))
shuffle0(nil0) → nil0
shuffle0(add(x)) → add(shuffle0(reverse0(x)))
quot → 00
reverse0(nil0) → nil0
app0(add(x), y) → add(app0(x, y))
app0(nil0, y) → y
reverse0(add(x)) → app0(reverse0(x), add(nil0))
minus(s0(x)) → minus(x)

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

(58) 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 rules of the TRS R:

concat0(leaf0, y) → y

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 0   
POL(REVERSE0(x1)) = x1   
POL(add(x1)) = x1   
POL(app0(x1, x2)) = x1 + x2   
POL(concat0(x1, x2)) = 2 + 2·x1 + x2   
POL(leaf0) = 0   
POL(minus(x1)) = x1   
POL(nil0) = 0   
POL(quot) = 0   
POL(rand0(x1)) = x1   
POL(reverse0(x1)) = x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = x1   

(59) Obligation:

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

REVERSE0(add(x)) → REVERSE0(x)

The TRS R consists of the following rules:

quot → s0(quot)
rand0(x) → rand0(s0(x))
shuffle0(nil0) → nil0
shuffle0(add(x)) → add(shuffle0(reverse0(x)))
quot → 00
reverse0(nil0) → nil0
app0(add(x), y) → add(app0(x, y))
app0(nil0, y) → y
reverse0(add(x)) → app0(reverse0(x), add(nil0))
minus(s0(x)) → minus(x)

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

(60) 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 rules of the TRS R:

quot → 00

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 1   
POL(REVERSE0(x1)) = 2·x1   
POL(add(x1)) = x1   
POL(app0(x1, x2)) = x1 + 2·x2   
POL(minus(x1)) = x1   
POL(nil0) = 0   
POL(quot) = 2   
POL(rand0(x1)) = x1   
POL(reverse0(x1)) = x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = 2·x1   

(61) Obligation:

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

REVERSE0(add(x)) → REVERSE0(x)

The TRS R consists of the following rules:

quot → s0(quot)
rand0(x) → rand0(s0(x))
shuffle0(nil0) → nil0
shuffle0(add(x)) → add(shuffle0(reverse0(x)))
reverse0(nil0) → nil0
app0(add(x), y) → add(app0(x, y))
app0(nil0, y) → y
reverse0(add(x)) → app0(reverse0(x), add(nil0))
minus(s0(x)) → minus(x)

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

(62) 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 rules of the TRS R:

shuffle0(nil0) → nil0

Used ordering: Polynomial interpretation [POLO]:

POL(REVERSE0(x1)) = 2·x1   
POL(add(x1)) = x1   
POL(app0(x1, x2)) = x1 + x2   
POL(minus(x1)) = x1   
POL(nil0) = 0   
POL(quot) = 0   
POL(rand0(x1)) = x1   
POL(reverse0(x1)) = x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = 2 + 2·x1   

(63) Obligation:

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

REVERSE0(add(x)) → REVERSE0(x)

The TRS R consists of the following rules:

quot → s0(quot)
rand0(x) → rand0(s0(x))
shuffle0(add(x)) → add(shuffle0(reverse0(x)))
reverse0(nil0) → nil0
app0(add(x), y) → add(app0(x, y))
app0(nil0, y) → y
reverse0(add(x)) → app0(reverse0(x), add(nil0))
minus(s0(x)) → minus(x)

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

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

REVERSE0(add(x)) → REVERSE0(x)

Strictly oriented rules of the TRS R:

reverse0(nil0) → nil0

Used ordering: Polynomial interpretation [POLO]:

POL(REVERSE0(x1)) = x1   
POL(add(x1)) = 2 + x1   
POL(app0(x1, x2)) = x1 + x2   
POL(minus(x1)) = x1   
POL(nil0) = 0   
POL(quot) = 0   
POL(rand0(x1)) = x1   
POL(reverse0(x1)) = 1 + x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = 2 + 2·x1   

(65) Obligation:

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

quot → s0(quot)
rand0(x) → rand0(s0(x))
shuffle0(add(x)) → add(shuffle0(reverse0(x)))
app0(add(x), y) → add(app0(x, y))
app0(nil0, y) → y
reverse0(add(x)) → app0(reverse0(x), add(nil0))
minus(s0(x)) → minus(x)

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

(66) PisEmptyProof (EQUIVALENT transformation)

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

(67) YES

(68) Obligation:

Relative ADP Problem with
absolute ADPs:

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

and relative ADPs:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
rand(x) → rand(s(x))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
quot(0, s(y)) → 0
reverse(nil) → nil
less_leaves(x, leaf) → false
app(add(n, x), y) → add(n, app(x, y))
less_leaves(leaf, cons(w, z)) → true
app(nil, y) → y
reverse(add(n, x)) → app(reverse(x), add(n, nil))
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z))
rand(x) → x

(69) 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.

(70) Obligation:

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

SHUFFLE(add(n, x)) → SHUFFLE(reverse(x))

The TRS R consists of the following rules:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
rand(x) → rand(s(x))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
quot(0, s(y)) → 0
reverse(nil) → nil
less_leaves(x, leaf) → false
app(add(n, x), y) → add(n, app(x, y))
less_leaves(leaf, cons(w, z)) → true
app(nil, y) → y
reverse(add(n, x)) → app(reverse(x), add(n, nil))
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z))
rand(x) → x

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

(71) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


SHUFFLE(add(n, x)) → SHUFFLE(reverse(x))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
POL( quot(x1, x2) ) = 2

POL( s(x1) ) = x1

POL( minus(x1, x2) ) = 2x1 + 2x2

POL( concat(x1, x2) ) = x1 + x2 + 1

POL( leaf ) = 0

POL( cons(x1, x2) ) = x1 + x2 + 2

POL( rand(x1) ) = 2x1

POL( shuffle(x1) ) = x1 + 1

POL( nil ) = 0

POL( add(x1, x2) ) = x2 + 1

POL( reverse(x1) ) = x1

POL( 0 ) = 0

POL( less_leaves(x1, x2) ) = 2x1 + x2 + 1

POL( false ) = 0

POL( app(x1, x2) ) = x1 + x2

POL( true ) = 0

POL( SHUFFLE(x1) ) = x1 + 2


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
rand(x) → rand(s(x))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
quot(0, s(y)) → 0
reverse(nil) → nil
less_leaves(x, leaf) → false
app(add(n, x), y) → add(n, app(x, y))
less_leaves(leaf, cons(w, z)) → true
app(nil, y) → y
reverse(add(n, x)) → app(reverse(x), add(n, nil))
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z))
rand(x) → x

(72) Obligation:

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

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
rand(x) → rand(s(x))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
quot(0, s(y)) → 0
reverse(nil) → nil
less_leaves(x, leaf) → false
app(add(n, x), y) → add(n, app(x, y))
less_leaves(leaf, cons(w, z)) → true
app(nil, y) → y
reverse(add(n, x)) → app(reverse(x), add(n, nil))
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z))
rand(x) → x

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

(73) PisEmptyProof (EQUIVALENT transformation)

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

(74) YES

(75) Obligation:

Relative ADP Problem with
absolute ADPs:

quot(s(x), s(y)) → s(QUOT(minus(x, y), s(y)))

and relative ADPs:

quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
rand(x) → rand(s(x))
shuffle(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
quot(0, s(y)) → 0
reverse(nil) → nil
less_leaves(x, leaf) → false
app(add(n, x), y) → add(n, app(x, y))
less_leaves(leaf, cons(w, z)) → true
app(nil, y) → y
reverse(add(n, x)) → app(reverse(x), add(n, nil))
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
less_leaves(cons(u, v), cons(w, z)) → less_leaves(concat(u, v), concat(w, z))
rand(x) → x

(76) 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:true = QUOT_2 = 1 less_leaves_2 = add_2 = app_2 = concat_2 = leaf = shuffle_1 = rand_1 = quot_2 = nil = false = s_1 = reverse_1 = 0 = minus_2 = 1 cons_2 =
Found this filtering by looking at the following order that orders at least one DP strictly:Combined order from the following AFS and order.
QUOT(x1, x2)  =  x1
s(x1)  =  s(x1)
minus(x1, x2)  =  x1
0  =  0
quot(x1, x2)  =  quot(x1, x2)

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

quot2 > 0 > s1

Status:
s1: multiset
0: multiset
quot2: [2,1]

(77) Obligation:

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

QUOT(s0(x)) → QUOT(minus(x))

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
concat0(leaf0, y) → y
concat0(cons0(u, v), y) → cons0(u, concat0(v, y))
rand0(x) → rand0(s0(x))
shuffle0(nil0) → nil0
shuffle0(add0(n, x)) → add0(n, shuffle0(reverse0(x)))
quot0(00, s0(y)) → 00
reverse0(nil0) → nil0
less_leaves0(x, leaf0) → false0
app0(add0(n, x), y) → add0(n, app0(x, y))
less_leaves0(leaf0, cons0(w, z)) → true0
app0(nil0, y) → y
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))
minus(s0(x)) → minus(x)
minus(x) → x
less_leaves0(cons0(u, v), cons0(w, z)) → less_leaves0(concat0(u, v), concat0(w, z))
rand0(x) → x

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

(78) 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 rules of the TRS R:

concat0(leaf0, y) → y
concat0(cons0(u, v), y) → cons0(u, concat0(v, y))
less_leaves0(x, leaf0) → false0
less_leaves0(leaf0, cons0(w, z)) → true0
less_leaves0(cons0(u, v), cons0(w, z)) → less_leaves0(concat0(u, v), concat0(w, z))
rand0(x) → x

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 0   
POL(QUOT(x1)) = x1   
POL(add0(x1, x2)) = x1 + x2   
POL(app0(x1, x2)) = x1 + x2   
POL(concat0(x1, x2)) = 2·x1 + x2   
POL(cons0(x1, x2)) = 1 + 2·x1 + x2   
POL(false0) = 0   
POL(leaf0) = 1   
POL(less_leaves0(x1, x2)) = x1 + x2   
POL(minus(x1)) = x1   
POL(nil0) = 0   
POL(quot0(x1, x2)) = x1 + x2   
POL(rand0(x1)) = 2 + x1   
POL(reverse0(x1)) = x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = x1   
POL(true0) = 0   

(79) Obligation:

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

QUOT(s0(x)) → QUOT(minus(x))

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
shuffle0(nil0) → nil0
shuffle0(add0(n, x)) → add0(n, shuffle0(reverse0(x)))
quot0(00, s0(y)) → 00
reverse0(nil0) → nil0
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))
minus(s0(x)) → minus(x)
minus(x) → x

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

(80) 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 rules of the TRS R:

shuffle0(nil0) → nil0
quot0(00, s0(y)) → 00

Used ordering: Polynomial interpretation [POLO]:

POL(00) = 0   
POL(QUOT(x1)) = x1   
POL(add0(x1, x2)) = x1 + x2   
POL(app0(x1, x2)) = x1 + x2   
POL(minus(x1)) = x1   
POL(nil0) = 0   
POL(quot0(x1, x2)) = 2 + 2·x1 + x2   
POL(rand0(x1)) = x1   
POL(reverse0(x1)) = x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = 2 + x1   

(81) Obligation:

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

QUOT(s0(x)) → QUOT(minus(x))

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
shuffle0(add0(n, x)) → add0(n, shuffle0(reverse0(x)))
reverse0(nil0) → nil0
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))
minus(s0(x)) → minus(x)
minus(x) → x

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

(82) 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 rules of the TRS R:

shuffle0(add0(n, x)) → add0(n, shuffle0(reverse0(x)))

Used ordering: Polynomial interpretation [POLO]:

POL(QUOT(x1)) = x1   
POL(add0(x1, x2)) = 2 + x1 + x2   
POL(app0(x1, x2)) = x1 + x2   
POL(minus(x1)) = x1   
POL(nil0) = 0   
POL(quot0(x1, x2)) = 2·x1 + x2   
POL(rand0(x1)) = x1   
POL(reverse0(x1)) = x1   
POL(s0(x1)) = x1   
POL(shuffle0(x1)) = 2·x1   

(83) Obligation:

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

QUOT(s0(x)) → QUOT(minus(x))

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
reverse0(nil0) → nil0
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))
minus(s0(x)) → minus(x)
minus(x) → x

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

(84) 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 rules of the TRS R:

reverse0(nil0) → nil0
reverse0(add0(n, x)) → app0(reverse0(x), add0(n, nil0))

Used ordering: Polynomial interpretation [POLO]:

POL(QUOT(x1)) = x1   
POL(add0(x1, x2)) = 2 + x1 + x2   
POL(app0(x1, x2)) = x1 + x2   
POL(minus(x1)) = x1   
POL(nil0) = 0   
POL(quot0(x1, x2)) = 2·x1 + x2   
POL(rand0(x1)) = x1   
POL(reverse0(x1)) = 2 + 2·x1   
POL(s0(x1)) = x1   

(85) Obligation:

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

QUOT(s0(x)) → QUOT(minus(x))

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
app0(add0(n, x), y) → add0(n, app0(x, y))
app0(nil0, y) → y
minus(s0(x)) → minus(x)
minus(x) → x

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

(86) 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 rules of the TRS R:

app0(nil0, y) → y

Used ordering: Polynomial interpretation [POLO]:

POL(QUOT(x1)) = x1   
POL(add0(x1, x2)) = x1 + x2   
POL(app0(x1, x2)) = 2·x1 + x2   
POL(minus(x1)) = x1   
POL(nil0) = 1   
POL(quot0(x1, x2)) = x1 + x2   
POL(rand0(x1)) = x1   
POL(s0(x1)) = x1   

(87) Obligation:

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

QUOT(s0(x)) → QUOT(minus(x))

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
app0(add0(n, x), y) → add0(n, app0(x, y))
minus(s0(x)) → minus(x)
minus(x) → x

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

(88) 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 rules of the TRS R:

app0(add0(n, x), y) → add0(n, app0(x, y))

Used ordering: Polynomial interpretation [POLO]:

POL(QUOT(x1)) = x1   
POL(add0(x1, x2)) = 2 + x1 + x2   
POL(app0(x1, x2)) = 2 + 2·x1 + x2   
POL(minus(x1)) = x1   
POL(quot0(x1, x2)) = 2·x1 + x2   
POL(rand0(x1)) = x1   
POL(s0(x1)) = x1   

(89) Obligation:

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

QUOT(s0(x)) → QUOT(minus(x))

The TRS R consists of the following rules:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
minus(s0(x)) → minus(x)
minus(x) → x

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

(90) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


QUOT(s0(x)) → QUOT(minus(x))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
QUOT(x1)  =  QUOT(x1)
s0(x1)  =  s0(x1)
minus(x1)  =  x1
quot0(x1, x2)  =  quot0(x1, x2)
rand0(x1)  =  rand0

Recursive path order with status [RPO].
Quasi-Precedence:
quot02 > [QUOT1, s01]
rand0 > [QUOT1, s01]

Status:
QUOT1: multiset
s01: multiset
quot02: [2,1]
rand0: []


The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
minus(s0(x)) → minus(x)
minus(x) → x

(91) Obligation:

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

quot0(s0(x), s0(y)) → s0(quot0(minus(x), s0(y)))
rand0(x) → rand0(s0(x))
minus(s0(x)) → minus(x)
minus(x) → x

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

(92) PisEmptyProof (EQUIVALENT transformation)

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

(93) YES