YES(O(1), O(n^3)) 4.88/1.86 YES(O(1), O(n^3)) 4.88/1.88 4.88/1.88 4.88/1.88
4.88/1.88 4.88/1.890 CpxTRS4.88/1.89
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))4.88/1.89
↳2 CdtProblem4.88/1.89
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)4.88/1.89
↳4 CdtProblem4.88/1.89
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))4.88/1.89
↳6 CdtProblem4.88/1.89
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^3))))4.88/1.89
↳8 CdtProblem4.88/1.89
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))4.88/1.89
↳10 BOUNDS(O(1), O(1))4.88/1.89
mul0(C(x, y), y') → add0(mul0(y, y'), y') 4.88/1.89
mul0(Z, y) → Z 4.88/1.89
add0(C(x, y), y') → add0(y, C(S, y')) 4.88/1.89
add0(Z, y) → y 4.88/1.89
second(C(x, y)) → y 4.88/1.89
isZero(C(x, y)) → False 4.88/1.89
isZero(Z) → True 4.88/1.89
goal(xs, ys) → mul0(xs, ys)
Tuples:
mul0(C(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.88/1.89
mul0(Z, z0) → Z 4.88/1.89
add0(C(z0, z1), z2) → add0(z1, C(S, z2)) 4.88/1.89
add0(Z, z0) → z0 4.88/1.89
second(C(z0, z1)) → z1 4.88/1.89
isZero(C(z0, z1)) → False 4.88/1.89
isZero(Z) → True 4.88/1.89
goal(z0, z1) → mul0(z0, z1)
S tuples:
MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2))) 4.88/1.89
GOAL(z0, z1) → c7(MUL0(z0, z1))
K tuples:none
MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2))) 4.88/1.89
GOAL(z0, z1) → c7(MUL0(z0, z1))
mul0, add0, second, isZero, goal
MUL0, ADD0, GOAL
c, c2, c7
GOAL(z0, z1) → c7(MUL0(z0, z1))
Tuples:
mul0(C(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.88/1.89
mul0(Z, z0) → Z 4.88/1.89
add0(C(z0, z1), z2) → add0(z1, C(S, z2)) 4.88/1.89
add0(Z, z0) → z0 4.88/1.89
second(C(z0, z1)) → z1 4.88/1.89
isZero(C(z0, z1)) → False 4.88/1.89
isZero(Z) → True 4.88/1.89
goal(z0, z1) → mul0(z0, z1)
S tuples:
MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
K tuples:none
MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
mul0, add0, second, isZero, goal
MUL0, ADD0
c, c2
We considered the (Usable) Rules:
MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2))
And the Tuples:
mul0(C(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.88/1.89
mul0(Z, z0) → Z 4.88/1.89
add0(C(z0, z1), z2) → add0(z1, C(S, z2)) 4.88/1.89
add0(Z, z0) → z0
The order we found is given by the following interpretation:
MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
POL(ADD0(x1, x2)) = [1] 4.88/1.89
POL(C(x1, x2)) = [2] + x1 + x2 4.88/1.89
POL(MUL0(x1, x2)) = [2]x1 4.88/1.89
POL(S) = [3] 4.88/1.89
POL(Z) = [3] 4.88/1.89
POL(add0(x1, x2)) = [3] 4.88/1.89
POL(c(x1, x2)) = x1 + x2 4.88/1.89
POL(c2(x1)) = x1 4.88/1.89
POL(mul0(x1, x2)) = 0
Tuples:
mul0(C(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.88/1.89
mul0(Z, z0) → Z 4.88/1.89
add0(C(z0, z1), z2) → add0(z1, C(S, z2)) 4.88/1.89
add0(Z, z0) → z0 4.88/1.89
second(C(z0, z1)) → z1 4.88/1.89
isZero(C(z0, z1)) → False 4.88/1.89
isZero(Z) → True 4.88/1.89
goal(z0, z1) → mul0(z0, z1)
S tuples:
MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
K tuples:
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
Defined Rule Symbols:
MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2))
mul0, add0, second, isZero, goal
MUL0, ADD0
c, c2
We considered the (Usable) Rules:
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
And the Tuples:
mul0(C(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.88/1.89
mul0(Z, z0) → Z 4.88/1.89
add0(C(z0, z1), z2) → add0(z1, C(S, z2)) 4.88/1.89
add0(Z, z0) → z0
The order we found is given by the following interpretation:
MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
POL(ADD0(x1, x2)) = x1 4.88/1.89
POL(C(x1, x2)) = [1] + x2 4.88/1.89
POL(MUL0(x1, x2)) = x12·x2 + x1·x22 4.88/1.89
POL(S) = 0 4.88/1.89
POL(Z) = 0 4.88/1.89
POL(add0(x1, x2)) = x1 + x2 4.88/1.89
POL(c(x1, x2)) = x1 + x2 4.88/1.89
POL(c2(x1)) = x1 4.88/1.89
POL(mul0(x1, x2)) = x2 + x1·x2
Tuples:
mul0(C(z0, z1), z2) → add0(mul0(z1, z2), z2) 4.88/1.89
mul0(Z, z0) → Z 4.88/1.89
add0(C(z0, z1), z2) → add0(z1, C(S, z2)) 4.88/1.89
add0(Z, z0) → z0 4.88/1.89
second(C(z0, z1)) → z1 4.88/1.89
isZero(C(z0, z1)) → False 4.88/1.89
isZero(Z) → True 4.88/1.89
goal(z0, z1) → mul0(z0, z1)
S tuples:none
MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
Defined Rule Symbols:
MUL0(C(z0, z1), z2) → c(ADD0(mul0(z1, z2), z2), MUL0(z1, z2)) 4.88/1.89
ADD0(C(z0, z1), z2) → c2(ADD0(z1, C(S, z2)))
mul0, add0, second, isZero, goal
MUL0, ADD0
c, c2