0 QTRS
↳1 AAECC Innermost (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 UsableRulesReductionPairsProof (⇔)
↳20 QDP
↳21 MRRProof (⇔)
↳22 QDP
↳23 PisEmptyProof (⇔)
↳24 TRUE
↳25 QDP
↳26 UsableRulesProof (⇔)
↳27 QDP
↳28 QReductionProof (⇔)
↳29 QDP
↳30 QDPSizeChangeProof (⇔)
↳31 TRUE
↳32 QDP
↳33 UsableRulesProof (⇔)
↳34 QDP
↳35 QReductionProof (⇔)
↳36 QDP
↳37 QDPSizeChangeProof (⇔)
↳38 TRUE
↳39 QDP
↳40 UsableRulesProof (⇔)
↳41 QDP
↳42 QReductionProof (⇔)
↳43 QDP
↳44 MRRProof (⇔)
↳45 QDP
↳46 PisEmptyProof (⇔)
↳47 TRUE
↳48 QDP
↳49 UsableRulesProof (⇔)
↳50 QDP
↳51 QReductionProof (⇔)
↳52 QDP
↳53 QDPSizeChangeProof (⇔)
↳54 TRUE
↳55 QDP
↳56 UsableRulesProof (⇔)
↳57 QDP
↳58 QReductionProof (⇔)
↳59 QDP
↳60 QDPOrderProof (⇔)
↳61 QDP
↳62 PisEmptyProof (⇔)
↳63 TRUE
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))
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))
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))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
MINUS(s(x), s(y)) → MINUS(x, y)
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
QUOT(s(x), s(y)) → MINUS(x, y)
APP(add(n, x), y) → APP(x, y)
REVERSE(add(n, x)) → APP(reverse(x), add(n, nil))
REVERSE(add(n, x)) → REVERSE(x)
SHUFFLE(add(n, x)) → SHUFFLE(reverse(x))
SHUFFLE(add(n, x)) → REVERSE(x)
CONCAT(cons(u, v), y) → CONCAT(v, y)
LESS_LEAVES(cons(u, v), cons(w, z)) → LESS_LEAVES(concat(u, v), concat(w, z))
LESS_LEAVES(cons(u, v), cons(w, z)) → CONCAT(u, v)
LESS_LEAVES(cons(u, v), cons(w, z)) → CONCAT(w, z)
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))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
CONCAT(cons(u, v), y) → CONCAT(v, y)
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))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
CONCAT(cons(u, v), y) → CONCAT(v, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
CONCAT(cons(u, v), y) → CONCAT(v, y)
From the DPs we obtained the following set of size-change graphs:
LESS_LEAVES(cons(u, v), cons(w, z)) → LESS_LEAVES(concat(u, v), concat(w, z))
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))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
LESS_LEAVES(cons(u, v), cons(w, z)) → LESS_LEAVES(concat(u, v), concat(w, z))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
LESS_LEAVES(cons(u, v), cons(w, z)) → LESS_LEAVES(concat(u, v), concat(w, z))
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
concat(leaf, x0)
concat(cons(x0, x1), x2)
Used ordering: POLO with Polynomial interpretation [POLO]:
concat(leaf, y) → y
POL(LESS_LEAVES(x1, x2)) = 2·x1 + 2·x2
POL(concat(x1, x2)) = 2 + x1 + x2
POL(cons(x1, x2)) = 2 + 2·x1 + x2
POL(leaf) = 0
LESS_LEAVES(cons(u, v), cons(w, z)) → LESS_LEAVES(concat(u, v), concat(w, z))
concat(cons(u, v), y) → cons(u, concat(v, y))
concat(leaf, x0)
concat(cons(x0, x1), x2)
LESS_LEAVES(cons(u, v), cons(w, z)) → LESS_LEAVES(concat(u, v), concat(w, z))
POL(LESS_LEAVES(x1, x2)) = x1 + x2
POL(concat(x1, x2)) = x1 + x2
POL(cons(x1, x2)) = 1 + x1 + x2
concat(cons(u, v), y) → cons(u, concat(v, y))
concat(leaf, x0)
concat(cons(x0, x1), x2)
APP(add(n, x), y) → APP(x, y)
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))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
APP(add(n, x), y) → APP(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
APP(add(n, x), y) → APP(x, y)
From the DPs we obtained the following set of size-change graphs:
REVERSE(add(n, x)) → REVERSE(x)
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))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
REVERSE(add(n, x)) → REVERSE(x)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
REVERSE(add(n, x)) → REVERSE(x)
From the DPs we obtained the following set of size-change graphs:
SHUFFLE(add(n, x)) → SHUFFLE(reverse(x))
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))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
SHUFFLE(add(n, x)) → SHUFFLE(reverse(x))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
SHUFFLE(add(n, x)) → SHUFFLE(reverse(x))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
SHUFFLE(add(n, x)) → SHUFFLE(reverse(x))
reverse(nil) → nil
POL(SHUFFLE(x1)) = x1
POL(add(x1, x2)) = 2 + x1 + x2
POL(app(x1, x2)) = x1 + x2
POL(nil) = 0
POL(reverse(x1)) = 1 + x1
reverse(add(n, x)) → app(reverse(x), add(n, nil))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
MINUS(s(x), s(y)) → MINUS(x, y)
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))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
MINUS(s(x), s(y)) → MINUS(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
MINUS(s(x), s(y)) → MINUS(x, y)
From the DPs we obtained the following set of size-change graphs:
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
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))
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
quot(0, s(x0))
quot(s(x0), s(x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, leaf)
less_leaves(leaf, cons(x0, x1))
less_leaves(cons(x0, x1), cons(x2, x3))
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x0, 0)
minus(s(x0), s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
QUOT(s(x), s(y)) → QUOT(minus(x, y), s(y))
POL(0) = 0
POL(QUOT(x1, x2)) = x1
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
minus(s(x), s(y)) → minus(x, y)
minus(x, 0) → x
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
minus(x0, 0)
minus(s(x0), s(x1))