(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( rand0(x1) ) = max{0, -2} |
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( minus(x1, x2) ) = x1 |
| POL( concat(x1, x2) ) = 2x1 + x2 + 1 |
| POL( cons(x1, x2) ) = 2x1 + x2 + 2 |
| POL( reverse(x1) ) = 2x1 + 2 |
| POL( less_leaves(x1, x2) ) = 2x1 + x2 + 1 |
| POL( app(x1, x2) ) = 2x2 + 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( minus(x1, x2) ) = 2x1 + 2x2 |
| POL( concat(x1, x2) ) = x1 + x2 + 1 |
| POL( cons(x1, x2) ) = x1 + x2 + 2 |
| POL( shuffle(x1) ) = x1 + 1 |
| POL( add(x1, x2) ) = x2 + 1 |
| POL( less_leaves(x1, x2) ) = 2x1 + x2 + 1 |
| POL( app(x1, x2) ) = x1 + x2 |
| 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