YES(O(1), O(n^2)) 2.78/1.14 YES(O(1), O(n^2)) 2.78/1.18 2.78/1.18 2.78/1.18
2.78/1.18 2.78/1.180 CpxTRS2.78/1.18
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))2.78/1.18
↳2 CdtProblem2.78/1.18
↳3 CdtUnreachableProof (⇔)2.78/1.18
↳4 CdtProblem2.78/1.18
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))2.78/1.18
↳6 CdtProblem2.78/1.18
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))2.78/1.18
↳8 CdtProblem2.78/1.18
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))2.78/1.18
↳10 CdtProblem2.78/1.18
↳11 SIsEmptyProof (BOTH BOUNDS(ID, ID))2.78/1.18
↳12 BOUNDS(O(1), O(1))2.78/1.18
app(nil, k) → k 2.78/1.18
app(l, nil) → l 2.78/1.18
app(cons(x, l), k) → cons(x, app(l, k)) 2.78/1.18
sum(cons(x, nil)) → cons(x, nil) 2.78/1.18
sum(cons(x, cons(y, l))) → sum(cons(plus(x, y), l)) 2.78/1.18
sum(app(l, cons(x, cons(y, k)))) → sum(app(l, sum(cons(x, cons(y, k))))) 2.78/1.18
plus(0, y) → y 2.78/1.18
plus(s(x), y) → s(plus(x, y))
Tuples:
app(nil, z0) → z0 2.78/1.18
app(z0, nil) → z0 2.78/1.18
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 2.78/1.18
sum(cons(z0, nil)) → cons(z0, nil) 2.78/1.18
sum(cons(z0, cons(z1, z2))) → sum(cons(plus(z0, z1), z2)) 2.78/1.18
sum(app(z0, cons(z1, cons(z2, z3)))) → sum(app(z0, sum(cons(z1, cons(z2, z3))))) 2.78/1.18
plus(0, z0) → z0 2.78/1.18
plus(s(z0), z1) → s(plus(z0, z1))
S tuples:
APP(cons(z0, z1), z2) → c2(APP(z1, z2)) 2.78/1.18
SUM(cons(z0, cons(z1, z2))) → c4(SUM(cons(plus(z0, z1), z2)), PLUS(z0, z1)) 2.78/1.18
SUM(app(z0, cons(z1, cons(z2, z3)))) → c5(SUM(app(z0, sum(cons(z1, cons(z2, z3))))), APP(z0, sum(cons(z1, cons(z2, z3)))), SUM(cons(z1, cons(z2, z3)))) 2.78/1.18
PLUS(s(z0), z1) → c7(PLUS(z0, z1))
K tuples:none
APP(cons(z0, z1), z2) → c2(APP(z1, z2)) 2.78/1.18
SUM(cons(z0, cons(z1, z2))) → c4(SUM(cons(plus(z0, z1), z2)), PLUS(z0, z1)) 2.78/1.18
SUM(app(z0, cons(z1, cons(z2, z3)))) → c5(SUM(app(z0, sum(cons(z1, cons(z2, z3))))), APP(z0, sum(cons(z1, cons(z2, z3)))), SUM(cons(z1, cons(z2, z3)))) 2.78/1.18
PLUS(s(z0), z1) → c7(PLUS(z0, z1))
app, sum, plus
APP, SUM, PLUS
c2, c4, c5, c7
SUM(app(z0, cons(z1, cons(z2, z3)))) → c5(SUM(app(z0, sum(cons(z1, cons(z2, z3))))), APP(z0, sum(cons(z1, cons(z2, z3)))), SUM(cons(z1, cons(z2, z3))))
Tuples:
app(nil, z0) → z0 2.78/1.18
app(z0, nil) → z0 2.78/1.18
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 2.78/1.18
sum(cons(z0, nil)) → cons(z0, nil) 2.78/1.18
sum(cons(z0, cons(z1, z2))) → sum(cons(plus(z0, z1), z2)) 2.78/1.18
sum(app(z0, cons(z1, cons(z2, z3)))) → sum(app(z0, sum(cons(z1, cons(z2, z3))))) 2.78/1.18
plus(0, z0) → z0 2.78/1.19
plus(s(z0), z1) → s(plus(z0, z1))
S tuples:
APP(cons(z0, z1), z2) → c2(APP(z1, z2)) 2.78/1.19
SUM(cons(z0, cons(z1, z2))) → c4(SUM(cons(plus(z0, z1), z2)), PLUS(z0, z1)) 2.78/1.19
PLUS(s(z0), z1) → c7(PLUS(z0, z1))
K tuples:none
APP(cons(z0, z1), z2) → c2(APP(z1, z2)) 2.78/1.19
SUM(cons(z0, cons(z1, z2))) → c4(SUM(cons(plus(z0, z1), z2)), PLUS(z0, z1)) 2.78/1.19
PLUS(s(z0), z1) → c7(PLUS(z0, z1))
app, sum, plus
APP, SUM, PLUS
c2, c4, c7
We considered the (Usable) Rules:
SUM(cons(z0, cons(z1, z2))) → c4(SUM(cons(plus(z0, z1), z2)), PLUS(z0, z1))
And the Tuples:
plus(0, z0) → z0 2.78/1.19
plus(s(z0), z1) → s(plus(z0, z1))
The order we found is given by the following interpretation:
APP(cons(z0, z1), z2) → c2(APP(z1, z2)) 2.78/1.19
SUM(cons(z0, cons(z1, z2))) → c4(SUM(cons(plus(z0, z1), z2)), PLUS(z0, z1)) 2.78/1.19
PLUS(s(z0), z1) → c7(PLUS(z0, z1))
POL(0) = 0 2.78/1.19
POL(APP(x1, x2)) = 0 2.78/1.19
POL(PLUS(x1, x2)) = [1] 2.78/1.19
POL(SUM(x1)) = [4]x1 2.78/1.19
POL(c2(x1)) = x1 2.78/1.19
POL(c4(x1, x2)) = x1 + x2 2.78/1.19
POL(c7(x1)) = x1 2.78/1.19
POL(cons(x1, x2)) = [3] + x2 2.78/1.19
POL(plus(x1, x2)) = [4] + [4]x1 + [3]x2 2.78/1.19
POL(s(x1)) = [2]
Tuples:
app(nil, z0) → z0 2.78/1.19
app(z0, nil) → z0 2.78/1.19
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 2.78/1.19
sum(cons(z0, nil)) → cons(z0, nil) 2.78/1.19
sum(cons(z0, cons(z1, z2))) → sum(cons(plus(z0, z1), z2)) 2.78/1.19
sum(app(z0, cons(z1, cons(z2, z3)))) → sum(app(z0, sum(cons(z1, cons(z2, z3))))) 2.78/1.19
plus(0, z0) → z0 2.78/1.19
plus(s(z0), z1) → s(plus(z0, z1))
S tuples:
APP(cons(z0, z1), z2) → c2(APP(z1, z2)) 2.78/1.19
SUM(cons(z0, cons(z1, z2))) → c4(SUM(cons(plus(z0, z1), z2)), PLUS(z0, z1)) 2.78/1.19
PLUS(s(z0), z1) → c7(PLUS(z0, z1))
K tuples:
APP(cons(z0, z1), z2) → c2(APP(z1, z2)) 2.78/1.19
PLUS(s(z0), z1) → c7(PLUS(z0, z1))
Defined Rule Symbols:
SUM(cons(z0, cons(z1, z2))) → c4(SUM(cons(plus(z0, z1), z2)), PLUS(z0, z1))
app, sum, plus
APP, SUM, PLUS
c2, c4, c7
We considered the (Usable) Rules:
APP(cons(z0, z1), z2) → c2(APP(z1, z2))
And the Tuples:
plus(0, z0) → z0 2.78/1.19
plus(s(z0), z1) → s(plus(z0, z1))
The order we found is given by the following interpretation:
APP(cons(z0, z1), z2) → c2(APP(z1, z2)) 2.78/1.19
SUM(cons(z0, cons(z1, z2))) → c4(SUM(cons(plus(z0, z1), z2)), PLUS(z0, z1)) 2.78/1.19
PLUS(s(z0), z1) → c7(PLUS(z0, z1))
POL(0) = 0 2.78/1.19
POL(APP(x1, x2)) = [4]x1 2.78/1.19
POL(PLUS(x1, x2)) = [4] 2.78/1.19
POL(SUM(x1)) = [5]x1 2.78/1.19
POL(c2(x1)) = x1 2.78/1.19
POL(c4(x1, x2)) = x1 + x2 2.78/1.19
POL(c7(x1)) = x1 2.78/1.19
POL(cons(x1, x2)) = [2] + x2 2.78/1.19
POL(plus(x1, x2)) = [2] + [2]x1 + [2]x2 2.78/1.19
POL(s(x1)) = [4]
Tuples:
app(nil, z0) → z0 2.78/1.19
app(z0, nil) → z0 2.78/1.19
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 2.78/1.19
sum(cons(z0, nil)) → cons(z0, nil) 2.78/1.19
sum(cons(z0, cons(z1, z2))) → sum(cons(plus(z0, z1), z2)) 2.78/1.19
sum(app(z0, cons(z1, cons(z2, z3)))) → sum(app(z0, sum(cons(z1, cons(z2, z3))))) 2.78/1.19
plus(0, z0) → z0 2.78/1.19
plus(s(z0), z1) → s(plus(z0, z1))
S tuples:
APP(cons(z0, z1), z2) → c2(APP(z1, z2)) 2.78/1.19
SUM(cons(z0, cons(z1, z2))) → c4(SUM(cons(plus(z0, z1), z2)), PLUS(z0, z1)) 2.78/1.19
PLUS(s(z0), z1) → c7(PLUS(z0, z1))
K tuples:
PLUS(s(z0), z1) → c7(PLUS(z0, z1))
Defined Rule Symbols:
SUM(cons(z0, cons(z1, z2))) → c4(SUM(cons(plus(z0, z1), z2)), PLUS(z0, z1)) 2.78/1.19
APP(cons(z0, z1), z2) → c2(APP(z1, z2))
app, sum, plus
APP, SUM, PLUS
c2, c4, c7
We considered the (Usable) Rules:
PLUS(s(z0), z1) → c7(PLUS(z0, z1))
And the Tuples:
plus(0, z0) → z0 2.78/1.19
plus(s(z0), z1) → s(plus(z0, z1))
The order we found is given by the following interpretation:
APP(cons(z0, z1), z2) → c2(APP(z1, z2)) 2.78/1.19
SUM(cons(z0, cons(z1, z2))) → c4(SUM(cons(plus(z0, z1), z2)), PLUS(z0, z1)) 2.78/1.19
PLUS(s(z0), z1) → c7(PLUS(z0, z1))
POL(0) = [3] 2.78/1.19
POL(APP(x1, x2)) = [3]x1 + [3]x1·x2 + [3]x12 2.78/1.19
POL(PLUS(x1, x2)) = x1 + x2 2.78/1.19
POL(SUM(x1)) = x12 2.78/1.19
POL(c2(x1)) = x1 2.78/1.19
POL(c4(x1, x2)) = x1 + x2 2.78/1.19
POL(c7(x1)) = x1 2.78/1.19
POL(cons(x1, x2)) = [1] + x1 + x2 2.78/1.19
POL(plus(x1, x2)) = x1 + x2 2.78/1.19
POL(s(x1)) = [1] + x1
Tuples:
app(nil, z0) → z0 2.78/1.19
app(z0, nil) → z0 2.78/1.19
app(cons(z0, z1), z2) → cons(z0, app(z1, z2)) 2.78/1.19
sum(cons(z0, nil)) → cons(z0, nil) 2.78/1.19
sum(cons(z0, cons(z1, z2))) → sum(cons(plus(z0, z1), z2)) 2.78/1.19
sum(app(z0, cons(z1, cons(z2, z3)))) → sum(app(z0, sum(cons(z1, cons(z2, z3))))) 2.78/1.19
plus(0, z0) → z0 2.78/1.19
plus(s(z0), z1) → s(plus(z0, z1))
S tuples:none
APP(cons(z0, z1), z2) → c2(APP(z1, z2)) 2.78/1.19
SUM(cons(z0, cons(z1, z2))) → c4(SUM(cons(plus(z0, z1), z2)), PLUS(z0, z1)) 2.78/1.19
PLUS(s(z0), z1) → c7(PLUS(z0, z1))
Defined Rule Symbols:
SUM(cons(z0, cons(z1, z2))) → c4(SUM(cons(plus(z0, z1), z2)), PLUS(z0, z1)) 2.78/1.19
APP(cons(z0, z1), z2) → c2(APP(z1, z2)) 2.78/1.19
PLUS(s(z0), z1) → c7(PLUS(z0, z1))
app, sum, plus
APP, SUM, PLUS
c2, c4, c7