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