YES(O(1), O(n^2)) 2.51/1.06 YES(O(1), O(n^2)) 2.51/1.10 2.51/1.10 2.51/1.10
2.51/1.10 2.51/1.100 CpxTRS2.51/1.10
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))2.51/1.10
↳2 CdtProblem2.51/1.10
↳3 CdtUnreachableProof (⇔)2.51/1.10
↳4 CdtProblem2.51/1.10
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))2.51/1.10
↳6 CdtProblem2.51/1.10
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))2.51/1.10
↳8 CdtProblem2.51/1.10
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))2.51/1.10
↳10 BOUNDS(O(1), O(1))2.51/1.10
rev(nil) → nil 2.51/1.10
rev(rev(x)) → x 2.51/1.10
rev(++(x, y)) → ++(rev(y), rev(x)) 2.51/1.10
++(nil, y) → y 2.51/1.10
++(x, nil) → x 2.51/1.10
++(.(x, y), z) → .(x, ++(y, z)) 2.51/1.10
++(x, ++(y, z)) → ++(++(x, y), z) 2.51/1.10
make(x) → .(x, nil)
Tuples:
rev(nil) → nil 2.51/1.10
rev(rev(z0)) → z0 2.51/1.10
rev(++(z0, z1)) → ++(rev(z1), rev(z0)) 2.51/1.10
++(nil, z0) → z0 2.51/1.10
++(z0, nil) → z0 2.51/1.10
++(.(z0, z1), z2) → .(z0, ++(z1, z2)) 2.51/1.10
++(z0, ++(z1, z2)) → ++(++(z0, z1), z2) 2.51/1.10
make(z0) → .(z0, nil)
S tuples:
REV(++(z0, z1)) → c2(++'(rev(z1), rev(z0)), REV(z1), REV(z0)) 2.51/1.10
++'(.(z0, z1), z2) → c5(++'(z1, z2)) 2.51/1.10
++'(z0, ++(z1, z2)) → c6(++'(++(z0, z1), z2), ++'(z0, z1))
K tuples:none
REV(++(z0, z1)) → c2(++'(rev(z1), rev(z0)), REV(z1), REV(z0)) 2.51/1.10
++'(.(z0, z1), z2) → c5(++'(z1, z2)) 2.51/1.10
++'(z0, ++(z1, z2)) → c6(++'(++(z0, z1), z2), ++'(z0, z1))
rev, ++, make
REV, ++'
c2, c5, c6
REV(++(z0, z1)) → c2(++'(rev(z1), rev(z0)), REV(z1), REV(z0))
Tuples:
rev(nil) → nil 2.51/1.10
rev(rev(z0)) → z0 2.51/1.10
rev(++(z0, z1)) → ++(rev(z1), rev(z0)) 2.51/1.10
++(nil, z0) → z0 2.51/1.10
++(z0, nil) → z0 2.51/1.10
++(.(z0, z1), z2) → .(z0, ++(z1, z2)) 2.51/1.10
++(z0, ++(z1, z2)) → ++(++(z0, z1), z2) 2.51/1.10
make(z0) → .(z0, nil)
S tuples:
++'(.(z0, z1), z2) → c5(++'(z1, z2)) 2.51/1.10
++'(z0, ++(z1, z2)) → c6(++'(++(z0, z1), z2), ++'(z0, z1))
K tuples:none
++'(.(z0, z1), z2) → c5(++'(z1, z2)) 2.51/1.10
++'(z0, ++(z1, z2)) → c6(++'(++(z0, z1), z2), ++'(z0, z1))
rev, ++, make
++'
c5, c6
We considered the (Usable) Rules:
++'(z0, ++(z1, z2)) → c6(++'(++(z0, z1), z2), ++'(z0, z1))
And the Tuples:
++(nil, z0) → z0 2.51/1.10
++(.(z0, z1), z2) → .(z0, ++(z1, z2)) 2.51/1.10
++(z0, ++(z1, z2)) → ++(++(z0, z1), z2) 2.51/1.10
++(z0, nil) → z0
The order we found is given by the following interpretation:
++'(.(z0, z1), z2) → c5(++'(z1, z2)) 2.51/1.10
++'(z0, ++(z1, z2)) → c6(++'(++(z0, z1), z2), ++'(z0, z1))
POL(++(x1, x2)) = [4] + x1 + [4]x2 2.88/1.11
POL(++'(x1, x2)) = [5] + [2]x2 2.88/1.11
POL(.(x1, x2)) = x1 2.88/1.11
POL(c5(x1)) = x1 2.88/1.11
POL(c6(x1, x2)) = x1 + x2 2.88/1.11
POL(nil) = 0
Tuples:
rev(nil) → nil 2.88/1.11
rev(rev(z0)) → z0 2.88/1.11
rev(++(z0, z1)) → ++(rev(z1), rev(z0)) 2.88/1.11
++(nil, z0) → z0 2.88/1.11
++(z0, nil) → z0 2.88/1.11
++(.(z0, z1), z2) → .(z0, ++(z1, z2)) 2.88/1.11
++(z0, ++(z1, z2)) → ++(++(z0, z1), z2) 2.88/1.11
make(z0) → .(z0, nil)
S tuples:
++'(.(z0, z1), z2) → c5(++'(z1, z2)) 2.88/1.11
++'(z0, ++(z1, z2)) → c6(++'(++(z0, z1), z2), ++'(z0, z1))
K tuples:
++'(.(z0, z1), z2) → c5(++'(z1, z2))
Defined Rule Symbols:
++'(z0, ++(z1, z2)) → c6(++'(++(z0, z1), z2), ++'(z0, z1))
rev, ++, make
++'
c5, c6
We considered the (Usable) Rules:
++'(.(z0, z1), z2) → c5(++'(z1, z2))
And the Tuples:
++(nil, z0) → z0 2.88/1.11
++(.(z0, z1), z2) → .(z0, ++(z1, z2)) 2.88/1.11
++(z0, ++(z1, z2)) → ++(++(z0, z1), z2) 2.88/1.11
++(z0, nil) → z0
The order we found is given by the following interpretation:
++'(.(z0, z1), z2) → c5(++'(z1, z2)) 2.88/1.11
++'(z0, ++(z1, z2)) → c6(++'(++(z0, z1), z2), ++'(z0, z1))
POL(++(x1, x2)) = [2] + x1 + x2 2.88/1.11
POL(++'(x1, x2)) = x1 + [3]x22 + x1·x2 2.88/1.11
POL(.(x1, x2)) = [2] + x1 + x2 2.88/1.11
POL(c5(x1)) = x1 2.88/1.11
POL(c6(x1, x2)) = x1 + x2 2.88/1.11
POL(nil) = [3]
Tuples:
rev(nil) → nil 2.88/1.11
rev(rev(z0)) → z0 2.88/1.11
rev(++(z0, z1)) → ++(rev(z1), rev(z0)) 2.88/1.11
++(nil, z0) → z0 2.88/1.11
++(z0, nil) → z0 2.88/1.11
++(.(z0, z1), z2) → .(z0, ++(z1, z2)) 2.88/1.11
++(z0, ++(z1, z2)) → ++(++(z0, z1), z2) 2.88/1.11
make(z0) → .(z0, nil)
S tuples:none
++'(.(z0, z1), z2) → c5(++'(z1, z2)) 2.88/1.11
++'(z0, ++(z1, z2)) → c6(++'(++(z0, z1), z2), ++'(z0, z1))
Defined Rule Symbols:
++'(z0, ++(z1, z2)) → c6(++'(++(z0, z1), z2), ++'(z0, z1)) 2.88/1.11
++'(.(z0, z1), z2) → c5(++'(z1, z2))
rev, ++, make
++'
c5, c6