YES(O(1), O(n^1)) 0.00/0.80 YES(O(1), O(n^1)) 0.00/0.81 0.00/0.81 0.00/0.81
0.00/0.81 0.00/0.810 CpxTRS0.00/0.81
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.81
↳2 CdtProblem0.00/0.81
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.81
↳4 CdtProblem0.00/0.81
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.81
↳6 CdtProblem0.00/0.81
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.81
↳8 CdtProblem0.00/0.81
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.81
↳10 CdtProblem0.00/0.81
↳11 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.81
↳12 BOUNDS(O(1), O(1))0.00/0.81
merge(x, nil) → x 0.00/0.81
merge(nil, y) → y 0.00/0.81
merge(++(x, y), ++(u, v)) → ++(x, merge(y, ++(u, v))) 0.00/0.81
merge(++(x, y), ++(u, v)) → ++(u, merge(++(x, y), v))
Tuples:
merge(z0, nil) → z0 0.00/0.81
merge(nil, z0) → z0 0.00/0.81
merge(++(z0, z1), ++(u, v)) → ++(z0, merge(z1, ++(u, v))) 0.00/0.81
merge(++(z0, z1), ++(u, v)) → ++(u, merge(++(z0, z1), v))
S tuples:
MERGE(++(z0, z1), ++(u, v)) → c2(MERGE(z1, ++(u, v))) 0.00/0.81
MERGE(++(z0, z1), ++(u, v)) → c3(MERGE(++(z0, z1), v))
K tuples:none
MERGE(++(z0, z1), ++(u, v)) → c2(MERGE(z1, ++(u, v))) 0.00/0.81
MERGE(++(z0, z1), ++(u, v)) → c3(MERGE(++(z0, z1), v))
merge
MERGE
c2, c3
Tuples:
merge(z0, nil) → z0 0.00/0.81
merge(nil, z0) → z0 0.00/0.81
merge(++(z0, z1), ++(u, v)) → ++(z0, merge(z1, ++(u, v))) 0.00/0.81
merge(++(z0, z1), ++(u, v)) → ++(u, merge(++(z0, z1), v))
S tuples:
MERGE(++(z0, z1), ++(u, v)) → c2(MERGE(z1, ++(u, v))) 0.00/0.81
MERGE(++(z0, z1), ++(u, v)) → c3
K tuples:none
MERGE(++(z0, z1), ++(u, v)) → c2(MERGE(z1, ++(u, v))) 0.00/0.81
MERGE(++(z0, z1), ++(u, v)) → c3
merge
MERGE
c2, c3
MERGE(++(z0, z1), ++(u, v)) → c3
Tuples:
merge(z0, nil) → z0 0.00/0.81
merge(nil, z0) → z0 0.00/0.81
merge(++(z0, z1), ++(u, v)) → ++(z0, merge(z1, ++(u, v))) 0.00/0.81
merge(++(z0, z1), ++(u, v)) → ++(u, merge(++(z0, z1), v))
S tuples:
MERGE(++(z0, z1), ++(u, v)) → c2(MERGE(z1, ++(u, v))) 0.00/0.81
MERGE(++(z0, z1), ++(u, v)) → c3
K tuples:none
MERGE(++(z0, z1), ++(u, v)) → c2(MERGE(z1, ++(u, v))) 0.00/0.81
MERGE(++(z0, z1), ++(u, v)) → c3
merge
MERGE
c2, c3
We considered the (Usable) Rules:none
MERGE(++(z0, z1), ++(u, v)) → c3
The order we found is given by the following interpretation:
MERGE(++(z0, z1), ++(u, v)) → c2(MERGE(z1, ++(u, v))) 0.00/0.81
MERGE(++(z0, z1), ++(u, v)) → c3
POL(++(x1, x2)) = [1] 0.00/0.81
POL(MERGE(x1, x2)) = [2]x2 0.00/0.81
POL(c2(x1)) = x1 0.00/0.81
POL(c3) = 0 0.00/0.81
POL(u) = [1] 0.00/0.81
POL(v) = [1]
Tuples:
merge(z0, nil) → z0 0.00/0.81
merge(nil, z0) → z0 0.00/0.81
merge(++(z0, z1), ++(u, v)) → ++(z0, merge(z1, ++(u, v))) 0.00/0.81
merge(++(z0, z1), ++(u, v)) → ++(u, merge(++(z0, z1), v))
S tuples:
MERGE(++(z0, z1), ++(u, v)) → c2(MERGE(z1, ++(u, v))) 0.00/0.81
MERGE(++(z0, z1), ++(u, v)) → c3
K tuples:
MERGE(++(z0, z1), ++(u, v)) → c2(MERGE(z1, ++(u, v)))
Defined Rule Symbols:
MERGE(++(z0, z1), ++(u, v)) → c3
merge
MERGE
c2, c3
We considered the (Usable) Rules:none
MERGE(++(z0, z1), ++(u, v)) → c2(MERGE(z1, ++(u, v)))
The order we found is given by the following interpretation:
MERGE(++(z0, z1), ++(u, v)) → c2(MERGE(z1, ++(u, v))) 0.00/0.81
MERGE(++(z0, z1), ++(u, v)) → c3
POL(++(x1, x2)) = [1] + x2 0.00/0.81
POL(MERGE(x1, x2)) = [3]x1 0.00/0.81
POL(c2(x1)) = x1 0.00/0.81
POL(c3) = 0 0.00/0.81
POL(u) = 0 0.00/0.81
POL(v) = 0
Tuples:
merge(z0, nil) → z0 0.00/0.81
merge(nil, z0) → z0 0.00/0.81
merge(++(z0, z1), ++(u, v)) → ++(z0, merge(z1, ++(u, v))) 0.00/0.81
merge(++(z0, z1), ++(u, v)) → ++(u, merge(++(z0, z1), v))
S tuples:none
MERGE(++(z0, z1), ++(u, v)) → c2(MERGE(z1, ++(u, v))) 0.00/0.81
MERGE(++(z0, z1), ++(u, v)) → c3
Defined Rule Symbols:
MERGE(++(z0, z1), ++(u, v)) → c3 0.00/0.81
MERGE(++(z0, z1), ++(u, v)) → c2(MERGE(z1, ++(u, v)))
merge
MERGE
c2, c3