YES
0 QTRS
↳1 Overlay + Local Confluence (⇔, 0 ms)
↳2 QTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 QDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 QDP
↳10 QReductionProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 QDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 QDP
↳17 QReductionProof (⇔, 0 ms)
↳18 QDP
↳19 TransformationProof (⇔, 0 ms)
↳20 QDP
↳21 DependencyGraphProof (⇔, 0 ms)
↳22 QDP
↳23 TransformationProof (⇔, 0 ms)
↳24 QDP
↳25 TransformationProof (⇔, 0 ms)
↳26 QDP
↳27 TransformationProof (⇔, 0 ms)
↳28 QDP
↳29 QDPOrderProof (⇔, 0 ms)
↳30 QDP
↳31 DependencyGraphProof (⇔, 0 ms)
↳32 TRUE
isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
less_leaves(u, v) → if1(isLeaf(u), isLeaf(v), u, v)
if1(b, true, u, v) → false
if1(b, false, u, v) → if2(b, u, v)
if2(true, u, v) → true
if2(false, u, v) → less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))
isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
less_leaves(u, v) → if1(isLeaf(u), isLeaf(v), u, v)
if1(b, true, u, v) → false
if1(b, false, u, v) → if2(b, u, v)
if2(true, u, v) → true
if2(false, u, v) → less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))
isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)
CONCAT(cons(u, v), y) → CONCAT(v, y)
LESS_LEAVES(u, v) → IF1(isLeaf(u), isLeaf(v), u, v)
LESS_LEAVES(u, v) → ISLEAF(u)
LESS_LEAVES(u, v) → ISLEAF(v)
IF1(b, false, u, v) → IF2(b, u, v)
IF2(false, u, v) → LESS_LEAVES(concat(left(u), right(u)), concat(left(v), right(v)))
IF2(false, u, v) → CONCAT(left(u), right(u))
IF2(false, u, v) → LEFT(u)
IF2(false, u, v) → RIGHT(u)
IF2(false, u, v) → CONCAT(left(v), right(v))
IF2(false, u, v) → LEFT(v)
IF2(false, u, v) → RIGHT(v)
isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
less_leaves(u, v) → if1(isLeaf(u), isLeaf(v), u, v)
if1(b, true, u, v) → false
if1(b, false, u, v) → if2(b, u, v)
if2(true, u, v) → true
if2(false, u, v) → less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))
isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)
CONCAT(cons(u, v), y) → CONCAT(v, y)
isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
less_leaves(u, v) → if1(isLeaf(u), isLeaf(v), u, v)
if1(b, true, u, v) → false
if1(b, false, u, v) → if2(b, u, v)
if2(true, u, v) → true
if2(false, u, v) → less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))
isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)
CONCAT(cons(u, v), y) → CONCAT(v, y)
isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)
isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)
CONCAT(cons(u, v), y) → CONCAT(v, y)
From the DPs we obtained the following set of size-change graphs:
IF2(false, u, v) → LESS_LEAVES(concat(left(u), right(u)), concat(left(v), right(v)))
LESS_LEAVES(u, v) → IF1(isLeaf(u), isLeaf(v), u, v)
IF1(b, false, u, v) → IF2(b, u, v)
isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
less_leaves(u, v) → if1(isLeaf(u), isLeaf(v), u, v)
if1(b, true, u, v) → false
if1(b, false, u, v) → if2(b, u, v)
if2(true, u, v) → true
if2(false, u, v) → less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))
isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)
IF2(false, u, v) → LESS_LEAVES(concat(left(u), right(u)), concat(left(v), right(v)))
LESS_LEAVES(u, v) → IF1(isLeaf(u), isLeaf(v), u, v)
IF1(b, false, u, v) → IF2(b, u, v)
isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)
less_leaves(x0, x1)
if1(x0, true, x1, x2)
if1(x0, false, x1, x2)
if2(true, x0, x1)
if2(false, x0, x1)
IF2(false, u, v) → LESS_LEAVES(concat(left(u), right(u)), concat(left(v), right(v)))
LESS_LEAVES(u, v) → IF1(isLeaf(u), isLeaf(v), u, v)
IF1(b, false, u, v) → IF2(b, u, v)
isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
LESS_LEAVES(y0, leaf) → IF1(isLeaf(y0), true, y0, leaf) → LESS_LEAVES(y0, leaf) → IF1(isLeaf(y0), true, y0, leaf)
LESS_LEAVES(y0, cons(x0, x1)) → IF1(isLeaf(y0), false, y0, cons(x0, x1)) → LESS_LEAVES(y0, cons(x0, x1)) → IF1(isLeaf(y0), false, y0, cons(x0, x1))
IF2(false, u, v) → LESS_LEAVES(concat(left(u), right(u)), concat(left(v), right(v)))
IF1(b, false, u, v) → IF2(b, u, v)
LESS_LEAVES(y0, leaf) → IF1(isLeaf(y0), true, y0, leaf)
LESS_LEAVES(y0, cons(x0, x1)) → IF1(isLeaf(y0), false, y0, cons(x0, x1))
isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
LESS_LEAVES(y0, cons(x0, x1)) → IF1(isLeaf(y0), false, y0, cons(x0, x1))
IF1(b, false, u, v) → IF2(b, u, v)
IF2(false, u, v) → LESS_LEAVES(concat(left(u), right(u)), concat(left(v), right(v)))
isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, right(cons(x0, x1)))) → IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, right(cons(x0, x1))))
IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(left(cons(x0, x1)), x1)) → IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(left(cons(x0, x1)), x1))
LESS_LEAVES(y0, cons(x0, x1)) → IF1(isLeaf(y0), false, y0, cons(x0, x1))
IF1(b, false, u, v) → IF2(b, u, v)
IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, right(cons(x0, x1))))
IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(left(cons(x0, x1)), x1))
isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, x1)) → IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, x1))
LESS_LEAVES(y0, cons(x0, x1)) → IF1(isLeaf(y0), false, y0, cons(x0, x1))
IF1(b, false, u, v) → IF2(b, u, v)
IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(left(cons(x0, x1)), x1))
IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, x1))
isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, x1)) → IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, x1))
LESS_LEAVES(y0, cons(x0, x1)) → IF1(isLeaf(y0), false, y0, cons(x0, x1))
IF1(b, false, u, v) → IF2(b, u, v)
IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, x1))
isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF2(false, y0, cons(x0, x1)) → LESS_LEAVES(concat(left(y0), right(y0)), concat(x0, x1))
concat2 > cons2
cons_2=2
concat_2=1
leaf=1
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
LESS_LEAVES(y0, cons(x0, x1)) → IF1(isLeaf(y0), false, y0, cons(x0, x1))
IF1(b, false, u, v) → IF2(b, u, v)
isLeaf(leaf) → true
isLeaf(cons(u, v)) → false
left(cons(u, v)) → u
right(cons(u, v)) → v
concat(leaf, y) → y
concat(cons(u, v), y) → cons(u, concat(v, y))
isLeaf(leaf)
isLeaf(cons(x0, x1))
left(cons(x0, x1))
right(cons(x0, x1))
concat(leaf, x0)
concat(cons(x0, x1), x2)